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