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 A | j ran h j R w
ordtypelem.3 G = h V ι v C | u C ¬ u R v
ordtypelem.5 T = x On | t A z F x z R t
ordtypelem.6 O = OrdIso R A
ordtypelem.7 φ R We A
ordtypelem.8 φ R Se A
Assertion ordtypelem6 φ M dom O N M O N R O M

Proof

Step Hyp Ref Expression
1 ordtypelem.1 F = recs G
2 ordtypelem.2 C = w A | j ran h j R w
3 ordtypelem.3 G = h V ι v C | u C ¬ u R v
4 ordtypelem.5 T = x On | t A z F x z R t
5 ordtypelem.6 O = OrdIso R A
6 ordtypelem.7 φ R We A
7 ordtypelem.8 φ 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 w A | j F M j R w | u w A | j F M j R w ¬ u R v w A | j F M j R w
11 simpr φ M dom O M dom O
12 1 2 3 4 5 6 7 ordtypelem4 φ O : T dom F A
13 12 fdmd φ dom O = T dom F
14 13 adantr φ M dom O dom O = T dom F
15 11 14 eleqtrd φ M dom O M T dom F
16 1 2 3 4 5 6 7 ordtypelem3 φ M T dom F F M v w A | j F M j R w | u w A | j F M j R w ¬ u R v
17 15 16 syldan φ M dom O F M v w A | j F M j R w | u w A | j F M j R w ¬ u R v
18 10 17 sselid φ M dom O F M w A | j F M j R w
19 breq2 w = F M j R w j R F M
20 19 ralbidv w = F M j F M j R w j F M j R F M
21 20 elrab F M w A | j F M j R w F M A j F M j R F M
22 21 simprbi F M w A | j F M j R w j F M j R F M
23 18 22 syl φ M dom O j 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 dom F dom F
32 13 31 eqsstrdi φ dom O dom F
33 32 sselda φ M dom O M dom F
34 ordelss Ord dom F M dom F M dom F
35 30 33 34 sylancr φ M dom O M dom F
36 breq1 j = F a j R F M F a R F M
37 36 ralima F Fn dom F M dom F j F M j R F M a M F a R F M
38 27 35 37 sylancr φ M dom O j F M j R F M a M F a R F M
39 23 38 mpbid φ M dom O a M F a R F M
40 39 adantrr φ M dom O N M a M F a R F M
41 simprr φ M dom O N M N M
42 9 40 41 rspcdva φ M dom O N M F N R F M
43 1 2 3 4 5 6 7 ordtypelem1 φ O = F T
44 43 adantr φ M dom O N M O = F T
45 44 fveq1d φ M dom O N M O N = F T N
46 1 2 3 4 5 6 7 ordtypelem2 φ Ord T
47 inss1 T dom F T
48 13 47 eqsstrdi φ dom O T
49 48 sselda φ M dom O M T
50 49 adantrr φ M dom O N M M T
51 ordelss Ord T M T M T
52 46 50 51 syl2an2r φ M dom O N M M T
53 52 41 sseldd φ M dom O N M N T
54 53 fvresd φ M dom O N M F T N = F N
55 45 54 eqtrd φ M dom O N M O N = F N
56 44 fveq1d φ M dom O N M O M = F T M
57 50 fvresd φ M dom O N M F T M = F M
58 56 57 eqtrd φ M dom O N M O M = F M
59 42 55 58 3brtr4d φ M dom O N M O N R O M
60 59 expr φ M dom O N M O N R O M