Theorem unfi 9211

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 5365. (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 4162	. . . . 5 ⊢ (𝑥 = ∅ → (𝐴 ∪ 𝑥) = (𝐴 ∪ ∅))
2	1	eleq1d 2826	. . . 4 ⊢ (𝑥 = ∅ → ((𝐴 ∪ 𝑥) ∈ Fin ↔ (𝐴 ∪ ∅) ∈ Fin))
3	2	imbi2d 340	. . 3 ⊢ (𝑥 = ∅ → ((𝐴 ∈ Fin → (𝐴 ∪ 𝑥) ∈ Fin) ↔ (𝐴 ∈ Fin → (𝐴 ∪ ∅) ∈ Fin)))
4		uneq2 4162	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝐴 ∪ 𝑥) = (𝐴 ∪ 𝑦))
5	4	eleq1d 2826	. . . 4 ⊢ (𝑥 = 𝑦 → ((𝐴 ∪ 𝑥) ∈ Fin ↔ (𝐴 ∪ 𝑦) ∈ Fin))
6	5	imbi2d 340	. . 3 ⊢ (𝑥 = 𝑦 → ((𝐴 ∈ Fin → (𝐴 ∪ 𝑥) ∈ Fin) ↔ (𝐴 ∈ Fin → (𝐴 ∪ 𝑦) ∈ Fin)))
7		uneq2 4162	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝐴 ∪ 𝑥) = (𝐴 ∪ (𝑦 ∪ {𝑧})))
8	7	eleq1d 2826	. . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐴 ∪ 𝑥) ∈ Fin ↔ (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))
9	8	imbi2d 340	. . 3 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐴 ∈ Fin → (𝐴 ∪ 𝑥) ∈ Fin) ↔ (𝐴 ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)))
10		uneq2 4162	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴 ∪ 𝑥) = (𝐴 ∪ 𝐵))
11	10	eleq1d 2826	. . . 4 ⊢ (𝑥 = 𝐵 → ((𝐴 ∪ 𝑥) ∈ Fin ↔ (𝐴 ∪ 𝐵) ∈ Fin))
12	11	imbi2d 340	. . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ Fin → (𝐴 ∪ 𝑥) ∈ Fin) ↔ (𝐴 ∈ Fin → (𝐴 ∪ 𝐵) ∈ Fin)))
13		un0 4394	. . . . 5 ⊢ (𝐴 ∪ ∅) = 𝐴
14	13	eleq1i 2832	. . . 4 ⊢ ((𝐴 ∪ ∅) ∈ Fin ↔ 𝐴 ∈ Fin)
15	14	biimpri 228	. . 3 ⊢ (𝐴 ∈ Fin → (𝐴 ∪ ∅) ∈ Fin)
16		snssi 4808	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐴 → {𝑧} ⊆ 𝐴)
17		ssequn2 4189	. . . . . . . . . . . . . 14 ⊢ ({𝑧} ⊆ 𝐴 ↔ (𝐴 ∪ {𝑧}) = 𝐴)
18	17	biimpi 216	. . . . . . . . . . . . 13 ⊢ ({𝑧} ⊆ 𝐴 → (𝐴 ∪ {𝑧}) = 𝐴)
19	18	uneq2d 4168	. . . . . . . . . . . 12 ⊢ ({𝑧} ⊆ 𝐴 → (𝑦 ∪ (𝐴 ∪ {𝑧})) = (𝑦 ∪ 𝐴))
20		un12 4173	. . . . . . . . . . . 12 ⊢ (𝐴 ∪ (𝑦 ∪ {𝑧})) = (𝑦 ∪ (𝐴 ∪ {𝑧}))
21		uncom 4158	. . . . . . . . . . . 12 ⊢ (𝐴 ∪ 𝑦) = (𝑦 ∪ 𝐴)
22	19, 20, 21	3eqtr4g 2802	. . . . . . . . . . 11 ⊢ ({𝑧} ⊆ 𝐴 → (𝐴 ∪ (𝑦 ∪ {𝑧})) = (𝐴 ∪ 𝑦))
23	16, 22	syl 17	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝐴 → (𝐴 ∪ (𝑦 ∪ {𝑧})) = (𝐴 ∪ 𝑦))
24	23	eleq1d 2826	. . . . . . . . 9 ⊢ (𝑧 ∈ 𝐴 → ((𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin ↔ (𝐴 ∪ 𝑦) ∈ Fin))
25	24	biimprd 248	. . . . . . . 8 ⊢ (𝑧 ∈ 𝐴 → ((𝐴 ∪ 𝑦) ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))
26	25	adantld 490	. . . . . . 7 ⊢ (𝑧 ∈ 𝐴 → ((¬ 𝑧 ∈ 𝑦 ∧ (𝐴 ∪ 𝑦) ∈ Fin) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))
27		isfi 9016	. . . . . . . . . . 11 ⊢ ((𝐴 ∪ 𝑦) ∈ Fin ↔ ∃𝑤 ∈ ω (𝐴 ∪ 𝑦) ≈ 𝑤)
28	27	biimpi 216	. . . . . . . . . 10 ⊢ ((𝐴 ∪ 𝑦) ∈ Fin → ∃𝑤 ∈ ω (𝐴 ∪ 𝑦) ≈ 𝑤)
29		r19.41v 3189	. . . . . . . . . . 11 ⊢ (∃𝑤 ∈ ω ((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦)) ↔ (∃𝑤 ∈ ω (𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦)))
30		disjsn 4711	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∪ 𝑦) ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ (𝐴 ∪ 𝑦))
31		elun 4153	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ (𝐴 ∪ 𝑦) ↔ (𝑧 ∈ 𝐴 ∨ 𝑧 ∈ 𝑦))
32	31	notbii 320	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑧 ∈ (𝐴 ∪ 𝑦) ↔ ¬ (𝑧 ∈ 𝐴 ∨ 𝑧 ∈ 𝑦))
33		pm4.56 991	. . . . . . . . . . . . . . . . . . 19 ⊢ ((¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦) ↔ ¬ (𝑧 ∈ 𝐴 ∨ 𝑧 ∈ 𝑦))
34	32, 33	bitr4i 278	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝑧 ∈ (𝐴 ∪ 𝑦) ↔ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦))
35	30, 34	sylbbr 236	. . . . . . . . . . . . . . . . 17 ⊢ ((¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦) → ((𝐴 ∪ 𝑦) ∩ {𝑧}) = ∅)
36		nnord 7895	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ ω → Ord 𝑤)
37		orddisj 6422	. . . . . . . . . . . . . . . . . . 19 ⊢ (Ord 𝑤 → (𝑤 ∩ {𝑤}) = ∅)
38	36, 37	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ω → (𝑤 ∩ {𝑤}) = ∅)
39		en2sn 9081	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ V ∧ 𝑤 ∈ V) → {𝑧} ≈ {𝑤})
40	39	el2v 3487	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑧} ≈ {𝑤}
41		unen 9086	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ {𝑧} ≈ {𝑤}) ∧ (((𝐴 ∪ 𝑦) ∩ {𝑧}) = ∅ ∧ (𝑤 ∩ {𝑤}) = ∅)) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
42	40, 41	mpanl2 701	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (((𝐴 ∪ 𝑦) ∩ {𝑧}) = ∅ ∧ (𝑤 ∩ {𝑤}) = ∅)) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
43	38, 42	sylanr2 683	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (((𝐴 ∪ 𝑦) ∩ {𝑧}) = ∅ ∧ 𝑤 ∈ ω)) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
44	35, 43	sylanr1 682	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ ((¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑤 ∈ ω)) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
45	44	3impb 1115	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑤 ∈ ω) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
46	45	3comr 1126	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∈ ω ∧ (𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦)) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
47	46	3expb 1121	. . . . . . . . . . . . 13 ⊢ ((𝑤 ∈ ω ∧ ((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦))) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
48		unass 4172	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∪ 𝑦) ∪ {𝑧}) = (𝐴 ∪ (𝑦 ∪ {𝑧}))
49		df-suc 6390	. . . . . . . . . . . . . . . . 17 ⊢ suc 𝑤 = (𝑤 ∪ {𝑤})
50		peano2 7912	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ω → suc 𝑤 ∈ ω)
51	49, 50	eqeltrrid 2846	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ ω → (𝑤 ∪ {𝑤}) ∈ ω)
52		breq2 5147	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = (𝑤 ∪ {𝑤}) → (((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ 𝑣 ↔ ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})))
53	52	rspcev 3622	. . . . . . . . . . . . . . . 16 ⊢ (((𝑤 ∪ {𝑤}) ∈ ω ∧ ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) → ∃𝑣 ∈ ω ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ 𝑣)
54	51, 53	sylan 580	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ ω ∧ ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) → ∃𝑣 ∈ ω ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ 𝑣)
55		isfi 9016	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∪ 𝑦) ∪ {𝑧}) ∈ Fin ↔ ∃𝑣 ∈ ω ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ 𝑣)
56	54, 55	sylibr 234	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∈ ω ∧ ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ∈ Fin)
57	48, 56	eqeltrrid 2846	. . . . . . . . . . . . 13 ⊢ ((𝑤 ∈ ω ∧ ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
58	47, 57	syldan 591	. . . . . . . . . . . 12 ⊢ ((𝑤 ∈ ω ∧ ((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦))) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
59	58	rexlimiva 3147	. . . . . . . . . . 11 ⊢ (∃𝑤 ∈ ω ((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
60	29, 59	sylbir 235	. . . . . . . . . 10 ⊢ ((∃𝑤 ∈ ω (𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
61	28, 60	sylan 580	. . . . . . . . 9 ⊢ (((𝐴 ∪ 𝑦) ∈ Fin ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
62	61	ancoms 458	. . . . . . . 8 ⊢ (((¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐴 ∪ 𝑦) ∈ Fin) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
63	62	expl 457	. . . . . . 7 ⊢ (¬ 𝑧 ∈ 𝐴 → ((¬ 𝑧 ∈ 𝑦 ∧ (𝐴 ∪ 𝑦) ∈ Fin) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))
64	26, 63	pm2.61i 182	. . . . . 6 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝐴 ∪ 𝑦) ∈ Fin) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
65	64	ex 412	. . . . 5 ⊢ (¬ 𝑧 ∈ 𝑦 → ((𝐴 ∪ 𝑦) ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))
66	65	imim2d 57	. . . 4 ⊢ (¬ 𝑧 ∈ 𝑦 → ((𝐴 ∈ Fin → (𝐴 ∪ 𝑦) ∈ Fin) → (𝐴 ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)))
67	66	adantl 481	. . 3 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((𝐴 ∈ Fin → (𝐴 ∪ 𝑦) ∈ Fin) → (𝐴 ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)))
68	3, 6, 9, 12, 15, 67	findcard2s 9205	. 2 ⊢ (𝐵 ∈ Fin → (𝐴 ∈ Fin → (𝐴 ∪ 𝐵) ∈ Fin))
69	68	impcom 407	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 848   = wceq 1540   ∈ wcel 2108  ∃wrex 3070  Vcvv 3480   ∪ cun 3949   ∩ cin 3950   ⊆ wss 3951  ∅c0 4333  {csn 4626   class class class wbr 5143  Ord word 6383  suc csuc 6386  ωcom 7887   ≈ cen 8982  Fincfn 8985

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-om 7888  df-en 8986  df-fin 8989

This theorem is referenced by:  unfid  9212  ssfi  9213  cnvfi  9216  fnfi  9218  unfib  9347  unfi2  9348  difinf  9349  imafiOLD  9354  pwfilem  9356  xpfi  9358  xpfiOLD  9359  prfiALT  9364  tpfi  9365  fodomfir  9368  iunfi  9383  fsuppun  9427  fsuppunfi  9428  ressuppfi  9435  fiin  9462  cantnfp1lem1  9718  ficardadju  10240  ficardun2  10242  ackbij1lem6  10264  ackbij1lem16  10274  fin23lem28  10380  fin23lem30  10382  isfin1-3  10426  axcclem  10497  hashun  14421  hashunlei  14464  hashmap  14474  hashbclem  14491  hashf1lem2  14495  hashf1  14496  hash7g  14525  s7f1o  15005  fsumsplitsn  15780  fsummsnunz  15790  fsumsplitsnun  15791  incexclem  15872  isumltss  15884  fprodsplitsn  16025  lcmfunsnlem2lem1  16675  lcmfunsnlem2lem2  16676  lcmfunsnlem2  16677  lcmfun  16682  ramub1lem1  17064  fpwipodrs  18585  acsfiindd  18598  mndpsuppfi  18779  symgfisg  19486  gsumzunsnd  19974  gsumunsnfd  19975  dsmmacl  21761  mplsubg  22022  mpllss  22023  fctop  23011  uncmp  23411  bwth  23418  lfinun  23533  locfincmp  23534  comppfsc  23540  1stckgenlem  23561  ptbasin  23585  cfinfil  23901  fin1aufil  23940  alexsubALTlem3  24057  tmdgsum  24103  tsmsfbas  24136  tsmsgsum  24147  tsmsres  24152  tsmsxplem1  24161  prdsmet  24380  prdsbl  24504  icccmplem2  24845  rrxmval  25439  rrxmet  25442  rrxdstprj1  25443  ovolfiniun  25536  volfiniun  25582  fta1glem2  26208  fta1lem  26349  aannenlem2  26371  aalioulem2  26375  dchrfi  27299  usgrfilem  29344  ffsrn  32740  eulerpartlemt  34373  ballotlemgun  34527  hgt750lemb  34671  hgt750leme  34673  lindsenlbs  37622  poimirlem31  37658  poimirlem32  37659  itg2addnclem2  37679  ftc1anclem7  37706  ftc1anc  37708  prdsbnd  37800  pclfinN  39902  elrfi  42705  mzpcompact2lem  42762  eldioph2  42773  lsmfgcl  43086  fiuneneq  43204  dvmptfprodlem  45959  dvnprodlem2  45962  fourierdlem50  46171  fourierdlem51  46172  fourierdlem54  46175  fourierdlem76  46197  fourierdlem80  46201  fourierdlem102  46223  fourierdlem103  46224  fourierdlem104  46225  fourierdlem114  46235  sge0resplit  46421  sge0iunmptlemfi  46428  sge0xaddlem1  46448  hoiprodp1  46603  sge0hsphoire  46604  hoidmvlelem1  46610  hoidmvlelem2  46611  hoidmvlelem5  46614  hspmbllem2  46642  fsummmodsnunz  47362