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 8112

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 8077	. 2 ⊢ (𝐵 ∈ Fin → (𝐵 ∖ 𝐴) ∈ Fin)
2		reeanv 3086	. . . 4 ⊢ (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ 𝑦) ↔ (∃𝑥 ∈ ω 𝐴 ≈ 𝑥 ∧ ∃𝑦 ∈ ω (𝐵 ∖ 𝐴) ≈ 𝑦))
3		isfi 7865	. . . . 5 ⊢ (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥)
4		isfi 7865	. . . . 5 ⊢ ((𝐵 ∖ 𝐴) ∈ Fin ↔ ∃𝑦 ∈ ω (𝐵 ∖ 𝐴) ≈ 𝑦)
5	3, 4	anbi12i 729	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ (𝐵 ∖ 𝐴) ∈ Fin) ↔ (∃𝑥 ∈ ω 𝐴 ≈ 𝑥 ∧ ∃𝑦 ∈ ω (𝐵 ∖ 𝐴) ≈ 𝑦))
6	2, 5	bitr4i 266	. . 3 ⊢ (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ 𝑦) ↔ (𝐴 ∈ Fin ∧ (𝐵 ∖ 𝐴) ∈ Fin))
7		nnacl 7578	. . . . 5 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝑥 +_𝑜 𝑦) ∈ ω)
8		unfilem3 8111	. . . . . . 7 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → 𝑦 ≈ ((𝑥 +_𝑜 𝑦) ∖ 𝑥))
9		entr 7894	. . . . . . . 8 ⊢ (((𝐵 ∖ 𝐴) ≈ 𝑦 ∧ 𝑦 ≈ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)) → (𝐵 ∖ 𝐴) ≈ ((𝑥 +_𝑜 𝑦) ∖ 𝑥))
10	9	expcom 450	. . . . . . 7 ⊢ (𝑦 ≈ ((𝑥 +_𝑜 𝑦) ∖ 𝑥) → ((𝐵 ∖ 𝐴) ≈ 𝑦 → (𝐵 ∖ 𝐴) ≈ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)))
11	8, 10	syl 17	. . . . . 6 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐵 ∖ 𝐴) ≈ 𝑦 → (𝐵 ∖ 𝐴) ≈ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)))
12		disjdif 3992	. . . . . . . 8 ⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅
13		disjdif 3992	. . . . . . . 8 ⊢ (𝑥 ∩ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)) = ∅
14		unen 7925	. . . . . . . 8 ⊢ (((𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)) ∧ ((𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅ ∧ (𝑥 ∩ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)) = ∅)) → (𝐴 ∪ (𝐵 ∖ 𝐴)) ≈ (𝑥 ∪ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)))
15	12, 13, 14	mpanr12 717	. . . . . . 7 ⊢ ((𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)) → (𝐴 ∪ (𝐵 ∖ 𝐴)) ≈ (𝑥 ∪ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)))
16		undif2 3996	. . . . . . . . 9 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)
17	16	a1i 11	. . . . . . . 8 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵))
18		nnaword1 7596	. . . . . . . . 9 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → 𝑥 ⊆ (𝑥 +_𝑜 𝑦))
19		undif 4001	. . . . . . . . 9 ⊢ (𝑥 ⊆ (𝑥 +_𝑜 𝑦) ↔ (𝑥 ∪ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)) = (𝑥 +_𝑜 𝑦))
20	18, 19	sylib 207	. . . . . . . 8 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝑥 ∪ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)) = (𝑥 +_𝑜 𝑦))
21	17, 20	breq12d 4596	. . . . . . 7 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ∪ (𝐵 ∖ 𝐴)) ≈ (𝑥 ∪ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)) ↔ (𝐴 ∪ 𝐵) ≈ (𝑥 +_𝑜 𝑦)))
22	15, 21	syl5ib 233	. . . . . 6 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ ((𝑥 +_𝑜 𝑦) ∖ 𝑥)) → (𝐴 ∪ 𝐵) ≈ (𝑥 +_𝑜 𝑦)))
23	11, 22	sylan2d 498	. . . . 5 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ 𝑦) → (𝐴 ∪ 𝐵) ≈ (𝑥 +_𝑜 𝑦)))
24		breq2 4587	. . . . . . 7 ⊢ (𝑧 = (𝑥 +_𝑜 𝑦) → ((𝐴 ∪ 𝐵) ≈ 𝑧 ↔ (𝐴 ∪ 𝐵) ≈ (𝑥 +_𝑜 𝑦)))
25	24	rspcev 3282	. . . . . 6 ⊢ (((𝑥 +_𝑜 𝑦) ∈ ω ∧ (𝐴 ∪ 𝐵) ≈ (𝑥 +_𝑜 𝑦)) → ∃𝑧 ∈ ω (𝐴 ∪ 𝐵) ≈ 𝑧)
26		isfi 7865	. . . . . 6 ⊢ ((𝐴 ∪ 𝐵) ∈ Fin ↔ ∃𝑧 ∈ ω (𝐴 ∪ 𝐵) ≈ 𝑧)
27	25, 26	sylibr 223	. . . . 5 ⊢ (((𝑥 +_𝑜 𝑦) ∈ ω ∧ (𝐴 ∪ 𝐵) ≈ (𝑥 +_𝑜 𝑦)) → (𝐴 ∪ 𝐵) ∈ Fin)
28	7, 23, 27	syl6an 566	. . . 4 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → ((𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ 𝑦) → (𝐴 ∪ 𝐵) ∈ Fin))
29	28	rexlimivv 3018	. . 3 ⊢ (∃𝑥 ∈ ω ∃𝑦 ∈ ω (𝐴 ≈ 𝑥 ∧ (𝐵 ∖ 𝐴) ≈ 𝑦) → (𝐴 ∪ 𝐵) ∈ Fin)
30	6, 29	sylbir 224	. 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 1475 ∈ wcel 1977 ∃wrex 2897 ∖ cdif 3537 ∪ cun 3538 ∩ cin 3539 ⊆ wss 3540 ∅c0 3874 class class class wbr 4583 (class class class)co 6549 ωcom 6957 +_𝑜 coa 7444 ≈ cen 7838 Fincfn 7841

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-ral 2901 df-rex 2902 df-reu 2903 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-oadd 7451 df-er 7629 df-en 7842 df-fin 7845

This theorem is referenced by: unfi2 8114 difinf 8115 xpfi 8116 prfi 8120 tpfi 8121 fnfi 8123 iunfi 8137 pwfilem 8143 fsuppun 8177 fsuppunfi 8178 ressuppfi 8184 fiin 8211 cantnfp1lem1 8458 ficardun2 8908 ackbij1lem6 8930 ackbij1lem16 8940 fin23lem28 9045 fin23lem30 9047 isfin1-3 9091 axcclem 9162 hashun 13032 hashunlei 13072 hashmap 13082 hashbclem 13093 hashf1lem1 13096 hashf1lem2 13097 hashf1 13098 fsummsnunz 14327 fsumsplitsnun 14328 incexclem 14407 isumltss 14419 fprodsplitsn 14559 lcmfunsnlem2lem1 15189 lcmfunsnlem2lem2 15190 lcmfunsnlem2 15191 lcmfun 15196 ramub1lem1 15568 fpwipodrs 16987 acsfiindd 17000 symgfisg 17711 gsumzunsnd 18178 gsumunsnfd 18179 psrbagaddcl 19191 mplsubg 19258 mpllss 19259 dsmmacl 19904 fctop 20618 uncmp 21016 bwth 21023 lfinun 21138 locfincmp 21139 comppfsc 21145 1stckgenlem 21166 ptbasin 21190 cfinfil 21507 fin1aufil 21546 alexsubALTlem3 21663 tmdgsum 21709 tsmsfbas 21741 tsmsgsum 21752 tsmsres 21757 tsmsxplem1 21766 prdsmet 21985 prdsbl 22106 icccmplem2 22434 rrxmval 22996 rrxmet 22999 rrxdstprj1 23000 ovolfiniun 23076 volfiniun 23122 fta1glem2 23730 fta1lem 23866 aannenlem2 23888 aalioulem2 23892 dchrfi 24780 usgrafilem2 25941 vdgrfiun 26429 konigsberg 26514 ffsrn 28892 eulerpartlemt 29760 ballotlemgun 29913 lindsenlbs 32574 poimirlem31 32610 poimirlem32 32611 itg2addnclem2 32632 ftc1anclem7 32661 ftc1anc 32663 prdsbnd 32762 pclfinN 34204 elrfi 36275 mzpcompact2lem 36332 eldioph2 36343 lsmfgcl 36662 fiuneneq 36794 fsumsplitsn 38637 dvmptfprodlem 38834 dvnprodlem2 38837 fourierdlem50 39049 fourierdlem51 39050 fourierdlem54 39053 fourierdlem76 39075 fourierdlem80 39079 fourierdlem102 39101 fourierdlem103 39102 fourierdlem104 39103 fourierdlem114 39113 sge0resplit 39299 sge0iunmptlemfi 39306 sge0xaddlem1 39326 hoiprodp1 39478 sge0hsphoire 39479 hoidmvlelem1 39485 hoidmvlelem2 39486 hoidmvlelem5 39489 hspmbllem2 39517 fsummmodsnunz 40374 usgrfilem 40546 mndpsuppfi 41950

W3C validator