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

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