MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  infpwfien Structured version   Visualization version   Unicode version

Theorem infpwfien 8524
Description: Any infinite well-orderable set is equinumerous to its set of finite subsets. (Contributed by Mario Carneiro, 18-May-2015.)
Assertion
Ref Expression
infpwfien  |-  ( ( A  e.  dom  card  /\ 
om  ~<_  A )  -> 
( ~P A  i^i  Fin )  ~~  A )

Proof of Theorem infpwfien
Dummy variables  m  n  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 infxpidm2 8479 . . . . . . 7  |-  ( ( A  e.  dom  card  /\ 
om  ~<_  A )  -> 
( A  X.  A
)  ~~  A )
2 infn0 7864 . . . . . . . 8  |-  ( om  ~<_  A  ->  A  =/=  (/) )
32adantl 472 . . . . . . 7  |-  ( ( A  e.  dom  card  /\ 
om  ~<_  A )  ->  A  =/=  (/) )
4 fseqen 8489 . . . . . . 7  |-  ( ( ( A  X.  A
)  ~~  A  /\  A  =/=  (/) )  ->  U_ n  e.  om  ( A  ^m  n )  ~~  ( om  X.  A ) )
51, 3, 4syl2anc 671 . . . . . 6  |-  ( ( A  e.  dom  card  /\ 
om  ~<_  A )  ->  U_ n  e.  om  ( A  ^m  n
)  ~~  ( om  X.  A ) )
6 xpdom1g 7700 . . . . . . 7  |-  ( ( A  e.  dom  card  /\ 
om  ~<_  A )  -> 
( om  X.  A
)  ~<_  ( A  X.  A ) )
7 domentr 7659 . . . . . . 7  |-  ( ( ( om  X.  A
)  ~<_  ( A  X.  A )  /\  ( A  X.  A )  ~~  A )  ->  ( om  X.  A )  ~<_  A )
86, 1, 7syl2anc 671 . . . . . 6  |-  ( ( A  e.  dom  card  /\ 
om  ~<_  A )  -> 
( om  X.  A
)  ~<_  A )
9 endomtr 7658 . . . . . 6  |-  ( (
U_ n  e.  om  ( A  ^m  n
)  ~~  ( om  X.  A )  /\  ( om  X.  A )  ~<_  A )  ->  U_ n  e. 
om  ( A  ^m  n )  ~<_  A )
105, 8, 9syl2anc 671 . . . . 5  |-  ( ( A  e.  dom  card  /\ 
om  ~<_  A )  ->  U_ n  e.  om  ( A  ^m  n
)  ~<_  A )
11 numdom 8500 . . . . 5  |-  ( ( A  e.  dom  card  /\ 
U_ n  e.  om  ( A  ^m  n
)  ~<_  A )  ->  U_ n  e.  om  ( A  ^m  n
)  e.  dom  card )
1210, 11syldan 477 . . . 4  |-  ( ( A  e.  dom  card  /\ 
om  ~<_  A )  ->  U_ n  e.  om  ( A  ^m  n
)  e.  dom  card )
13 eliun 4297 . . . . . . . . 9  |-  ( x  e.  U_ n  e. 
om  ( A  ^m  n )  <->  E. n  e.  om  x  e.  ( A  ^m  n ) )
14 elmapi 7524 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( A  ^m  n )  ->  x : n --> A )
1514ad2antll 740 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  dom  card  /\  om  ~<_  A )  /\  ( n  e.  om  /\  x  e.  ( A  ^m  n ) ) )  ->  x :
n --> A )
16 frn 5762 . . . . . . . . . . . . . 14  |-  ( x : n --> A  ->  ran  x  C_  A )
1715, 16syl 17 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  dom  card  /\  om  ~<_  A )  /\  ( n  e.  om  /\  x  e.  ( A  ^m  n ) ) )  ->  ran  x  C_  A )
18 vex 3060 . . . . . . . . . . . . . . 15  |-  x  e. 
_V
1918rnex 6759 . . . . . . . . . . . . . 14  |-  ran  x  e.  _V
2019elpw 3969 . . . . . . . . . . . . 13  |-  ( ran  x  e.  ~P A  <->  ran  x  C_  A )
2117, 20sylibr 217 . . . . . . . . . . . 12  |-  ( ( ( A  e.  dom  card  /\  om  ~<_  A )  /\  ( n  e.  om  /\  x  e.  ( A  ^m  n ) ) )  ->  ran  x  e. 
~P A )
22 simprl 769 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  dom  card  /\  om  ~<_  A )  /\  ( n  e.  om  /\  x  e.  ( A  ^m  n ) ) )  ->  n  e.  om )
23 ssid 3463 . . . . . . . . . . . . . 14  |-  n  C_  n
24 ssnnfi 7822 . . . . . . . . . . . . . 14  |-  ( ( n  e.  om  /\  n  C_  n )  ->  n  e.  Fin )
2522, 23, 24sylancl 673 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  dom  card  /\  om  ~<_  A )  /\  ( n  e.  om  /\  x  e.  ( A  ^m  n ) ) )  ->  n  e.  Fin )
26 ffn 5755 . . . . . . . . . . . . . . 15  |-  ( x : n --> A  ->  x  Fn  n )
27 dffn4 5826 . . . . . . . . . . . . . . 15  |-  ( x  Fn  n  <->  x :
n -onto-> ran  x )
2826, 27sylib 201 . . . . . . . . . . . . . 14  |-  ( x : n --> A  ->  x : n -onto-> ran  x
)
2915, 28syl 17 . . . . . . . . . . . . 13  |-  ( ( ( A  e.  dom  card  /\  om  ~<_  A )  /\  ( n  e.  om  /\  x  e.  ( A  ^m  n ) ) )  ->  x :
n -onto-> ran  x )
30 fofi 7891 . . . . . . . . . . . . 13  |-  ( ( n  e.  Fin  /\  x : n -onto-> ran  x
)  ->  ran  x  e. 
Fin )
3125, 29, 30syl2anc 671 . . . . . . . . . . . 12  |-  ( ( ( A  e.  dom  card  /\  om  ~<_  A )  /\  ( n  e.  om  /\  x  e.  ( A  ^m  n ) ) )  ->  ran  x  e. 
Fin )
3221, 31elind 3630 . . . . . . . . . . 11  |-  ( ( ( A  e.  dom  card  /\  om  ~<_  A )  /\  ( n  e.  om  /\  x  e.  ( A  ^m  n ) ) )  ->  ran  x  e.  ( ~P A  i^i  Fin ) )
3332expr 624 . . . . . . . . . 10  |-  ( ( ( A  e.  dom  card  /\  om  ~<_  A )  /\  n  e.  om )  ->  ( x  e.  ( A  ^m  n )  ->  ran  x  e.  ( ~P A  i^i  Fin ) ) )
3433rexlimdva 2891 . . . . . . . . 9  |-  ( ( A  e.  dom  card  /\ 
om  ~<_  A )  -> 
( E. n  e. 
om  x  e.  ( A  ^m  n )  ->  ran  x  e.  ( ~P A  i^i  Fin ) ) )
3513, 34syl5bi 225 . . . . . . . 8  |-  ( ( A  e.  dom  card  /\ 
om  ~<_  A )  -> 
( x  e.  U_ n  e.  om  ( A  ^m  n )  ->  ran  x  e.  ( ~P A  i^i  Fin )
) )
3635imp 435 . . . . . . 7  |-  ( ( ( A  e.  dom  card  /\  om  ~<_  A )  /\  x  e.  U_ n  e. 
om  ( A  ^m  n ) )  ->  ran  x  e.  ( ~P A  i^i  Fin )
)
37 eqid 2462 . . . . . . 7  |-  ( x  e.  U_ n  e. 
om  ( A  ^m  n )  |->  ran  x
)  =  ( x  e.  U_ n  e. 
om  ( A  ^m  n )  |->  ran  x
)
3836, 37fmptd 6074 . . . . . 6  |-  ( ( 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 ) )
39 ffn 5755 . . . . . 6  |-  ( ( x  e.  U_ n  e.  om  ( A  ^m  n )  |->  ran  x
) : U_ n  e.  om  ( A  ^m  n ) --> ( ~P A  i^i  Fin )  ->  ( x  e.  U_ n  e.  om  ( A  ^m  n )  |->  ran  x )  Fn  U_ n  e.  om  ( A  ^m  n ) )
4038, 39syl 17 . . . . 5  |-  ( ( 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 ) )
41 frn 5762 . . . . . . 7  |-  ( ( x  e.  U_ n  e.  om  ( A  ^m  n )  |->  ran  x
) : U_ n  e.  om  ( A  ^m  n ) --> ( ~P A  i^i  Fin )  ->  ran  ( x  e. 
U_ n  e.  om  ( A  ^m  n
)  |->  ran  x )  C_  ( ~P A  i^i  Fin ) )
4238, 41syl 17 . . . . . 6  |-  ( ( A  e.  dom  card  /\ 
om  ~<_  A )  ->  ran  ( x  e.  U_ n  e.  om  ( A  ^m  n )  |->  ran  x )  C_  ( ~P A  i^i  Fin )
)
43 inss2 3665 . . . . . . . . . . . 12  |-  ( ~P A  i^i  Fin )  C_ 
Fin
44 simpr 467 . . . . . . . . . . . 12  |-  ( ( ( A  e.  dom  card  /\  om  ~<_  A )  /\  y  e.  ( ~P A  i^i  Fin ) )  ->  y  e.  ( ~P A  i^i  Fin ) )
4543, 44sseldi 3442 . . . . . . . . . . 11  |-  ( ( ( A  e.  dom  card  /\  om  ~<_  A )  /\  y  e.  ( ~P A  i^i  Fin ) )  ->  y  e.  Fin )
46 isfi 7624 . . . . . . . . . . 11  |-  ( y  e.  Fin  <->  E. m  e.  om  y  ~~  m
)
4745, 46sylib 201 . . . . . . . . . 10  |-  ( ( ( A  e.  dom  card  /\  om  ~<_  A )  /\  y  e.  ( ~P A  i^i  Fin ) )  ->  E. m  e.  om  y  ~~  m )
48 ensym 7649 . . . . . . . . . . . . 13  |-  ( y 
~~  m  ->  m  ~~  y )
49 bren 7609 . . . . . . . . . . . . 13  |-  ( m 
~~  y  <->  E. x  x : m -1-1-onto-> y )
5048, 49sylib 201 . . . . . . . . . . . 12  |-  ( y 
~~  m  ->  E. x  x : m -1-1-onto-> y )
51 simprl 769 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 )
52 f1of 5841 . . . . . . . . . . . . . . . . . . . 20  |-  ( x : m -1-1-onto-> y  ->  x : m --> y )
5352ad2antll 740 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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 )
54 inss1 3664 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ~P A  i^i  Fin )  C_ 
~P A
55 simplr 767 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 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 )
)
5654, 55sseldi 3442 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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
)
5756elpwid 3973 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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 )
5853, 57fssd 5765 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 )
59 simplll 773 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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 )
60 vex 3060 . . . . . . . . . . . . . . . . . . 19  |-  m  e. 
_V
61 elmapg 7516 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  dom  card  /\  m  e.  _V )  ->  ( x  e.  ( A  ^m  m )  <-> 
x : m --> A ) )
6259, 60, 61sylancl 673 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 ) )
6358, 62mpbird 240 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 ) )
64 oveq2 6328 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  m  ->  ( A  ^m  n )  =  ( A  ^m  m
) )
6564eleq2d 2525 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  m  ->  (
x  e.  ( A  ^m  n )  <->  x  e.  ( A  ^m  m
) ) )
6665rspcev 3162 . . . . . . . . . . . . . . . . 17  |-  ( ( m  e.  om  /\  x  e.  ( A  ^m  m ) )  ->  E. n  e.  om  x  e.  ( A  ^m  n ) )
6751, 63, 66syl2anc 671 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 ) )
6867, 13sylibr 217 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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 ) )
69 f1ofo 5848 . . . . . . . . . . . . . . . . . 18  |-  ( x : m -1-1-onto-> y  ->  x : m -onto-> y )
7069ad2antll 740 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 )
71 forn 5823 . . . . . . . . . . . . . . . . 17  |-  ( x : m -onto-> y  ->  ran  x  =  y )
7270, 71syl 17 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 )
7372eqcomd 2468 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 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
)
7468, 73jca 539 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 ) )
7574expr 624 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 ) ) )
7675eximdv 1775 . . . . . . . . . . . 12  |-  ( ( ( ( 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 ) ) )
7750, 76syl5 33 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) ) )
7877rexlimdva 2891 . . . . . . . . . 10  |-  ( ( ( 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 ) ) )
7947, 78mpd 15 . . . . . . . . 9  |-  ( ( ( 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 ) )
8079ex 440 . . . . . . . 8  |-  ( ( 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 ) ) )
81 vex 3060 . . . . . . . . . 10  |-  y  e. 
_V
8237elrnmpt 5103 . . . . . . . . . 10  |-  ( 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 ) )
8381, 82ax-mp 5 . . . . . . . . 9  |-  ( 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 )
84 df-rex 2755 . . . . . . . . 9  |-  ( 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 ) )
8583, 84bitri 257 . . . . . . . 8  |-  ( 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 ) )
8680, 85syl6ibr 235 . . . . . . 7  |-  ( ( 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
) ) )
8786ssrdv 3450 . . . . . 6  |-  ( ( A  e.  dom  card  /\ 
om  ~<_  A )  -> 
( ~P A  i^i  Fin )  C_  ran  ( x  e.  U_ n  e. 
om  ( A  ^m  n )  |->  ran  x
) )
8842, 87eqssd 3461 . . . . 5  |-  ( ( A  e.  dom  card  /\ 
om  ~<_  A )  ->  ran  ( x  e.  U_ n  e.  om  ( A  ^m  n )  |->  ran  x )  =  ( ~P A  i^i  Fin ) )
89 df-fo 5611 . . . . 5  |-  ( ( 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 ) ) )
9040, 88, 89sylanbrc 675 . . . 4  |-  ( ( 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 ) )
91 fodomnum 8519 . . . 4  |-  ( 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
) ) )
9212, 90, 91sylc 62 . . 3  |-  ( ( A  e.  dom  card  /\ 
om  ~<_  A )  -> 
( ~P A  i^i  Fin )  ~<_  U_ n  e.  om  ( A  ^m  n
) )
93 domtr 7653 . . 3  |-  ( ( ( ~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 )
9492, 10, 93syl2anc 671 . 2  |-  ( ( A  e.  dom  card  /\ 
om  ~<_  A )  -> 
( ~P A  i^i  Fin )  ~<_  A )
95 pwexg 4604 . . . . 5  |-  ( A  e.  dom  card  ->  ~P A  e.  _V )
9695adantr 471 . . . 4  |-  ( ( A  e.  dom  card  /\ 
om  ~<_  A )  ->  ~P A  e.  _V )
97 inex1g 4562 . . . 4  |-  ( ~P A  e.  _V  ->  ( ~P A  i^i  Fin )  e.  _V )
9896, 97syl 17 . . 3  |-  ( ( A  e.  dom  card  /\ 
om  ~<_  A )  -> 
( ~P A  i^i  Fin )  e.  _V )
99 infpwfidom 8490 . . 3  |-  ( ( ~P A  i^i  Fin )  e.  _V  ->  A  ~<_  ( ~P A  i^i  Fin ) )
10098, 99syl 17 . 2  |-  ( ( A  e.  dom  card  /\ 
om  ~<_  A )  ->  A  ~<_  ( ~P A  i^i  Fin ) )
101 sbth 7723 . 2  |-  ( ( ( ~P A  i^i  Fin )  ~<_  A  /\  A  ~<_  ( ~P A  i^i  Fin ) )  ->  ( ~P A  i^i  Fin )  ~~  A )
10294, 100, 101syl2anc 671 1  |-  ( ( A  e.  dom  card  /\ 
om  ~<_  A )  -> 
( ~P A  i^i  Fin )  ~~  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375    = wceq 1455   E.wex 1674    e. wcel 1898    =/= wne 2633   E.wrex 2750   _Vcvv 3057    i^i cin 3415    C_ wss 3416   (/)c0 3743   ~Pcpw 3963   U_ciun 4292   class class class wbr 4418    |-> cmpt 4477    X. cxp 4854   dom cdm 4856   ran crn 4857    Fn wfn 5600   -->wf 5601   -onto->wfo 5603   -1-1-onto->wf1o 5604  (class class class)co 6320   omcom 6724    ^m cmap 7503    ~~ cen 7597    ~<_ cdom 7598   Fincfn 7600   cardccrd 8400
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4531  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-inf2 8177
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-br 4419  df-opab 4478  df-mpt 4479  df-tr 4514  df-eprel 4767  df-id 4771  df-po 4777  df-so 4778  df-fr 4815  df-se 4816  df-we 4817  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-pred 5403  df-ord 5449  df-on 5450  df-lim 5451  df-suc 5452  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-isom 5614  df-riota 6282  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-om 6725  df-1st 6825  df-2nd 6826  df-wrecs 7059  df-recs 7121  df-rdg 7159  df-seqom 7196  df-1o 7213  df-oadd 7217  df-er 7394  df-map 7505  df-en 7601  df-dom 7602  df-sdom 7603  df-fin 7604  df-oi 8056  df-card 8404  df-acn 8407
This theorem is referenced by:  inffien  8525  isnumbasgrplem3  36010
  Copyright terms: Public domain W3C validator