Theorem ackbij1lem11

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

	Ref	Expression
Hypothesis	ackbij.f	|- F = ( x e. ( ~P _om i^i Fin ) |-> ( card ` U_ y e. x ( { y } X. ~P y ) ) )
Assertion	ackbij1lem11	|- ( ( A e. ( ~P _om i^i Fin ) /\ B C_ A ) -> B e. ( ~P _om i^i Fin ) )

Proof

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