Theorem unfi 9139

Description: The union of two finite sets is finite. Part of Corollary 6K of [Enderton] p. 144. (Contributed by NM, 16-Nov-2002.) Avoid ax-pow 5322. (Revised by BTernaryTau, 7-Aug-2024.)

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		uneq2 4115	. . . . 5 ⊢ (𝑥 = ∅ → (𝐴 ∪ 𝑥) = (𝐴 ∪ ∅))
2	1	eleq1d 2847	. . . 4 ⊢ (𝑥 = ∅ → ((𝐴 ∪ 𝑥) ∈ Fin ↔ (𝐴 ∪ ∅) ∈ Fin))
3	2	imbi2d 342	. . 3 ⊢ (𝑥 = ∅ → ((𝐴 ∈ Fin → (𝐴 ∪ 𝑥) ∈ Fin) ↔ (𝐴 ∈ Fin → (𝐴 ∪ ∅) ∈ Fin)))
4		uneq2 4115	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝐴 ∪ 𝑥) = (𝐴 ∪ 𝑦))
5	4	eleq1d 2847	. . . 4 ⊢ (𝑥 = 𝑦 → ((𝐴 ∪ 𝑥) ∈ Fin ↔ (𝐴 ∪ 𝑦) ∈ Fin))
6	5	imbi2d 342	. . 3 ⊢ (𝑥 = 𝑦 → ((𝐴 ∈ Fin → (𝐴 ∪ 𝑥) ∈ Fin) ↔ (𝐴 ∈ Fin → (𝐴 ∪ 𝑦) ∈ Fin)))
7		uneq2 4115	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝐴 ∪ 𝑥) = (𝐴 ∪ (𝑦 ∪ {𝑧})))
8	7	eleq1d 2847	. . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐴 ∪ 𝑥) ∈ Fin ↔ (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))
9	8	imbi2d 342	. . 3 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐴 ∈ Fin → (𝐴 ∪ 𝑥) ∈ Fin) ↔ (𝐴 ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)))
10		uneq2 4115	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴 ∪ 𝑥) = (𝐴 ∪ 𝐵))
11	10	eleq1d 2847	. . . 4 ⊢ (𝑥 = 𝐵 → ((𝐴 ∪ 𝑥) ∈ Fin ↔ (𝐴 ∪ 𝐵) ∈ Fin))
12	11	imbi2d 342	. . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ Fin → (𝐴 ∪ 𝑥) ∈ Fin) ↔ (𝐴 ∈ Fin → (𝐴 ∪ 𝐵) ∈ Fin)))
13		un0 4348	. . . . 5 ⊢ (𝐴 ∪ ∅) = 𝐴
14	13	eleq1i 2853	. . . 4 ⊢ ((𝐴 ∪ ∅) ∈ Fin ↔ 𝐴 ∈ Fin)
15	14	biimpri 230	. . 3 ⊢ (𝐴 ∈ Fin → (𝐴 ∪ ∅) ∈ Fin)
16		snssi 4744	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐴 → {𝑧} ⊆ 𝐴)
17		ssequn2 4141	. . . . . . . . . . . . . 14 ⊢ ({𝑧} ⊆ 𝐴 ↔ (𝐴 ∪ {𝑧}) = 𝐴)
18	17	biimpi 218	. . . . . . . . . . . . 13 ⊢ ({𝑧} ⊆ 𝐴 → (𝐴 ∪ {𝑧}) = 𝐴)
19	18	uneq2d 4121	. . . . . . . . . . . 12 ⊢ ({𝑧} ⊆ 𝐴 → (𝑦 ∪ (𝐴 ∪ {𝑧})) = (𝑦 ∪ 𝐴))
20		un12 4125	. . . . . . . . . . . 12 ⊢ (𝐴 ∪ (𝑦 ∪ {𝑧})) = (𝑦 ∪ (𝐴 ∪ {𝑧}))
21		uncom 4111	. . . . . . . . . . . 12 ⊢ (𝐴 ∪ 𝑦) = (𝑦 ∪ 𝐴)
22	19, 20, 21	3eqtr4g 2822	. . . . . . . . . . 11 ⊢ ({𝑧} ⊆ 𝐴 → (𝐴 ∪ (𝑦 ∪ {𝑧})) = (𝐴 ∪ 𝑦))
23	16, 22	syl 17	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝐴 → (𝐴 ∪ (𝑦 ∪ {𝑧})) = (𝐴 ∪ 𝑦))
24	23	eleq1d 2847	. . . . . . . . 9 ⊢ (𝑧 ∈ 𝐴 → ((𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin ↔ (𝐴 ∪ 𝑦) ∈ Fin))
25	24	biimprd 250	. . . . . . . 8 ⊢ (𝑧 ∈ 𝐴 → ((𝐴 ∪ 𝑦) ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))
26	25	adantld 494	. . . . . . 7 ⊢ (𝑧 ∈ 𝐴 → ((¬ 𝑧 ∈ 𝑦 ∧ (𝐴 ∪ 𝑦) ∈ Fin) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))
27		isfi 8956	. . . . . . . . . . 11 ⊢ ((𝐴 ∪ 𝑦) ∈ Fin ↔ ∃𝑤 ∈ ω (𝐴 ∪ 𝑦) ≈ 𝑤)
28	27	biimpi 218	. . . . . . . . . 10 ⊢ ((𝐴 ∪ 𝑦) ∈ Fin → ∃𝑤 ∈ ω (𝐴 ∪ 𝑦) ≈ 𝑤)
29		r19.41v 3192	. . . . . . . . . . 11 ⊢ (∃𝑤 ∈ ω ((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦)) ↔ (∃𝑤 ∈ ω (𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦)))
30		disjsn 4670	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∪ 𝑦) ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ (𝐴 ∪ 𝑦))
31		elun 4106	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ (𝐴 ∪ 𝑦) ↔ (𝑧 ∈ 𝐴 ∨ 𝑧 ∈ 𝑦))
32	31	notbii 322	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑧 ∈ (𝐴 ∪ 𝑦) ↔ ¬ (𝑧 ∈ 𝐴 ∨ 𝑧 ∈ 𝑦))
33		pm4.56 1002	. . . . . . . . . . . . . . . . . . 19 ⊢ ((¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦) ↔ ¬ (𝑧 ∈ 𝐴 ∨ 𝑧 ∈ 𝑦))
34	32, 33	bitr4i 280	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝑧 ∈ (𝐴 ∪ 𝑦) ↔ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦))
35	30, 34	sylbbr 238	. . . . . . . . . . . . . . . . 17 ⊢ ((¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦) → ((𝐴 ∪ 𝑦) ∩ {𝑧}) = ∅)
36		nnord 7854	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ ω → Ord 𝑤)
37		orddisj 6384	. . . . . . . . . . . . . . . . . . 19 ⊢ (Ord 𝑤 → (𝑤 ∩ {𝑤}) = ∅)
38	36, 37	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ω → (𝑤 ∩ {𝑤}) = ∅)
39		en2sn 9022	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ V ∧ 𝑤 ∈ V) → {𝑧} ≈ {𝑤})
40	39	el2v 3461	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑧} ≈ {𝑤}
41		unen 9026	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ {𝑧} ≈ {𝑤}) ∧ (((𝐴 ∪ 𝑦) ∩ {𝑧}) = ∅ ∧ (𝑤 ∩ {𝑤}) = ∅)) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
42	40, 41	mpanl2 711	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (((𝐴 ∪ 𝑦) ∩ {𝑧}) = ∅ ∧ (𝑤 ∩ {𝑤}) = ∅)) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
43	38, 42	sylanr2 693	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (((𝐴 ∪ 𝑦) ∩ {𝑧}) = ∅ ∧ 𝑤 ∈ ω)) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
44	35, 43	sylanr1 692	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ ((¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑤 ∈ ω)) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
45	44	3impb 1127	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑤 ∈ ω) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
46	45	3comr 1138	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∈ ω ∧ (𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦)) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
47	46	3expb 1133	. . . . . . . . . . . . 13 ⊢ ((𝑤 ∈ ω ∧ ((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦))) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
48		unass 4124	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∪ 𝑦) ∪ {𝑧}) = (𝐴 ∪ (𝑦 ∪ {𝑧}))
49		df-suc 6352	. . . . . . . . . . . . . . . . 17 ⊢ suc 𝑤 = (𝑤 ∪ {𝑤})
50		peano2 7870	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ω → suc 𝑤 ∈ ω)
51	49, 50	eqeltrrid 2867	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ ω → (𝑤 ∪ {𝑤}) ∈ ω)
52		breq2 5104	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = (𝑤 ∪ {𝑤}) → (((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ 𝑣 ↔ ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})))
53	52	rspcev 3581	. . . . . . . . . . . . . . . 16 ⊢ (((𝑤 ∪ {𝑤}) ∈ ω ∧ ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) → ∃𝑣 ∈ ω ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ 𝑣)
54	51, 53	sylan 589	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ ω ∧ ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) → ∃𝑣 ∈ ω ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ 𝑣)
55		isfi 8956	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∪ 𝑦) ∪ {𝑧}) ∈ Fin ↔ ∃𝑣 ∈ ω ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ 𝑣)
56	54, 55	sylibr 236	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∈ ω ∧ ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ∈ Fin)
57	48, 56	eqeltrrid 2867	. . . . . . . . . . . . 13 ⊢ ((𝑤 ∈ ω ∧ ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
58	47, 57	syldan 600	. . . . . . . . . . . 12 ⊢ ((𝑤 ∈ ω ∧ ((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦))) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
59	58	rexlimiva 3155	. . . . . . . . . . 11 ⊢ (∃𝑤 ∈ ω ((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
60	29, 59	sylbir 237	. . . . . . . . . 10 ⊢ ((∃𝑤 ∈ ω (𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
61	28, 60	sylan 589	. . . . . . . . 9 ⊢ (((𝐴 ∪ 𝑦) ∈ Fin ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
62	61	ancoms 462	. . . . . . . 8 ⊢ (((¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐴 ∪ 𝑦) ∈ Fin) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
63	62	expl 461	. . . . . . 7 ⊢ (¬ 𝑧 ∈ 𝐴 → ((¬ 𝑧 ∈ 𝑦 ∧ (𝐴 ∪ 𝑦) ∈ Fin) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))
64	26, 63	pm2.61i 183	. . . . . 6 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝐴 ∪ 𝑦) ∈ Fin) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
65	64	ex 416	. . . . 5 ⊢ (¬ 𝑧 ∈ 𝑦 → ((𝐴 ∪ 𝑦) ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))
66	65	imim2d 57	. . . 4 ⊢ (¬ 𝑧 ∈ 𝑦 → ((𝐴 ∈ Fin → (𝐴 ∪ 𝑦) ∈ Fin) → (𝐴 ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)))
67	66	adantl 485	. . 3 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((𝐴 ∈ Fin → (𝐴 ∪ 𝑦) ∈ Fin) → (𝐴 ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)))
68	3, 6, 9, 12, 15, 67	findcard2s 9134	. 2 ⊢ (𝐵 ∈ Fin → (𝐴 ∈ Fin → (𝐴 ∪ 𝐵) ∈ Fin))
69	68	impcom 411	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∨ wo 858   = wceq 1560   ∈ wcel 2142  ∃wrex 3086  Vcvv 3454   ∪ cun 3902   ∩ cin 3903   ⊆ wss 3904  ∅c0 4285  {csn 4582   class class class wbr 5100  Ord word 6345  suc csuc 6348  ωcom 7846   ≈ cen 8924  Fincfn 8927

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pr 5390  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-tr 5208  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-om 7847  df-en 8928  df-fin 8931

This theorem is referenced by:  unfid  9140  ssfi  9141  cnvfi  9144  fnfi  9146  unfib  9253  unfi2  9254  difinf  9255  imafiOLD  9260  pwfilem  9262  xpfi  9264  prfiALT  9269  tpfi  9270  fodomfir  9272  iunfi  9286  fsuppun  9333  fsuppunfi  9334  ressuppfi  9341  fiin  9368  cantnfp1lem1  9633  ficardadju  10156  ficardun2  10158  ackbij1lem6  10180  ackbij1lem16  10190  fin23lem28  10297  fin23lem30  10299  isfin1-3  10343  axcclem  10414  hashun  14395  hashunlei  14438  hashmap  14448  hashbclem  14465  hashf1lem2  14469  hashf1  14470  hash7g  14499  s7f1o  14979  fsumsplitsn  15771  fsummsnunz  15781  fsumsplitsnun  15782  incexclem  15866  isumltss  15878  fprodsplitsn  16019  lcmfunsnlem2lem1  16672  lcmfunsnlem2lem2  16673  lcmfunsnlem2  16674  lcmfun  16679  ramub1lem1  17062  fpwipodrs  18572  acsfiindd  18585  mndpsuppfi  18800  symgfisg  19508  gsumzunsnd  19996  gsumunsnfd  19997  dsmmacl  21790  mplsubg  22050  mpllss  22051  fctop  23061  uncmp  23460  bwth  23467  lfinun  23582  locfincmp  23583  comppfsc  23589  1stckgenlem  23610  ptbasin  23634  cfinfil  23950  fin1aufil  23989  alexsubALTlem3  24106  tmdgsum  24152  tsmsfbas  24185  tsmsgsum  24196  tsmsres  24201  tsmsxplem1  24210  prdsmet  24427  prdsbl  24548  icccmplem2  24881  rrxmval  25464  rrxmet  25467  rrxdstprj1  25468  ovolfiniun  25560  volfiniun  25606  fta1glem2  26226  fta1lem  26368  aannenlem2  26390  aalioulem2  26394  dchrfi  27316  usgrfilem  29525  ffsrn  32927  eulerpartlemt  34665  ballotlemgun  34819  hgt750lemb  34947  hgt750leme  34949  lindsenlbs  38111  poimirlem31  38147  poimirlem32  38148  itg2addnclem2  38168  ftc1anclem7  38195  ftc1anc  38197  prdsbnd  38289  pclfinN  40521  elrfi  43272  mzpcompact2lem  43329  eldioph2  43340  lsmfgcl  43648  fiuneneq  43766  dvmptfprodlem  46515  dvnprodlem2  46518  fourierdlem50  46727  fourierdlem51  46728  fourierdlem54  46731  fourierdlem76  46753  fourierdlem80  46757  fourierdlem102  46779  fourierdlem103  46780  fourierdlem104  46781  fourierdlem114  46791  sge0resplit  46977  sge0iunmptlemfi  46984  sge0xaddlem1  47004  hoiprodp1  47159  sge0hsphoire  47160  hoidmvlelem1  47166  hoidmvlelem2  47167  hoidmvlelem5  47170  hspmbllem2  47198  fsummmodsnunz  47974