Theorem unfi 8785

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 8750	. 2 ⊢ (𝐵 ∈ Fin → (𝐵 ∖ 𝐴) ∈ Fin)
2		reeanv 3367	. . . 4 ⊢ (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ 𝑦) ↔ (∃𝑥 ∈ ω 𝐴 ≈ 𝑥 ∧ ∃𝑦 ∈ ω (𝐵 ∖ 𝐴) ≈ 𝑦))
3		isfi 8533	. . . . 5 ⊢ (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)
4		isfi 8533	. . . . 5 ⊢ ((𝐵 ∖ 𝐴) ∈ Fin ↔ ∃𝑦 ∈ ω (𝐵 ∖ 𝐴) ≈ 𝑦)
5	3, 4	anbi12i 628	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ (𝐵 ∖ 𝐴) ∈ Fin) ↔ (∃𝑥 ∈ ω 𝐴 ≈ 𝑥 ∧ ∃𝑦 ∈ ω (𝐵 ∖ 𝐴) ≈ 𝑦))
6	2, 5	bitr4i 280	. . 3 ⊢ (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ 𝑦) ↔ (𝐴 ∈ Fin ∧ (𝐵 ∖ 𝐴) ∈ Fin))
7		nnacl 8237	. . . . 5 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝑥 +o 𝑦) ∈ ω)
8		unfilem3 8784	. . . . . . 7 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → 𝑦 ≈ ((𝑥 +o 𝑦) ∖ 𝑥))
9		entr 8561	. . . . . . . 8 ⊢ (((𝐵 ∖ 𝐴) ≈ 𝑦 ∧ 𝑦 ≈ ((𝑥 +o 𝑦) ∖ 𝑥)) → (𝐵 ∖ 𝐴) ≈ ((𝑥 +o 𝑦) ∖ 𝑥))
10	9	expcom 416	. . . . . . 7 ⊢ (𝑦 ≈ ((𝑥 +o 𝑦) ∖ 𝑥) → ((𝐵 ∖ 𝐴) ≈ 𝑦 → (𝐵 ∖ 𝐴) ≈ ((𝑥 +o 𝑦) ∖ 𝑥)))
11	8, 10	syl 17	. . . . . 6 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐵 ∖ 𝐴) ≈ 𝑦 → (𝐵 ∖ 𝐴) ≈ ((𝑥 +o 𝑦) ∖ 𝑥)))
12		disjdif 4421	. . . . . . . 8 ⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅
13		disjdif 4421	. . . . . . . 8 ⊢ (𝑥 ∩ ((𝑥 +o 𝑦) ∖ 𝑥)) = ∅
14		unen 8596	. . . . . . . 8 ⊢ (((𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ ((𝑥 +o 𝑦) ∖ 𝑥)) ∧ ((𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅ ∧ (𝑥 ∩ ((𝑥 +o 𝑦) ∖ 𝑥)) = ∅)) → (𝐴 ∪ (𝐵 ∖ 𝐴)) ≈ (𝑥 ∪ ((𝑥 +o 𝑦) ∖ 𝑥)))
15	12, 13, 14	mpanr12 703	. . . . . . 7 ⊢ ((𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ ((𝑥 +o 𝑦) ∖ 𝑥)) → (𝐴 ∪ (𝐵 ∖ 𝐴)) ≈ (𝑥 ∪ ((𝑥 +o 𝑦) ∖ 𝑥)))
16		undif2 4425	. . . . . . . . 9 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)
17	16	a1i 11	. . . . . . . 8 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵))
18		nnaword1 8255	. . . . . . . . 9 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → 𝑥 ⊆ (𝑥 +o 𝑦))
19		undif 4430	. . . . . . . . 9 ⊢ (𝑥 ⊆ (𝑥 +o 𝑦) ↔ (𝑥 ∪ ((𝑥 +o 𝑦) ∖ 𝑥)) = (𝑥 +o 𝑦))
20	18, 19	sylib 220	. . . . . . . 8 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝑥 ∪ ((𝑥 +o 𝑦) ∖ 𝑥)) = (𝑥 +o 𝑦))
21	17, 20	breq12d 5079	. . . . . . 7 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ∪ (𝐵 ∖ 𝐴)) ≈ (𝑥 ∪ ((𝑥 +o 𝑦) ∖ 𝑥)) ↔ (𝐴 ∪ 𝐵) ≈ (𝑥 +o 𝑦)))
22	15, 21	syl5ib 246	. . . . . 6 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ ((𝑥 +o 𝑦) ∖ 𝑥)) → (𝐴 ∪ 𝐵) ≈ (𝑥 +o 𝑦)))
23	11, 22	sylan2d 606	. . . . 5 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ 𝑦) → (𝐴 ∪ 𝐵) ≈ (𝑥 +o 𝑦)))
24		breq2 5070	. . . . . . 7 ⊢ (𝑧 = (𝑥 +o 𝑦) → ((𝐴 ∪ 𝐵) ≈ 𝑧 ↔ (𝐴 ∪ 𝐵) ≈ (𝑥 +o 𝑦)))
25	24	rspcev 3623	. . . . . 6 ⊢ (((𝑥 +o 𝑦) ∈ ω ∧ (𝐴 ∪ 𝐵) ≈ (𝑥 +o 𝑦)) → ∃𝑧 ∈ ω (𝐴 ∪ 𝐵) ≈ 𝑧)
26		isfi 8533	. . . . . 6 ⊢ ((𝐴 ∪ 𝐵) ∈ Fin ↔ ∃𝑧 ∈ ω (𝐴 ∪ 𝐵) ≈ 𝑧)
27	25, 26	sylibr 236	. . . . 5 ⊢ (((𝑥 +o 𝑦) ∈ ω ∧ (𝐴 ∪ 𝐵) ≈ (𝑥 +o 𝑦)) → (𝐴 ∪ 𝐵) ∈ Fin)
28	7, 23, 27	syl6an 682	. . . 4 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ 𝑦) → (𝐴 ∪ 𝐵) ∈ Fin))
29	28	rexlimivv 3292	. . 3 ⊢ (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ 𝑦) → (𝐴 ∪ 𝐵) ∈ Fin)
30	6, 29	sylbir 237	. 2 ⊢ ((𝐴 ∈ Fin ∧ (𝐵 ∖ 𝐴) ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin)
31	1, 30	sylan2 594	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∃wrex 3139   ∖ cdif 3933   ∪ cun 3934   ∩ cin 3935   ⊆ wss 3936  ∅c0 4291   class class class wbr 5066  (class class class)co 7156  ωcom 7580   +_o coa 8099   ≈ cen 8506  Fincfn 8509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-int 4877  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-ov 7159  df-oprab 7160  df-mpo 7161  df-om 7581  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-oadd 8106  df-er 8289  df-en 8510  df-fin 8513

This theorem is referenced by:  unfi2  8787  difinf  8788  xpfi  8789  prfi  8793  tpfi  8794  fnfi  8796  iunfi  8812  pwfilem  8818  fsuppun  8852  fsuppunfi  8853  ressuppfi  8859  fiin  8886  cantnfp1lem1  9141  ficardun2  9625  ackbij1lem6  9647  ackbij1lem16  9657  fin23lem28  9762  fin23lem30  9764  isfin1-3  9808  axcclem  9879  hashun  13744  hashunlei  13787  hashmap  13797  hashbclem  13811  hashf1lem1  13814  hashf1lem2  13815  hashf1  13816  fsumsplitsn  15100  fsummsnunz  15109  fsumsplitsnun  15110  incexclem  15191  isumltss  15203  fprodsplitsn  15343  lcmfunsnlem2lem1  15982  lcmfunsnlem2lem2  15983  lcmfunsnlem2  15984  lcmfun  15989  ramub1lem1  16362  fpwipodrs  17774  acsfiindd  17787  symgfisg  18596  gsumzunsnd  19076  gsumunsnfd  19077  psrbagaddcl  20150  mplsubg  20217  mpllss  20218  dsmmacl  20885  fctop  21612  uncmp  22011  bwth  22018  lfinun  22133  locfincmp  22134  comppfsc  22140  1stckgenlem  22161  ptbasin  22185  cfinfil  22501  fin1aufil  22540  alexsubALTlem3  22657  tmdgsum  22703  tsmsfbas  22736  tsmsgsum  22747  tsmsres  22752  tsmsxplem1  22761  prdsmet  22980  prdsbl  23101  icccmplem2  23431  rrxmval  24008  rrxmet  24011  rrxdstprj1  24012  ovolfiniun  24102  volfiniun  24148  fta1glem2  24760  fta1lem  24896  aannenlem2  24918  aalioulem2  24922  dchrfi  25831  usgrfilem  27109  ffsrn  30465  eulerpartlemt  31629  ballotlemgun  31782  hgt750lemb  31927  hgt750leme  31929  lindsenlbs  34902  poimirlem31  34938  poimirlem32  34939  itg2addnclem2  34959  ftc1anclem7  34988  ftc1anc  34990  prdsbnd  35086  pclfinN  37051  elrfi  39340  mzpcompact2lem  39397  eldioph2  39408  lsmfgcl  39723  fiuneneq  39846  unfid  41471  dvmptfprodlem  42278  dvnprodlem2  42281  fourierdlem50  42490  fourierdlem51  42491  fourierdlem54  42494  fourierdlem76  42516  fourierdlem80  42520  fourierdlem102  42542  fourierdlem103  42543  fourierdlem104  42544  fourierdlem114  42554  sge0resplit  42737  sge0iunmptlemfi  42744  sge0xaddlem1  42764  hoiprodp1  42919  sge0hsphoire  42920  hoidmvlelem1  42926  hoidmvlelem2  42927  hoidmvlelem5  42930  hspmbllem2  42958  fsummmodsnunz  43584  mndpsuppfi  44472