Metamath Proof Explorer

Theorem unfi

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 . (Revised by BTernaryTau, 7-Aug-2024)

Ref Expression
Assertion unfi ⊢ A ∈ Fin ∧ B ∈ Fin → A ∪ B ∈ Fin

Proof

Step Hyp Ref Expression
1 uneq2 ⊢ x = ∅ → A ∪ x = A ∪ ∅
2 1 eleq1d ⊢ x = ∅ → A ∪ x ∈ Fin ↔ A ∪ ∅ ∈ Fin
3 2 imbi2d ⊢ x = ∅ → A ∈ Fin → A ∪ x ∈ Fin ↔ A ∈ Fin → A ∪ ∅ ∈ Fin
4 uneq2 ⊢ x = y → A ∪ x = A ∪ y
5 4 eleq1d ⊢ x = y → A ∪ x ∈ Fin ↔ A ∪ y ∈ Fin
6 5 imbi2d ⊢ x = y → A ∈ Fin → A ∪ x ∈ Fin ↔ A ∈ Fin → A ∪ y ∈ Fin
7 uneq2 ⊢ x = y ∪ z → A ∪ x = A ∪ y ∪ z
8 7 eleq1d ⊢ x = y ∪ z → A ∪ x ∈ Fin ↔ A ∪ y ∪ z ∈ Fin
9 8 imbi2d ⊢ x = y ∪ z → A ∈ Fin → A ∪ x ∈ Fin ↔ A ∈ Fin → A ∪ y ∪ z ∈ Fin
10 uneq2 ⊢ x = B → A ∪ x = A ∪ B
11 10 eleq1d ⊢ x = B → A ∪ x ∈ Fin ↔ A ∪ B ∈ Fin
12 11 imbi2d ⊢ x = B → A ∈ Fin → A ∪ x ∈ Fin ↔ A ∈ Fin → A ∪ B ∈ Fin
13 un0 ⊢ A ∪ ∅ = A
14 13 eleq1i ⊢ A ∪ ∅ ∈ Fin ↔ A ∈ Fin
15 14 biimpri ⊢ A ∈ Fin → A ∪ ∅ ∈ Fin
16 snssi ⊢ z ∈ A → z ⊆ A
17 ssequn2 ⊢ z ⊆ A ↔ A ∪ z = A
18 17 biimpi ⊢ z ⊆ A → A ∪ z = A
19 18 uneq2d ⊢ z ⊆ A → y ∪ A ∪ z = y ∪ A
20 un12 ⊢ A ∪ y ∪ z = y ∪ A ∪ z
21 uncom ⊢ A ∪ y = y ∪ A
22 19 20 21 3eqtr4g ⊢ z ⊆ A → A ∪ y ∪ z = A ∪ y
23 16 22 syl ⊢ z ∈ A → A ∪ y ∪ z = A ∪ y
24 23 eleq1d ⊢ z ∈ A → A ∪ y ∪ z ∈ Fin ↔ A ∪ y ∈ Fin
25 24 biimprd ⊢ z ∈ A → A ∪ y ∈ Fin → A ∪ y ∪ z ∈ Fin
26 25 adantld ⊢ z ∈ A → ¬ z ∈ y ∧ A ∪ y ∈ Fin → A ∪ y ∪ z ∈ Fin
27 isfi ⊢ A ∪ y ∈ Fin ↔ ∃ w ∈ ω A ∪ y ≈ w
28 27 biimpi ⊢ A ∪ y ∈ Fin → ∃ w ∈ ω A ∪ y ≈ w
29 r19.41v ⊢ ∃ w ∈ ω A ∪ y ≈ w ∧ ¬ z ∈ A ∧ ¬ z ∈ y ↔ ∃ w ∈ ω A ∪ y ≈ w ∧ ¬ z ∈ A ∧ ¬ z ∈ y
30 disjsn ⊢ A ∪ y ∩ z = ∅ ↔ ¬ z ∈ A ∪ y
31 elun ⊢ z ∈ A ∪ y ↔ z ∈ A ∨ z ∈ y
32 31 notbii ⊢ ¬ z ∈ A ∪ y ↔ ¬ z ∈ A ∨ z ∈ y
33 pm4.56 ⊢ ¬ z ∈ A ∧ ¬ z ∈ y ↔ ¬ z ∈ A ∨ z ∈ y
34 32 33 bitr4i ⊢ ¬ z ∈ A ∪ y ↔ ¬ z ∈ A ∧ ¬ z ∈ y
35 30 34 sylbbr ⊢ ¬ z ∈ A ∧ ¬ z ∈ y → A ∪ y ∩ z = ∅
36 nnord ⊢ w ∈ ω → Ord ⁡ w
37 orddisj ⊢ Ord ⁡ w → w ∩ w = ∅
38 36 37 syl ⊢ w ∈ ω → w ∩ w = ∅
39 en2sn ⊢ z ∈ V ∧ w ∈ V → z ≈ w
40 39 el2v ⊢ z ≈ w
41 unen ⊢ A ∪ y ≈ w ∧ z ≈ w ∧ A ∪ y ∩ z = ∅ ∧ w ∩ w = ∅ → A ∪ y ∪ z ≈ w ∪ w
42 40 41 mpanl2 ⊢ A ∪ y ≈ w ∧ A ∪ y ∩ z = ∅ ∧ w ∩ w = ∅ → A ∪ y ∪ z ≈ w ∪ w
43 38 42 sylanr2 ⊢ A ∪ y ≈ w ∧ A ∪ y ∩ z = ∅ ∧ w ∈ ω → A ∪ y ∪ z ≈ w ∪ w
44 35 43 sylanr1 ⊢ A ∪ y ≈ w ∧ ¬ z ∈ A ∧ ¬ z ∈ y ∧ w ∈ ω → A ∪ y ∪ z ≈ w ∪ w
45 44 3impb ⊢ A ∪ y ≈ w ∧ ¬ z ∈ A ∧ ¬ z ∈ y ∧ w ∈ ω → A ∪ y ∪ z ≈ w ∪ w
46 45 3comr ⊢ w ∈ ω ∧ A ∪ y ≈ w ∧ ¬ z ∈ A ∧ ¬ z ∈ y → A ∪ y ∪ z ≈ w ∪ w
47 46 3expb ⊢ w ∈ ω ∧ A ∪ y ≈ w ∧ ¬ z ∈ A ∧ ¬ z ∈ y → A ∪ y ∪ z ≈ w ∪ w
48 unass ⊢ A ∪ y ∪ z = A ∪ y ∪ z
49 df-suc ⊢ suc ⁡ w = w ∪ w
50 peano2 ⊢ w ∈ ω → suc ⁡ w ∈ ω
51 49 50 eqeltrrid ⊢ w ∈ ω → w ∪ w ∈ ω
52 breq2 ⊢ v = w ∪ w → A ∪ y ∪ z ≈ v ↔ A ∪ y ∪ z ≈ w ∪ w
53 52 rspcev ⊢ w ∪ w ∈ ω ∧ A ∪ y ∪ z ≈ w ∪ w → ∃ v ∈ ω A ∪ y ∪ z ≈ v
54 51 53 sylan ⊢ w ∈ ω ∧ A ∪ y ∪ z ≈ w ∪ w → ∃ v ∈ ω A ∪ y ∪ z ≈ v
55 isfi ⊢ A ∪ y ∪ z ∈ Fin ↔ ∃ v ∈ ω A ∪ y ∪ z ≈ v
56 54 55 sylibr ⊢ w ∈ ω ∧ A ∪ y ∪ z ≈ w ∪ w → A ∪ y ∪ z ∈ Fin
57 48 56 eqeltrrid ⊢ w ∈ ω ∧ A ∪ y ∪ z ≈ w ∪ w → A ∪ y ∪ z ∈ Fin
58 47 57 syldan ⊢ w ∈ ω ∧ A ∪ y ≈ w ∧ ¬ z ∈ A ∧ ¬ z ∈ y → A ∪ y ∪ z ∈ Fin
59 58 rexlimiva ⊢ ∃ w ∈ ω A ∪ y ≈ w ∧ ¬ z ∈ A ∧ ¬ z ∈ y → A ∪ y ∪ z ∈ Fin
60 29 59 sylbir ⊢ ∃ w ∈ ω A ∪ y ≈ w ∧ ¬ z ∈ A ∧ ¬ z ∈ y → A ∪ y ∪ z ∈ Fin
61 28 60 sylan ⊢ A ∪ y ∈ Fin ∧ ¬ z ∈ A ∧ ¬ z ∈ y → A ∪ y ∪ z ∈ Fin
62 61 ancoms ⊢ ¬ z ∈ A ∧ ¬ z ∈ y ∧ A ∪ y ∈ Fin → A ∪ y ∪ z ∈ Fin
63 62 expl ⊢ ¬ z ∈ A → ¬ z ∈ y ∧ A ∪ y ∈ Fin → A ∪ y ∪ z ∈ Fin
64 26 63 pm2.61i ⊢ ¬ z ∈ y ∧ A ∪ y ∈ Fin → A ∪ y ∪ z ∈ Fin
65 64 ex ⊢ ¬ z ∈ y → A ∪ y ∈ Fin → A ∪ y ∪ z ∈ Fin
66 65 imim2d ⊢ ¬ z ∈ y → A ∈ Fin → A ∪ y ∈ Fin → A ∈ Fin → A ∪ y ∪ z ∈ Fin
67 66 adantl ⊢ y ∈ Fin ∧ ¬ z ∈ y → A ∈ Fin → A ∪ y ∈ Fin → A ∈ Fin → A ∪ y ∪ z ∈ Fin
68 3 6 9 12 15 67 findcard2s ⊢ B ∈ Fin → A ∈ Fin → A ∪ B ∈ Fin
69 68 impcom ⊢ A ∈ Fin ∧ B ∈ Fin → A ∪ B ∈ Fin