Step |
Hyp |
Ref |
Expression |
1 |
|
pwexg |
|- ( A e. V -> ~P A e. _V ) |
2 |
|
inex1g |
|- ( ~P A e. _V -> ( ~P A i^i Fin ) e. _V ) |
3 |
|
infpwfidom |
|- ( ( ~P A i^i Fin ) e. _V -> A ~<_ ( ~P A i^i Fin ) ) |
4 |
1 2 3
|
3syl |
|- ( A e. V -> A ~<_ ( ~P A i^i Fin ) ) |
5 |
|
inex1g |
|- ( ~P A e. _V -> ( ~P A i^i dom card ) e. _V ) |
6 |
1 5
|
syl |
|- ( A e. V -> ( ~P A i^i dom card ) e. _V ) |
7 |
|
finnum |
|- ( x e. Fin -> x e. dom card ) |
8 |
7
|
ssriv |
|- Fin C_ dom card |
9 |
|
sslin |
|- ( Fin C_ dom card -> ( ~P A i^i Fin ) C_ ( ~P A i^i dom card ) ) |
10 |
8 9
|
ax-mp |
|- ( ~P A i^i Fin ) C_ ( ~P A i^i dom card ) |
11 |
|
ssdomg |
|- ( ( ~P A i^i dom card ) e. _V -> ( ( ~P A i^i Fin ) C_ ( ~P A i^i dom card ) -> ( ~P A i^i Fin ) ~<_ ( ~P A i^i dom card ) ) ) |
12 |
6 10 11
|
mpisyl |
|- ( A e. V -> ( ~P A i^i Fin ) ~<_ ( ~P A i^i dom card ) ) |
13 |
|
domtr |
|- ( ( A ~<_ ( ~P A i^i Fin ) /\ ( ~P A i^i Fin ) ~<_ ( ~P A i^i dom card ) ) -> A ~<_ ( ~P A i^i dom card ) ) |
14 |
4 12 13
|
syl2anc |
|- ( A e. V -> A ~<_ ( ~P A i^i dom card ) ) |
15 |
|
eqid |
|- { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( f ` ( `' r " { y } ) ) = y ) ) } = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( f ` ( `' r " { y } ) ) = y ) ) } |
16 |
15
|
fpwwecbv |
|- { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( f ` ( `' r " { y } ) ) = y ) ) } = { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a ( f ` ( `' s " { z } ) ) = z ) ) } |
17 |
|
eqid |
|- U. dom { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( f ` ( `' r " { y } ) ) = y ) ) } = U. dom { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( f ` ( `' r " { y } ) ) = y ) ) } |
18 |
|
eqid |
|- ( `' ( { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( f ` ( `' r " { y } ) ) = y ) ) } ` U. dom { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( f ` ( `' r " { y } ) ) = y ) ) } ) " { ( f ` U. dom { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( f ` ( `' r " { y } ) ) = y ) ) } ) } ) = ( `' ( { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( f ` ( `' r " { y } ) ) = y ) ) } ` U. dom { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( f ` ( `' r " { y } ) ) = y ) ) } ) " { ( f ` U. dom { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( f ` ( `' r " { y } ) ) = y ) ) } ) } ) |
19 |
16 17 18
|
canthnumlem |
|- ( A e. V -> -. f : ( ~P A i^i dom card ) -1-1-> A ) |
20 |
|
f1of1 |
|- ( f : ( ~P A i^i dom card ) -1-1-onto-> A -> f : ( ~P A i^i dom card ) -1-1-> A ) |
21 |
19 20
|
nsyl |
|- ( A e. V -> -. f : ( ~P A i^i dom card ) -1-1-onto-> A ) |
22 |
21
|
nexdv |
|- ( A e. V -> -. E. f f : ( ~P A i^i dom card ) -1-1-onto-> A ) |
23 |
|
ensym |
|- ( A ~~ ( ~P A i^i dom card ) -> ( ~P A i^i dom card ) ~~ A ) |
24 |
|
bren |
|- ( ( ~P A i^i dom card ) ~~ A <-> E. f f : ( ~P A i^i dom card ) -1-1-onto-> A ) |
25 |
23 24
|
sylib |
|- ( A ~~ ( ~P A i^i dom card ) -> E. f f : ( ~P A i^i dom card ) -1-1-onto-> A ) |
26 |
22 25
|
nsyl |
|- ( A e. V -> -. A ~~ ( ~P A i^i dom card ) ) |
27 |
|
brsdom |
|- ( A ~< ( ~P A i^i dom card ) <-> ( A ~<_ ( ~P A i^i dom card ) /\ -. A ~~ ( ~P A i^i dom card ) ) ) |
28 |
14 26 27
|
sylanbrc |
|- ( A e. V -> A ~< ( ~P A i^i dom card ) ) |