Theorem unfi 7779

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 7744	. 2 |- ( B e. Fin -> ( B \ A ) e. Fin )
2		reeanv 3022	. . . 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 7532	. . . . 5 |- ( A e. Fin <-> E. x e. om A ~~ x )
4		isfi 7532	. . . . 5 |- ( ( B \ A ) e. Fin <-> E. y e. om ( B \ A ) ~~ y )
5	3, 4	anbi12i 695	. . . 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 252	. . 3 |- ( E. x e. om E. y e. om ( A ~~ x /\ ( B \ A ) ~~ y ) <-> ( A e. Fin /\ ( B \ A ) e. Fin ) )
7		nnacl 7252	. . . . 5 |- ( ( x e. om /\ y e. om ) -> ( x +o y ) e. om )
8		unfilem3 7778	. . . . . . 7 |- ( ( x e. om /\ y e. om ) -> y ~~ ( ( x +o y ) \ x ) )
9		entr 7560	. . . . . . . 8 |- ( ( ( B \ A ) ~~ y /\ y ~~ ( ( x +o y ) \ x ) ) -> ( B \ A ) ~~ ( ( x +o y ) \ x ) )
10	9	expcom 433	. . . . . . 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 3888	. . . . . . . 8 |- ( A i^i ( B \ A ) ) = (/)
13		disjdif 3888	. . . . . . . 8 |- ( x i^i ( ( x +o y ) \ x ) ) = (/)
14		unen 7591	. . . . . . . 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 683	. . . . . . 7 |- ( ( A ~~ x /\ ( B \ A ) ~~ ( ( x +o y ) \ x ) ) -> ( A u. ( B \ A ) ) ~~ ( x u. ( ( x +o y ) \ x ) ) )
16		undif2 3892	. . . . . . . . 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 7270	. . . . . . . . 9 |- ( ( x e. om /\ y e. om ) -> x C_ ( x +o y ) )
19		undif 3896	. . . . . . . . 9 |- ( x C_ ( x +o y ) <-> ( x u. ( ( x +o y ) \ x ) ) = ( x +o y ) )
20	18, 19	sylib 196	. . . . . . . 8 |- ( ( x e. om /\ y e. om ) -> ( x u. ( ( x +o y ) \ x ) ) = ( x +o y ) )
21	17, 20	breq12d 4452	. . . . . . 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 219	. . . . . 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 480	. . . . 5 |- ( ( x e. om /\ y e. om ) -> ( ( A ~~ x /\ ( B \ A ) ~~ y ) -> ( A u. B ) ~~ ( x +o y ) ) )
24		breq2 4443	. . . . . . 7 |- ( z = ( x +o y ) -> ( ( A u. B ) ~~ z <-> ( A u. B ) ~~ ( x +o y ) ) )
25	24	rspcev 3207	. . . . . 6 |- ( ( ( x +o y ) e. om /\ ( A u. B ) ~~ ( x +o y ) ) -> E. z e. om ( A u. B ) ~~ z )
26		isfi 7532	. . . . . 6 |- ( ( A u. B ) e. Fin <-> E. z e. om ( A u. B ) ~~ z )
27	25, 26	sylibr 212	. . . . 5 |- ( ( ( x +o y ) e. om /\ ( A u. B ) ~~ ( x +o y ) ) -> ( A u. B ) e. Fin )
28	7, 23, 27	syl6an 543	. . . 4 |- ( ( x e. om /\ y e. om ) -> ( ( A ~~ x /\ ( B \ A ) ~~ y ) -> ( A u. B ) e. Fin ) )
29	28	rexlimivv 2951	. . 3 |- ( E. x e. om E. y e. om ( A ~~ x /\ ( B \ A ) ~~ y ) -> ( A u. B ) e. Fin )
30	6, 29	sylbir 213	. 2 |- ( ( A e. Fin /\ ( B \ A ) e. Fin ) -> ( A u. B ) e. Fin )
31	1, 30	sylan2 472	1 |- ( ( A e. Fin /\ B e. Fin ) -> ( A u. B ) e. Fin )

Syntax hints:   -> wi 4   /\ wa 367   = wceq 1398   e. wcel 1823   E.wrex 2805   \ cdif 3458   u. cun 3459   i^i cin 3460   C_ wss 3461   (/)c0 3783   class class class wbr 4439  (class class class)co 6270   omcom 6673   +o coa 7119   ~~ cen 7506   Fincfn 7509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-reu 2811  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-tp 4021  df-op 4023  df-uni 4236  df-int 4272  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-tr 4533  df-eprel 4780  df-id 4784  df-po 4789  df-so 4790  df-fr 4827  df-we 4829  df-ord 4870  df-on 4871  df-lim 4872  df-suc 4873  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-om 6674  df-recs 7034  df-rdg 7068  df-oadd 7126  df-er 7303  df-en 7510  df-fin 7513

This theorem is referenced by:  unfi2  7781  difinf  7782  xpfi  7783  prfi  7787  tpfi  7788  fnfi  7790  iunfi  7800  pwfilem  7806  fsuppun  7840  fsuppunfi  7841  ressuppfi  7847  fiin  7874  wemapso2OLD  7969  cantnfp1lem1  8088  cantnfp1lem1OLD  8114  ficardun2  8574  ackbij1lem6  8596  ackbij1lem16  8606  fin23lem28  8711  fin23lem30  8713  isfin1-3  8757  axcclem  8828  hashun  12433  hashunlei  12467  hashmap  12477  hashbclem  12485  hashf1lem1  12488  hashf1lem2  12489  hashf1  12490  fsummsnunz  13651  fsumsplitsnun  13652  incexclem  13730  isumltss  13742  ramub1lem1  14628  fpwipodrs  15993  acsfiindd  16006  symgfisg  16692  gsumzaddlemOLD  17135  gsumzunsnd  17178  gsumunsnfd  17179  dprdfaddOLD  17262  psrbagaddcl  18215  psrbagaddclOLD  18216  mplsubg  18293  mpllss  18294  funsnfsupOLD  18451  dsmmacl  18945  fctop  19672  uncmp  20070  bwth  20077  lfinun  20192  locfincmp  20193  comppfsc  20199  1stckgenlem  20220  ptbasin  20244  cfinfil  20560  fin1aufil  20599  alexsubALTlem3  20715  tmdgsum  20760  tsmsfbas  20792  tsmsgsum  20803  tsmsgsumOLD  20806  tsmsresOLD  20811  tsmsres  20812  tsmsxplem1  20821  prdsmet  21039  prdsbl  21160  icccmplem2  21494  rrxmval  21998  rrxmet  22001  rrxdstprj1  22002  ovolfiniun  22078  volfiniun  22123  fta1glem2  22733  fta1lem  22869  aannenlem2  22891  aalioulem2  22895  dchrfi  23728  usgrafilem2  24614  vdgrfiun  25104  konigsberg  25189  ffsrn  27783  eulerpartlemt  28574  ballotlemgun  28727  itg2addnclem2  30307  ftc1anclem7  30336  ftc1anc  30338  prdsbnd  30529  elrfi  30866  mzpcompact2lem  30923  eldioph2  30934  lsmfgcl  31259  fiuneneq  31395  fsumsplitsn  31810  fprodsplitsn  31831  dvmptfprodlem  31980  dvnprodlem2  31983  fourierdlem50  32178  fourierdlem51  32179  fourierdlem54  32182  fourierdlem76  32204  fourierdlem80  32208  fourierdlem102  32230  fourierdlem103  32231  fourierdlem104  32232  fourierdlem114  32242  fsummmodsnunz  32720  usgfislem2  32817  usgfisALTlem2  32821  mndpsuppfi  33222  pclfinN  36021