unfi - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > unfi		Structured version Visualization version GIF version

Theorem unfi 8268

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 8233	. 2 ⊢ (𝐵 ∈ Fin → (𝐵 ∖ 𝐴) ∈ Fin)
2		reeanv 3136	. . . 4 ⊢ (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ 𝑦) ↔ (∃𝑥 ∈ ω 𝐴 ≈ 𝑥 ∧ ∃𝑦 ∈ ω (𝐵 ∖ 𝐴) ≈ 𝑦))
3		isfi 8021	. . . . 5 ⊢ (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)
4		isfi 8021	. . . . 5 ⊢ ((𝐵 ∖ 𝐴) ∈ Fin ↔ ∃𝑦 ∈ ω (𝐵 ∖ 𝐴) ≈ 𝑦)
5	3, 4	anbi12i 733	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ (𝐵 ∖ 𝐴) ∈ Fin) ↔ (∃𝑥 ∈ ω 𝐴 ≈ 𝑥 ∧ ∃𝑦 ∈ ω (𝐵 ∖ 𝐴) ≈ 𝑦))
6	2, 5	bitr4i 267	. . 3 ⊢ (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ 𝑦) ↔ (𝐴 ∈ Fin ∧ (𝐵 ∖ 𝐴) ∈ Fin))
7		nnacl 7736	. . . . 5 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝑥 +_𝑜 𝑦) ∈ ω)
8		unfilem3 8267	. . . . . . 7 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → 𝑦 ≈ ((𝑥 +_𝑜 𝑦) ∖ 𝑥))
9		entr 8049	. . . . . . . 8 ⊢ (((𝐵 ∖ 𝐴) ≈ 𝑦 ∧ 𝑦 ≈ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)) → (𝐵 ∖ 𝐴) ≈ ((𝑥 +_𝑜 𝑦) ∖ 𝑥))
10	9	expcom 450	. . . . . . 7 ⊢ (𝑦 ≈ ((𝑥 +_𝑜 𝑦) ∖ 𝑥) → ((𝐵 ∖ 𝐴) ≈ 𝑦 → (𝐵 ∖ 𝐴) ≈ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)))
11	8, 10	syl 17	. . . . . 6 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐵 ∖ 𝐴) ≈ 𝑦 → (𝐵 ∖ 𝐴) ≈ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)))
12		disjdif 4073	. . . . . . . 8 ⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅
13		disjdif 4073	. . . . . . . 8 ⊢ (𝑥 ∩ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)) = ∅
14		unen 8081	. . . . . . . 8 ⊢ (((𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)) ∧ ((𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅ ∧ (𝑥 ∩ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)) = ∅)) → (𝐴 ∪ (𝐵 ∖ 𝐴)) ≈ (𝑥 ∪ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)))
15	12, 13, 14	mpanr12 721	. . . . . . 7 ⊢ ((𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)) → (𝐴 ∪ (𝐵 ∖ 𝐴)) ≈ (𝑥 ∪ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)))
16		undif2 4077	. . . . . . . . 9 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)
17	16	a1i 11	. . . . . . . 8 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵))
18		nnaword1 7754	. . . . . . . . 9 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → 𝑥 ⊆ (𝑥 +_𝑜 𝑦))
19		undif 4082	. . . . . . . . 9 ⊢ (𝑥 ⊆ (𝑥 +_𝑜 𝑦) ↔ (𝑥 ∪ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)) = (𝑥 +_𝑜 𝑦))
20	18, 19	sylib 208	. . . . . . . 8 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝑥 ∪ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)) = (𝑥 +_𝑜 𝑦))
21	17, 20	breq12d 4698	. . . . . . 7 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ∪ (𝐵 ∖ 𝐴)) ≈ (𝑥 ∪ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)) ↔ (𝐴 ∪ 𝐵) ≈ (𝑥 +_𝑜 𝑦)))
22	15, 21	syl5ib 234	. . . . . 6 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)) → (𝐴 ∪ 𝐵) ≈ (𝑥 +_𝑜 𝑦)))
23	11, 22	sylan2d 498	. . . . 5 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ 𝑦) → (𝐴 ∪ 𝐵) ≈ (𝑥 +_𝑜 𝑦)))
24		breq2 4689	. . . . . . 7 ⊢ (𝑧 = (𝑥 +_𝑜 𝑦) → ((𝐴 ∪ 𝐵) ≈ 𝑧 ↔ (𝐴 ∪ 𝐵) ≈ (𝑥 +_𝑜 𝑦)))
25	24	rspcev 3340	. . . . . 6 ⊢ (((𝑥 +_𝑜 𝑦) ∈ ω ∧ (𝐴 ∪ 𝐵) ≈ (𝑥 +_𝑜 𝑦)) → ∃𝑧 ∈ ω (𝐴 ∪ 𝐵) ≈ 𝑧)
26		isfi 8021	. . . . . 6 ⊢ ((𝐴 ∪ 𝐵) ∈ Fin ↔ ∃𝑧 ∈ ω (𝐴 ∪ 𝐵) ≈ 𝑧)
27	25, 26	sylibr 224	. . . . 5 ⊢ (((𝑥 +_𝑜 𝑦) ∈ ω ∧ (𝐴 ∪ 𝐵) ≈ (𝑥 +_𝑜 𝑦)) → (𝐴 ∪ 𝐵) ∈ Fin)
28	7, 23, 27	syl6an 567	. . . 4 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ 𝑦) → (𝐴 ∪ 𝐵) ∈ Fin))
29	28	rexlimivv 3065	. . 3 ⊢ (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ 𝑦) → (𝐴 ∪ 𝐵) ∈ Fin)
30	6, 29	sylbir 225	. 2 ⊢ ((𝐴 ∈ Fin ∧ (𝐵 ∖ 𝐴) ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin)
31	1, 30	sylan2 490	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 383 = wceq 1523 ∈ wcel 2030 ∃wrex 2942 ∖ cdif 3604 ∪ cun 3605 ∩ cin 3606 ⊆ wss 3607 ∅c0 3948 class class class wbr 4685 (class class class)co 6690 ωcom 7107 +_𝑜 coa 7602 ≈ cen 7994 Fincfn 7997

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-8 2032 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-sep 4814 ax-nul 4822 ax-pow 4873 ax-pr 4936 ax-un 6991

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1055 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-eu 2502 df-mo 2503 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ne 2824 df-ral 2946 df-rex 2947 df-reu 2948 df-rab 2950 df-v 3233 df-sbc 3469 df-csb 3567 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-pss 3623 df-nul 3949 df-if 4120 df-pw 4193 df-sn 4211 df-pr 4213 df-tp 4215 df-op 4217 df-uni 4469 df-int 4508 df-iun 4554 df-br 4686 df-opab 4746 df-mpt 4763 df-tr 4786 df-id 5053 df-eprel 5058 df-po 5064 df-so 5065 df-fr 5102 df-we 5104 df-xp 5149 df-rel 5150 df-cnv 5151 df-co 5152 df-dm 5153 df-rn 5154 df-res 5155 df-ima 5156 df-pred 5718 df-ord 5764 df-on 5765 df-lim 5766 df-suc 5767 df-iota 5889 df-fun 5928 df-fn 5929 df-f 5930 df-f1 5931 df-fo 5932 df-f1o 5933 df-fv 5934 df-ov 6693 df-oprab 6694 df-mpt2 6695 df-om 7108 df-wrecs 7452 df-recs 7513 df-rdg 7551 df-oadd 7609 df-er 7787 df-en 7998 df-fin 8001

This theorem is referenced by: unfi2 8270 difinf 8271 xpfi 8272 prfi 8276 tpfi 8277 fnfi 8279 iunfi 8295 pwfilem 8301 fsuppun 8335 fsuppunfi 8336 ressuppfi 8342 fiin 8369 cantnfp1lem1 8613 ficardun2 9063 ackbij1lem6 9085 ackbij1lem16 9095 fin23lem28 9200 fin23lem30 9202 isfin1-3 9246 axcclem 9317 hashun 13209 hashunlei 13250 hashmap 13260 hashbclem 13274 hashf1lem1 13277 hashf1lem2 13278 hashf1 13279 fsumsplitsn 14518 fsummsnunz 14527 fsumsplitsnun 14528 fsummsnunzOLD 14529 fsumsplitsnunOLD 14530 incexclem 14612 isumltss 14624 fprodsplitsn 14764 lcmfunsnlem2lem1 15398 lcmfunsnlem2lem2 15399 lcmfunsnlem2 15400 lcmfun 15405 ramub1lem1 15777 fpwipodrs 17211 acsfiindd 17224 symgfisg 17934 gsumzunsnd 18401 gsumunsnfd 18402 psrbagaddcl 19418 mplsubg 19485 mpllss 19486 dsmmacl 20133 fctop 20856 uncmp 21254 bwth 21261 lfinun 21376 locfincmp 21377 comppfsc 21383 1stckgenlem 21404 ptbasin 21428 cfinfil 21744 fin1aufil 21783 alexsubALTlem3 21900 tmdgsum 21946 tsmsfbas 21978 tsmsgsum 21989 tsmsres 21994 tsmsxplem1 22003 prdsmet 22222 prdsbl 22343 icccmplem2 22673 rrxmval 23234 rrxmet 23237 rrxdstprj1 23238 ovolfiniun 23315 volfiniun 23361 fta1glem2 23971 fta1lem 24107 aannenlem2 24129 aalioulem2 24133 dchrfi 25025 usgrfilem 26264 ffsrn 29632 eulerpartlemt 30561 ballotlemgun 30714 hgt750lemb 30862 hgt750leme 30864 lindsenlbs 33534 poimirlem31 33570 poimirlem32 33571 itg2addnclem2 33592 ftc1anclem7 33621 ftc1anc 33623 prdsbnd 33722 pclfinN 35504 elrfi 37574 mzpcompact2lem 37631 eldioph2 37642 lsmfgcl 37961 fiuneneq 38092 unfid 39659 dvmptfprodlem 40477 dvnprodlem2 40480 fourierdlem50 40691 fourierdlem51 40692 fourierdlem54 40695 fourierdlem76 40717 fourierdlem80 40721 fourierdlem102 40743 fourierdlem103 40744 fourierdlem104 40745 fourierdlem114 40755 sge0resplit 40941 sge0iunmptlemfi 40948 sge0xaddlem1 40968 hoiprodp1 41123 sge0hsphoire 41124 hoidmvlelem1 41130 hoidmvlelem2 41131 hoidmvlelem5 41134 hspmbllem2 41162 fsummmodsnunz 41670 mndpsuppfi 42481

W3C validator