Theorem unfi 7078

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

Step	Hyp	Ref	Expression
1		diffi 7043	. 2 |- ( B e. Fin -> ( B \ A ) e. Fin )
2		reeanv 2680	. . . 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 6839	. . . . 5 |- ( A e. Fin <-> E. x e. om A ~~ x )
4		isfi 6839	. . . . 5 |- ( ( B \ A ) e. Fin <-> E. y e. om ( B \ A ) ~~ y )
5	3, 4	anbi12i 681	. . . 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 245	. . 3 |- ( E. x e. om E. y e. om ( A ~~ x /\ ( B \ A ) ~~ y ) <-> ( A e. Fin /\ ( B \ A ) e. Fin ) )
7		nnacl 6563	. . . . 5 |- ( ( x e. om /\ y e. om ) -> ( x +o y ) e. om )
8		unfilem3 7077	. . . . . . 7 |- ( ( x e. om /\ y e. om ) -> y ~~ ( ( x +o y ) \ x ) )
9		entr 6867	. . . . . . . 8 |- ( ( ( B \ A ) ~~ y /\ y ~~ ( ( x +o y ) \ x ) ) -> ( B \ A ) ~~ ( ( x +o y ) \ x ) )
10	9	expcom 426	. . . . . . 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 3487	. . . . . . . 8 |- ( A i^i ( B \ A ) ) = (/)
13		disjdif 3487	. . . . . . . 8 |- ( x i^i ( ( x +o y ) \ x ) ) = (/)
14		unen 6897	. . . . . . . 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 669	. . . . . . 7 |- ( ( A ~~ x /\ ( B \ A ) ~~ ( ( x +o y ) \ x ) ) -> ( A u. ( B \ A ) ) ~~ ( x u. ( ( x +o y ) \ x ) ) )
16		undif2 3491	. . . . . . . . 9 |- ( A u. ( B \ A ) ) = ( A u. B )
17	16	a1i 12	. . . . . . . 8 |- ( ( x e. om /\ y e. om ) -> ( A u. ( B \ A ) ) = ( A u. B ) )
18		nnaword1 6581	. . . . . . . . 9 |- ( ( x e. om /\ y e. om ) -> x C_ ( x +o y ) )
19		undif 3495	. . . . . . . . 9 |- ( x C_ ( x +o y ) <-> ( x u. ( ( x +o y ) \ x ) ) = ( x +o y ) )
20	18, 19	sylib 190	. . . . . . . 8 |- ( ( x e. om /\ y e. om ) -> ( x u. ( ( x +o y ) \ x ) ) = ( x +o y ) )
21	17, 20	breq12d 3996	. . . . . . 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 212	. . . . . 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 470	. . . . 5 |- ( ( x e. om /\ y e. om ) -> ( ( A ~~ x /\ ( B \ A ) ~~ y ) -> ( A u. B ) ~~ ( x +o y ) ) )
24		breq2 3987	. . . . . . 7 |- ( z = ( x +o y ) -> ( ( A u. B ) ~~ z <-> ( A u. B ) ~~ ( x +o y ) ) )
25	24	rcla4ev 2852	. . . . . 6 |- ( ( ( x +o y ) e. om /\ ( A u. B ) ~~ ( x +o y ) ) -> E. z e. om ( A u. B ) ~~ z )
26		isfi 6839	. . . . . 6 |- ( ( A u. B ) e. Fin <-> E. z e. om ( A u. B ) ~~ z )
27	25, 26	sylibr 205	. . . . 5 |- ( ( ( x +o y ) e. om /\ ( A u. B ) ~~ ( x +o y ) ) -> ( A u. B ) e. Fin )
28	7, 23, 27	ee12an 1359	. . . 4 |- ( ( x e. om /\ y e. om ) -> ( ( A ~~ x /\ ( B \ A ) ~~ y ) -> ( A u. B ) e. Fin ) )
29	28	rexlimivv 2645	. . 3 |- ( E. x e. om E. y e. om ( A ~~ x /\ ( B \ A ) ~~ y ) -> ( A u. B ) e. Fin )
30	6, 29	sylbir 206	. 2 |- ( ( A e. Fin /\ ( B \ A ) e. Fin ) -> ( A u. B ) e. Fin )
31	1, 30	sylan2 462	1 |- ( ( A e. Fin /\ B e. Fin ) -> ( A u. B ) e. Fin )

Syntax hints:   -> wi 6   /\ wa 360   = wceq 1619   e. wcel 1621   E.wrex 2517   \ cdif 3110   u. cun 3111   i^i cin 3112   C_ wss 3113   (/)c0 3416   class class class wbr 3983   omcom 4614  (class class class)co 5778   +o coa 6430   ~~ cen 6814   Fincfn 6817

This theorem is referenced by:  unfi2  7080  difinf  7081  xpfi  7082  prfi  7085  tpfi  7086  fnfi  7088  iunfi  7098  pwfilem  7104  fiin  7129  wemapso2  7221  cantnfp1lem1  7334  ficardun2  7783  ackbij1lem6  7805  ackbij1lem16  7815  fin23lem28  7920  fin23lem30  7922  isfin1-3  7966  axcclem  8037  hashun  11316  hashunlei  11328  hashmap  11338  hashbclem  11341  hashf1lem1  11344  hashf1lem2  11345  hashf1  11346  isumltss  12255  ramub1lem1  13021  fpwipodrs  14215  acsfiindd  14228  gsumzaddlem  15151  gsumunsn  15169  dprdfadd  15203  psrbagaddcl  16064  mplsubg  16129  mpllss  16130  fctop  16689  uncmp  17078  1stckgenlem  17196  ptbasin  17220  cfinfil  17536  fin1aufil  17575  alexsubALTlem3  17691  tmdgsum  17726  tsmsfbas  17758  tsmsgsum  17769  tsmsres  17774  tsmsxplem1  17783  prdsmet  17882  prdsbl  17985  icccmplem2  18276  ovolfiniun  18808  volfiniun  18852  fta1glem2  19500  fta1lem  19635  aannenlem2  19657  aalioulem2  19661  dchrfi  20442  ballotlemgun  23030  vdgrun  23251  konigsberg  23269  locfincmp  25657  comppfsc  25660  prdsbnd  25870  funsnfsup  26115  elrfi  26122  mzpcompact2lem  26182  eldioph2  26194  lsmfgcl  26525  dsmmacl  26560  symgfisg  26762  fiuneneq  26866  pclfinN  29240

This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-sep 4101  ax-nul 4109  ax-pow 4146  ax-pr 4172  ax-un 4470

This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2121  df-mo 2122  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2521  df-rex 2522  df-reu 2523  df-rab 2525  df-v 2759  df-sbc 2953  df-csb 3043  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-pss 3129  df-nul 3417  df-if 3526  df-pw 3587  df-sn 3606  df-pr 3607  df-tp 3608  df-op 3609  df-uni 3788  df-int 3823  df-iun 3867  df-br 3984  df-opab 4038  df-mpt 4039  df-tr 4074  df-eprel 4263  df-id 4267  df-po 4272  df-so 4273  df-fr 4310  df-we 4312  df-ord 4353  df-on 4354  df-lim 4355  df-suc 4356  df-om 4615  df-xp 4661  df-rel 4662  df-cnv 4663  df-co 4664  df-dm 4665  df-rn 4666  df-res 4667  df-ima 4668  df-fun 4669  df-fn 4670  df-f 4671  df-f1 4672  df-fo 4673  df-f1o 4674  df-fv 4675  df-ov 5781  df-oprab 5782  df-mpt2 5783  df-recs 6342  df-rdg 6377  df-oadd 6437  df-er 6614  df-en 6818  df-fin 6821