Metamath Proof Explorer

Theorem hsmexlem1

Description: Lemma for hsmex . Bound the order type of a limited-cardinality set of ordinals. (Contributed by Stefan O'Rear, 14-Feb-2015) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Hypothesis hsmexlem.o 
|- O = OrdIso ( _E , A )
Assertion hsmexlem1 
|- ( ( A C_ On /\ A ~<_* B ) -> dom O e. ( har ` ~P B ) )

Proof

Step Hyp Ref Expression
1 hsmexlem.o 
 |-  O = OrdIso ( _E , A )
2 1 oicl 
 |-  Ord dom O
3 relwdom 
 |-  Rel ~<_*
4 3 brrelex1i 
 |-  ( A ~<_* B -> A e. _V )
5 4 adantl 
 |-  ( ( A C_ On /\ A ~<_* B ) -> A e. _V )
6 uniexg 
 |-  ( A e. _V -> U. A e. _V )
7 sucexg 
 |-  ( U. A e. _V -> suc U. A e. _V )
8 5 6 7 3syl 
 |-  ( ( A C_ On /\ A ~<_* B ) -> suc U. A e. _V )
9 1 oif 
 |-  O : dom O --> A
10 onsucuni 
 |-  ( A C_ On -> A C_ suc U. A )
11 10 adantr 
 |-  ( ( A C_ On /\ A ~<_* B ) -> A C_ suc U. A )
12 fss 
 |-  ( ( O : dom O --> A /\ A C_ suc U. A ) -> O : dom O --> suc U. A )
13 9 11 12 sylancr 
 |-  ( ( A C_ On /\ A ~<_* B ) -> O : dom O --> suc U. A )
14 1 oismo 
 |-  ( A C_ On -> ( Smo O /\ ran O = A ) )
15 14 adantr 
 |-  ( ( A C_ On /\ A ~<_* B ) -> ( Smo O /\ ran O = A ) )
16 15 simpld 
 |-  ( ( A C_ On /\ A ~<_* B ) -> Smo O )
17 ssorduni 
 |-  ( A C_ On -> Ord U. A )
18 17 adantr 
 |-  ( ( A C_ On /\ A ~<_* B ) -> Ord U. A )
19 ordsuc 
 |-  ( Ord U. A <-> Ord suc U. A )
20 18 19 sylib 
 |-  ( ( A C_ On /\ A ~<_* B ) -> Ord suc U. A )
21 smorndom 
 |-  ( ( O : dom O --> suc U. A /\ Smo O /\ Ord suc U. A ) -> dom O C_ suc U. A )
22 13 16 20 21 syl3anc 
 |-  ( ( A C_ On /\ A ~<_* B ) -> dom O C_ suc U. A )
23 8 22 ssexd 
 |-  ( ( A C_ On /\ A ~<_* B ) -> dom O e. _V )
24 elong 
 |-  ( dom O e. _V -> ( dom O e. On <-> Ord dom O ) )
25 23 24 syl 
 |-  ( ( A C_ On /\ A ~<_* B ) -> ( dom O e. On <-> Ord dom O ) )
26 2 25 mpbiri 
 |-  ( ( A C_ On /\ A ~<_* B ) -> dom O e. On )
27 canth2g 
 |-  ( dom O e. _V -> dom O ~< ~P dom O )
28 sdomdom 
 |-  ( dom O ~< ~P dom O -> dom O ~<_ ~P dom O )
29 23 27 28 3syl 
 |-  ( ( A C_ On /\ A ~<_* B ) -> dom O ~<_ ~P dom O )
30 simpl 
 |-  ( ( A C_ On /\ A ~<_* B ) -> A C_ On )
31 epweon 
 |-  _E We On
32 wess 
 |-  ( A C_ On -> ( _E We On -> _E We A ) )
33 30 31 32 mpisyl 
 |-  ( ( A C_ On /\ A ~<_* B ) -> _E We A )
34 epse 
 |-  _E Se A
35 1 oiiso2 
 |-  ( ( _E We A /\ _E Se A ) -> O Isom _E , _E ( dom O , ran O ) )
36 33 34 35 sylancl 
 |-  ( ( A C_ On /\ A ~<_* B ) -> O Isom _E , _E ( dom O , ran O ) )
37 isof1o 
 |-  ( O Isom _E , _E ( dom O , ran O ) -> O : dom O -1-1-onto-> ran O )
38 36 37 syl 
 |-  ( ( A C_ On /\ A ~<_* B ) -> O : dom O -1-1-onto-> ran O )
39 15 simprd 
 |-  ( ( A C_ On /\ A ~<_* B ) -> ran O = A )
40 39 f1oeq3d 
 |-  ( ( A C_ On /\ A ~<_* B ) -> ( O : dom O -1-1-onto-> ran O <-> O : dom O -1-1-onto-> A ) )
41 38 40 mpbid 
 |-  ( ( A C_ On /\ A ~<_* B ) -> O : dom O -1-1-onto-> A )
42 f1oen2g 
 |-  ( ( dom O e. On /\ A e. _V /\ O : dom O -1-1-onto-> A ) -> dom O ~~ A )
43 26 5 41 42 syl3anc 
 |-  ( ( A C_ On /\ A ~<_* B ) -> dom O ~~ A )
44 endom 
 |-  ( dom O ~~ A -> dom O ~<_ A )
45 domwdom 
 |-  ( dom O ~<_ A -> dom O ~<_* A )
46 43 44 45 3syl 
 |-  ( ( A C_ On /\ A ~<_* B ) -> dom O ~<_* A )
47 wdomtr 
 |-  ( ( dom O ~<_* A /\ A ~<_* B ) -> dom O ~<_* B )
48 46 47 sylancom 
 |-  ( ( A C_ On /\ A ~<_* B ) -> dom O ~<_* B )
49 wdompwdom 
 |-  ( dom O ~<_* B -> ~P dom O ~<_ ~P B )
50 48 49 syl 
 |-  ( ( A C_ On /\ A ~<_* B ) -> ~P dom O ~<_ ~P B )
51 domtr 
 |-  ( ( dom O ~<_ ~P dom O /\ ~P dom O ~<_ ~P B ) -> dom O ~<_ ~P B )
52 29 50 51 syl2anc 
 |-  ( ( A C_ On /\ A ~<_* B ) -> dom O ~<_ ~P B )
53 elharval 
 |-  ( dom O e. ( har ` ~P B ) <-> ( dom O e. On /\ dom O ~<_ ~P B ) )
54 26 52 53 sylanbrc 
 |-  ( ( A C_ On /\ A ~<_* B ) -> dom O e. ( har ` ~P B ) )