Metamath Proof Explorer


Theorem ordtypelem10

Description: Lemma for ordtype . Using ax-rep , exclude the possibility that O is a proper class and does not enumerate all of A . (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 ordtypelem10 φ O Isom E , R dom O A

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 ordtypelem8 φ O Isom E , R dom O ran O
9 1 2 3 4 5 6 7 ordtypelem4 φ O : T dom F A
10 9 frnd φ ran O A
11 simprl φ b A ¬ b ran O b A
12 6 adantr φ b A ¬ b ran O R We A
13 7 adantr φ b A ¬ b ran O R Se A
14 9 ffund φ Fun O
15 14 funfnd φ O Fn dom O
16 15 adantr φ b A ¬ b ran O O Fn dom O
17 1 2 3 4 5 12 13 ordtypelem8 φ b A ¬ b ran O O Isom E , R dom O ran O
18 isof1o O Isom E , R dom O ran O O : dom O 1-1 onto ran O
19 f1of1 O : dom O 1-1 onto ran O O : dom O 1-1 ran O
20 17 18 19 3syl φ b A ¬ b ran O O : dom O 1-1 ran O
21 simpl b A ¬ b ran O b A
22 seex R Se A b A c A | c R b V
23 7 21 22 syl2an φ b A ¬ b ran O c A | c R b V
24 10 adantr φ b A ¬ b ran O ran O A
25 rexnal m dom O ¬ O m R b ¬ m dom O O m R b
26 1 2 3 4 5 6 7 ordtypelem7 φ b A m dom O O m R b b ran O
27 26 ord φ b A m dom O ¬ O m R b b ran O
28 27 rexlimdva φ b A m dom O ¬ O m R b b ran O
29 25 28 syl5bir φ b A ¬ m dom O O m R b b ran O
30 29 con1d φ b A ¬ b ran O m dom O O m R b
31 30 impr φ b A ¬ b ran O m dom O O m R b
32 breq1 c = O m c R b O m R b
33 32 ralrn O Fn dom O c ran O c R b m dom O O m R b
34 16 33 syl φ b A ¬ b ran O c ran O c R b m dom O O m R b
35 31 34 mpbird φ b A ¬ b ran O c ran O c R b
36 ssrab ran O c A | c R b ran O A c ran O c R b
37 24 35 36 sylanbrc φ b A ¬ b ran O ran O c A | c R b
38 23 37 ssexd φ b A ¬ b ran O ran O V
39 f1dmex O : dom O 1-1 ran O ran O V dom O V
40 20 38 39 syl2anc φ b A ¬ b ran O dom O V
41 16 40 fnexd φ b A ¬ b ran O O V
42 1 2 3 4 5 12 13 41 ordtypelem9 φ b A ¬ b ran O O Isom E , R dom O A
43 isof1o O Isom E , R dom O A O : dom O 1-1 onto A
44 f1ofo O : dom O 1-1 onto A O : dom O onto A
45 forn O : dom O onto A ran O = A
46 42 43 44 45 4syl φ b A ¬ b ran O ran O = A
47 11 46 eleqtrrd φ b A ¬ b ran O b ran O
48 47 expr φ b A ¬ b ran O b ran O
49 48 pm2.18d φ b A b ran O
50 10 49 eqelssd φ ran O = A
51 isoeq5 ran O = A O Isom E , R dom O ran O O Isom E , R dom O A
52 50 51 syl φ O Isom E , R dom O ran O O Isom E , R dom O A
53 8 52 mpbid φ O Isom E , R dom O A