Theorem unfi 7367

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

Assertion

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

Proof of Theorem unfi

Dummy variables x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		diffi 7332	. 2 |- ( B e. Fin -> ( B \ A ) e. Fin )
2		reeanv 2868	. . . 4 |- ( 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 7124	. . . . 5 |- ( A e. Fin <-> E. x e. om A ~~ x )
4		isfi 7124	. . . . 5 |- ( ( B \ A ) e. Fin <-> E. y e. om ( B \ A ) ~~ y )
5	3, 4	anbi12i 679	. . . 4 |- ( ( A e. Fin /\ ( B \ A ) e. Fin ) <-> ( E. x e. om A ~~ x /\ E. y e. om ( B \ A ) ~~ y ) )
6	2, 5	bitr4i 244	. . 3 |- ( E. x e. om E. y e. om ( A ~~ x /\ ( B \ A ) ~~ y ) <-> ( A e. Fin /\ ( B \ A ) e. Fin ) )
7		nnacl 6847	. . . . 5 |- ( ( x e. om /\ y e. om ) -> ( x +o y ) e. om )
8		unfilem3 7366	. . . . . . 7 |- ( ( x e. om /\ y e. om ) -> y ~~ ( ( x +o y ) \ x ) )
9		entr 7152	. . . . . . . 8 |- ( ( ( B \ A ) ~~ y /\ y ~~ ( ( x +o y ) \ x ) ) -> ( B \ A ) ~~ ( ( x +o y ) \ x ) )
10	9	expcom 425	. . . . . . 7 |- ( y ~~ ( ( x +o y ) \ x ) -> ( ( B \ A ) ~~ y -> ( B \ A ) ~~ ( ( x +o y ) \ x ) ) )
11	8, 10	syl 16	. . . . . 6 |- ( ( x e. om /\ y e. om ) -> ( ( B \ A ) ~~ y -> ( B \ A ) ~~ ( ( x +o y ) \ x ) ) )
12		disjdif 3693	. . . . . . . 8 |- ( A i^i ( B \ A ) ) = (/)
13		disjdif 3693	. . . . . . . 8 |- ( x i^i ( ( x +o y ) \ x ) ) = (/)
14		unen 7182	. . . . . . . 8 |- ( ( ( 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 667	. . . . . . 7 |- ( ( A ~~ x /\ ( B \ A ) ~~ ( ( x +o y ) \ x ) ) -> ( A u. ( B \ A ) ) ~~ ( x u. ( ( x +o y ) \ x ) ) )
16		undif2 3697	. . . . . . . . 9 |- ( A u. ( B \ A ) ) = ( A u. B )
17	16	a1i 11	. . . . . . . 8 |- ( ( x e. om /\ y e. om ) -> ( A u. ( B \ A ) ) = ( A u. B ) )
18		nnaword1 6865	. . . . . . . . 9 |- ( ( x e. om /\ y e. om ) -> x C_ ( x +o y ) )
19		undif 3701	. . . . . . . . 9 |- ( x C_ ( x +o y ) <-> ( x u. ( ( x +o y ) \ x ) ) = ( x +o y ) )
20	18, 19	sylib 189	. . . . . . . 8 |- ( ( x e. om /\ y e. om ) -> ( x u. ( ( x +o y ) \ x ) ) = ( x +o y ) )
21	17, 20	breq12d 4218	. . . . . . 7 |- ( ( 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 211	. . . . . 6 |- ( ( x e. om /\ y e. om ) -> ( ( A ~~ x /\ ( B \ A ) ~~ ( ( x +o y ) \ x ) ) -> ( A u. B ) ~~ ( x +o y ) ) )
23	11, 22	sylan2d 469	. . . . 5 |- ( ( x e. om /\ y e. om ) -> ( ( A ~~ x /\ ( B \ A ) ~~ y ) -> ( A u. B ) ~~ ( x +o y ) ) )
24		breq2 4209	. . . . . . 7 |- ( z = ( x +o y ) -> ( ( A u. B ) ~~ z <-> ( A u. B ) ~~ ( x +o y ) ) )
25	24	rspcev 3045	. . . . . 6 |- ( ( ( x +o y ) e. om /\ ( A u. B ) ~~ ( x +o y ) ) -> E. z e. om ( A u. B ) ~~ z )
26		isfi 7124	. . . . . 6 |- ( ( A u. B ) e. Fin <-> E. z e. om ( A u. B ) ~~ z )
27	25, 26	sylibr 204	. . . . 5 |- ( ( ( x +o y ) e. om /\ ( A u. B ) ~~ ( x +o y ) ) -> ( A u. B ) e. Fin )
28	7, 23, 27	ee12an 1372	. . . 4 |- ( ( x e. om /\ y e. om ) -> ( ( A ~~ x /\ ( B \ A ) ~~ y ) -> ( A u. B ) e. Fin ) )
29	28	rexlimivv 2828	. . 3 |- ( E. x e. om E. y e. om ( A ~~ x /\ ( B \ A ) ~~ y ) -> ( A u. B ) e. Fin )
30	6, 29	sylbir 205	. 2 |- ( ( A e. Fin /\ ( B \ A ) e. Fin ) -> ( A u. B ) e. Fin )
31	1, 30	sylan2 461	1 |- ( ( A e. Fin /\ B e. Fin ) -> ( A u. B ) e. Fin )

Syntax hints:   -> wi 4   /\ wa 359   = wceq 1652   e. wcel 1725   E.wrex 2699   \ cdif 3310   u. cun 3311   i^i cin 3312   C_ wss 3313   (/)c0 3621   class class class wbr 4205   omcom 4838  (class class class)co 6074   +o coa 6714   ~~ cen 7099   Fincfn 7102

This theorem is referenced by:  unfi2  7369  difinf  7370  xpfi  7371  prfi  7374  tpfi  7375  fnfi  7377  iunfi  7387  pwfilem  7394  fiin  7420  wemapso2  7514  cantnfp1lem1  7627  ficardun2  8076  ackbij1lem6  8098  ackbij1lem16  8108  fin23lem28  8213  fin23lem30  8215  isfin1-3  8259  axcclem  8330  hashun  11649  hashunlei  11677  hashmap  11691  hashbclem  11694  hashf1lem1  11697  hashf1lem2  11698  hashf1  11699  incexclem  12609  isumltss  12621  ramub1lem1  13387  fpwipodrs  14583  acsfiindd  14596  gsumzaddlem  15519  gsumunsn  15537  dprdfadd  15571  psrbagaddcl  16428  mplsubg  16493  mpllss  16494  fctop  17061  uncmp  17459  1stckgenlem  17578  ptbasin  17602  cfinfil  17918  fin1aufil  17957  alexsubALTlem3  18073  tmdgsum  18118  tsmsfbas  18150  tsmsgsum  18161  tsmsres  18166  tsmsxplem1  18175  prdsmet  18393  prdsbl  18514  icccmplem2  18847  ovolfiniun  19390  volfiniun  19434  fta1glem2  20082  fta1lem  20217  aannenlem2  20239  aalioulem2  20243  dchrfi  21032  usgrafilem2  21419  vdgrfiun  21666  konigsberg  21702  ballotlemgun  24775  itg2addnclem2  26248  ftc1anclem7  26277  ftc1anc  26279  locfincmp  26376  comppfsc  26379  prdsbnd  26494  funsnfsup  26735  elrfi  26740  mzpcompact2lem  26800  eldioph2  26812  lsmfgcl  27141  dsmmacl  27176  symgfisg  27378  fiuneneq  27482  pclfinN  30635

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-sep 4323  ax-nul 4331  ax-pow 4370  ax-pr 4396  ax-un 4694

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2703  df-rex 2704  df-reu 2705  df-rab 2707  df-v 2951  df-sbc 3155  df-csb 3245  df-dif 3316  df-un 3318  df-in 3320  df-ss 3327  df-pss 3329  df-nul 3622  df-if 3733  df-pw 3794  df-sn 3813  df-pr 3814  df-tp 3815  df-op 3816  df-uni 4009  df-int 4044  df-iun 4088  df-br 4206  df-opab 4260  df-mpt 4261  df-tr 4296  df-eprel 4487  df-id 4491  df-po 4496  df-so 4497  df-fr 4534  df-we 4536  df-ord 4577  df-on 4578  df-lim 4579  df-suc 4580  df-om 4839  df-xp 4877  df-rel 4878  df-cnv 4879  df-co 4880  df-dm 4881  df-rn 4882  df-res 4883  df-ima 4884  df-iota 5411  df-fun 5449  df-fn 5450  df-f 5451  df-f1 5452  df-fo 5453  df-f1o 5454  df-fv 5455  df-ov 6077  df-oprab 6078  df-mpt2 6079  df-recs 6626  df-rdg 6661  df-oadd 6721  df-er 6898  df-en 7103  df-fin 7106