Metamath Proof Explorer

Theorem infpwfien

Description: Any infinite well-orderable set is equinumerous to its set of finite subsets. (Contributed by Mario Carneiro, 18-May-2015)

Ref Expression
Assertion infpwfien 
|- ( ( A e. dom card /\ _om ~<_ A ) -> ( ~P A i^i Fin ) ~~ A )

Proof

Step Hyp Ref Expression
1 infxpidm2 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( A X. A ) ~~ A )
2 infn0 
 |-  ( _om ~<_ A -> A =/= (/) )
3 2 adantl 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> A =/= (/) )
4 fseqen 
 |-  ( ( ( A X. A ) ~~ A /\ A =/= (/) ) -> U_ n e. _om ( A ^m n ) ~~ ( _om X. A ) )
5 1 3 4 syl2anc 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> U_ n e. _om ( A ^m n ) ~~ ( _om X. A ) )
6 xpdom1g 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( _om X. A ) ~<_ ( A X. A ) )
7 domentr 
 |-  ( ( ( _om X. A ) ~<_ ( A X. A ) /\ ( A X. A ) ~~ A ) -> ( _om X. A ) ~<_ A )
8 6 1 7 syl2anc 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( _om X. A ) ~<_ A )
9 endomtr 
 |-  ( ( U_ n e. _om ( A ^m n ) ~~ ( _om X. A ) /\ ( _om X. A ) ~<_ A ) -> U_ n e. _om ( A ^m n ) ~<_ A )
10 5 8 9 syl2anc 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> U_ n e. _om ( A ^m n ) ~<_ A )
11 numdom 
 |-  ( ( A e. dom card /\ U_ n e. _om ( A ^m n ) ~<_ A ) -> U_ n e. _om ( A ^m n ) e. dom card )
12 10 11 syldan 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> U_ n e. _om ( A ^m n ) e. dom card )
13 eliun 
 |-  ( x e. U_ n e. _om ( A ^m n ) <-> E. n e. _om x e. ( A ^m n ) )
14 elmapi 
 |-  ( x e. ( A ^m n ) -> x : n --> A )
15 14 ad2antll 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( n e. _om /\ x e. ( A ^m n ) ) ) -> x : n --> A )
16 15 frnd 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( n e. _om /\ x e. ( A ^m n ) ) ) -> ran x C_ A )
17 vex 
 |-  x e. _V
18 17 rnex 
 |-  ran x e. _V
19 18 elpw 
 |-  ( ran x e. ~P A <-> ran x C_ A )
20 16 19 sylibr 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( n e. _om /\ x e. ( A ^m n ) ) ) -> ran x e. ~P A )
21 simprl 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( n e. _om /\ x e. ( A ^m n ) ) ) -> n e. _om )
22 ssid 
 |-  n C_ n
23 ssnnfi 
 |-  ( ( n e. _om /\ n C_ n ) -> n e. Fin )
24 21 22 23 sylancl 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( n e. _om /\ x e. ( A ^m n ) ) ) -> n e. Fin )
25 ffn 
 |-  ( x : n --> A -> x Fn n )
26 dffn4 
 |-  ( x Fn n <-> x : n -onto-> ran x )
27 25 26 sylib 
 |-  ( x : n --> A -> x : n -onto-> ran x )
28 15 27 syl 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( n e. _om /\ x e. ( A ^m n ) ) ) -> x : n -onto-> ran x )
29 fofi 
 |-  ( ( n e. Fin /\ x : n -onto-> ran x ) -> ran x e. Fin )
30 24 28 29 syl2anc 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( n e. _om /\ x e. ( A ^m n ) ) ) -> ran x e. Fin )
31 20 30 elind 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( n e. _om /\ x e. ( A ^m n ) ) ) -> ran x e. ( ~P A i^i Fin ) )
32 31 expr 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ n e. _om ) -> ( x e. ( A ^m n ) -> ran x e. ( ~P A i^i Fin ) ) )
33 32 rexlimdva 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( E. n e. _om x e. ( A ^m n ) -> ran x e. ( ~P A i^i Fin ) ) )
34 13 33 biimtrid 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( x e. U_ n e. _om ( A ^m n ) -> ran x e. ( ~P A i^i Fin ) ) )
35 34 imp 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ x e. U_ n e. _om ( A ^m n ) ) -> ran x e. ( ~P A i^i Fin ) )
36 35 fmpttd 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( x e. U_ n e. _om ( A ^m n ) |-> ran x ) : U_ n e. _om ( A ^m n ) --> ( ~P A i^i Fin ) )
37 36 ffnd 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( x e. U_ n e. _om ( A ^m n ) |-> ran x ) Fn U_ n e. _om ( A ^m n ) )
38 36 frnd 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ran ( x e. U_ n e. _om ( A ^m n ) |-> ran x ) C_ ( ~P A i^i Fin ) )
39 simpr 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) -> y e. ( ~P A i^i Fin ) )
40 39 elin2d 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) -> y e. Fin )
41 isfi 
 |-  ( y e. Fin <-> E. m e. _om y ~~ m )
42 40 41 sylib 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) -> E. m e. _om y ~~ m )
43 ensym 
 |-  ( y ~~ m -> m ~~ y )
44 bren 
 |-  ( m ~~ y <-> E. x x : m -1-1-onto-> y )
45 43 44 sylib 
 |-  ( y ~~ m -> E. x x : m -1-1-onto-> y )
46 simprl 
 |-  ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ ( m e. _om /\ x : m -1-1-onto-> y ) ) -> m e. _om )
47 f1of 
 |-  ( x : m -1-1-onto-> y -> x : m --> y )
48 47 ad2antll 
 |-  ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ ( m e. _om /\ x : m -1-1-onto-> y ) ) -> x : m --> y )
49 simplr 
 |-  ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ ( m e. _om /\ x : m -1-1-onto-> y ) ) -> y e. ( ~P A i^i Fin ) )
50 49 elin1d 
 |-  ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ ( m e. _om /\ x : m -1-1-onto-> y ) ) -> y e. ~P A )
51 50 elpwid 
 |-  ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ ( m e. _om /\ x : m -1-1-onto-> y ) ) -> y C_ A )
52 48 51 fssd 
 |-  ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ ( m e. _om /\ x : m -1-1-onto-> y ) ) -> x : m --> A )
53 simplll 
 |-  ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ ( m e. _om /\ x : m -1-1-onto-> y ) ) -> A e. dom card )
54 vex 
 |-  m e. _V
55 elmapg 
 |-  ( ( A e. dom card /\ m e. _V ) -> ( x e. ( A ^m m ) <-> x : m --> A ) )
56 53 54 55 sylancl 
 |-  ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ ( m e. _om /\ x : m -1-1-onto-> y ) ) -> ( x e. ( A ^m m ) <-> x : m --> A ) )
57 52 56 mpbird 
 |-  ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ ( m e. _om /\ x : m -1-1-onto-> y ) ) -> x e. ( A ^m m ) )
58 oveq2 
 |-  ( n = m -> ( A ^m n ) = ( A ^m m ) )
59 58 eleq2d 
 |-  ( n = m -> ( x e. ( A ^m n ) <-> x e. ( A ^m m ) ) )
60 59 rspcev 
 |-  ( ( m e. _om /\ x e. ( A ^m m ) ) -> E. n e. _om x e. ( A ^m n ) )
61 46 57 60 syl2anc 
 |-  ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ ( m e. _om /\ x : m -1-1-onto-> y ) ) -> E. n e. _om x e. ( A ^m n ) )
62 61 13 sylibr 
 |-  ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ ( m e. _om /\ x : m -1-1-onto-> y ) ) -> x e. U_ n e. _om ( A ^m n ) )
63 f1ofo 
 |-  ( x : m -1-1-onto-> y -> x : m -onto-> y )
64 63 ad2antll 
 |-  ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ ( m e. _om /\ x : m -1-1-onto-> y ) ) -> x : m -onto-> y )
65 forn 
 |-  ( x : m -onto-> y -> ran x = y )
66 64 65 syl 
 |-  ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ ( m e. _om /\ x : m -1-1-onto-> y ) ) -> ran x = y )
67 66 eqcomd 
 |-  ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ ( m e. _om /\ x : m -1-1-onto-> y ) ) -> y = ran x )
68 62 67 jca 
 |-  ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ ( m e. _om /\ x : m -1-1-onto-> y ) ) -> ( x e. U_ n e. _om ( A ^m n ) /\ y = ran x ) )
69 68 expr 
 |-  ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ m e. _om ) -> ( x : m -1-1-onto-> y -> ( x e. U_ n e. _om ( A ^m n ) /\ y = ran x ) ) )
70 69 eximdv 
 |-  ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ m e. _om ) -> ( E. x x : m -1-1-onto-> y -> E. x ( x e. U_ n e. _om ( A ^m n ) /\ y = ran x ) ) )
71 45 70 syl5 
 |-  ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) /\ m e. _om ) -> ( y ~~ m -> E. x ( x e. U_ n e. _om ( A ^m n ) /\ y = ran x ) ) )
72 71 rexlimdva 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) -> ( E. m e. _om y ~~ m -> E. x ( x e. U_ n e. _om ( A ^m n ) /\ y = ran x ) ) )
73 42 72 mpd 
 |-  ( ( ( A e. dom card /\ _om ~<_ A ) /\ y e. ( ~P A i^i Fin ) ) -> E. x ( x e. U_ n e. _om ( A ^m n ) /\ y = ran x ) )
74 73 ex 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( y e. ( ~P A i^i Fin ) -> E. x ( x e. U_ n e. _om ( A ^m n ) /\ y = ran x ) ) )
75 eqid 
 |-  ( x e. U_ n e. _om ( A ^m n ) |-> ran x ) = ( x e. U_ n e. _om ( A ^m n ) |-> ran x )
76 75 elrnmpt 
 |-  ( y e. _V -> ( y e. ran ( x e. U_ n e. _om ( A ^m n ) |-> ran x ) <-> E. x e. U_ n e. _om ( A ^m n ) y = ran x ) )
77 76 elv 
 |-  ( y e. ran ( x e. U_ n e. _om ( A ^m n ) |-> ran x ) <-> E. x e. U_ n e. _om ( A ^m n ) y = ran x )
78 df-rex 
 |-  ( E. x e. U_ n e. _om ( A ^m n ) y = ran x <-> E. x ( x e. U_ n e. _om ( A ^m n ) /\ y = ran x ) )
79 77 78 bitri 
 |-  ( y e. ran ( x e. U_ n e. _om ( A ^m n ) |-> ran x ) <-> E. x ( x e. U_ n e. _om ( A ^m n ) /\ y = ran x ) )
80 74 79 imbitrrdi 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( y e. ( ~P A i^i Fin ) -> y e. ran ( x e. U_ n e. _om ( A ^m n ) |-> ran x ) ) )
81 80 ssrdv 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( ~P A i^i Fin ) C_ ran ( x e. U_ n e. _om ( A ^m n ) |-> ran x ) )
82 38 81 eqssd 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ran ( x e. U_ n e. _om ( A ^m n ) |-> ran x ) = ( ~P A i^i Fin ) )
83 df-fo 
 |-  ( ( x e. U_ n e. _om ( A ^m n ) |-> ran x ) : U_ n e. _om ( A ^m n ) -onto-> ( ~P A i^i Fin ) <-> ( ( x e. U_ n e. _om ( A ^m n ) |-> ran x ) Fn U_ n e. _om ( A ^m n ) /\ ran ( x e. U_ n e. _om ( A ^m n ) |-> ran x ) = ( ~P A i^i Fin ) ) )
84 37 82 83 sylanbrc 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( x e. U_ n e. _om ( A ^m n ) |-> ran x ) : U_ n e. _om ( A ^m n ) -onto-> ( ~P A i^i Fin ) )
85 fodomnum 
 |-  ( U_ n e. _om ( A ^m n ) e. dom card -> ( ( x e. U_ n e. _om ( A ^m n ) |-> ran x ) : U_ n e. _om ( A ^m n ) -onto-> ( ~P A i^i Fin ) -> ( ~P A i^i Fin ) ~<_ U_ n e. _om ( A ^m n ) ) )
86 12 84 85 sylc 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( ~P A i^i Fin ) ~<_ U_ n e. _om ( A ^m n ) )
87 domtr 
 |-  ( ( ( ~P A i^i Fin ) ~<_ U_ n e. _om ( A ^m n ) /\ U_ n e. _om ( A ^m n ) ~<_ A ) -> ( ~P A i^i Fin ) ~<_ A )
88 86 10 87 syl2anc 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( ~P A i^i Fin ) ~<_ A )
89 pwexg 
 |-  ( A e. dom card -> ~P A e. _V )
90 89 adantr 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ~P A e. _V )
91 inex1g 
 |-  ( ~P A e. _V -> ( ~P A i^i Fin ) e. _V )
92 90 91 syl 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( ~P A i^i Fin ) e. _V )
93 infpwfidom 
 |-  ( ( ~P A i^i Fin ) e. _V -> A ~<_ ( ~P A i^i Fin ) )
94 92 93 syl 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> A ~<_ ( ~P A i^i Fin ) )
95 sbth 
 |-  ( ( ( ~P A i^i Fin ) ~<_ A /\ A ~<_ ( ~P A i^i Fin ) ) -> ( ~P A i^i Fin ) ~~ A )
96 88 94 95 syl2anc 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( ~P A i^i Fin ) ~~ A )