Metamath Proof Explorer


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