Theorem unfi 7785

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 7749	. 2 |- ( B e. Fin -> ( B \ A ) e. Fin )
2		reeanv 3009	. . . 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 7537	. . . . 5 |- ( A e. Fin <-> E. x e. om A ~~ x )
4		isfi 7537	. . . . 5 |- ( ( B \ A ) e. Fin <-> E. y e. om ( B \ A ) ~~ y )
5	3, 4	anbi12i 697	. . . 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 7258	. . . . 5 |- ( ( x e. om /\ y e. om ) -> ( x +o y ) e. om )
8		unfilem3 7784	. . . . . . 7 |- ( ( x e. om /\ y e. om ) -> y ~~ ( ( x +o y ) \ x ) )
9		entr 7565	. . . . . . . 8 |- ( ( ( B \ A ) ~~ y /\ y ~~ ( ( x +o y ) \ x ) ) -> ( B \ A ) ~~ ( ( x +o y ) \ x ) )
10	9	expcom 435	. . . . . . 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 3882	. . . . . . . 8 |- ( A i^i ( B \ A ) ) = (/)
13		disjdif 3882	. . . . . . . 8 |- ( x i^i ( ( x +o y ) \ x ) ) = (/)
14		unen 7596	. . . . . . . 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 685	. . . . . . 7 |- ( ( A ~~ x /\ ( B \ A ) ~~ ( ( x +o y ) \ x ) ) -> ( A u. ( B \ A ) ) ~~ ( x u. ( ( x +o y ) \ x ) ) )
16		undif2 3886	. . . . . . . . 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 7276	. . . . . . . . 9 |- ( ( x e. om /\ y e. om ) -> x C_ ( x +o y ) )
19		undif 3890	. . . . . . . . 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 4446	. . . . . . 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 482	. . . . 5 |- ( ( x e. om /\ y e. om ) -> ( ( A ~~ x /\ ( B \ A ) ~~ y ) -> ( A u. B ) ~~ ( x +o y ) ) )
24		breq2 4437	. . . . . . 7 |- ( z = ( x +o y ) -> ( ( A u. B ) ~~ z <-> ( A u. B ) ~~ ( x +o y ) ) )
25	24	rspcev 3194	. . . . . 6 |- ( ( ( x +o y ) e. om /\ ( A u. B ) ~~ ( x +o y ) ) -> E. z e. om ( A u. B ) ~~ z )
26		isfi 7537	. . . . . 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 545	. . . 4 |- ( ( x e. om /\ y e. om ) -> ( ( A ~~ x /\ ( B \ A ) ~~ y ) -> ( A u. B ) e. Fin ) )
29	28	rexlimivv 2938	. . 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 474	1 |- ( ( A e. Fin /\ B e. Fin ) -> ( A u. B ) e. Fin )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1381   e. wcel 1802   E.wrex 2792   \ cdif 3455   u. cun 3456   i^i cin 3457   C_ wss 3458   (/)c0 3767   class class class wbr 4433  (class class class)co 6277   omcom 6681   +o coa 7125   ~~ cen 7511   Fincfn 7514

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pow 4611  ax-pr 4672  ax-un 6573

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-reu 2798  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3418  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-pss 3474  df-nul 3768  df-if 3923  df-pw 3995  df-sn 4011  df-pr 4013  df-tp 4015  df-op 4017  df-uni 4231  df-int 4268  df-iun 4313  df-br 4434  df-opab 4492  df-mpt 4493  df-tr 4527  df-eprel 4777  df-id 4781  df-po 4786  df-so 4787  df-fr 4824  df-we 4826  df-ord 4867  df-on 4868  df-lim 4869  df-suc 4870  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-f1 5579  df-fo 5580  df-f1o 5581  df-fv 5582  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-om 6682  df-recs 7040  df-rdg 7074  df-oadd 7132  df-er 7309  df-en 7515  df-fin 7518

This theorem is referenced by:  unfi2  7787  difinf  7788  xpfi  7789  prfi  7793  tpfi  7794  fnfi  7796  iunfi  7806  pwfilem  7812  fsuppun  7846  fsuppunfi  7847  ressuppfi  7853  fiin  7880  wemapso2OLD  7975  cantnfp1lem1  8095  cantnfp1lem1OLD  8121  ficardun2  8581  ackbij1lem6  8603  ackbij1lem16  8613  fin23lem28  8718  fin23lem30  8720  isfin1-3  8764  axcclem  8835  hashun  12424  hashunlei  12457  hashmap  12467  hashbclem  12475  hashf1lem1  12478  hashf1lem2  12479  hashf1  12480  fsummsnunz  13543  fsumsplitsnun  13544  incexclem  13622  isumltss  13634  ramub1lem1  14416  fpwipodrs  15663  acsfiindd  15676  symgfisg  16362  gsumzaddlemOLD  16805  gsumzunsnd  16851  gsumunsnfd  16852  dprdfaddOLD  16935  psrbagaddcl  17888  psrbagaddclOLD  17889  mplsubg  17966  mpllss  17967  funsnfsupOLD  18124  dsmmacl  18639  fctop  19371  uncmp  19769  bwth  19776  lfinun  19892  locfincmp  19893  comppfsc  19899  1stckgenlem  19920  ptbasin  19944  cfinfil  20260  fin1aufil  20299  alexsubALTlem3  20415  tmdgsum  20460  tsmsfbas  20492  tsmsgsum  20503  tsmsgsumOLD  20506  tsmsresOLD  20511  tsmsres  20512  tsmsxplem1  20521  prdsmet  20739  prdsbl  20860  icccmplem2  21194  rrxmval  21698  rrxmet  21701  rrxdstprj1  21702  ovolfiniun  21778  volfiniun  21823  fta1glem2  22433  fta1lem  22568  aannenlem2  22590  aalioulem2  22594  dchrfi  23395  usgrafilem2  24277  vdgrfiun  24767  konigsberg  24852  ffsrn  27417  eulerpartlemt  28176  ballotlemgun  28329  itg2addnclem2  30035  ftc1anclem7  30064  ftc1anc  30066  prdsbnd  30257  elrfi  30594  mzpcompact2lem  30652  eldioph2  30663  lsmfgcl  30988  fiuneneq  31123  fourierdlem50  31824  fourierdlem51  31825  fourierdlem54  31828  fourierdlem76  31850  fourierdlem80  31854  fourierdlem102  31876  fourierdlem103  31877  fourierdlem104  31878  fourierdlem114  31888  fsummmodsnunz  32182  usgfislem2  32279  usgfisALTlem2  32283  mndpsuppfi  32678  pclfinN  35326