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 syl5bi
 |-  ( ( 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 syl6ibr
 |-  ( ( 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 )