Metamath Proof Explorer

Theorem ordtypelem6

Description: Lemma for ordtype . (Contributed by Mario Carneiro, 24-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 ordtypelem6 
|- ( ( ph /\ M e. dom O ) -> ( N e. M -> ( O ` N ) R ( O ` M ) ) )

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 fveq2 
 |-  ( a = N -> ( F ` a ) = ( F ` N ) )
9 8 breq1d 
 |-  ( a = N -> ( ( F ` a ) R ( F ` M ) <-> ( F ` N ) R ( F ` M ) ) )
10 ssrab2 
 |-  { v e. { w e. A | A. j e. ( F " M ) j R w } | A. u e. { w e. A | A. j e. ( F " M ) j R w } -. u R v } C_ { w e. A | A. j e. ( F " M ) j R w }
11 simpr 
 |-  ( ( ph /\ M e. dom O ) -> M e. dom O )
12 1 2 3 4 5 6 7 ordtypelem4 
 |-  ( ph -> O : ( T i^i dom F ) --> A )
13 12 fdmd 
 |-  ( ph -> dom O = ( T i^i dom F ) )
14 13 adantr 
 |-  ( ( ph /\ M e. dom O ) -> dom O = ( T i^i dom F ) )
15 11 14 eleqtrd 
 |-  ( ( ph /\ M e. dom O ) -> M e. ( T i^i dom F ) )
16 1 2 3 4 5 6 7 ordtypelem3 
 |-  ( ( ph /\ M e. ( T i^i dom F ) ) -> ( F ` M ) e. { v e. { w e. A | A. j e. ( F " M ) j R w } | A. u e. { w e. A | A. j e. ( F " M ) j R w } -. u R v } )
17 15 16 syldan 
 |-  ( ( ph /\ M e. dom O ) -> ( F ` M ) e. { v e. { w e. A | A. j e. ( F " M ) j R w } | A. u e. { w e. A | A. j e. ( F " M ) j R w } -. u R v } )
18 10 17 sselid 
 |-  ( ( ph /\ M e. dom O ) -> ( F ` M ) e. { w e. A | A. j e. ( F " M ) j R w } )
19 breq2 
 |-  ( w = ( F ` M ) -> ( j R w <-> j R ( F ` M ) ) )
20 19 ralbidv 
 |-  ( w = ( F ` M ) -> ( A. j e. ( F " M ) j R w <-> A. j e. ( F " M ) j R ( F ` M ) ) )
21 20 elrab 
 |-  ( ( F ` M ) e. { w e. A | A. j e. ( F " M ) j R w } <-> ( ( F ` M ) e. A /\ A. j e. ( F " M ) j R ( F ` M ) ) )
22 21 simprbi 
 |-  ( ( F ` M ) e. { w e. A | A. j e. ( F " M ) j R w } -> A. j e. ( F " M ) j R ( F ` M ) )
23 18 22 syl 
 |-  ( ( ph /\ M e. dom O ) -> A. j e. ( F " M ) j R ( F ` M ) )
24 1 tfr1a 
 |-  ( Fun F /\ Lim dom F )
25 24 simpli 
 |-  Fun F
26 funfn 
 |-  ( Fun F <-> F Fn dom F )
27 25 26 mpbi 
 |-  F Fn dom F
28 24 simpri 
 |-  Lim dom F
29 limord 
 |-  ( Lim dom F -> Ord dom F )
30 28 29 ax-mp 
 |-  Ord dom F
31 inss2 
 |-  ( T i^i dom F ) C_ dom F
32 13 31 eqsstrdi 
 |-  ( ph -> dom O C_ dom F )
33 32 sselda 
 |-  ( ( ph /\ M e. dom O ) -> M e. dom F )
34 ordelss 
 |-  ( ( Ord dom F /\ M e. dom F ) -> M C_ dom F )
35 30 33 34 sylancr 
 |-  ( ( ph /\ M e. dom O ) -> M C_ dom F )
36 breq1 
 |-  ( j = ( F ` a ) -> ( j R ( F ` M ) <-> ( F ` a ) R ( F ` M ) ) )
37 36 ralima 
 |-  ( ( F Fn dom F /\ M C_ dom F ) -> ( A. j e. ( F " M ) j R ( F ` M ) <-> A. a e. M ( F ` a ) R ( F ` M ) ) )
38 27 35 37 sylancr 
 |-  ( ( ph /\ M e. dom O ) -> ( A. j e. ( F " M ) j R ( F ` M ) <-> A. a e. M ( F ` a ) R ( F ` M ) ) )
39 23 38 mpbid 
 |-  ( ( ph /\ M e. dom O ) -> A. a e. M ( F ` a ) R ( F ` M ) )
40 39 adantrr 
 |-  ( ( ph /\ ( M e. dom O /\ N e. M ) ) -> A. a e. M ( F ` a ) R ( F ` M ) )
41 simprr 
 |-  ( ( ph /\ ( M e. dom O /\ N e. M ) ) -> N e. M )
42 9 40 41 rspcdva 
 |-  ( ( ph /\ ( M e. dom O /\ N e. M ) ) -> ( F ` N ) R ( F ` M ) )
43 1 2 3 4 5 6 7 ordtypelem1 
 |-  ( ph -> O = ( F |` T ) )
44 43 adantr 
 |-  ( ( ph /\ ( M e. dom O /\ N e. M ) ) -> O = ( F |` T ) )
45 44 fveq1d 
 |-  ( ( ph /\ ( M e. dom O /\ N e. M ) ) -> ( O ` N ) = ( ( F |` T ) ` N ) )
46 1 2 3 4 5 6 7 ordtypelem2 
 |-  ( ph -> Ord T )
47 inss1 
 |-  ( T i^i dom F ) C_ T
48 13 47 eqsstrdi 
 |-  ( ph -> dom O C_ T )
49 48 sselda 
 |-  ( ( ph /\ M e. dom O ) -> M e. T )
50 49 adantrr 
 |-  ( ( ph /\ ( M e. dom O /\ N e. M ) ) -> M e. T )
51 ordelss 
 |-  ( ( Ord T /\ M e. T ) -> M C_ T )
52 46 50 51 syl2an2r 
 |-  ( ( ph /\ ( M e. dom O /\ N e. M ) ) -> M C_ T )
53 52 41 sseldd 
 |-  ( ( ph /\ ( M e. dom O /\ N e. M ) ) -> N e. T )
54 53 fvresd 
 |-  ( ( ph /\ ( M e. dom O /\ N e. M ) ) -> ( ( F |` T ) ` N ) = ( F ` N ) )
55 45 54 eqtrd 
 |-  ( ( ph /\ ( M e. dom O /\ N e. M ) ) -> ( O ` N ) = ( F ` N ) )
56 44 fveq1d 
 |-  ( ( ph /\ ( M e. dom O /\ N e. M ) ) -> ( O ` M ) = ( ( F |` T ) ` M ) )
57 50 fvresd 
 |-  ( ( ph /\ ( M e. dom O /\ N e. M ) ) -> ( ( F |` T ) ` M ) = ( F ` M ) )
58 56 57 eqtrd 
 |-  ( ( ph /\ ( M e. dom O /\ N e. M ) ) -> ( O ` M ) = ( F ` M ) )
59 42 55 58 3brtr4d 
 |-  ( ( ph /\ ( M e. dom O /\ N e. M ) ) -> ( O ` N ) R ( O ` M ) )
60 59 expr 
 |-  ( ( ph /\ M e. dom O ) -> ( N e. M -> ( O ` N ) R ( O ` M ) ) )