# 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$