Theorem unfi 8212

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	⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin)

Proof of Theorem unfi

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		diffi 8177	. 2 ⊢ (𝐵 ∈ Fin → (𝐵 ∖ 𝐴) ∈ Fin)
2		reeanv 3102	. . . 4 ⊢ (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ 𝑦) ↔ (∃𝑥 ∈ ω 𝐴 ≈ 𝑥 ∧ ∃𝑦 ∈ ω (𝐵 ∖ 𝐴) ≈ 𝑦))
3		isfi 7964	. . . . 5 ⊢ (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)
4		isfi 7964	. . . . 5 ⊢ ((𝐵 ∖ 𝐴) ∈ Fin ↔ ∃𝑦 ∈ ω (𝐵 ∖ 𝐴) ≈ 𝑦)
5	3, 4	anbi12i 732	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ (𝐵 ∖ 𝐴) ∈ Fin) ↔ (∃𝑥 ∈ ω 𝐴 ≈ 𝑥 ∧ ∃𝑦 ∈ ω (𝐵 ∖ 𝐴) ≈ 𝑦))
6	2, 5	bitr4i 267	. . 3 ⊢ (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ 𝑦) ↔ (𝐴 ∈ Fin ∧ (𝐵 ∖ 𝐴) ∈ Fin))
7		nnacl 7676	. . . . 5 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝑥 +𝑜 𝑦) ∈ ω)
8		unfilem3 8211	. . . . . . 7 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → 𝑦 ≈ ((𝑥 +𝑜 𝑦) ∖ 𝑥))
9		entr 7993	. . . . . . . 8 ⊢ (((𝐵 ∖ 𝐴) ≈ 𝑦 ∧ 𝑦 ≈ ((𝑥 +𝑜 𝑦) ∖ 𝑥)) → (𝐵 ∖ 𝐴) ≈ ((𝑥 +𝑜 𝑦) ∖ 𝑥))
10	9	expcom 451	. . . . . . 7 ⊢ (𝑦 ≈ ((𝑥 +𝑜 𝑦) ∖ 𝑥) → ((𝐵 ∖ 𝐴) ≈ 𝑦 → (𝐵 ∖ 𝐴) ≈ ((𝑥 +𝑜 𝑦) ∖ 𝑥)))
11	8, 10	syl 17	. . . . . 6 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐵 ∖ 𝐴) ≈ 𝑦 → (𝐵 ∖ 𝐴) ≈ ((𝑥 +𝑜 𝑦) ∖ 𝑥)))
12		disjdif 4031	. . . . . . . 8 ⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅
13		disjdif 4031	. . . . . . . 8 ⊢ (𝑥 ∩ ((𝑥 +𝑜 𝑦) ∖ 𝑥)) = ∅
14		unen 8025	. . . . . . . 8 ⊢ (((𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ ((𝑥 +𝑜 𝑦) ∖ 𝑥)) ∧ ((𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅ ∧ (𝑥 ∩ ((𝑥 +𝑜 𝑦) ∖ 𝑥)) = ∅)) → (𝐴 ∪ (𝐵 ∖ 𝐴)) ≈ (𝑥 ∪ ((𝑥 +𝑜 𝑦) ∖ 𝑥)))
15	12, 13, 14	mpanr12 720	. . . . . . 7 ⊢ ((𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ ((𝑥 +𝑜 𝑦) ∖ 𝑥)) → (𝐴 ∪ (𝐵 ∖ 𝐴)) ≈ (𝑥 ∪ ((𝑥 +𝑜 𝑦) ∖ 𝑥)))
16		undif2 4035	. . . . . . . . 9 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)
17	16	a1i 11	. . . . . . . 8 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵))
18		nnaword1 7694	. . . . . . . . 9 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → 𝑥 ⊆ (𝑥 +𝑜 𝑦))
19		undif 4040	. . . . . . . . 9 ⊢ (𝑥 ⊆ (𝑥 +𝑜 𝑦) ↔ (𝑥 ∪ ((𝑥 +𝑜 𝑦) ∖ 𝑥)) = (𝑥 +𝑜 𝑦))
20	18, 19	sylib 208	. . . . . . . 8 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝑥 ∪ ((𝑥 +𝑜 𝑦) ∖ 𝑥)) = (𝑥 +𝑜 𝑦))
21	17, 20	breq12d 4657	. . . . . . 7 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ∪ (𝐵 ∖ 𝐴)) ≈ (𝑥 ∪ ((𝑥 +𝑜 𝑦) ∖ 𝑥)) ↔ (𝐴 ∪ 𝐵) ≈ (𝑥 +𝑜 𝑦)))
22	15, 21	syl5ib 234	. . . . . 6 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ ((𝑥 +𝑜 𝑦) ∖ 𝑥)) → (𝐴 ∪ 𝐵) ≈ (𝑥 +𝑜 𝑦)))
23	11, 22	sylan2d 499	. . . . 5 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ 𝑦) → (𝐴 ∪ 𝐵) ≈ (𝑥 +𝑜 𝑦)))
24		breq2 4648	. . . . . . 7 ⊢ (𝑧 = (𝑥 +𝑜 𝑦) → ((𝐴 ∪ 𝐵) ≈ 𝑧 ↔ (𝐴 ∪ 𝐵) ≈ (𝑥 +𝑜 𝑦)))
25	24	rspcev 3304	. . . . . 6 ⊢ (((𝑥 +𝑜 𝑦) ∈ ω ∧ (𝐴 ∪ 𝐵) ≈ (𝑥 +𝑜 𝑦)) → ∃𝑧 ∈ ω (𝐴 ∪ 𝐵) ≈ 𝑧)
26		isfi 7964	. . . . . 6 ⊢ ((𝐴 ∪ 𝐵) ∈ Fin ↔ ∃𝑧 ∈ ω (𝐴 ∪ 𝐵) ≈ 𝑧)
27	25, 26	sylibr 224	. . . . 5 ⊢ (((𝑥 +𝑜 𝑦) ∈ ω ∧ (𝐴 ∪ 𝐵) ≈ (𝑥 +𝑜 𝑦)) → (𝐴 ∪ 𝐵) ∈ Fin)
28	7, 23, 27	syl6an 567	. . . 4 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ 𝑦) → (𝐴 ∪ 𝐵) ∈ Fin))
29	28	rexlimivv 3032	. . 3 ⊢ (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ 𝑦) → (𝐴 ∪ 𝐵) ∈ Fin)
30	6, 29	sylbir 225	. 2 ⊢ ((𝐴 ∈ Fin ∧ (𝐵 ∖ 𝐴) ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin)
31	1, 30	sylan2 491	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin)

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1481   ∈ wcel 1988  ∃wrex 2910   ∖ cdif 3564   ∪ cun 3565   ∩ cin 3566   ⊆ wss 3567  ∅c0 3907   class class class wbr 4644  (class class class)co 6635  ωcom 7050   +_𝑜 coa 7542   ≈ cen 7937  Fincfn 7940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-reu 2916  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-om 7051  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-oadd 7549  df-er 7727  df-en 7941  df-fin 7944

This theorem is referenced by:  unfi2  8214  difinf  8215  xpfi  8216  prfi  8220  tpfi  8221  fnfi  8223  iunfi  8239  pwfilem  8245  fsuppun  8279  fsuppunfi  8280  ressuppfi  8286  fiin  8313  cantnfp1lem1  8560  ficardun2  9010  ackbij1lem6  9032  ackbij1lem16  9042  fin23lem28  9147  fin23lem30  9149  isfin1-3  9193  axcclem  9264  hashun  13154  hashunlei  13195  hashmap  13205  hashbclem  13219  hashf1lem1  13222  hashf1lem2  13223  hashf1  13224  fsumsplitsn  14455  fsummsnunz  14464  fsumsplitsnun  14465  fsummsnunzOLD  14466  fsumsplitsnunOLD  14467  incexclem  14549  isumltss  14561  fprodsplitsn  14701  lcmfunsnlem2lem1  15332  lcmfunsnlem2lem2  15333  lcmfunsnlem2  15334  lcmfun  15339  ramub1lem1  15711  fpwipodrs  17145  acsfiindd  17158  symgfisg  17869  gsumzunsnd  18336  gsumunsnfd  18337  psrbagaddcl  19351  mplsubg  19418  mpllss  19419  dsmmacl  20066  fctop  20789  uncmp  21187  bwth  21194  lfinun  21309  locfincmp  21310  comppfsc  21316  1stckgenlem  21337  ptbasin  21361  cfinfil  21678  fin1aufil  21717  alexsubALTlem3  21834  tmdgsum  21880  tsmsfbas  21912  tsmsgsum  21923  tsmsres  21928  tsmsxplem1  21937  prdsmet  22156  prdsbl  22277  icccmplem2  22607  rrxmval  23169  rrxmet  23172  rrxdstprj1  23173  ovolfiniun  23250  volfiniun  23296  fta1glem2  23907  fta1lem  24043  aannenlem2  24065  aalioulem2  24069  dchrfi  24961  usgrfilem  26200  ffsrn  29478  eulerpartlemt  30407  ballotlemgun  30560  hgt750lemb  30708  hgt750leme  30710  lindsenlbs  33375  poimirlem31  33411  poimirlem32  33412  itg2addnclem2  33433  ftc1anclem7  33462  ftc1anc  33464  prdsbnd  33563  pclfinN  35005  elrfi  37076  mzpcompact2lem  37133  eldioph2  37144  lsmfgcl  37463  fiuneneq  37594  dvmptfprodlem  39922  dvnprodlem2  39925  fourierdlem50  40136  fourierdlem51  40137  fourierdlem54  40140  fourierdlem76  40162  fourierdlem80  40166  fourierdlem102  40188  fourierdlem103  40189  fourierdlem104  40190  fourierdlem114  40200  sge0resplit  40386  sge0iunmptlemfi  40393  sge0xaddlem1  40413  hoiprodp1  40565  sge0hsphoire  40566  hoidmvlelem1  40572  hoidmvlelem2  40573  hoidmvlelem5  40576  hspmbllem2  40604  fsummmodsnunz  41109  mndpsuppfi  41921