Metamath Proof Explorer


Theorem ordtypelem8

Description: Lemma for ordtype . (Contributed by Mario Carneiro, 25-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 ordtypelem8 φ O Isom E , R dom O ran O

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 1 2 3 4 5 6 7 ordtypelem4 φ O : T dom F A
9 8 fdmd φ dom O = T dom F
10 inss1 T dom F T
11 1 2 3 4 5 6 7 ordtypelem2 φ Ord T
12 ordsson Ord T T On
13 11 12 syl φ T On
14 10 13 sstrid φ T dom F On
15 9 14 eqsstrd φ dom O On
16 epweon E We On
17 weso E We On E Or On
18 16 17 ax-mp E Or On
19 soss dom O On E Or On E Or dom O
20 15 18 19 mpisyl φ E Or dom O
21 8 frnd φ ran O A
22 wess ran O A R We A R We ran O
23 21 6 22 sylc φ R We ran O
24 weso R We ran O R Or ran O
25 sopo R Or ran O R Po ran O
26 23 24 25 3syl φ R Po ran O
27 8 ffund φ Fun O
28 funforn Fun O O : dom O onto ran O
29 27 28 sylib φ O : dom O onto ran O
30 epel a E b a b
31 1 2 3 4 5 6 7 ordtypelem6 φ b dom O a b O a R O b
32 30 31 syl5bi φ b dom O a E b O a R O b
33 32 ralrimiva φ b dom O a E b O a R O b
34 33 ralrimivw φ a dom O b dom O a E b O a R O b
35 soisoi E Or dom O R Po ran O O : dom O onto ran O a dom O b dom O a E b O a R O b O Isom E , R dom O ran O
36 20 26 29 34 35 syl22anc φ O Isom E , R dom O ran O