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 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 ordtypelem10 
|- ( ph -> O Isom _E , R ( dom O , A ) )

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 1 2 3 4 5 6 7 ordtypelem8 
 |-  ( ph -> O Isom _E , R ( dom O , ran O ) )
9 1 2 3 4 5 6 7 ordtypelem4 
 |-  ( ph -> O : ( T i^i dom F ) --> A )
10 9 frnd 
 |-  ( ph -> ran O C_ A )
11 simprl 
 |-  ( ( ph /\ ( b e. A /\ -. b e. ran O ) ) -> b e. A )
12 6 adantr 
 |-  ( ( ph /\ ( b e. A /\ -. b e. ran O ) ) -> R We A )
13 7 adantr 
 |-  ( ( ph /\ ( b e. A /\ -. b e. ran O ) ) -> R Se A )
14 9 ffund 
 |-  ( ph -> Fun O )
15 14 funfnd 
 |-  ( ph -> O Fn dom O )
16 15 adantr 
 |-  ( ( ph /\ ( b e. A /\ -. b e. ran O ) ) -> O Fn dom O )
17 1 2 3 4 5 12 13 ordtypelem8 
 |-  ( ( ph /\ ( b e. A /\ -. b e. 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 
 |-  ( ( ph /\ ( b e. A /\ -. b e. ran O ) ) -> O : dom O -1-1-> ran O )
21 simpl 
 |-  ( ( b e. A /\ -. b e. ran O ) -> b e. A )
22 seex 
 |-  ( ( R Se A /\ b e. A ) -> { c e. A | c R b } e. _V )
23 7 21 22 syl2an 
 |-  ( ( ph /\ ( b e. A /\ -. b e. ran O ) ) -> { c e. A | c R b } e. _V )
24 10 adantr 
 |-  ( ( ph /\ ( b e. A /\ -. b e. ran O ) ) -> ran O C_ A )
25 rexnal 
 |-  ( E. m e. dom O -. ( O ` m ) R b <-> -. A. m e. dom O ( O ` m ) R b )
26 1 2 3 4 5 6 7 ordtypelem7 
 |-  ( ( ( ph /\ b e. A ) /\ m e. dom O ) -> ( ( O ` m ) R b \/ b e. ran O ) )
27 26 ord 
 |-  ( ( ( ph /\ b e. A ) /\ m e. dom O ) -> ( -. ( O ` m ) R b -> b e. ran O ) )
28 27 rexlimdva 
 |-  ( ( ph /\ b e. A ) -> ( E. m e. dom O -. ( O ` m ) R b -> b e. ran O ) )
29 25 28 syl5bir 
 |-  ( ( ph /\ b e. A ) -> ( -. A. m e. dom O ( O ` m ) R b -> b e. ran O ) )
30 29 con1d 
 |-  ( ( ph /\ b e. A ) -> ( -. b e. ran O -> A. m e. dom O ( O ` m ) R b ) )
31 30 impr 
 |-  ( ( ph /\ ( b e. A /\ -. b e. ran O ) ) -> A. m e. 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 -> ( A. c e. ran O c R b <-> A. m e. dom O ( O ` m ) R b ) )
34 16 33 syl 
 |-  ( ( ph /\ ( b e. A /\ -. b e. ran O ) ) -> ( A. c e. ran O c R b <-> A. m e. dom O ( O ` m ) R b ) )
35 31 34 mpbird 
 |-  ( ( ph /\ ( b e. A /\ -. b e. ran O ) ) -> A. c e. ran O c R b )
36 ssrab 
 |-  ( ran O C_ { c e. A | c R b } <-> ( ran O C_ A /\ A. c e. ran O c R b ) )
37 24 35 36 sylanbrc 
 |-  ( ( ph /\ ( b e. A /\ -. b e. ran O ) ) -> ran O C_ { c e. A | c R b } )
38 23 37 ssexd 
 |-  ( ( ph /\ ( b e. A /\ -. b e. ran O ) ) -> ran O e. _V )
39 f1dmex 
 |-  ( ( O : dom O -1-1-> ran O /\ ran O e. _V ) -> dom O e. _V )
40 20 38 39 syl2anc 
 |-  ( ( ph /\ ( b e. A /\ -. b e. ran O ) ) -> dom O e. _V )
41 16 40 fnexd 
 |-  ( ( ph /\ ( b e. A /\ -. b e. ran O ) ) -> O e. _V )
42 1 2 3 4 5 12 13 41 ordtypelem9 
 |-  ( ( ph /\ ( b e. A /\ -. b e. 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 
 |-  ( ( ph /\ ( b e. A /\ -. b e. ran O ) ) -> ran O = A )
47 11 46 eleqtrrd 
 |-  ( ( ph /\ ( b e. A /\ -. b e. ran O ) ) -> b e. ran O )
48 47 expr 
 |-  ( ( ph /\ b e. A ) -> ( -. b e. ran O -> b e. ran O ) )
49 48 pm2.18d 
 |-  ( ( ph /\ b e. A ) -> b e. ran O )
50 10 49 eqelssd 
 |-  ( ph -> 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 
 |-  ( ph -> ( O Isom _E , R ( dom O , ran O ) <-> O Isom _E , R ( dom O , A ) ) )
53 8 52 mpbid 
 |-  ( ph -> O Isom _E , R ( dom O , A ) )