Theorem unfi 8638

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 8603	. 2 ⊢ (𝐵 ∈ Fin → (𝐵 ∖ 𝐴) ∈ Fin)
2		reeanv 3330	. . . 4 ⊢ (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ 𝑦) ↔ (∃𝑥 ∈ ω 𝐴 ≈ 𝑥 ∧ ∃𝑦 ∈ ω (𝐵 ∖ 𝐴) ≈ 𝑦))
3		isfi 8388	. . . . 5 ⊢ (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)
4		isfi 8388	. . . . 5 ⊢ ((𝐵 ∖ 𝐴) ∈ Fin ↔ ∃𝑦 ∈ ω (𝐵 ∖ 𝐴) ≈ 𝑦)
5	3, 4	anbi12i 626	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ (𝐵 ∖ 𝐴) ∈ Fin) ↔ (∃𝑥 ∈ ω 𝐴 ≈ 𝑥 ∧ ∃𝑦 ∈ ω (𝐵 ∖ 𝐴) ≈ 𝑦))
6	2, 5	bitr4i 279	. . 3 ⊢ (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ 𝑦) ↔ (𝐴 ∈ Fin ∧ (𝐵 ∖ 𝐴) ∈ Fin))
7		nnacl 8094	. . . . 5 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝑥 +o 𝑦) ∈ ω)
8		unfilem3 8637	. . . . . . 7 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → 𝑦 ≈ ((𝑥 +o 𝑦) ∖ 𝑥))
9		entr 8416	. . . . . . . 8 ⊢ (((𝐵 ∖ 𝐴) ≈ 𝑦 ∧ 𝑦 ≈ ((𝑥 +o 𝑦) ∖ 𝑥)) → (𝐵 ∖ 𝐴) ≈ ((𝑥 +o 𝑦) ∖ 𝑥))
10	9	expcom 414	. . . . . . 7 ⊢ (𝑦 ≈ ((𝑥 +o 𝑦) ∖ 𝑥) → ((𝐵 ∖ 𝐴) ≈ 𝑦 → (𝐵 ∖ 𝐴) ≈ ((𝑥 +o 𝑦) ∖ 𝑥)))
11	8, 10	syl 17	. . . . . 6 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐵 ∖ 𝐴) ≈ 𝑦 → (𝐵 ∖ 𝐴) ≈ ((𝑥 +o 𝑦) ∖ 𝑥)))
12		disjdif 4341	. . . . . . . 8 ⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅
13		disjdif 4341	. . . . . . . 8 ⊢ (𝑥 ∩ ((𝑥 +o 𝑦) ∖ 𝑥)) = ∅
14		unen 8451	. . . . . . . 8 ⊢ (((𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ ((𝑥 +o 𝑦) ∖ 𝑥)) ∧ ((𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅ ∧ (𝑥 ∩ ((𝑥 +o 𝑦) ∖ 𝑥)) = ∅)) → (𝐴 ∪ (𝐵 ∖ 𝐴)) ≈ (𝑥 ∪ ((𝑥 +o 𝑦) ∖ 𝑥)))
15	12, 13, 14	mpanr12 701	. . . . . . 7 ⊢ ((𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ ((𝑥 +o 𝑦) ∖ 𝑥)) → (𝐴 ∪ (𝐵 ∖ 𝐴)) ≈ (𝑥 ∪ ((𝑥 +o 𝑦) ∖ 𝑥)))
16		undif2 4345	. . . . . . . . 9 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)
17	16	a1i 11	. . . . . . . 8 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵))
18		nnaword1 8112	. . . . . . . . 9 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → 𝑥 ⊆ (𝑥 +o 𝑦))
19		undif 4350	. . . . . . . . 9 ⊢ (𝑥 ⊆ (𝑥 +o 𝑦) ↔ (𝑥 ∪ ((𝑥 +o 𝑦) ∖ 𝑥)) = (𝑥 +o 𝑦))
20	18, 19	sylib 219	. . . . . . . 8 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝑥 ∪ ((𝑥 +o 𝑦) ∖ 𝑥)) = (𝑥 +o 𝑦))
21	17, 20	breq12d 4981	. . . . . . 7 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ∪ (𝐵 ∖ 𝐴)) ≈ (𝑥 ∪ ((𝑥 +o 𝑦) ∖ 𝑥)) ↔ (𝐴 ∪ 𝐵) ≈ (𝑥 +o 𝑦)))
22	15, 21	syl5ib 245	. . . . . 6 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ ((𝑥 +o 𝑦) ∖ 𝑥)) → (𝐴 ∪ 𝐵) ≈ (𝑥 +o 𝑦)))
23	11, 22	sylan2d 604	. . . . 5 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ 𝑦) → (𝐴 ∪ 𝐵) ≈ (𝑥 +o 𝑦)))
24		breq2 4972	. . . . . . 7 ⊢ (𝑧 = (𝑥 +o 𝑦) → ((𝐴 ∪ 𝐵) ≈ 𝑧 ↔ (𝐴 ∪ 𝐵) ≈ (𝑥 +o 𝑦)))
25	24	rspcev 3561	. . . . . 6 ⊢ (((𝑥 +o 𝑦) ∈ ω ∧ (𝐴 ∪ 𝐵) ≈ (𝑥 +o 𝑦)) → ∃𝑧 ∈ ω (𝐴 ∪ 𝐵) ≈ 𝑧)
26		isfi 8388	. . . . . 6 ⊢ ((𝐴 ∪ 𝐵) ∈ Fin ↔ ∃𝑧 ∈ ω (𝐴 ∪ 𝐵) ≈ 𝑧)
27	25, 26	sylibr 235	. . . . 5 ⊢ (((𝑥 +o 𝑦) ∈ ω ∧ (𝐴 ∪ 𝐵) ≈ (𝑥 +o 𝑦)) → (𝐴 ∪ 𝐵) ∈ Fin)
28	7, 23, 27	syl6an 680	. . . 4 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ 𝑦) → (𝐴 ∪ 𝐵) ∈ Fin))
29	28	rexlimivv 3257	. . 3 ⊢ (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ 𝑦) → (𝐴 ∪ 𝐵) ∈ Fin)
30	6, 29	sylbir 236	. 2 ⊢ ((𝐴 ∈ Fin ∧ (𝐵 ∖ 𝐴) ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin)
31	1, 30	sylan2 592	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1525   ∈ wcel 2083  ∃wrex 3108   ∖ cdif 3862   ∪ cun 3863   ∩ cin 3864   ⊆ wss 3865  ∅c0 4217   class class class wbr 4968  (class class class)co 7023  ωcom 7443   +_o coa 7957   ≈ cen 8361  Fincfn 8364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-ral 3112  df-rex 3113  df-reu 3114  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-pss 3882  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-tp 4483  df-op 4485  df-uni 4752  df-int 4789  df-iun 4833  df-br 4969  df-opab 5031  df-mpt 5048  df-tr 5071  df-id 5355  df-eprel 5360  df-po 5369  df-so 5370  df-fr 5409  df-we 5411  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-pred 6030  df-ord 6076  df-on 6077  df-lim 6078  df-suc 6079  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-ov 7026  df-oprab 7027  df-mpo 7028  df-om 7444  df-wrecs 7805  df-recs 7867  df-rdg 7905  df-oadd 7964  df-er 8146  df-en 8365  df-fin 8368

This theorem is referenced by:  unfi2  8640  difinf  8641  xpfi  8642  prfi  8646  tpfi  8647  fnfi  8649  iunfi  8665  pwfilem  8671  fsuppun  8705  fsuppunfi  8706  ressuppfi  8712  fiin  8739  cantnfp1lem1  8994  ficardun2  9478  ackbij1lem6  9500  ackbij1lem16  9510  fin23lem28  9615  fin23lem30  9617  isfin1-3  9661  axcclem  9732  hashun  13595  hashunlei  13638  hashmap  13648  hashbclem  13662  hashf1lem1  13665  hashf1lem2  13666  hashf1  13667  fsumsplitsn  14937  fsummsnunz  14946  fsumsplitsnun  14947  incexclem  15028  isumltss  15040  fprodsplitsn  15180  lcmfunsnlem2lem1  15815  lcmfunsnlem2lem2  15816  lcmfunsnlem2  15817  lcmfun  15822  ramub1lem1  16195  fpwipodrs  17607  acsfiindd  17620  symgfisg  18331  gsumzunsnd  18800  gsumunsnfd  18801  psrbagaddcl  19842  mplsubg  19909  mpllss  19910  dsmmacl  20571  fctop  21300  uncmp  21699  bwth  21706  lfinun  21821  locfincmp  21822  comppfsc  21828  1stckgenlem  21849  ptbasin  21873  cfinfil  22189  fin1aufil  22228  alexsubALTlem3  22345  tmdgsum  22391  tsmsfbas  22423  tsmsgsum  22434  tsmsres  22439  tsmsxplem1  22448  prdsmet  22667  prdsbl  22788  icccmplem2  23118  rrxmval  23695  rrxmet  23698  rrxdstprj1  23699  ovolfiniun  23789  volfiniun  23835  fta1glem2  24447  fta1lem  24583  aannenlem2  24605  aalioulem2  24609  dchrfi  25517  usgrfilem  26796  ffsrn  30149  eulerpartlemt  31242  ballotlemgun  31395  hgt750lemb  31540  hgt750leme  31542  lindsenlbs  34439  poimirlem31  34475  poimirlem32  34476  itg2addnclem2  34496  ftc1anclem7  34525  ftc1anc  34527  prdsbnd  34624  pclfinN  36588  elrfi  38797  mzpcompact2lem  38854  eldioph2  38865  lsmfgcl  39180  fiuneneq  39303  unfid  40982  dvmptfprodlem  41792  dvnprodlem2  41795  fourierdlem50  42005  fourierdlem51  42006  fourierdlem54  42009  fourierdlem76  42031  fourierdlem80  42035  fourierdlem102  42057  fourierdlem103  42058  fourierdlem104  42059  fourierdlem114  42069  sge0resplit  42252  sge0iunmptlemfi  42259  sge0xaddlem1  42279  hoiprodp1  42434  sge0hsphoire  42435  hoidmvlelem1  42441  hoidmvlelem2  42442  hoidmvlelem5  42445  hspmbllem2  42473  fsummmodsnunz  43073  mndpsuppfi  43925