Step |
Hyp |
Ref |
Expression |
1 |
|
infpwfien |
|- ( ( A e. dom card /\ _om ~<_ A ) -> ( ~P A i^i Fin ) ~~ A ) |
2 |
|
relen |
|- Rel ~~ |
3 |
2
|
brrelex1i |
|- ( ( ~P A i^i Fin ) ~~ A -> ( ~P A i^i Fin ) e. _V ) |
4 |
1 3
|
syl |
|- ( ( A e. dom card /\ _om ~<_ A ) -> ( ~P A i^i Fin ) e. _V ) |
5 |
|
difss |
|- ( ( ~P A i^i Fin ) \ { (/) } ) C_ ( ~P A i^i Fin ) |
6 |
|
ssdomg |
|- ( ( ~P A i^i Fin ) e. _V -> ( ( ( ~P A i^i Fin ) \ { (/) } ) C_ ( ~P A i^i Fin ) -> ( ( ~P A i^i Fin ) \ { (/) } ) ~<_ ( ~P A i^i Fin ) ) ) |
7 |
4 5 6
|
mpisyl |
|- ( ( A e. dom card /\ _om ~<_ A ) -> ( ( ~P A i^i Fin ) \ { (/) } ) ~<_ ( ~P A i^i Fin ) ) |
8 |
|
domentr |
|- ( ( ( ( ~P A i^i Fin ) \ { (/) } ) ~<_ ( ~P A i^i Fin ) /\ ( ~P A i^i Fin ) ~~ A ) -> ( ( ~P A i^i Fin ) \ { (/) } ) ~<_ A ) |
9 |
7 1 8
|
syl2anc |
|- ( ( A e. dom card /\ _om ~<_ A ) -> ( ( ~P A i^i Fin ) \ { (/) } ) ~<_ A ) |
10 |
|
numdom |
|- ( ( A e. dom card /\ ( ( ~P A i^i Fin ) \ { (/) } ) ~<_ A ) -> ( ( ~P A i^i Fin ) \ { (/) } ) e. dom card ) |
11 |
9 10
|
syldan |
|- ( ( A e. dom card /\ _om ~<_ A ) -> ( ( ~P A i^i Fin ) \ { (/) } ) e. dom card ) |
12 |
|
eqid |
|- ( x e. ( ( ~P A i^i Fin ) \ { (/) } ) |-> |^| x ) = ( x e. ( ( ~P A i^i Fin ) \ { (/) } ) |-> |^| x ) |
13 |
12
|
fifo |
|- ( A e. dom card -> ( x e. ( ( ~P A i^i Fin ) \ { (/) } ) |-> |^| x ) : ( ( ~P A i^i Fin ) \ { (/) } ) -onto-> ( fi ` A ) ) |
14 |
13
|
adantr |
|- ( ( A e. dom card /\ _om ~<_ A ) -> ( x e. ( ( ~P A i^i Fin ) \ { (/) } ) |-> |^| x ) : ( ( ~P A i^i Fin ) \ { (/) } ) -onto-> ( fi ` A ) ) |
15 |
|
fodomnum |
|- ( ( ( ~P A i^i Fin ) \ { (/) } ) e. dom card -> ( ( x e. ( ( ~P A i^i Fin ) \ { (/) } ) |-> |^| x ) : ( ( ~P A i^i Fin ) \ { (/) } ) -onto-> ( fi ` A ) -> ( fi ` A ) ~<_ ( ( ~P A i^i Fin ) \ { (/) } ) ) ) |
16 |
11 14 15
|
sylc |
|- ( ( A e. dom card /\ _om ~<_ A ) -> ( fi ` A ) ~<_ ( ( ~P A i^i Fin ) \ { (/) } ) ) |
17 |
|
domtr |
|- ( ( ( fi ` A ) ~<_ ( ( ~P A i^i Fin ) \ { (/) } ) /\ ( ( ~P A i^i Fin ) \ { (/) } ) ~<_ A ) -> ( fi ` A ) ~<_ A ) |
18 |
16 9 17
|
syl2anc |
|- ( ( A e. dom card /\ _om ~<_ A ) -> ( fi ` A ) ~<_ A ) |
19 |
|
fvex |
|- ( fi ` A ) e. _V |
20 |
|
ssfii |
|- ( A e. dom card -> A C_ ( fi ` A ) ) |
21 |
20
|
adantr |
|- ( ( A e. dom card /\ _om ~<_ A ) -> A C_ ( fi ` A ) ) |
22 |
|
ssdomg |
|- ( ( fi ` A ) e. _V -> ( A C_ ( fi ` A ) -> A ~<_ ( fi ` A ) ) ) |
23 |
19 21 22
|
mpsyl |
|- ( ( A e. dom card /\ _om ~<_ A ) -> A ~<_ ( fi ` A ) ) |
24 |
|
sbth |
|- ( ( ( fi ` A ) ~<_ A /\ A ~<_ ( fi ` A ) ) -> ( fi ` A ) ~~ A ) |
25 |
18 23 24
|
syl2anc |
|- ( ( A e. dom card /\ _om ~<_ A ) -> ( fi ` A ) ~~ A ) |