Theorem ackbij1lem6

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

	Ref	Expression
Assertion	ackbij1lem6	|- ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( A u. B ) e. ( ~P _om i^i Fin ) )

Proof

Step	Hyp	Ref	Expression
1		elinel2	|- ( A e. ( ~P _om i^i Fin ) -> A e. Fin )
2		elinel2	|- ( B e. ( ~P _om i^i Fin ) -> B e. Fin )
3		unfi	|- ( ( A e. Fin /\ B e. Fin ) -> ( A u. B ) e. Fin )
4	1 2 3	syl2an	|- ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( A u. B ) e. Fin )
5		elinel1	|- ( A e. ( ~P _om i^i Fin ) -> A e. ~P _om )
6		elinel1	|- ( B e. ( ~P _om i^i Fin ) -> B e. ~P _om )
7		elpwi	|- ( A e. ~P _om -> A C_ _om )
8		elpwi	|- ( B e. ~P _om -> B C_ _om )
9		simpl	|- ( ( A C_ _om /\ B C_ _om ) -> A C_ _om )
10		simpr	|- ( ( A C_ _om /\ B C_ _om ) -> B C_ _om )
11	9 10	unssd	|- ( ( A C_ _om /\ B C_ _om ) -> ( A u. B ) C_ _om )
12	7 8 11	syl2an	|- ( ( A e. ~P _om /\ B e. ~P _om ) -> ( A u. B ) C_ _om )
13	5 6 12	syl2an	|- ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( A u. B ) C_ _om )
14	4 13	elpwd	|- ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( A u. B ) e. ~P _om )
15	14 4	elind	|- ( ( A e. ( ~P _om i^i Fin ) /\ B e. ( ~P _om i^i Fin ) ) -> ( A u. B ) e. ( ~P _om i^i Fin ) )