| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ackbij.f |
|- F = ( x e. ( ~P _om i^i Fin ) |-> ( card ` U_ y e. x ( { y } X. ~P y ) ) ) |
| 2 |
|
ssexg |
|- ( ( B C_ A /\ A e. ( ~P _om i^i Fin ) ) -> B e. _V ) |
| 3 |
|
elinel1 |
|- ( A e. ( ~P _om i^i Fin ) -> A e. ~P _om ) |
| 4 |
3
|
elpwid |
|- ( A e. ( ~P _om i^i Fin ) -> A C_ _om ) |
| 5 |
|
sstr |
|- ( ( B C_ A /\ A C_ _om ) -> B C_ _om ) |
| 6 |
4 5
|
sylan2 |
|- ( ( B C_ A /\ A e. ( ~P _om i^i Fin ) ) -> B C_ _om ) |
| 7 |
2 6
|
elpwd |
|- ( ( B C_ A /\ A e. ( ~P _om i^i Fin ) ) -> B e. ~P _om ) |
| 8 |
7
|
ancoms |
|- ( ( A e. ( ~P _om i^i Fin ) /\ B C_ A ) -> B e. ~P _om ) |
| 9 |
|
elinel2 |
|- ( A e. ( ~P _om i^i Fin ) -> A e. Fin ) |
| 10 |
|
ssfi |
|- ( ( A e. Fin /\ B C_ A ) -> B e. Fin ) |
| 11 |
9 10
|
sylan |
|- ( ( A e. ( ~P _om i^i Fin ) /\ B C_ A ) -> B e. Fin ) |
| 12 |
8 11
|
elind |
|- ( ( A e. ( ~P _om i^i Fin ) /\ B C_ A ) -> B e. ( ~P _om i^i Fin ) ) |