Theorem unfi 7835

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 7800	. 2 |- ( B e. Fin -> ( B \ A ) e. Fin )
2		reeanv 2994	. . . 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 7591	. . . . 5 |- ( A e. Fin <-> E. x e. om A ~~ x )
4		isfi 7591	. . . . 5 |- ( ( B \ A ) e. Fin <-> E. y e. om ( B \ A ) ~~ y )
5	3, 4	anbi12i 701	. . . 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 255	. . 3 |- ( E. x e. om E. y e. om ( A ~~ x /\ ( B \ A ) ~~ y ) <-> ( A e. Fin /\ ( B \ A ) e. Fin ) )
7		nnacl 7311	. . . . 5 |- ( ( x e. om /\ y e. om ) -> ( x +o y ) e. om )
8		unfilem3 7834	. . . . . . 7 |- ( ( x e. om /\ y e. om ) -> y ~~ ( ( x +o y ) \ x ) )
9		entr 7619	. . . . . . . 8 |- ( ( ( B \ A ) ~~ y /\ y ~~ ( ( x +o y ) \ x ) ) -> ( B \ A ) ~~ ( ( x +o y ) \ x ) )
10	9	expcom 436	. . . . . . 7 |- ( y ~~ ( ( x +o y ) \ x ) -> ( ( B \ A ) ~~ y -> ( B \ A ) ~~ ( ( x +o y ) \ x ) ) )
11	8, 10	syl 17	. . . . . 6 |- ( ( x e. om /\ y e. om ) -> ( ( B \ A ) ~~ y -> ( B \ A ) ~~ ( ( x +o y ) \ x ) ) )
12		disjdif 3864	. . . . . . . 8 |- ( A i^i ( B \ A ) ) = (/)
13		disjdif 3864	. . . . . . . 8 |- ( x i^i ( ( x +o y ) \ x ) ) = (/)
14		unen 7650	. . . . . . . 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 689	. . . . . . 7 |- ( ( A ~~ x /\ ( B \ A ) ~~ ( ( x +o y ) \ x ) ) -> ( A u. ( B \ A ) ) ~~ ( x u. ( ( x +o y ) \ x ) ) )
16		undif2 3868	. . . . . . . . 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 7329	. . . . . . . . 9 |- ( ( x e. om /\ y e. om ) -> x C_ ( x +o y ) )
19		undif 3873	. . . . . . . . 9 |- ( x C_ ( x +o y ) <-> ( x u. ( ( x +o y ) \ x ) ) = ( x +o y ) )
20	18, 19	sylib 199	. . . . . . . 8 |- ( ( x e. om /\ y e. om ) -> ( x u. ( ( x +o y ) \ x ) ) = ( x +o y ) )
21	17, 20	breq12d 4430	. . . . . . 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 222	. . . . . 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 484	. . . . 5 |- ( ( x e. om /\ y e. om ) -> ( ( A ~~ x /\ ( B \ A ) ~~ y ) -> ( A u. B ) ~~ ( x +o y ) ) )
24		breq2 4421	. . . . . . 7 |- ( z = ( x +o y ) -> ( ( A u. B ) ~~ z <-> ( A u. B ) ~~ ( x +o y ) ) )
25	24	rspcev 3179	. . . . . 6 |- ( ( ( x +o y ) e. om /\ ( A u. B ) ~~ ( x +o y ) ) -> E. z e. om ( A u. B ) ~~ z )
26		isfi 7591	. . . . . 6 |- ( ( A u. B ) e. Fin <-> E. z e. om ( A u. B ) ~~ z )
27	25, 26	sylibr 215	. . . . 5 |- ( ( ( x +o y ) e. om /\ ( A u. B ) ~~ ( x +o y ) ) -> ( A u. B ) e. Fin )
28	7, 23, 27	syl6an 547	. . . 4 |- ( ( x e. om /\ y e. om ) -> ( ( A ~~ x /\ ( B \ A ) ~~ y ) -> ( A u. B ) e. Fin ) )
29	28	rexlimivv 2920	. . 3 |- ( E. x e. om E. y e. om ( A ~~ x /\ ( B \ A ) ~~ y ) -> ( A u. B ) e. Fin )
30	6, 29	sylbir 216	. 2 |- ( ( A e. Fin /\ ( B \ A ) e. Fin ) -> ( A u. B ) e. Fin )
31	1, 30	sylan2 476	1 |- ( ( A e. Fin /\ B e. Fin ) -> ( A u. B ) e. Fin )

Syntax hints:   -> wi 4   /\ wa 370   = wceq 1437   e. wcel 1867   E.wrex 2774   \ cdif 3430   u. cun 3431   i^i cin 3432   C_ wss 3433   (/)c0 3758   class class class wbr 4417  (class class class)co 6296   omcom 6697   +o coa 7178   ~~ cen 7565   Fincfn 7568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6588

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-reu 2780  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-pss 3449  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-tp 3998  df-op 4000  df-uni 4214  df-int 4250  df-iun 4295  df-br 4418  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4756  df-id 4760  df-po 4766  df-so 4767  df-fr 4804  df-we 4806  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-pred 5390  df-ord 5436  df-on 5437  df-lim 5438  df-suc 5439  df-iota 5556  df-fun 5594  df-fn 5595  df-f 5596  df-f1 5597  df-fo 5598  df-f1o 5599  df-fv 5600  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6698  df-wrecs 7027  df-recs 7089  df-rdg 7127  df-oadd 7185  df-er 7362  df-en 7569  df-fin 7572

This theorem is referenced by:  unfi2  7837  difinf  7838  xpfi  7839  prfi  7843  tpfi  7844  fnfi  7846  iunfi  7859  pwfilem  7865  fsuppun  7899  fsuppunfi  7900  ressuppfi  7906  fiin  7933  cantnfp1lem1  8173  ficardun2  8622  ackbij1lem6  8644  ackbij1lem16  8654  fin23lem28  8759  fin23lem30  8761  isfin1-3  8805  axcclem  8876  hashun  12547  hashunlei  12581  hashmap  12591  hashbclem  12599  hashf1lem1  12602  hashf1lem2  12603  hashf1  12604  fsummsnunz  13782  fsumsplitsnun  13783  incexclem  13861  isumltss  13873  fprodsplitsn  14010  lcmfunsnlem2lem1  14571  lcmfunsnlem2lem2  14572  lcmfunsnlem2  14573  lcmfun  14578  ramub1lem1  14936  fpwipodrs  16354  acsfiindd  16367  symgfisg  17053  gsumzunsnd  17516  gsumunsnfd  17517  psrbagaddcl  18522  mplsubg  18589  mpllss  18590  dsmmacl  19228  fctop  19943  uncmp  20342  bwth  20349  lfinun  20464  locfincmp  20465  comppfsc  20471  1stckgenlem  20492  ptbasin  20516  cfinfil  20832  fin1aufil  20871  alexsubALTlem3  20988  tmdgsum  21034  tsmsfbas  21066  tsmsgsum  21077  tsmsres  21082  tsmsxplem1  21091  prdsmet  21309  prdsbl  21430  icccmplem2  21745  rrxmval  22245  rrxmet  22248  rrxdstprj1  22249  ovolfiniun  22328  volfiniun  22374  fta1glem2  22989  fta1lem  23125  aannenlem2  23147  aalioulem2  23151  dchrfi  24043  usgrafilem2  24982  vdgrfiun  25472  konigsberg  25557  ffsrn  28154  eulerpartlemt  29027  ballotlemgun  29180  poimirlem31  31675  poimirlem32  31676  itg2addnclem2  31698  ftc1anclem7  31727  ftc1anc  31729  prdsbnd  31829  pclfinN  33174  elrfi  35245  mzpcompact2lem  35302  eldioph2  35313  lsmfgcl  35642  fiuneneq  35774  fsumsplitsn  37228  dvmptfprodlem  37392  dvnprodlem2  37395  fourierdlem50  37592  fourierdlem51  37593  fourierdlem54  37596  fourierdlem76  37618  fourierdlem80  37622  fourierdlem102  37644  fourierdlem103  37645  fourierdlem104  37646  fourierdlem114  37656  sge0resplit  37786  sge0iunmptlemfi  37793  fsummmodsnunz  38431  usgfislem2  38528  usgfisALTlem2  38532  mndpsuppfi  38933