Metamath Proof Explorer


Theorem ackbij2lem1

Description: Lemma for ackbij2 . (Contributed by Stefan O'Rear, 18-Nov-2014)

Ref Expression
Assertion ackbij2lem1
|- ( A e. _om -> ~P A C_ ( ~P _om i^i Fin ) )

Proof

Step Hyp Ref Expression
1 ordom
 |-  Ord _om
2 ordelss
 |-  ( ( Ord _om /\ A e. _om ) -> A C_ _om )
3 1 2 mpan
 |-  ( A e. _om -> A C_ _om )
4 3 sspwd
 |-  ( A e. _om -> ~P A C_ ~P _om )
5 4 sselda
 |-  ( ( A e. _om /\ a e. ~P A ) -> a e. ~P _om )
6 nnfi
 |-  ( A e. _om -> A e. Fin )
7 elpwi
 |-  ( a e. ~P A -> a C_ A )
8 ssfi
 |-  ( ( A e. Fin /\ a C_ A ) -> a e. Fin )
9 6 7 8 syl2an
 |-  ( ( A e. _om /\ a e. ~P A ) -> a e. Fin )
10 5 9 elind
 |-  ( ( A e. _om /\ a e. ~P A ) -> a e. ( ~P _om i^i Fin ) )
11 10 ex
 |-  ( A e. _om -> ( a e. ~P A -> a e. ( ~P _om i^i Fin ) ) )
12 11 ssrdv
 |-  ( A e. _om -> ~P A C_ ( ~P _om i^i Fin ) )