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 8394

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 8359	. 2 ⊢ (𝐵 ∈ Fin → (𝐵 ∖ 𝐴) ∈ Fin)
2		reeanv 3245	. . . 4 ⊢ (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ 𝑦) ↔ (∃𝑥 ∈ ω 𝐴 ≈ 𝑥 ∧ ∃𝑦 ∈ ω (𝐵 ∖ 𝐴) ≈ 𝑦))
3		isfi 8147	. . . . 5 ⊢ (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)
4		isfi 8147	. . . . 5 ⊢ ((𝐵 ∖ 𝐴) ∈ Fin ↔ ∃𝑦 ∈ ω (𝐵 ∖ 𝐴) ≈ 𝑦)
5	3, 4	anbi12i 735	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ (𝐵 ∖ 𝐴) ∈ Fin) ↔ (∃𝑥 ∈ ω 𝐴 ≈ 𝑥 ∧ ∃𝑦 ∈ ω (𝐵 ∖ 𝐴) ≈ 𝑦))
6	2, 5	bitr4i 267	. . 3 ⊢ (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ 𝑦) ↔ (𝐴 ∈ Fin ∧ (𝐵 ∖ 𝐴) ∈ Fin))
7		nnacl 7862	. . . . 5 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝑥 +_𝑜 𝑦) ∈ ω)
8		unfilem3 8393	. . . . . . 7 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → 𝑦 ≈ ((𝑥 +_𝑜 𝑦) ∖ 𝑥))
9		entr 8175	. . . . . . . 8 ⊢ (((𝐵 ∖ 𝐴) ≈ 𝑦 ∧ 𝑦 ≈ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)) → (𝐵 ∖ 𝐴) ≈ ((𝑥 +_𝑜 𝑦) ∖ 𝑥))
10	9	expcom 450	. . . . . . 7 ⊢ (𝑦 ≈ ((𝑥 +_𝑜 𝑦) ∖ 𝑥) → ((𝐵 ∖ 𝐴) ≈ 𝑦 → (𝐵 ∖ 𝐴) ≈ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)))
11	8, 10	syl 17	. . . . . 6 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐵 ∖ 𝐴) ≈ 𝑦 → (𝐵 ∖ 𝐴) ≈ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)))
12		disjdif 4184	. . . . . . . 8 ⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅
13		disjdif 4184	. . . . . . . 8 ⊢ (𝑥 ∩ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)) = ∅
14		unen 8207	. . . . . . . 8 ⊢ (((𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)) ∧ ((𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅ ∧ (𝑥 ∩ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)) = ∅)) → (𝐴 ∪ (𝐵 ∖ 𝐴)) ≈ (𝑥 ∪ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)))
15	12, 13, 14	mpanr12 723	. . . . . . 7 ⊢ ((𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)) → (𝐴 ∪ (𝐵 ∖ 𝐴)) ≈ (𝑥 ∪ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)))
16		undif2 4188	. . . . . . . . 9 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)
17	16	a1i 11	. . . . . . . 8 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵))
18		nnaword1 7880	. . . . . . . . 9 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → 𝑥 ⊆ (𝑥 +_𝑜 𝑦))
19		undif 4193	. . . . . . . . 9 ⊢ (𝑥 ⊆ (𝑥 +_𝑜 𝑦) ↔ (𝑥 ∪ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)) = (𝑥 +_𝑜 𝑦))
20	18, 19	sylib 208	. . . . . . . 8 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝑥 ∪ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)) = (𝑥 +_𝑜 𝑦))
21	17, 20	breq12d 4817	. . . . . . 7 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ∪ (𝐵 ∖ 𝐴)) ≈ (𝑥 ∪ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)) ↔ (𝐴 ∪ 𝐵) ≈ (𝑥 +_𝑜 𝑦)))
22	15, 21	syl5ib 234	. . . . . 6 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)) → (𝐴 ∪ 𝐵) ≈ (𝑥 +_𝑜 𝑦)))
23	11, 22	sylan2d 500	. . . . 5 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ 𝑦) → (𝐴 ∪ 𝐵) ≈ (𝑥 +_𝑜 𝑦)))
24		breq2 4808	. . . . . . 7 ⊢ (𝑧 = (𝑥 +_𝑜 𝑦) → ((𝐴 ∪ 𝐵) ≈ 𝑧 ↔ (𝐴 ∪ 𝐵) ≈ (𝑥 +_𝑜 𝑦)))
25	24	rspcev 3449	. . . . . 6 ⊢ (((𝑥 +_𝑜 𝑦) ∈ ω ∧ (𝐴 ∪ 𝐵) ≈ (𝑥 +_𝑜 𝑦)) → ∃𝑧 ∈ ω (𝐴 ∪ 𝐵) ≈ 𝑧)
26		isfi 8147	. . . . . 6 ⊢ ((𝐴 ∪ 𝐵) ∈ Fin ↔ ∃𝑧 ∈ ω (𝐴 ∪ 𝐵) ≈ 𝑧)
27	25, 26	sylibr 224	. . . . 5 ⊢ (((𝑥 +_𝑜 𝑦) ∈ ω ∧ (𝐴 ∪ 𝐵) ≈ (𝑥 +_𝑜 𝑦)) → (𝐴 ∪ 𝐵) ∈ Fin)
28	7, 23, 27	syl6an 569	. . . 4 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ 𝑦) → (𝐴 ∪ 𝐵) ∈ Fin))
29	28	rexlimivv 3174	. . 3 ⊢ (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ 𝑦) → (𝐴 ∪ 𝐵) ∈ Fin)
30	6, 29	sylbir 225	. 2 ⊢ ((𝐴 ∈ Fin ∧ (𝐵 ∖ 𝐴) ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin)
31	1, 30	sylan2 492	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 383 = wceq 1632 ∈ wcel 2139 ∃wrex 3051 ∖ cdif 3712 ∪ cun 3713 ∩ cin 3714 ⊆ wss 3715 ∅c0 4058 class class class wbr 4804 (class class class)co 6814 ωcom 7231 +_𝑜 coa 7727 ≈ cen 8120 Fincfn 8123

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-8 2141 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 ax-sep 4933 ax-nul 4941 ax-pow 4992 ax-pr 5055 ax-un 7115

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-eu 2611 df-mo 2612 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-ne 2933 df-ral 3055 df-rex 3056 df-reu 3057 df-rab 3059 df-v 3342 df-sbc 3577 df-csb 3675 df-dif 3718 df-un 3720 df-in 3722 df-ss 3729 df-pss 3731 df-nul 4059 df-if 4231 df-pw 4304 df-sn 4322 df-pr 4324 df-tp 4326 df-op 4328 df-uni 4589 df-int 4628 df-iun 4674 df-br 4805 df-opab 4865 df-mpt 4882 df-tr 4905 df-id 5174 df-eprel 5179 df-po 5187 df-so 5188 df-fr 5225 df-we 5227 df-xp 5272 df-rel 5273 df-cnv 5274 df-co 5275 df-dm 5276 df-rn 5277 df-res 5278 df-ima 5279 df-pred 5841 df-ord 5887 df-on 5888 df-lim 5889 df-suc 5890 df-iota 6012 df-fun 6051 df-fn 6052 df-f 6053 df-f1 6054 df-fo 6055 df-f1o 6056 df-fv 6057 df-ov 6817 df-oprab 6818 df-mpt2 6819 df-om 7232 df-wrecs 7577 df-recs 7638 df-rdg 7676 df-oadd 7734 df-er 7913 df-en 8124 df-fin 8127

This theorem is referenced by: unfi2 8396 difinf 8397 xpfi 8398 prfi 8402 tpfi 8403 fnfi 8405 iunfi 8421 pwfilem 8427 fsuppun 8461 fsuppunfi 8462 ressuppfi 8468 fiin 8495 cantnfp1lem1 8750 ficardun2 9237 ackbij1lem6 9259 ackbij1lem16 9269 fin23lem28 9374 fin23lem30 9376 isfin1-3 9420 axcclem 9491 hashun 13383 hashunlei 13424 hashmap 13434 hashbclem 13448 hashf1lem1 13451 hashf1lem2 13452 hashf1 13453 fsumsplitsn 14693 fsummsnunz 14702 fsumsplitsnun 14703 fsummsnunzOLD 14704 fsumsplitsnunOLD 14705 incexclem 14787 isumltss 14799 fprodsplitsn 14939 lcmfunsnlem2lem1 15573 lcmfunsnlem2lem2 15574 lcmfunsnlem2 15575 lcmfun 15580 ramub1lem1 15952 fpwipodrs 17385 acsfiindd 17398 symgfisg 18108 gsumzunsnd 18575 gsumunsnfd 18576 psrbagaddcl 19592 mplsubg 19659 mpllss 19660 dsmmacl 20307 fctop 21030 uncmp 21428 bwth 21435 lfinun 21550 locfincmp 21551 comppfsc 21557 1stckgenlem 21578 ptbasin 21602 cfinfil 21918 fin1aufil 21957 alexsubALTlem3 22074 tmdgsum 22120 tsmsfbas 22152 tsmsgsum 22163 tsmsres 22168 tsmsxplem1 22177 prdsmet 22396 prdsbl 22517 icccmplem2 22847 rrxmval 23408 rrxmet 23411 rrxdstprj1 23412 ovolfiniun 23489 volfiniun 23535 fta1glem2 24145 fta1lem 24281 aannenlem2 24303 aalioulem2 24307 dchrfi 25200 usgrfilem 26439 ffsrn 29834 eulerpartlemt 30763 ballotlemgun 30916 hgt750lemb 31064 hgt750leme 31066 lindsenlbs 33735 poimirlem31 33771 poimirlem32 33772 itg2addnclem2 33793 ftc1anclem7 33822 ftc1anc 33824 prdsbnd 33923 pclfinN 35707 elrfi 37777 mzpcompact2lem 37834 eldioph2 37845 lsmfgcl 38164 fiuneneq 38295 unfid 39862 dvmptfprodlem 40680 dvnprodlem2 40683 fourierdlem50 40894 fourierdlem51 40895 fourierdlem54 40898 fourierdlem76 40920 fourierdlem80 40924 fourierdlem102 40946 fourierdlem103 40947 fourierdlem104 40948 fourierdlem114 40958 sge0resplit 41144 sge0iunmptlemfi 41151 sge0xaddlem1 41171 hoiprodp1 41326 sge0hsphoire 41327 hoidmvlelem1 41333 hoidmvlelem2 41334 hoidmvlelem5 41337 hspmbllem2 41365 fsummmodsnunz 41873 mndpsuppfi 42684

W3C validator