MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ordtypelem7 Unicode version

Theorem ordtypelem7 7457
Description: Lemma for ordtype 7465. 
ran  O is an initial segment of  A under the well-order  R. (Contributed by Mario Carneiro, 25-Jun-2015.)
Hypotheses
Ref Expression
ordtypelem.1  |-  F  = recs ( G )
ordtypelem.2  |-  C  =  { w  e.  A  |  A. j  e.  ran  h  j R w }
ordtypelem.3  |-  G  =  ( h  e.  _V  |->  ( iota_ v  e.  C A. u  e.  C  -.  u R v ) )
ordtypelem.5  |-  T  =  { x  e.  On  |  E. t  e.  A  A. z  e.  ( F " x ) z R t }
ordtypelem.6  |-  O  = OrdIso
( R ,  A
)
ordtypelem.7  |-  ( ph  ->  R  We  A )
ordtypelem.8  |-  ( ph  ->  R Se  A )
Assertion
Ref Expression
ordtypelem7  |-  ( ( ( ph  /\  N  e.  A )  /\  M  e.  dom  O )  -> 
( ( O `  M ) R N  \/  N  e.  ran  O ) )
Distinct variable groups:    v, u, C    h, j, t, u, v, w, x, z, M    j, N, u, w    R, h, j, t, u, v, w, x, z    A, h, j, t, u, v, w, x, z    t, O, u, v, x    ph, t, x    h, F, j, t, u, v, w, x, z
Allowed substitution hints:    ph( z, w, v, u, h, j)    C( x, z, w, t, h, j)    T( x, z, w, v, u, t, h, j)    G( x, z, w, v, u, t, h, j)    N( x, z, v, t, h)    O( z, w, h, j)

Proof of Theorem ordtypelem7
Dummy variables  a 
b are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eldif 3298 . . . . . 6  |-  ( N  e.  ( A  \  ran  O )  <->  ( N  e.  A  /\  -.  N  e.  ran  O ) )
2 ordtypelem.1 . . . . . . . . . . . 12  |-  F  = recs ( G )
3 ordtypelem.2 . . . . . . . . . . . 12  |-  C  =  { w  e.  A  |  A. j  e.  ran  h  j R w }
4 ordtypelem.3 . . . . . . . . . . . 12  |-  G  =  ( h  e.  _V  |->  ( iota_ v  e.  C A. u  e.  C  -.  u R v ) )
5 ordtypelem.5 . . . . . . . . . . . 12  |-  T  =  { x  e.  On  |  E. t  e.  A  A. z  e.  ( F " x ) z R t }
6 ordtypelem.6 . . . . . . . . . . . 12  |-  O  = OrdIso
( R ,  A
)
7 ordtypelem.7 . . . . . . . . . . . 12  |-  ( ph  ->  R  We  A )
8 ordtypelem.8 . . . . . . . . . . . 12  |-  ( ph  ->  R Se  A )
92, 3, 4, 5, 6, 7, 8ordtypelem4 7454 . . . . . . . . . . 11  |-  ( ph  ->  O : ( T  i^i  dom  F ) --> A )
109adantr 452 . . . . . . . . . 10  |-  ( (
ph  /\  N  e.  ( A  \  ran  O
) )  ->  O : ( T  i^i  dom 
F ) --> A )
11 fdm 5562 . . . . . . . . . 10  |-  ( O : ( T  i^i  dom 
F ) --> A  ->  dom  O  =  ( T  i^i  dom  F )
)
1210, 11syl 16 . . . . . . . . 9  |-  ( (
ph  /\  N  e.  ( A  \  ran  O
) )  ->  dom  O  =  ( T  i^i  dom 
F ) )
13 inss1 3529 . . . . . . . . . 10  |-  ( T  i^i  dom  F )  C_  T
142, 3, 4, 5, 6, 7, 8ordtypelem2 7452 . . . . . . . . . . . 12  |-  ( ph  ->  Ord  T )
1514adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  N  e.  ( A  \  ran  O
) )  ->  Ord  T )
16 ordsson 4737 . . . . . . . . . . 11  |-  ( Ord 
T  ->  T  C_  On )
1715, 16syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  N  e.  ( A  \  ran  O
) )  ->  T  C_  On )
1813, 17syl5ss 3327 . . . . . . . . 9  |-  ( (
ph  /\  N  e.  ( A  \  ran  O
) )  ->  ( T  i^i  dom  F )  C_  On )
1912, 18eqsstrd 3350 . . . . . . . 8  |-  ( (
ph  /\  N  e.  ( A  \  ran  O
) )  ->  dom  O 
C_  On )
2019sseld 3315 . . . . . . 7  |-  ( (
ph  /\  N  e.  ( A  \  ran  O
) )  ->  ( M  e.  dom  O  ->  M  e.  On )
)
21 eleq1 2472 . . . . . . . . . . 11  |-  ( a  =  b  ->  (
a  e.  dom  O  <->  b  e.  dom  O ) )
22 fveq2 5695 . . . . . . . . . . . 12  |-  ( a  =  b  ->  ( O `  a )  =  ( O `  b ) )
2322breq1d 4190 . . . . . . . . . . 11  |-  ( a  =  b  ->  (
( O `  a
) R N  <->  ( O `  b ) R N ) )
2421, 23imbi12d 312 . . . . . . . . . 10  |-  ( a  =  b  ->  (
( a  e.  dom  O  ->  ( O `  a ) R N )  <->  ( b  e. 
dom  O  ->  ( O `
 b ) R N ) ) )
2524imbi2d 308 . . . . . . . . 9  |-  ( a  =  b  ->  (
( ( ph  /\  N  e.  ( A  \  ran  O ) )  ->  ( a  e. 
dom  O  ->  ( O `
 a ) R N ) )  <->  ( ( ph  /\  N  e.  ( A  \  ran  O
) )  ->  (
b  e.  dom  O  ->  ( O `  b
) R N ) ) ) )
26 eleq1 2472 . . . . . . . . . . 11  |-  ( a  =  M  ->  (
a  e.  dom  O  <->  M  e.  dom  O ) )
27 fveq2 5695 . . . . . . . . . . . 12  |-  ( a  =  M  ->  ( O `  a )  =  ( O `  M ) )
2827breq1d 4190 . . . . . . . . . . 11  |-  ( a  =  M  ->  (
( O `  a
) R N  <->  ( O `  M ) R N ) )
2926, 28imbi12d 312 . . . . . . . . . 10  |-  ( a  =  M  ->  (
( a  e.  dom  O  ->  ( O `  a ) R N )  <->  ( M  e. 
dom  O  ->  ( O `
 M ) R N ) ) )
3029imbi2d 308 . . . . . . . . 9  |-  ( a  =  M  ->  (
( ( ph  /\  N  e.  ( A  \  ran  O ) )  ->  ( a  e. 
dom  O  ->  ( O `
 a ) R N ) )  <->  ( ( ph  /\  N  e.  ( A  \  ran  O
) )  ->  ( M  e.  dom  O  -> 
( O `  M
) R N ) ) ) )
31 r19.21v 2761 . . . . . . . . . 10  |-  ( A. b  e.  a  (
( ph  /\  N  e.  ( A  \  ran  O ) )  ->  (
b  e.  dom  O  ->  ( O `  b
) R N ) )  <->  ( ( ph  /\  N  e.  ( A 
\  ran  O )
)  ->  A. b  e.  a  ( b  e.  dom  O  ->  ( O `  b ) R N ) ) )
322tfr1a 6622 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( Fun 
F  /\  Lim  dom  F
)
3332simpri 449 . . . . . . . . . . . . . . . . . . . . . 22  |-  Lim  dom  F
34 limord 4608 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( Lim 
dom  F  ->  Ord  dom  F )
3533, 34ax-mp 8 . . . . . . . . . . . . . . . . . . . . 21  |-  Ord  dom  F
36 ordin 4579 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( Ord  T  /\  Ord  dom 
F )  ->  Ord  ( T  i^i  dom  F
) )
3715, 35, 36sylancl 644 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  N  e.  ( A  \  ran  O
) )  ->  Ord  ( T  i^i  dom  F
) )
38 ordeq 4556 . . . . . . . . . . . . . . . . . . . . 21  |-  ( dom 
O  =  ( T  i^i  dom  F )  ->  ( Ord  dom  O  <->  Ord  ( T  i^i  dom  F ) ) )
3912, 38syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  N  e.  ( A  \  ran  O
) )  ->  ( Ord  dom  O  <->  Ord  ( T  i^i  dom  F )
) )
4037, 39mpbird 224 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  N  e.  ( A  \  ran  O
) )  ->  Ord  dom 
O )
41 ordelss 4565 . . . . . . . . . . . . . . . . . . 19  |-  ( ( Ord  dom  O  /\  a  e.  dom  O )  ->  a  C_  dom  O )
4240, 41sylan 458 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  a  e.  dom  O )  -> 
a  C_  dom  O )
4342sselda 3316 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  a  e.  dom  O )  /\  b  e.  a )  ->  b  e.  dom  O )
44 pm5.5 327 . . . . . . . . . . . . . . . . 17  |-  ( b  e.  dom  O  -> 
( ( b  e. 
dom  O  ->  ( O `
 b ) R N )  <->  ( O `  b ) R N ) )
4543, 44syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  a  e.  dom  O )  /\  b  e.  a )  ->  (
( b  e.  dom  O  ->  ( O `  b ) R N )  <->  ( O `  b ) R N ) )
4645ralbidva 2690 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  a  e.  dom  O )  -> 
( A. b  e.  a  ( b  e. 
dom  O  ->  ( O `
 b ) R N )  <->  A. b  e.  a  ( O `  b ) R N ) )
47 eldifn 3438 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  ( A  \  ran  O )  ->  -.  N  e.  ran  O )
4847ad2antlr 708 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  -.  N  e.  ran  O )
499ad2antrr 707 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  O :
( T  i^i  dom  F ) --> A )
50 ffn 5558 . . . . . . . . . . . . . . . . . . . . 21  |-  ( O : ( T  i^i  dom 
F ) --> A  ->  O  Fn  ( T  i^i  dom  F ) )
5149, 50syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  O  Fn  ( T  i^i  dom  F
) )
52 simprl 733 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  a  e.  dom  O )
5349, 11syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  dom  O  =  ( T  i^i  dom  F ) )
5452, 53eleqtrd 2488 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  a  e.  ( T  i^i  dom  F
) )
55 fnfvelrn 5834 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( O  Fn  ( T  i^i  dom  F )  /\  a  e.  ( T  i^i  dom  F )
)  ->  ( O `  a )  e.  ran  O )
5651, 54, 55syl2anc 643 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  ( O `  a )  e.  ran  O )
57 eleq1 2472 . . . . . . . . . . . . . . . . . . 19  |-  ( ( O `  a )  =  N  ->  (
( O `  a
)  e.  ran  O  <->  N  e.  ran  O ) )
5856, 57syl5ibcom 212 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  ( ( O `  a )  =  N  ->  N  e. 
ran  O ) )
5948, 58mtod 170 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  -.  ( O `  a )  =  N )
60 eldifi 3437 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  ( A  \  ran  O )  ->  N  e.  A )
6160ad2antlr 708 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  N  e.  A )
62 simprr 734 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  A. b  e.  a  ( O `  b ) R N )
632, 3, 4, 5, 6, 7, 8ordtypelem1 7451 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  O  =  ( F  |`  T ) )
6463ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  O  =  ( F  |`  T ) )
6542adantrr 698 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  a  C_  dom  O )
6665, 53sseqtrd 3352 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  a  C_  ( T  i^i  dom  F
) )
6766, 13syl6ss 3328 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  a  C_  T )
68 fveq1 5694 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( O  =  ( F  |`  T )  ->  ( O `  b )  =  ( ( F  |`  T ) `  b
) )
69 ssel2 3311 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( a  C_  T  /\  b  e.  a )  ->  b  e.  T )
70 fvres 5712 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( b  e.  T  ->  (
( F  |`  T ) `
 b )  =  ( F `  b
) )
7169, 70syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( a  C_  T  /\  b  e.  a )  ->  ( ( F  |`  T ) `  b
)  =  ( F `
 b ) )
7268, 71sylan9eq 2464 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( O  =  ( F  |`  T )  /\  (
a  C_  T  /\  b  e.  a )
)  ->  ( O `  b )  =  ( F `  b ) )
7372anassrs 630 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( O  =  ( F  |`  T )  /\  a  C_  T )  /\  b  e.  a )  ->  ( O `  b )  =  ( F `  b ) )
7473breq1d 4190 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( O  =  ( F  |`  T )  /\  a  C_  T )  /\  b  e.  a )  ->  ( ( O `  b ) R N  <->  ( F `  b ) R N ) )
7574ralbidva 2690 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( O  =  ( F  |`  T )  /\  a  C_  T )  ->  ( A. b  e.  a 
( O `  b
) R N  <->  A. b  e.  a  ( F `  b ) R N ) )
7664, 67, 75syl2anc 643 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  ( A. b  e.  a  ( O `  b ) R N  <->  A. b  e.  a  ( F `  b
) R N ) )
7762, 76mpbid 202 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  A. b  e.  a  ( F `  b ) R N )
7832simpli 445 . . . . . . . . . . . . . . . . . . . . . 22  |-  Fun  F
79 funfn 5449 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( Fun 
F  <->  F  Fn  dom  F )
8078, 79mpbi 200 . . . . . . . . . . . . . . . . . . . . 21  |-  F  Fn  dom  F
81 inss2 3530 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( T  i^i  dom  F )  C_ 
dom  F
8266, 81syl6ss 3328 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  a  C_  dom  F )
83 breq1 4183 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  ( F `  b )  ->  (
j R N  <->  ( F `  b ) R N ) )
8483ralima 5945 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( F  Fn  dom  F  /\  a  C_  dom  F
)  ->  ( A. j  e.  ( F " a ) j R N  <->  A. b  e.  a  ( F `  b
) R N ) )
8580, 82, 84sylancr 645 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  ( A. j  e.  ( F " a ) j R N  <->  A. b  e.  a  ( F `  b
) R N ) )
8677, 85mpbird 224 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  A. j  e.  ( F " a
) j R N )
87 breq2 4184 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  =  N  ->  (
j R w  <->  j R N ) )
8887ralbidv 2694 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  N  ->  ( A. j  e.  ( F " a ) j R w  <->  A. j  e.  ( F " a
) j R N ) )
8988elrab 3060 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  { w  e.  A  |  A. j  e.  ( F " a
) j R w }  <->  ( N  e.  A  /\  A. j  e.  ( F " a
) j R N ) )
9061, 86, 89sylanbrc 646 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  N  e.  { w  e.  A  |  A. j  e.  ( F " a ) j R w } )
9164fveq1d 5697 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  ( O `  a )  =  ( ( F  |`  T ) `
 a ) )
9213, 54sseldi 3314 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  a  e.  T )
93 fvres 5712 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  e.  T  ->  (
( F  |`  T ) `
 a )  =  ( F `  a
) )
9492, 93syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  ( ( F  |`  T ) `  a )  =  ( F `  a ) )
9591, 94eqtrd 2444 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  ( O `  a )  =  ( F `  a ) )
96 simpll 731 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  ph )
972, 3, 4, 5, 6, 7, 8ordtypelem3 7453 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  a  e.  ( T  i^i  dom  F
) )  ->  ( F `  a )  e.  { v  e.  {
w  e.  A  |  A. j  e.  ( F " a ) j R w }  |  A. u  e.  { w  e.  A  |  A. j  e.  ( F " a ) j R w }  -.  u R v } )
9896, 54, 97syl2anc 643 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  ( F `  a )  e.  {
v  e.  { w  e.  A  |  A. j  e.  ( F " a ) j R w }  |  A. u  e.  { w  e.  A  |  A. j  e.  ( F " a ) j R w }  -.  u R v } )
9995, 98eqeltrd 2486 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  ( O `  a )  e.  {
v  e.  { w  e.  A  |  A. j  e.  ( F " a ) j R w }  |  A. u  e.  { w  e.  A  |  A. j  e.  ( F " a ) j R w }  -.  u R v } )
100 breq2 4184 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( v  =  ( O `  a )  ->  (
u R v  <->  u R
( O `  a
) ) )
101100notbid 286 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( v  =  ( O `  a )  ->  ( -.  u R v  <->  -.  u R ( O `  a ) ) )
102101ralbidv 2694 . . . . . . . . . . . . . . . . . . . . 21  |-  ( v  =  ( O `  a )  ->  ( A. u  e.  { w  e.  A  |  A. j  e.  ( F " a ) j R w }  -.  u R v  <->  A. u  e.  { w  e.  A  |  A. j  e.  ( F " a ) j R w }  -.  u R ( O `
 a ) ) )
103102elrab 3060 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( O `  a )  e.  { v  e. 
{ w  e.  A  |  A. j  e.  ( F " a ) j R w }  |  A. u  e.  {
w  e.  A  |  A. j  e.  ( F " a ) j R w }  -.  u R v }  <->  ( ( O `  a )  e.  { w  e.  A  |  A. j  e.  ( F " a ) j R w }  /\  A. u  e.  {
w  e.  A  |  A. j  e.  ( F " a ) j R w }  -.  u R ( O `  a ) ) )
104103simprbi 451 . . . . . . . . . . . . . . . . . . 19  |-  ( ( O `  a )  e.  { v  e. 
{ w  e.  A  |  A. j  e.  ( F " a ) j R w }  |  A. u  e.  {
w  e.  A  |  A. j  e.  ( F " a ) j R w }  -.  u R v }  ->  A. u  e.  { w  e.  A  |  A. j  e.  ( F " a ) j R w }  -.  u R ( O `  a ) )
10599, 104syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  A. u  e.  { w  e.  A  |  A. j  e.  ( F " a ) j R w }  -.  u R ( O `
 a ) )
106 breq1 4183 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  =  N  ->  (
u R ( O `
 a )  <->  N R
( O `  a
) ) )
107106notbid 286 . . . . . . . . . . . . . . . . . . 19  |-  ( u  =  N  ->  ( -.  u R ( O `
 a )  <->  -.  N R ( O `  a ) ) )
108107rspcv 3016 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  { w  e.  A  |  A. j  e.  ( F " a
) j R w }  ->  ( A. u  e.  { w  e.  A  |  A. j  e.  ( F " a ) j R w }  -.  u R ( O `  a )  ->  -.  N R ( O `  a ) ) )
10990, 105, 108sylc 58 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  -.  N R ( O `  a ) )
110 weso 4541 . . . . . . . . . . . . . . . . . . . . 21  |-  ( R  We  A  ->  R  Or  A )
1117, 110syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  R  Or  A )
112111ad2antrr 707 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  R  Or  A )
11349, 54ffvelrnd 5838 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  ( O `  a )  e.  A
)
114 sotric 4497 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R  Or  A  /\  ( ( O `  a )  e.  A  /\  N  e.  A
) )  ->  (
( O `  a
) R N  <->  -.  (
( O `  a
)  =  N  \/  N R ( O `  a ) ) ) )
115112, 113, 61, 114syl12anc 1182 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  ( ( O `  a ) R N  <->  -.  ( ( O `  a )  =  N  \/  N R ( O `  a ) ) ) )
116 ioran 477 . . . . . . . . . . . . . . . . . 18  |-  ( -.  ( ( O `  a )  =  N  \/  N R ( O `  a ) )  <->  ( -.  ( O `  a )  =  N  /\  -.  N R ( O `  a ) ) )
117115, 116syl6bb 253 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  ( ( O `  a ) R N  <->  ( -.  ( O `  a )  =  N  /\  -.  N R ( O `  a ) ) ) )
11859, 109, 117mpbir2and 889 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  ( O `  a ) R N )
119118expr 599 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  a  e.  dom  O )  -> 
( A. b  e.  a  ( O `  b ) R N  ->  ( O `  a ) R N ) )
12046, 119sylbid 207 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  a  e.  dom  O )  -> 
( A. b  e.  a  ( b  e. 
dom  O  ->  ( O `
 b ) R N )  ->  ( O `  a ) R N ) )
121120ex 424 . . . . . . . . . . . . 13  |-  ( (
ph  /\  N  e.  ( A  \  ran  O
) )  ->  (
a  e.  dom  O  ->  ( A. b  e.  a  ( b  e. 
dom  O  ->  ( O `
 b ) R N )  ->  ( O `  a ) R N ) ) )
122121com23 74 . . . . . . . . . . . 12  |-  ( (
ph  /\  N  e.  ( A  \  ran  O
) )  ->  ( A. b  e.  a 
( b  e.  dom  O  ->  ( O `  b ) R N )  ->  ( a  e.  dom  O  ->  ( O `  a ) R N ) ) )
123122a2i 13 . . . . . . . . . . 11  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  ->  A. b  e.  a  ( b  e.  dom  O  ->  ( O `  b ) R N ) )  -> 
( ( ph  /\  N  e.  ( A  \  ran  O ) )  ->  ( a  e. 
dom  O  ->  ( O `
 a ) R N ) ) )
124123a1i 11 . . . . . . . . . 10  |-  ( a  e.  On  ->  (
( ( ph  /\  N  e.  ( A  \  ran  O ) )  ->  A. b  e.  a  ( b  e.  dom  O  ->  ( O `  b ) R N ) )  ->  (
( ph  /\  N  e.  ( A  \  ran  O ) )  ->  (
a  e.  dom  O  ->  ( O `  a
) R N ) ) ) )
12531, 124syl5bi 209 . . . . . . . . 9  |-  ( a  e.  On  ->  ( A. b  e.  a 
( ( ph  /\  N  e.  ( A  \  ran  O ) )  ->  ( b  e. 
dom  O  ->  ( O `
 b ) R N ) )  -> 
( ( ph  /\  N  e.  ( A  \  ran  O ) )  ->  ( a  e. 
dom  O  ->  ( O `
 a ) R N ) ) ) )
12625, 30, 125tfis3 4804 . . . . . . . 8  |-  ( M  e.  On  ->  (
( ph  /\  N  e.  ( A  \  ran  O ) )  ->  ( M  e.  dom  O  -> 
( O `  M
) R N ) ) )
127126com3l 77 . . . . . . 7  |-  ( (
ph  /\  N  e.  ( A  \  ran  O
) )  ->  ( M  e.  dom  O  -> 
( M  e.  On  ->  ( O `  M
) R N ) ) )
12820, 127mpdd 38 . . . . . 6  |-  ( (
ph  /\  N  e.  ( A  \  ran  O
) )  ->  ( M  e.  dom  O  -> 
( O `  M
) R N ) )
1291, 128sylan2br 463 . . . . 5  |-  ( (
ph  /\  ( N  e.  A  /\  -.  N  e.  ran  O ) )  ->  ( M  e. 
dom  O  ->  ( O `
 M ) R N ) )
130129anassrs 630 . . . 4  |-  ( ( ( ph  /\  N  e.  A )  /\  -.  N  e.  ran  O )  ->  ( M  e. 
dom  O  ->  ( O `
 M ) R N ) )
131130impancom 428 . . 3  |-  ( ( ( ph  /\  N  e.  A )  /\  M  e.  dom  O )  -> 
( -.  N  e. 
ran  O  ->  ( O `
 M ) R N ) )
132131orrd 368 . 2  |-  ( ( ( ph  /\  N  e.  A )  /\  M  e.  dom  O )  -> 
( N  e.  ran  O  \/  ( O `  M ) R N ) )
133132orcomd 378 1  |-  ( ( ( ph  /\  N  e.  A )  /\  M  e.  dom  O )  -> 
( ( O `  M ) R N  \/  N  e.  ran  O ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    \/ wo 358    /\ wa 359    = wceq 1649    e. wcel 1721   A.wral 2674   E.wrex 2675   {crab 2678   _Vcvv 2924    \ cdif 3285    i^i cin 3287    C_ wss 3288   class class class wbr 4180    e. cmpt 4234    Or wor 4470   Se wse 4507    We wwe 4508   Ord word 4548   Oncon0 4549   Lim wlim 4550   dom cdm 4845   ran crn 4846    |` cres 4847   "cima 4848   Fun wfun 5415    Fn wfn 5416   -->wf 5417   ` cfv 5421   iota_crio 6509  recscrecs 6599  OrdIsocoi 7442
This theorem is referenced by:  ordtypelem9  7459  ordtypelem10  7460  oiiniseg  7466
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298  ax-nul 4306  ax-pow 4345  ax-pr 4371  ax-un 4668
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-rex 2680  df-reu 2681  df-rmo 2682  df-rab 2683  df-v 2926  df-sbc 3130  df-csb 3220  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-pss 3304  df-nul 3597  df-if 3708  df-pw 3769  df-sn 3788  df-pr 3789  df-tp 3790  df-op 3791  df-uni 3984  df-iun 4063  df-br 4181  df-opab 4235  df-mpt 4236  df-tr 4271  df-eprel 4462  df-id 4466  df-po 4471  df-so 4472  df-fr 4509  df-se 4510  df-we 4511  df-ord 4552  df-on 4553  df-lim 4554  df-suc 4555  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5385  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-riota 6516  df-recs 6600  df-oi 7443
  Copyright terms: Public domain W3C validator