Step | Hyp | Ref
| Expression |
1 | | isfi 6739 |
. . . 4
⊢ (𝐴 ∈ Fin ↔ ∃𝑛 ∈ ω 𝐴 ≈ 𝑛) |
2 | 1 | biimpi 119 |
. . 3
⊢ (𝐴 ∈ Fin → ∃𝑛 ∈ ω 𝐴 ≈ 𝑛) |
3 | 2 | 3ad2ant1 1013 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ ¬ 𝐵 ∈ 𝐴) → ∃𝑛 ∈ ω 𝐴 ≈ 𝑛) |
4 | | peano2 4579 |
. . . . 5
⊢ (𝑛 ∈ ω → suc 𝑛 ∈
ω) |
5 | 4 | ad2antrl 487 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ ¬ 𝐵 ∈ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) → suc 𝑛 ∈ ω) |
6 | | simprr 527 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ ¬ 𝐵 ∈ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) → 𝐴 ≈ 𝑛) |
7 | | simpl2 996 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ ¬ 𝐵 ∈ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) → 𝐵 ∈ 𝑉) |
8 | | simprl 526 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ ¬ 𝐵 ∈ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) → 𝑛 ∈ ω) |
9 | | en2sn 6791 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑉 ∧ 𝑛 ∈ ω) → {𝐵} ≈ {𝑛}) |
10 | 7, 8, 9 | syl2anc 409 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ ¬ 𝐵 ∈ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) → {𝐵} ≈ {𝑛}) |
11 | | disjsn 3645 |
. . . . . . . . 9
⊢ ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ 𝐴) |
12 | 11 | biimpri 132 |
. . . . . . . 8
⊢ (¬
𝐵 ∈ 𝐴 → (𝐴 ∩ {𝐵}) = ∅) |
13 | 12 | 3ad2ant3 1015 |
. . . . . . 7
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ ¬ 𝐵 ∈ 𝐴) → (𝐴 ∩ {𝐵}) = ∅) |
14 | 13 | adantr 274 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ ¬ 𝐵 ∈ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) → (𝐴 ∩ {𝐵}) = ∅) |
15 | | nnord 4596 |
. . . . . . . . 9
⊢ (𝑛 ∈ ω → Ord 𝑛) |
16 | | ordirr 4526 |
. . . . . . . . 9
⊢ (Ord
𝑛 → ¬ 𝑛 ∈ 𝑛) |
17 | 15, 16 | syl 14 |
. . . . . . . 8
⊢ (𝑛 ∈ ω → ¬
𝑛 ∈ 𝑛) |
18 | | disjsn 3645 |
. . . . . . . 8
⊢ ((𝑛 ∩ {𝑛}) = ∅ ↔ ¬ 𝑛 ∈ 𝑛) |
19 | 17, 18 | sylibr 133 |
. . . . . . 7
⊢ (𝑛 ∈ ω → (𝑛 ∩ {𝑛}) = ∅) |
20 | 19 | ad2antrl 487 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ ¬ 𝐵 ∈ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) → (𝑛 ∩ {𝑛}) = ∅) |
21 | | unen 6794 |
. . . . . 6
⊢ (((𝐴 ≈ 𝑛 ∧ {𝐵} ≈ {𝑛}) ∧ ((𝐴 ∩ {𝐵}) = ∅ ∧ (𝑛 ∩ {𝑛}) = ∅)) → (𝐴 ∪ {𝐵}) ≈ (𝑛 ∪ {𝑛})) |
22 | 6, 10, 14, 20, 21 | syl22anc 1234 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ ¬ 𝐵 ∈ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) → (𝐴 ∪ {𝐵}) ≈ (𝑛 ∪ {𝑛})) |
23 | | df-suc 4356 |
. . . . 5
⊢ suc 𝑛 = (𝑛 ∪ {𝑛}) |
24 | 22, 23 | breqtrrdi 4031 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ ¬ 𝐵 ∈ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) → (𝐴 ∪ {𝐵}) ≈ suc 𝑛) |
25 | | breq2 3993 |
. . . . 5
⊢ (𝑚 = suc 𝑛 → ((𝐴 ∪ {𝐵}) ≈ 𝑚 ↔ (𝐴 ∪ {𝐵}) ≈ suc 𝑛)) |
26 | 25 | rspcev 2834 |
. . . 4
⊢ ((suc
𝑛 ∈ ω ∧
(𝐴 ∪ {𝐵}) ≈ suc 𝑛) → ∃𝑚 ∈ ω (𝐴 ∪ {𝐵}) ≈ 𝑚) |
27 | 5, 24, 26 | syl2anc 409 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ ¬ 𝐵 ∈ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) → ∃𝑚 ∈ ω (𝐴 ∪ {𝐵}) ≈ 𝑚) |
28 | | isfi 6739 |
. . 3
⊢ ((𝐴 ∪ {𝐵}) ∈ Fin ↔ ∃𝑚 ∈ ω (𝐴 ∪ {𝐵}) ≈ 𝑚) |
29 | 27, 28 | sylibr 133 |
. 2
⊢ (((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ ¬ 𝐵 ∈ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) → (𝐴 ∪ {𝐵}) ∈ Fin) |
30 | 3, 29 | rexlimddv 2592 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ∧ ¬ 𝐵 ∈ 𝐴) → (𝐴 ∪ {𝐵}) ∈ Fin) |