Metamath Proof Explorer

Theorem unfi

Description: The union of two finite sets is finite. Part of Corollary 6K of Enderton p. 144. (Contributed by NM, 16-Nov-2002)

Ref Expression
Assertion unfi 
|- ( ( A e. Fin /\ B e. Fin ) -> ( A u. B ) e. Fin )

Proof

Step Hyp Ref Expression
1 diffi 
 |-  ( B e. Fin -> ( B \ A ) e. Fin )
2 reeanv 
 |-  ( E. x e. _om E. y e. _om ( A ~~ x /\ ( B \ A ) ~~ y ) <-> ( E. x e. _om A ~~ x /\ E. y e. _om ( B \ A ) ~~ y ) )
3 isfi 
 |-  ( A e. Fin <-> E. x e. _om A ~~ x )
4 isfi 
 |-  ( ( B \ A ) e. Fin <-> E. y e. _om ( B \ A ) ~~ y )
5 3 4 anbi12i 
 |-  ( ( A e. Fin /\ ( B \ A ) e. Fin ) <-> ( E. x e. _om A ~~ x /\ E. y e. _om ( B \ A ) ~~ y ) )
6 2 5 bitr4i 
 |-  ( E. x e. _om E. y e. _om ( A ~~ x /\ ( B \ A ) ~~ y ) <-> ( A e. Fin /\ ( B \ A ) e. Fin ) )
7 nnacl 
 |-  ( ( x e. _om /\ y e. _om ) -> ( x +o y ) e. _om )
8 unfilem3 
 |-  ( ( x e. _om /\ y e. _om ) -> y ~~ ( ( x +o y ) \ x ) )
9 entr 
 |-  ( ( ( B \ A ) ~~ y /\ y ~~ ( ( x +o y ) \ x ) ) -> ( B \ A ) ~~ ( ( x +o y ) \ x ) )
10 9 expcom 
 |-  ( y ~~ ( ( x +o y ) \ x ) -> ( ( B \ A ) ~~ y -> ( B \ A ) ~~ ( ( x +o y ) \ x ) ) )
11 8 10 syl 
 |-  ( ( x e. _om /\ y e. _om ) -> ( ( B \ A ) ~~ y -> ( B \ A ) ~~ ( ( x +o y ) \ x ) ) )
12 disjdif 
 |-  ( A i^i ( B \ A ) ) = (/)
13 disjdif 
 |-  ( x i^i ( ( x +o y ) \ x ) ) = (/)
14 unen 
 |-  ( ( ( A ~~ x /\ ( B \ A ) ~~ ( ( x +o y ) \ x ) ) /\ ( ( A i^i ( B \ A ) ) = (/) /\ ( x i^i ( ( x +o y ) \ x ) ) = (/) ) ) -> ( A u. ( B \ A ) ) ~~ ( x u. ( ( x +o y ) \ x ) ) )
15 12 13 14 mpanr12 
 |-  ( ( A ~~ x /\ ( B \ A ) ~~ ( ( x +o y ) \ x ) ) -> ( A u. ( B \ A ) ) ~~ ( x u. ( ( x +o y ) \ x ) ) )
16 undif2 
 |-  ( A u. ( B \ A ) ) = ( A u. B )
17 16 a1i 
 |-  ( ( x e. _om /\ y e. _om ) -> ( A u. ( B \ A ) ) = ( A u. B ) )
18 nnaword1 
 |-  ( ( x e. _om /\ y e. _om ) -> x C_ ( x +o y ) )
19 undif 
 |-  ( x C_ ( x +o y ) <-> ( x u. ( ( x +o y ) \ x ) ) = ( x +o y ) )
20 18 19 sylib 
 |-  ( ( x e. _om /\ y e. _om ) -> ( x u. ( ( x +o y ) \ x ) ) = ( x +o y ) )
21 17 20 breq12d 
 |-  ( ( x e. _om /\ y e. _om ) -> ( ( A u. ( B \ A ) ) ~~ ( x u. ( ( x +o y ) \ x ) ) <-> ( A u. B ) ~~ ( x +o y ) ) )
22 15 21 syl5ib 
 |-  ( ( x e. _om /\ y e. _om ) -> ( ( A ~~ x /\ ( B \ A ) ~~ ( ( x +o y ) \ x ) ) -> ( A u. B ) ~~ ( x +o y ) ) )
23 11 22 sylan2d 
 |-  ( ( x e. _om /\ y e. _om ) -> ( ( A ~~ x /\ ( B \ A ) ~~ y ) -> ( A u. B ) ~~ ( x +o y ) ) )
24 breq2 
 |-  ( z = ( x +o y ) -> ( ( A u. B ) ~~ z <-> ( A u. B ) ~~ ( x +o y ) ) )
25 24 rspcev 
 |-  ( ( ( x +o y ) e. _om /\ ( A u. B ) ~~ ( x +o y ) ) -> E. z e. _om ( A u. B ) ~~ z )
26 isfi 
 |-  ( ( A u. B ) e. Fin <-> E. z e. _om ( A u. B ) ~~ z )
27 25 26 sylibr 
 |-  ( ( ( x +o y ) e. _om /\ ( A u. B ) ~~ ( x +o y ) ) -> ( A u. B ) e. Fin )
28 7 23 27 syl6an 
 |-  ( ( x e. _om /\ y e. _om ) -> ( ( A ~~ x /\ ( B \ A ) ~~ y ) -> ( A u. B ) e. Fin ) )
29 28 rexlimivv 
 |-  ( E. x e. _om E. y e. _om ( A ~~ x /\ ( B \ A ) ~~ y ) -> ( A u. B ) e. Fin )
30 6 29 sylbir 
 |-  ( ( A e. Fin /\ ( B \ A ) e. Fin ) -> ( A u. B ) e. Fin )
31 1 30 sylan2 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( A u. B ) e. Fin )