Theorem unfi 7864

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 7829	. 2 |- ( B e. Fin -> ( B \ A ) e. Fin )
2		reeanv 2970	. . . 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 7619	. . . . 5 |- ( A e. Fin <-> E. x e. om A ~~ x )
4		isfi 7619	. . . . 5 |- ( ( B \ A ) e. Fin <-> E. y e. om ( B \ A ) ~~ y )
5	3, 4	anbi12i 708	. . . 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 260	. . 3 |- ( E. x e. om E. y e. om ( A ~~ x /\ ( B \ A ) ~~ y ) <-> ( A e. Fin /\ ( B \ A ) e. Fin ) )
7		nnacl 7338	. . . . 5 |- ( ( x e. om /\ y e. om ) -> ( x +o y ) e. om )
8		unfilem3 7863	. . . . . . 7 |- ( ( x e. om /\ y e. om ) -> y ~~ ( ( x +o y ) \ x ) )
9		entr 7647	. . . . . . . 8 |- ( ( ( B \ A ) ~~ y /\ y ~~ ( ( x +o y ) \ x ) ) -> ( B \ A ) ~~ ( ( x +o y ) \ x ) )
10	9	expcom 441	. . . . . . 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 3851	. . . . . . . 8 |- ( A i^i ( B \ A ) ) = (/)
13		disjdif 3851	. . . . . . . 8 |- ( x i^i ( ( x +o y ) \ x ) ) = (/)
14		unen 7678	. . . . . . . 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 696	. . . . . . 7 |- ( ( A ~~ x /\ ( B \ A ) ~~ ( ( x +o y ) \ x ) ) -> ( A u. ( B \ A ) ) ~~ ( x u. ( ( x +o y ) \ x ) ) )
16		undif2 3855	. . . . . . . . 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 7356	. . . . . . . . 9 |- ( ( x e. om /\ y e. om ) -> x C_ ( x +o y ) )
19		undif 3860	. . . . . . . . 9 |- ( x C_ ( x +o y ) <-> ( x u. ( ( x +o y ) \ x ) ) = ( x +o y ) )
20	18, 19	sylib 201	. . . . . . . 8 |- ( ( x e. om /\ y e. om ) -> ( x u. ( ( x +o y ) \ x ) ) = ( x +o y ) )
21	17, 20	breq12d 4429	. . . . . . 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 227	. . . . . 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 489	. . . . 5 |- ( ( x e. om /\ y e. om ) -> ( ( A ~~ x /\ ( B \ A ) ~~ y ) -> ( A u. B ) ~~ ( x +o y ) ) )
24		breq2 4420	. . . . . . 7 |- ( z = ( x +o y ) -> ( ( A u. B ) ~~ z <-> ( A u. B ) ~~ ( x +o y ) ) )
25	24	rspcev 3162	. . . . . 6 |- ( ( ( x +o y ) e. om /\ ( A u. B ) ~~ ( x +o y ) ) -> E. z e. om ( A u. B ) ~~ z )
26		isfi 7619	. . . . . 6 |- ( ( A u. B ) e. Fin <-> E. z e. om ( A u. B ) ~~ z )
27	25, 26	sylibr 217	. . . . 5 |- ( ( ( x +o y ) e. om /\ ( A u. B ) ~~ ( x +o y ) ) -> ( A u. B ) e. Fin )
28	7, 23, 27	syl6an 552	. . . 4 |- ( ( x e. om /\ y e. om ) -> ( ( A ~~ x /\ ( B \ A ) ~~ y ) -> ( A u. B ) e. Fin ) )
29	28	rexlimivv 2896	. . 3 |- ( E. x e. om E. y e. om ( A ~~ x /\ ( B \ A ) ~~ y ) -> ( A u. B ) e. Fin )
30	6, 29	sylbir 218	. 2 |- ( ( A e. Fin /\ ( B \ A ) e. Fin ) -> ( A u. B ) e. Fin )
31	1, 30	sylan2 481	1 |- ( ( A e. Fin /\ B e. Fin ) -> ( A u. B ) e. Fin )

Syntax hints:   -> wi 4   /\ wa 375   = wceq 1455   e. wcel 1898   E.wrex 2750   \ cdif 3413   u. cun 3414   i^i cin 3415   C_ wss 3416   (/)c0 3743   class class class wbr 4416  (class class class)co 6315   omcom 6719   +o coa 7205   ~~ cen 7592   Fincfn 7595

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-om 6720  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-oadd 7212  df-er 7389  df-en 7596  df-fin 7599

This theorem is referenced by:  unfi2  7866  difinf  7867  xpfi  7868  prfi  7872  tpfi  7873  fnfi  7875  iunfi  7888  pwfilem  7894  fsuppun  7928  fsuppunfi  7929  ressuppfi  7935  fiin  7962  cantnfp1lem1  8209  ficardun2  8659  ackbij1lem6  8681  ackbij1lem16  8691  fin23lem28  8796  fin23lem30  8798  isfin1-3  8842  axcclem  8913  hashun  12593  hashunlei  12630  hashmap  12640  hashbclem  12648  hashf1lem1  12651  hashf1lem2  12652  hashf1  12653  fsummsnunz  13864  fsumsplitsnun  13865  incexclem  13943  isumltss  13955  fprodsplitsn  14092  lcmfunsnlem2lem1  14660  lcmfunsnlem2lem2  14661  lcmfunsnlem2  14662  lcmfun  14667  ramub1lem1  15033  fpwipodrs  16459  acsfiindd  16472  symgfisg  17158  gsumzunsnd  17637  gsumunsnfd  17638  psrbagaddcl  18643  mplsubg  18710  mpllss  18711  dsmmacl  19353  fctop  20068  uncmp  20467  bwth  20474  lfinun  20589  locfincmp  20590  comppfsc  20596  1stckgenlem  20617  ptbasin  20641  cfinfil  20957  fin1aufil  20996  alexsubALTlem3  21113  tmdgsum  21159  tsmsfbas  21191  tsmsgsum  21202  tsmsres  21207  tsmsxplem1  21216  prdsmet  21434  prdsbl  21555  icccmplem2  21890  rrxmval  22408  rrxmet  22411  rrxdstprj1  22412  ovolfiniun  22503  volfiniun  22549  fta1glem2  23166  fta1lem  23309  aannenlem2  23334  aalioulem2  23338  dchrfi  24232  usgrafilem2  25189  vdgrfiun  25679  konigsberg  25764  ffsrn  28363  eulerpartlemt  29253  ballotlemgun  29406  ballotlemgunOLD  29444  poimirlem31  32016  poimirlem32  32017  itg2addnclem2  32039  ftc1anclem7  32068  ftc1anc  32070  prdsbnd  32170  pclfinN  33510  elrfi  35581  mzpcompact2lem  35638  eldioph2  35649  lsmfgcl  35977  fiuneneq  36116  fsumsplitsn  37687  dvmptfprodlem  37857  dvnprodlem2  37860  fourierdlem50  38058  fourierdlem51  38059  fourierdlem54  38062  fourierdlem76  38084  fourierdlem80  38088  fourierdlem102  38110  fourierdlem103  38111  fourierdlem104  38112  fourierdlem114  38122  sge0resplit  38286  sge0iunmptlemfi  38293  sge0xaddlem1  38313  hoiprodp1  38448  sge0hsphoire  38449  hoidmvlelem1  38455  hoidmvlelem2  38456  hoidmvlelem5  38459  hspmbllem2  38487  fsummmodsnunz  39140  usgrfilem  39443  usgfislem2  40030  usgfisALTlem2  40034  mndpsuppfi  40433