Theorem unfi 7337

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 7302	. 2 |- ( B e. Fin -> ( B \ A ) e. Fin )
2		reeanv 2839	. . . 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 7094	. . . . 5 |- ( A e. Fin <-> E. x e. om A ~~ x )
4		isfi 7094	. . . . 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 6817	. . . . 5 |- ( ( x e. om /\ y e. om ) -> ( x +o y ) e. om )
8		unfilem3 7336	. . . . . . 7 |- ( ( x e. om /\ y e. om ) -> y ~~ ( ( x +o y ) \ x ) )
9		entr 7122	. . . . . . . 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 3664	. . . . . . . 8 |- ( A i^i ( B \ A ) ) = (/)
13		disjdif 3664	. . . . . . . 8 |- ( x i^i ( ( x +o y ) \ x ) ) = (/)
14		unen 7152	. . . . . . . 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 3668	. . . . . . . . 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 6835	. . . . . . . . 9 |- ( ( x e. om /\ y e. om ) -> x C_ ( x +o y ) )
19		undif 3672	. . . . . . . . 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 4189	. . . . . . 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 4180	. . . . . . 7 |- ( z = ( x +o y ) -> ( ( A u. B ) ~~ z <-> ( A u. B ) ~~ ( x +o y ) ) )
25	24	rspcev 3016	. . . . . 6 |- ( ( ( x +o y ) e. om /\ ( A u. B ) ~~ ( x +o y ) ) -> E. z e. om ( A u. B ) ~~ z )
26		isfi 7094	. . . . . 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 1369	. . . 4 |- ( ( x e. om /\ y e. om ) -> ( ( A ~~ x /\ ( B \ A ) ~~ y ) -> ( A u. B ) e. Fin ) )
29	28	rexlimivv 2799	. . 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 1649   e. wcel 1721   E.wrex 2671   \ cdif 3281   u. cun 3282   i^i cin 3283   C_ wss 3284   (/)c0 3592   class class class wbr 4176   omcom 4808  (class class class)co 6044   +o coa 6684   ~~ cen 7069   Fincfn 7072

This theorem is referenced by:  unfi2  7339  difinf  7340  xpfi  7341  prfi  7344  tpfi  7345  fnfi  7347  iunfi  7357  pwfilem  7363  fiin  7389  wemapso2  7481  cantnfp1lem1  7594  ficardun2  8043  ackbij1lem6  8065  ackbij1lem16  8075  fin23lem28  8180  fin23lem30  8182  isfin1-3  8226  axcclem  8297  hashun  11615  hashunlei  11643  hashmap  11657  hashbclem  11660  hashf1lem1  11663  hashf1lem2  11664  hashf1  11665  incexclem  12575  isumltss  12587  ramub1lem1  13353  fpwipodrs  14549  acsfiindd  14562  gsumzaddlem  15485  gsumunsn  15503  dprdfadd  15537  psrbagaddcl  16394  mplsubg  16459  mpllss  16460  fctop  17027  uncmp  17424  1stckgenlem  17542  ptbasin  17566  cfinfil  17882  fin1aufil  17921  alexsubALTlem3  18037  tmdgsum  18082  tsmsfbas  18114  tsmsgsum  18125  tsmsres  18130  tsmsxplem1  18139  prdsmet  18357  prdsbl  18478  icccmplem2  18811  ovolfiniun  19354  volfiniun  19398  fta1glem2  20046  fta1lem  20181  aannenlem2  20203  aalioulem2  20207  dchrfi  20996  usgrafilem2  21383  vdgrfiun  21630  konigsberg  21666  ballotlemgun  24739  itg2addnclem2  26160  locfincmp  26278  comppfsc  26281  prdsbnd  26396  funsnfsup  26637  elrfi  26642  mzpcompact2lem  26702  eldioph2  26714  lsmfgcl  27044  dsmmacl  27079  symgfisg  27281  fiuneneq  27385  pclfinN  30386

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-sep 4294  ax-nul 4302  ax-pow 4341  ax-pr 4367  ax-un 4664

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-reu 2677  df-rab 2679  df-v 2922  df-sbc 3126  df-csb 3216  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-pss 3300  df-nul 3593  df-if 3704  df-pw 3765  df-sn 3784  df-pr 3785  df-tp 3786  df-op 3787  df-uni 3980  df-int 4015  df-iun 4059  df-br 4177  df-opab 4231  df-mpt 4232  df-tr 4267  df-eprel 4458  df-id 4462  df-po 4467  df-so 4468  df-fr 4505  df-we 4507  df-ord 4548  df-on 4549  df-lim 4550  df-suc 4551  df-om 4809  df-xp 4847  df-rel 4848  df-cnv 4849  df-co 4850  df-dm 4851  df-rn 4852  df-res 4853  df-ima 4854  df-iota 5381  df-fun 5419  df-fn 5420  df-f 5421  df-f1 5422  df-fo 5423  df-f1o 5424  df-fv 5425  df-ov 6047  df-oprab 6048  df-mpt2 6049  df-recs 6596  df-rdg 6631  df-oadd 6691  df-er 6868  df-en 7073  df-fin 7076