Theorem unfi 9224

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 5334. (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 4164	. . . . 5 ⊢ (𝑥 = ∅ → (𝐴 ∪ 𝑥) = (𝐴 ∪ ∅))
2	1	eleq1d 2849	. . . 4 ⊢ (𝑥 = ∅ → ((𝐴 ∪ 𝑥) ∈ Fin ↔ (𝐴 ∪ ∅) ∈ Fin))
3	2	imbi2d 343	. . 3 ⊢ (𝑥 = ∅ → ((𝐴 ∈ Fin → (𝐴 ∪ 𝑥) ∈ Fin) ↔ (𝐴 ∈ Fin → (𝐴 ∪ ∅) ∈ Fin)))
4		uneq2 4164	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝐴 ∪ 𝑥) = (𝐴 ∪ 𝑦))
5	4	eleq1d 2849	. . . 4 ⊢ (𝑥 = 𝑦 → ((𝐴 ∪ 𝑥) ∈ Fin ↔ (𝐴 ∪ 𝑦) ∈ Fin))
6	5	imbi2d 343	. . 3 ⊢ (𝑥 = 𝑦 → ((𝐴 ∈ Fin → (𝐴 ∪ 𝑥) ∈ Fin) ↔ (𝐴 ∈ Fin → (𝐴 ∪ 𝑦) ∈ Fin)))
7		uneq2 4164	. . . . 5 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝐴 ∪ 𝑥) = (𝐴 ∪ (𝑦 ∪ {𝑧})))
8	7	eleq1d 2849	. . . 4 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐴 ∪ 𝑥) ∈ Fin ↔ (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))
9	8	imbi2d 343	. . 3 ⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐴 ∈ Fin → (𝐴 ∪ 𝑥) ∈ Fin) ↔ (𝐴 ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)))
10		uneq2 4164	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝐴 ∪ 𝑥) = (𝐴 ∪ 𝐵))
11	10	eleq1d 2849	. . . 4 ⊢ (𝑥 = 𝐵 → ((𝐴 ∪ 𝑥) ∈ Fin ↔ (𝐴 ∪ 𝐵) ∈ Fin))
12	11	imbi2d 343	. . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ∈ Fin → (𝐴 ∪ 𝑥) ∈ Fin) ↔ (𝐴 ∈ Fin → (𝐴 ∪ 𝐵) ∈ Fin)))
13		un0 4347	. . . . 5 ⊢ (𝐴 ∪ ∅) = 𝐴
14	13	eleq1i 2855	. . . 4 ⊢ ((𝐴 ∪ ∅) ∈ Fin ↔ 𝐴 ∈ Fin)
15	14	biimpri 231	. . 3 ⊢ (𝐴 ∈ Fin → (𝐴 ∪ ∅) ∈ Fin)
16		snssi 4748	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝐴 → {𝑧} ⊆ 𝐴)
17		ssequn2 4190	. . . . . . . . . . . . . 14 ⊢ ({𝑧} ⊆ 𝐴 ↔ (𝐴 ∪ {𝑧}) = 𝐴)
18	17	biimpi 219	. . . . . . . . . . . . 13 ⊢ ({𝑧} ⊆ 𝐴 → (𝐴 ∪ {𝑧}) = 𝐴)
19	18	uneq2d 4170	. . . . . . . . . . . 12 ⊢ ({𝑧} ⊆ 𝐴 → (𝑦 ∪ (𝐴 ∪ {𝑧})) = (𝑦 ∪ 𝐴))
20		un12 4174	. . . . . . . . . . . 12 ⊢ (𝐴 ∪ (𝑦 ∪ {𝑧})) = (𝑦 ∪ (𝐴 ∪ {𝑧}))
21		uncom 4160	. . . . . . . . . . . 12 ⊢ (𝐴 ∪ 𝑦) = (𝑦 ∪ 𝐴)
22	19, 20, 21	3eqtr4g 2823	. . . . . . . . . . 11 ⊢ ({𝑧} ⊆ 𝐴 → (𝐴 ∪ (𝑦 ∪ {𝑧})) = (𝐴 ∪ 𝑦))
23	16, 22	syl 18	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝐴 → (𝐴 ∪ (𝑦 ∪ {𝑧})) = (𝐴 ∪ 𝑦))
24	23	eleq1d 2849	. . . . . . . . 9 ⊢ (𝑧 ∈ 𝐴 → ((𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin ↔ (𝐴 ∪ 𝑦) ∈ Fin))
25	24	biimprd 251	. . . . . . . 8 ⊢ (𝑧 ∈ 𝐴 → ((𝐴 ∪ 𝑦) ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))
26	25	adantld 496	. . . . . . 7 ⊢ (𝑧 ∈ 𝐴 → ((¬ 𝑧 ∈ 𝑦 ∧ (𝐴 ∪ 𝑦) ∈ Fin) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))
27		isfi 9040	. . . . . . . . . . 11 ⊢ ((𝐴 ∪ 𝑦) ∈ Fin ↔ ∃𝑤 ∈ ω (𝐴 ∪ 𝑦) ≈ 𝑤)
28	27	biimpi 219	. . . . . . . . . 10 ⊢ ((𝐴 ∪ 𝑦) ∈ Fin → ∃𝑤 ∈ ω (𝐴 ∪ 𝑦) ≈ 𝑤)
29		r19.41v 3196	. . . . . . . . . . 11 ⊢ (∃𝑤 ∈ ω ((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦)) ↔ (∃𝑤 ∈ ω (𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦)))
30		disjsn 4673	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∪ 𝑦) ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ (𝐴 ∪ 𝑦))
31		elun 4155	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ (𝐴 ∪ 𝑦) ↔ (𝑧 ∈ 𝐴 ∨ 𝑧 ∈ 𝑦))
32	31	notbii 323	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑧 ∈ (𝐴 ∪ 𝑦) ↔ ¬ (𝑧 ∈ 𝐴 ∨ 𝑧 ∈ 𝑦))
33		pm4.56 1004	. . . . . . . . . . . . . . . . . . 19 ⊢ ((¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦) ↔ ¬ (𝑧 ∈ 𝐴 ∨ 𝑧 ∈ 𝑦))
34	32, 33	bitr4i 281	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ 𝑧 ∈ (𝐴 ∪ 𝑦) ↔ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦))
35	30, 34	sylbbr 239	. . . . . . . . . . . . . . . . 17 ⊢ ((¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦) → ((𝐴 ∪ 𝑦) ∩ {𝑧}) = ∅)
36		nnord 7919	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ ω → Ord 𝑤)
37		orddisj 6427	. . . . . . . . . . . . . . . . . . 19 ⊢ (Ord 𝑤 → (𝑤 ∩ {𝑤}) = ∅)
38	36, 37	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ ω → (𝑤 ∩ {𝑤}) = ∅)
39		en2sn 9107	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ V ∧ 𝑤 ∈ V) → {𝑧} ≈ {𝑤})
40	39	el2v 3461	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑧} ≈ {𝑤}
41		unen 9111	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ {𝑧} ≈ {𝑤}) ∧ (((𝐴 ∪ 𝑦) ∩ {𝑧}) = ∅ ∧ (𝑤 ∩ {𝑤}) = ∅)) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
42	40, 41	mpanl2 714	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (((𝐴 ∪ 𝑦) ∩ {𝑧}) = ∅ ∧ (𝑤 ∩ {𝑤}) = ∅)) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
43	38, 42	sylanr2 696	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (((𝐴 ∪ 𝑦) ∩ {𝑧}) = ∅ ∧ 𝑤 ∈ ω)) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
44	35, 43	sylanr1 695	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ ((¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑤 ∈ ω)) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
45	44	3impb 1132	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦) ∧ 𝑤 ∈ ω) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
46	45	3comr 1143	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∈ ω ∧ (𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦)) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
47	46	3expb 1138	. . . . . . . . . . . . 13 ⊢ ((𝑤 ∈ ω ∧ ((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦))) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤}))
48		unass 4173	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∪ 𝑦) ∪ {𝑧}) = (𝐴 ∪ (𝑦 ∪ {𝑧}))
49		df-suc 6394	. . . . . . . . . . . . . . . . 17 ⊢ suc 𝑤 = (𝑤 ∪ {𝑤})
50		peano2 7935	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ ω → suc 𝑤 ∈ ω)
51	49, 50	eqeltrrid 2869	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ ω → (𝑤 ∪ {𝑤}) ∈ ω)
52		breq2 5112	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = (𝑤 ∪ {𝑤}) → (((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ 𝑣 ↔ ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})))
53	52	rspcev 3580	. . . . . . . . . . . . . . . 16 ⊢ (((𝑤 ∪ {𝑤}) ∈ ω ∧ ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) → ∃𝑣 ∈ ω ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ 𝑣)
54	51, 53	sylan 592	. . . . . . . . . . . . . . 15 ⊢ ((𝑤 ∈ ω ∧ ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) → ∃𝑣 ∈ ω ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ 𝑣)
55		isfi 9040	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∪ 𝑦) ∪ {𝑧}) ∈ Fin ↔ ∃𝑣 ∈ ω ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ 𝑣)
56	54, 55	sylibr 237	. . . . . . . . . . . . . 14 ⊢ ((𝑤 ∈ ω ∧ ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) → ((𝐴 ∪ 𝑦) ∪ {𝑧}) ∈ Fin)
57	48, 56	eqeltrrid 2869	. . . . . . . . . . . . 13 ⊢ ((𝑤 ∈ ω ∧ ((𝐴 ∪ 𝑦) ∪ {𝑧}) ≈ (𝑤 ∪ {𝑤})) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
58	47, 57	syldan 603	. . . . . . . . . . . 12 ⊢ ((𝑤 ∈ ω ∧ ((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦))) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
59	58	rexlimiva 3159	. . . . . . . . . . 11 ⊢ (∃𝑤 ∈ ω ((𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
60	29, 59	sylbir 238	. . . . . . . . . 10 ⊢ ((∃𝑤 ∈ ω (𝐴 ∪ 𝑦) ≈ 𝑤 ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
61	28, 60	sylan 592	. . . . . . . . 9 ⊢ (((𝐴 ∪ 𝑦) ∈ Fin ∧ (¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦)) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
62	61	ancoms 464	. . . . . . . 8 ⊢ (((¬ 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝐴 ∪ 𝑦) ∈ Fin) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
63	62	expl 463	. . . . . . 7 ⊢ (¬ 𝑧 ∈ 𝐴 → ((¬ 𝑧 ∈ 𝑦 ∧ (𝐴 ∪ 𝑦) ∈ Fin) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))
64	26, 63	pm2.61i 184	. . . . . 6 ⊢ ((¬ 𝑧 ∈ 𝑦 ∧ (𝐴 ∪ 𝑦) ∈ Fin) → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)
65	64	ex 418	. . . . 5 ⊢ (¬ 𝑧 ∈ 𝑦 → ((𝐴 ∪ 𝑦) ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin))
66	65	imim2d 58	. . . 4 ⊢ (¬ 𝑧 ∈ 𝑦 → ((𝐴 ∈ Fin → (𝐴 ∪ 𝑦) ∈ Fin) → (𝐴 ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)))
67	66	adantl 487	. . 3 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((𝐴 ∈ Fin → (𝐴 ∪ 𝑦) ∈ Fin) → (𝐴 ∈ Fin → (𝐴 ∪ (𝑦 ∪ {𝑧})) ∈ Fin)))
68	3, 6, 9, 12, 15, 67	findcard2s 9219	. 2 ⊢ (𝐵 ∈ Fin → (𝐴 ∈ Fin → (𝐴 ∪ 𝐵) ∈ Fin))
69	68	impcom 413	1 ⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (𝐴 ∪ 𝐵) ∈ Fin)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2147  ∃wrex 3090  Vcvv 3454   ⊆ wss 3900   ∩ cin 4092   ∪ cun 4152  ∅c0 4281  {csn 4588   class class class wbr 5108  Ord word 6387  suc csuc 6390  ωcom 7911   ≈ cen 9008  Fincfn 9011

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398  ax-un 7783

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-om 7912  df-en 9012  df-fin 9015

This theorem is used by:  unfid  9225  ssfi  9226  cnvfi  9229  fnfi  9231  unfib  9339  unfi2  9340  difinf  9341  pwfilem  9347  xpfi  9349  prfiALT  9354  tpfi  9355  fodomfir  9357  iunfi  9370  fsuppun  9416  fsuppunfi  9417  ressuppfi  9424  fiin  9451  cantnfp1lem1  9716  hfun  9955  ficardadju  10317  ficardun2  10319  ackbij1lem6  10341  ackbij1lem16  10351  fin23lem28  10457  fin23lem30  10459  isfin1-3  10503  axcclem  10574  hashun  14567  hashunlei  14611  hashmap  14621  hashbclem  14638  hashf1lem2  14642  hashf1  14643  hash7g  14672  s7f1o  15162  fsumsplitsn  15954  fsummsnunz  15964  fsumsplitsnun  15965  incexclem  16049  isumltss  16061  fprodsplitsn  16200  lcmfunsnlem2lem1  16857  lcmfunsnlem2lem2  16858  lcmfunsnlem2  16859  lcmfun  16864  ramub1lem1  17248  fpwipodrs  18764  acsfiindd  18777  mndpsuppfi  19010  symgfisg  19733  gsumzunsnd  20221  gsumunsnfd  20222  dsmmacl  22102  lindsenlbs  22212  mplsubg  22364  mpllss  22365  fctop  23377  uncmp  23776  bwth  23783  lfinun  23899  locfincmp  23900  comppfsc  23906  1stckgenlem  23927  ptbasin  23951  cfinfil  24267  fin1aufil  24306  alexsubALTlem3  24423  tmdgsum  24469  tsmsfbas  24502  tsmsgsum  24513  tsmsres  24518  tsmsxplem1  24527  prdsmet  24744  prdsbl  24865  icccmplem2  25198  rrxmval  25781  rrxmet  25784  rrxdstprj1  25785  ovolfiniun  25877  volfiniun  25923  fta1glem2  26542  fta1lem  26683  aannenlem2  26713  aalioulem2  26717  dchrfi  27639  usgrfilem  29965  ffsrn  33416  eulerpartlemt  35114  ballotlemgun  35268  hgt750lemb  35396  hgt750leme  35398  poimirlem31  38837  poimirlem32  38838  itg2addnclem2  38858  ftc1anclem7  38885  ftc1anc  38887  prdsbnd  38993  pclfinN  41223  elrfi  43971  mzpcompact2lem  44028  eldioph2  44039  lsmfgcl  44342  fiuneneq  44455  dvmptfprodlem  47227  dvnprodlem2  47230  fourierdlem50  47439  fourierdlem51  47440  fourierdlem54  47443  fourierdlem76  47465  fourierdlem80  47469  fourierdlem102  47491  fourierdlem103  47492  fourierdlem104  47493  fourierdlem114  47503  sge0resplit  47689  sge0iunmptlemfi  47696  sge0xaddlem1  47716  hoiprodp1  47871  sge0hsphoire  47872  hoidmvlelem1  47878  hoidmvlelem2  47879  hoidmvlelem5  47882  hspmbllem2  47910  fsummmodsnunz  48726