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

Theorem ordtypelem7 7496
Description: Lemma for ordtype 7504. 
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 3332 . . . . . 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 7493 . . . . . . . . . . 11  |-  ( ph  ->  O : ( T  i^i  dom  F ) --> A )
109adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  N  e.  ( A  \  ran  O
) )  ->  O : ( T  i^i  dom 
F ) --> A )
11 fdm 5598 . . . . . . . . . 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 3563 . . . . . . . . . 10  |-  ( T  i^i  dom  F )  C_  T
142, 3, 4, 5, 6, 7, 8ordtypelem2 7491 . . . . . . . . . . . 12  |-  ( ph  ->  Ord  T )
1514adantr 453 . . . . . . . . . . 11  |-  ( (
ph  /\  N  e.  ( A  \  ran  O
) )  ->  Ord  T )
16 ordsson 4773 . . . . . . . . . . 11  |-  ( Ord 
T  ->  T  C_  On )
1715, 16syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  N  e.  ( A  \  ran  O
) )  ->  T  C_  On )
1813, 17syl5ss 3361 . . . . . . . . 9  |-  ( (
ph  /\  N  e.  ( A  \  ran  O
) )  ->  ( T  i^i  dom  F )  C_  On )
1912, 18eqsstrd 3384 . . . . . . . 8  |-  ( (
ph  /\  N  e.  ( A  \  ran  O
) )  ->  dom  O 
C_  On )
2019sseld 3349 . . . . . . 7  |-  ( (
ph  /\  N  e.  ( A  \  ran  O
) )  ->  ( M  e.  dom  O  ->  M  e.  On )
)
21 eleq1 2498 . . . . . . . . . . 11  |-  ( a  =  b  ->  (
a  e.  dom  O  <->  b  e.  dom  O ) )
22 fveq2 5731 . . . . . . . . . . . 12  |-  ( a  =  b  ->  ( O `  a )  =  ( O `  b ) )
2322breq1d 4225 . . . . . . . . . . 11  |-  ( a  =  b  ->  (
( O `  a
) R N  <->  ( O `  b ) R N ) )
2421, 23imbi12d 313 . . . . . . . . . 10  |-  ( a  =  b  ->  (
( a  e.  dom  O  ->  ( O `  a ) R N )  <->  ( b  e. 
dom  O  ->  ( O `
 b ) R N ) ) )
2524imbi2d 309 . . . . . . . . 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 2498 . . . . . . . . . . 11  |-  ( a  =  M  ->  (
a  e.  dom  O  <->  M  e.  dom  O ) )
27 fveq2 5731 . . . . . . . . . . . 12  |-  ( a  =  M  ->  ( O `  a )  =  ( O `  M ) )
2827breq1d 4225 . . . . . . . . . . 11  |-  ( a  =  M  ->  (
( O `  a
) R N  <->  ( O `  M ) R N ) )
2926, 28imbi12d 313 . . . . . . . . . 10  |-  ( a  =  M  ->  (
( a  e.  dom  O  ->  ( O `  a ) R N )  <->  ( M  e. 
dom  O  ->  ( O `
 M ) R N ) ) )
3029imbi2d 309 . . . . . . . . 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 2795 . . . . . . . . . 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 6658 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( Fun 
F  /\  Lim  dom  F
)
3332simpri 450 . . . . . . . . . . . . . . . . . . . . . 22  |-  Lim  dom  F
34 limord 4643 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( Lim 
dom  F  ->  Ord  dom  F )
3533, 34ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21  |-  Ord  dom  F
36 ordin 4614 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( Ord  T  /\  Ord  dom 
F )  ->  Ord  ( T  i^i  dom  F
) )
3715, 35, 36sylancl 645 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  N  e.  ( A  \  ran  O
) )  ->  Ord  ( T  i^i  dom  F
) )
38 ordeq 4591 . . . . . . . . . . . . . . . . . . . . 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 225 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  N  e.  ( A  \  ran  O
) )  ->  Ord  dom 
O )
41 ordelss 4600 . . . . . . . . . . . . . . . . . . 19  |-  ( ( Ord  dom  O  /\  a  e.  dom  O )  ->  a  C_  dom  O )
4240, 41sylan 459 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  a  e.  dom  O )  -> 
a  C_  dom  O )
4342sselda 3350 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  a  e.  dom  O )  /\  b  e.  a )  ->  b  e.  dom  O )
44 pm5.5 328 . . . . . . . . . . . . . . . . 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 2723 . . . . . . . . . . . . . . 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 3472 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  ( A  \  ran  O )  ->  -.  N  e.  ran  O )
4847ad2antlr 709 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  -.  N  e.  ran  O )
499ad2antrr 708 . . . . . . . . . . . . . . . . . . . . 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 5594 . . . . . . . . . . . . . . . . . . . . 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 734 . . . . . . . . . . . . . . . . . . . . 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 2514 . . . . . . . . . . . . . . . . . . . 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 5870 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( O  Fn  ( T  i^i  dom  F )  /\  a  e.  ( T  i^i  dom  F )
)  ->  ( O `  a )  e.  ran  O )
5651, 54, 55syl2anc 644 . . . . . . . . . . . . . . . . . . 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 2498 . . . . . . . . . . . . . . . . . . 19  |-  ( ( O `  a )  =  N  ->  (
( O `  a
)  e.  ran  O  <->  N  e.  ran  O ) )
5856, 57syl5ibcom 213 . . . . . . . . . . . . . . . . . 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 171 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  -.  ( O `  a )  =  N )
60 eldifi 3471 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  ( A  \  ran  O )  ->  N  e.  A )
6160ad2antlr 709 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  N  e.  A )
62 simprr 735 . . . . . . . . . . . . . . . . . . . . 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 7490 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  O  =  ( F  |`  T ) )
6463ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  O  =  ( F  |`  T ) )
6542adantrr 699 . . . . . . . . . . . . . . . . . . . . . . . 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 3386 . . . . . . . . . . . . . . . . . . . . . . 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 3362 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  a  C_  T )
68 fveq1 5730 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( O  =  ( F  |`  T )  ->  ( O `  b )  =  ( ( F  |`  T ) `  b
) )
69 ssel2 3345 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( a  C_  T  /\  b  e.  a )  ->  b  e.  T )
70 fvres 5748 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2490 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( O  =  ( F  |`  T )  /\  (
a  C_  T  /\  b  e.  a )
)  ->  ( O `  b )  =  ( F `  b ) )
7372anassrs 631 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( O  =  ( F  |`  T )  /\  a  C_  T )  /\  b  e.  a )  ->  ( O `  b )  =  ( F `  b ) )
7473breq1d 4225 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( O  =  ( F  |`  T )  /\  a  C_  T )  /\  b  e.  a )  ->  ( ( O `  b ) R N  <->  ( F `  b ) R N ) )
7574ralbidva 2723 . . . . . . . . . . . . . . . . . . . . . 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 644 . . . . . . . . . . . . . . . . . . . . 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 203 . . . . . . . . . . . . . . . . . . . 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 446 . . . . . . . . . . . . . . . . . . . . . 22  |-  Fun  F
79 funfn 5485 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( Fun 
F  <->  F  Fn  dom  F )
8078, 79mpbi 201 . . . . . . . . . . . . . . . . . . . . 21  |-  F  Fn  dom  F
81 inss2 3564 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( T  i^i  dom  F )  C_ 
dom  F
8266, 81syl6ss 3362 . . . . . . . . . . . . . . . . . . . . 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 4218 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  ( F `  b )  ->  (
j R N  <->  ( F `  b ) R N ) )
8483ralima 5981 . . . . . . . . . . . . . . . . . . . . 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 646 . . . . . . . . . . . . . . . . . . . 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 225 . . . . . . . . . . . . . . . . . . 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 4219 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  =  N  ->  (
j R w  <->  j R N ) )
8887ralbidv 2727 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  N  ->  ( A. j  e.  ( F " a ) j R w  <->  A. j  e.  ( F " a
) j R N ) )
8988elrab 3094 . . . . . . . . . . . . . . . . . . 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 647 . . . . . . . . . . . . . . . . . 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 5733 . . . . . . . . . . . . . . . . . . . . 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 3348 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  a  e.  T )
93 fvres 5748 . . . . . . . . . . . . . . . . . . . . . 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 2470 . . . . . . . . . . . . . . . . . . . 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 732 . . . . . . . . . . . . . . . . . . . . 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 7492 . . . . . . . . . . . . . . . . . . . . 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 644 . . . . . . . . . . . . . . . . . . . 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 2512 . . . . . . . . . . . . . . . . . . 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 4219 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( v  =  ( O `  a )  ->  (
u R v  <->  u R
( O `  a
) ) )
101100notbid 287 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( v  =  ( O `  a )  ->  ( -.  u R v  <->  -.  u R ( O `  a ) ) )
102101ralbidv 2727 . . . . . . . . . . . . . . . . . . . . 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 3094 . . . . . . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . . . . . 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 4218 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  =  N  ->  (
u R ( O `
 a )  <->  N R
( O `  a
) ) )
107106notbid 287 . . . . . . . . . . . . . . . . . . 19  |-  ( u  =  N  ->  ( -.  u R ( O `
 a )  <->  -.  N R ( O `  a ) ) )
108107rspcv 3050 . . . . . . . . . . . . . . . . . 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 59 . . . . . . . . . . . . . . . . 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 4576 . . . . . . . . . . . . . . . . . . . . 21  |-  ( R  We  A  ->  R  Or  A )
1117, 110syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  R  Or  A )
112111ad2antrr 708 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  R  Or  A )
11349, 54ffvelrnd 5874 . . . . . . . . . . . . . . . . . . 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 4532 . . . . . . . . . . . . . . . . . . 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 1183 . . . . . . . . . . . . . . . . . 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 478 . . . . . . . . . . . . . . . . . 18  |-  ( -.  ( ( O `  a )  =  N  \/  N R ( O `  a ) )  <->  ( -.  ( O `  a )  =  N  /\  -.  N R ( O `  a ) ) )
117115, 116syl6bb 254 . . . . . . . . . . . . . . . . 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 890 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  N  e.  ( A  \  ran  O ) )  /\  (
a  e.  dom  O  /\  A. b  e.  a  ( O `  b
) R N ) )  ->  ( O `  a ) R N )
119118expr 600 . . . . . . . . . . . . . . 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 208 . . . . . . . . . . . . . 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 425 . . . . . . . . . . . . 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 75 . . . . . . . . . . . 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 210 . . . . . . . . 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 4840 . . . . . . . 8  |-  ( M  e.  On  ->  (
( ph  /\  N  e.  ( A  \  ran  O ) )  ->  ( M  e.  dom  O  -> 
( O `  M
) R N ) ) )
127126com3l 78 . . . . . . 7  |-  ( (
ph  /\  N  e.  ( A  \  ran  O
) )  ->  ( M  e.  dom  O  -> 
( M  e.  On  ->  ( O `  M
) R N ) ) )
12820, 127mpdd 39 . . . . . 6  |-  ( (
ph  /\  N  e.  ( A  \  ran  O
) )  ->  ( M  e.  dom  O  -> 
( O `  M
) R N ) )
1291, 128sylan2br 464 . . . . 5  |-  ( (
ph  /\  ( N  e.  A  /\  -.  N  e.  ran  O ) )  ->  ( M  e. 
dom  O  ->  ( O `
 M ) R N ) )
130129anassrs 631 . . . 4  |-  ( ( ( ph  /\  N  e.  A )  /\  -.  N  e.  ran  O )  ->  ( M  e. 
dom  O  ->  ( O `
 M ) R N ) )
131130impancom 429 . . 3  |-  ( ( ( ph  /\  N  e.  A )  /\  M  e.  dom  O )  -> 
( -.  N  e. 
ran  O  ->  ( O `
 M ) R N ) )
132131orrd 369 . 2  |-  ( ( ( ph  /\  N  e.  A )  /\  M  e.  dom  O )  -> 
( N  e.  ran  O  \/  ( O `  M ) R N ) )
133132orcomd 379 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 178    \/ wo 359    /\ wa 360    = wceq 1653    e. wcel 1726   A.wral 2707   E.wrex 2708   {crab 2711   _Vcvv 2958    \ cdif 3319    i^i cin 3321    C_ wss 3322   class class class wbr 4215    e. cmpt 4269    Or wor 4505   Se wse 4542    We wwe 4543   Ord word 4583   Oncon0 4584   Lim wlim 4585   dom cdm 4881   ran crn 4882    |` cres 4883   "cima 4884   Fun wfun 5451    Fn wfn 5452   -->wf 5453   ` cfv 5457   iota_crio 6545  recscrecs 6635  OrdIsocoi 7481
This theorem is referenced by:  ordtypelem9  7498  ordtypelem10  7499  oiiniseg  7505
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-iun 4097  df-br 4216  df-opab 4270  df-mpt 4271  df-tr 4306  df-eprel 4497  df-id 4501  df-po 4506  df-so 4507  df-fr 4544  df-se 4545  df-we 4546  df-ord 4587  df-on 4588  df-lim 4589  df-suc 4590  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-riota 6552  df-recs 6636  df-oi 7482
  Copyright terms: Public domain W3C validator