This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )