Metamath Proof Explorer

Theorem ordtypelem7

Description: Lemma for ordtype . ran O is an initial segment of A under the well-order R . (Contributed by Mario Carneiro, 25-Jun-2015)

Ref Expression
Hypotheses 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 ordtypelem7 
|- ( ( ( ph /\ N e. A ) /\ M e. dom O ) -> ( ( O ` M ) R N \/ N e. ran O ) )

Proof

Step Hyp Ref Expression
1 ordtypelem.1 
 |-  F = recs ( G )
2 ordtypelem.2 
 |-  C = { w e. A | A. j e. ran h j R w }
3 ordtypelem.3 
 |-  G = ( h e. _V |-> ( iota_ v e. C A. u e. C -. u R v ) )
4 ordtypelem.5 
 |-  T = { x e. On | E. t e. A A. z e. ( F " x ) z R t }
5 ordtypelem.6 
 |-  O = OrdIso ( R , A )
6 ordtypelem.7 
 |-  ( ph -> R We A )
7 ordtypelem.8 
 |-  ( ph -> R Se A )
8 eldif 
 |-  ( N e. ( A \ ran O ) <-> ( N e. A /\ -. N e. ran O ) )
9 1 2 3 4 5 6 7 ordtypelem4 
 |-  ( ph -> O : ( T i^i dom F ) --> A )
10 9 adantr 
 |-  ( ( ph /\ N e. ( A \ ran O ) ) -> O : ( T i^i dom F ) --> A )
11 10 fdmd 
 |-  ( ( ph /\ N e. ( A \ ran O ) ) -> dom O = ( T i^i dom F ) )
12 inss1 
 |-  ( T i^i dom F ) C_ T
13 1 2 3 4 5 6 7 ordtypelem2 
 |-  ( ph -> Ord T )
14 13 adantr 
 |-  ( ( ph /\ N e. ( A \ ran O ) ) -> Ord T )
15 ordsson 
 |-  ( Ord T -> T C_ On )
16 14 15 syl 
 |-  ( ( ph /\ N e. ( A \ ran O ) ) -> T C_ On )
17 12 16 sstrid 
 |-  ( ( ph /\ N e. ( A \ ran O ) ) -> ( T i^i dom F ) C_ On )
18 11 17 eqsstrd 
 |-  ( ( ph /\ N e. ( A \ ran O ) ) -> dom O C_ On )
19 18 sseld 
 |-  ( ( ph /\ N e. ( A \ ran O ) ) -> ( M e. dom O -> M e. On ) )
20 eleq1 
 |-  ( a = b -> ( a e. dom O <-> b e. dom O ) )
21 fveq2 
 |-  ( a = b -> ( O ` a ) = ( O ` b ) )
22 21 breq1d 
 |-  ( a = b -> ( ( O ` a ) R N <-> ( O ` b ) R N ) )
23 20 22 imbi12d 
 |-  ( a = b -> ( ( a e. dom O -> ( O ` a ) R N ) <-> ( b e. dom O -> ( O ` b ) R N ) ) )
24 23 imbi2d 
 |-  ( 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 ) ) ) )
25 eleq1 
 |-  ( a = M -> ( a e. dom O <-> M e. dom O ) )
26 fveq2 
 |-  ( a = M -> ( O ` a ) = ( O ` M ) )
27 26 breq1d 
 |-  ( a = M -> ( ( O ` a ) R N <-> ( O ` M ) R N ) )
28 25 27 imbi12d 
 |-  ( a = M -> ( ( a e. dom O -> ( O ` a ) R N ) <-> ( M e. dom O -> ( O ` M ) R N ) ) )
29 28 imbi2d 
 |-  ( 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 ) ) ) )
30 r19.21v 
 |-  ( 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 ) ) )
31 1 tfr1a 
 |-  ( Fun F /\ Lim dom F )
32 31 simpri 
 |-  Lim dom F
33 limord 
 |-  ( Lim dom F -> Ord dom F )
34 32 33 ax-mp 
 |-  Ord dom F
35 ordin 
 |-  ( ( Ord T /\ Ord dom F ) -> Ord ( T i^i dom F ) )
36 14 34 35 sylancl 
 |-  ( ( ph /\ N e. ( A \ ran O ) ) -> Ord ( T i^i dom F ) )
37 ordeq 
 |-  ( dom O = ( T i^i dom F ) -> ( Ord dom O <-> Ord ( T i^i dom F ) ) )
38 11 37 syl 
 |-  ( ( ph /\ N e. ( A \ ran O ) ) -> ( Ord dom O <-> Ord ( T i^i dom F ) ) )
39 36 38 mpbird 
 |-  ( ( ph /\ N e. ( A \ ran O ) ) -> Ord dom O )
40 ordelss 
 |-  ( ( Ord dom O /\ a e. dom O ) -> a C_ dom O )
41 39 40 sylan 
 |-  ( ( ( ph /\ N e. ( A \ ran O ) ) /\ a e. dom O ) -> a C_ dom O )
42 41 sselda 
 |-  ( ( ( ( ph /\ N e. ( A \ ran O ) ) /\ a e. dom O ) /\ b e. a ) -> b e. dom O )
43 pm5.5 
 |-  ( b e. dom O -> ( ( b e. dom O -> ( O ` b ) R N ) <-> ( O ` b ) R N ) )
44 42 43 syl 
 |-  ( ( ( ( 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 ) )
45 44 ralbidva 
 |-  ( ( ( 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 ) )
46 eldifn 
 |-  ( N e. ( A \ ran O ) -> -. N e. ran O )
47 46 ad2antlr 
 |-  ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> -. N e. ran O )
48 9 ad2antrr 
 |-  ( ( ( 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 )
49 48 ffnd 
 |-  ( ( ( 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 ) )
50 simprl 
 |-  ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> a e. dom O )
51 48 fdmd 
 |-  ( ( ( 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 ) )
52 50 51 eleqtrd 
 |-  ( ( ( 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 ) )
53 fnfvelrn 
 |-  ( ( O Fn ( T i^i dom F ) /\ a e. ( T i^i dom F ) ) -> ( O ` a ) e. ran O )
54 49 52 53 syl2anc 
 |-  ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> ( O ` a ) e. ran O )
55 eleq1 
 |-  ( ( O ` a ) = N -> ( ( O ` a ) e. ran O <-> N e. ran O ) )
56 54 55 syl5ibcom 
 |-  ( ( ( 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 ) )
57 47 56 mtod 
 |-  ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> -. ( O ` a ) = N )
58 breq1 
 |-  ( u = N -> ( u R ( O ` a ) <-> N R ( O ` a ) ) )
59 58 notbid 
 |-  ( u = N -> ( -. u R ( O ` a ) <-> -. N R ( O ` a ) ) )
60 1 2 3 4 5 6 7 ordtypelem1 
 |-  ( ph -> O = ( F |` T ) )
61 60 ad2antrr 
 |-  ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> O = ( F |` T ) )
62 61 fveq1d 
 |-  ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> ( O ` a ) = ( ( F |` T ) ` a ) )
63 52 elin1d 
 |-  ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> a e. T )
64 63 fvresd 
 |-  ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> ( ( F |` T ) ` a ) = ( F ` a ) )
65 62 64 eqtrd 
 |-  ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> ( O ` a ) = ( F ` a ) )
66 simpll 
 |-  ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> ph )
67 1 2 3 4 5 6 7 ordtypelem3 
 |-  ( ( 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 } )
68 66 52 67 syl2anc 
 |-  ( ( ( 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 } )
69 65 68 eqeltrd 
 |-  ( ( ( 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 } )
70 breq2 
 |-  ( v = ( O ` a ) -> ( u R v <-> u R ( O ` a ) ) )
71 70 notbid 
 |-  ( v = ( O ` a ) -> ( -. u R v <-> -. u R ( O ` a ) ) )
72 71 ralbidv 
 |-  ( 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 ) ) )
73 72 elrab 
 |-  ( ( 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 ) ) )
74 73 simprbi 
 |-  ( ( 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 ) )
75 69 74 syl 
 |-  ( ( ( 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 ) )
76 breq2 
 |-  ( w = N -> ( j R w <-> j R N ) )
77 76 ralbidv 
 |-  ( w = N -> ( A. j e. ( F " a ) j R w <-> A. j e. ( F " a ) j R N ) )
78 eldifi 
 |-  ( N e. ( A \ ran O ) -> N e. A )
79 78 ad2antlr 
 |-  ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> N e. A )
80 simprr 
 |-  ( ( ( 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 )
81 41 adantrr 
 |-  ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> a C_ dom O )
82 48 81 fssdmd 
 |-  ( ( ( 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 ) )
83 82 12 sstrdi 
 |-  ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> a C_ T )
84 fveq1 
 |-  ( O = ( F |` T ) -> ( O ` b ) = ( ( F |` T ) ` b ) )
85 ssel2 
 |-  ( ( a C_ T /\ b e. a ) -> b e. T )
86 85 fvresd 
 |-  ( ( a C_ T /\ b e. a ) -> ( ( F |` T ) ` b ) = ( F ` b ) )
87 84 86 sylan9eq 
 |-  ( ( O = ( F |` T ) /\ ( a C_ T /\ b e. a ) ) -> ( O ` b ) = ( F ` b ) )
88 87 anassrs 
 |-  ( ( ( O = ( F |` T ) /\ a C_ T ) /\ b e. a ) -> ( O ` b ) = ( F ` b ) )
89 88 breq1d 
 |-  ( ( ( O = ( F |` T ) /\ a C_ T ) /\ b e. a ) -> ( ( O ` b ) R N <-> ( F ` b ) R N ) )
90 89 ralbidva 
 |-  ( ( O = ( F |` T ) /\ a C_ T ) -> ( A. b e. a ( O ` b ) R N <-> A. b e. a ( F ` b ) R N ) )
91 61 83 90 syl2anc 
 |-  ( ( ( 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 ) )
92 80 91 mpbid 
 |-  ( ( ( 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 )
93 31 simpli 
 |-  Fun F
94 funfn 
 |-  ( Fun F <-> F Fn dom F )
95 93 94 mpbi 
 |-  F Fn dom F
96 inss2 
 |-  ( T i^i dom F ) C_ dom F
97 82 96 sstrdi 
 |-  ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> a C_ dom F )
98 breq1 
 |-  ( j = ( F ` b ) -> ( j R N <-> ( F ` b ) R N ) )
99 98 ralima 
 |-  ( ( F Fn dom F /\ a C_ dom F ) -> ( A. j e. ( F " a ) j R N <-> A. b e. a ( F ` b ) R N ) )
100 95 97 99 sylancr 
 |-  ( ( ( 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 ) )
101 92 100 mpbird 
 |-  ( ( ( 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 )
102 77 79 101 elrabd 
 |-  ( ( ( 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 } )
103 59 75 102 rspcdva 
 |-  ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> -. N R ( O ` a ) )
104 weso 
 |-  ( R We A -> R Or A )
105 6 104 syl 
 |-  ( ph -> R Or A )
106 105 ad2antrr 
 |-  ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> R Or A )
107 48 52 ffvelrnd 
 |-  ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> ( O ` a ) e. A )
108 sotric 
 |-  ( ( R Or A /\ ( ( O ` a ) e. A /\ N e. A ) ) -> ( ( O ` a ) R N <-> -. ( ( O ` a ) = N \/ N R ( O ` a ) ) ) )
109 106 107 79 108 syl12anc 
 |-  ( ( ( 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 ) ) ) )
110 ioran 
 |-  ( -. ( ( O ` a ) = N \/ N R ( O ` a ) ) <-> ( -. ( O ` a ) = N /\ -. N R ( O ` a ) ) )
111 109 110 bitrdi 
 |-  ( ( ( 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 ) ) ) )
112 57 103 111 mpbir2and 
 |-  ( ( ( ph /\ N e. ( A \ ran O ) ) /\ ( a e. dom O /\ A. b e. a ( O ` b ) R N ) ) -> ( O ` a ) R N )
113 112 expr 
 |-  ( ( ( ph /\ N e. ( A \ ran O ) ) /\ a e. dom O ) -> ( A. b e. a ( O ` b ) R N -> ( O ` a ) R N ) )
114 45 113 sylbid 
 |-  ( ( ( 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 ) )
115 114 ex 
 |-  ( ( 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 ) ) )
116 115 com23 
 |-  ( ( 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 ) ) )
117 116 a2i 
 |-  ( ( ( 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 ) ) )
118 117 a1i 
 |-  ( 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 ) ) ) )
119 30 118 syl5bi 
 |-  ( 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 ) ) ) )
120 24 29 119 tfis3 
 |-  ( M e. On -> ( ( ph /\ N e. ( A \ ran O ) ) -> ( M e. dom O -> ( O ` M ) R N ) ) )
121 120 com3l 
 |-  ( ( ph /\ N e. ( A \ ran O ) ) -> ( M e. dom O -> ( M e. On -> ( O ` M ) R N ) ) )
122 19 121 mpdd 
 |-  ( ( ph /\ N e. ( A \ ran O ) ) -> ( M e. dom O -> ( O ` M ) R N ) )
123 8 122 sylan2br 
 |-  ( ( ph /\ ( N e. A /\ -. N e. ran O ) ) -> ( M e. dom O -> ( O ` M ) R N ) )
124 123 anassrs 
 |-  ( ( ( ph /\ N e. A ) /\ -. N e. ran O ) -> ( M e. dom O -> ( O ` M ) R N ) )
125 124 impancom 
 |-  ( ( ( ph /\ N e. A ) /\ M e. dom O ) -> ( -. N e. ran O -> ( O ` M ) R N ) )
126 125 orrd 
 |-  ( ( ( ph /\ N e. A ) /\ M e. dom O ) -> ( N e. ran O \/ ( O ` M ) R N ) )
127 126 orcomd 
 |-  ( ( ( ph /\ N e. A ) /\ M e. dom O ) -> ( ( O ` M ) R N \/ N e. ran O ) )