Proof of Theorem addnidpi
Step | Hyp | Ref
| Expression |
1 | | pinn 10634 |
. . . . 5
⊢ (𝐴 ∈ N →
𝐴 ∈
ω) |
2 | | elni2 10633 |
. . . . . 6
⊢ (𝐵 ∈ N ↔
(𝐵 ∈ ω ∧
∅ ∈ 𝐵)) |
3 | | nnaordi 8449 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ω ∧ 𝐴 ∈ ω) → (∅
∈ 𝐵 → (𝐴 +o ∅) ∈
(𝐴 +o 𝐵))) |
4 | | nna0 8435 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ω → (𝐴 +o ∅) = 𝐴) |
5 | 4 | eleq1d 2823 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ω → ((𝐴 +o ∅) ∈
(𝐴 +o 𝐵) ↔ 𝐴 ∈ (𝐴 +o 𝐵))) |
6 | | nnord 7720 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ω → Ord 𝐴) |
7 | | ordirr 6284 |
. . . . . . . . . . . . . 14
⊢ (Ord
𝐴 → ¬ 𝐴 ∈ 𝐴) |
8 | 6, 7 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ω → ¬
𝐴 ∈ 𝐴) |
9 | | eleq2 2827 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 +o 𝐵) = 𝐴 → (𝐴 ∈ (𝐴 +o 𝐵) ↔ 𝐴 ∈ 𝐴)) |
10 | 9 | notbid 318 |
. . . . . . . . . . . . 13
⊢ ((𝐴 +o 𝐵) = 𝐴 → (¬ 𝐴 ∈ (𝐴 +o 𝐵) ↔ ¬ 𝐴 ∈ 𝐴)) |
11 | 8, 10 | syl5ibrcom 246 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ω → ((𝐴 +o 𝐵) = 𝐴 → ¬ 𝐴 ∈ (𝐴 +o 𝐵))) |
12 | 11 | con2d 134 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ω → (𝐴 ∈ (𝐴 +o 𝐵) → ¬ (𝐴 +o 𝐵) = 𝐴)) |
13 | 5, 12 | sylbid 239 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ω → ((𝐴 +o ∅) ∈
(𝐴 +o 𝐵) → ¬ (𝐴 +o 𝐵) = 𝐴)) |
14 | 13 | adantl 482 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ω ∧ 𝐴 ∈ ω) → ((𝐴 +o ∅) ∈
(𝐴 +o 𝐵) → ¬ (𝐴 +o 𝐵) = 𝐴)) |
15 | 3, 14 | syld 47 |
. . . . . . . 8
⊢ ((𝐵 ∈ ω ∧ 𝐴 ∈ ω) → (∅
∈ 𝐵 → ¬
(𝐴 +o 𝐵) = 𝐴)) |
16 | 15 | expcom 414 |
. . . . . . 7
⊢ (𝐴 ∈ ω → (𝐵 ∈ ω → (∅
∈ 𝐵 → ¬
(𝐴 +o 𝐵) = 𝐴))) |
17 | 16 | imp32 419 |
. . . . . 6
⊢ ((𝐴 ∈ ω ∧ (𝐵 ∈ ω ∧ ∅
∈ 𝐵)) → ¬
(𝐴 +o 𝐵) = 𝐴) |
18 | 2, 17 | sylan2b 594 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ N) →
¬ (𝐴 +o
𝐵) = 𝐴) |
19 | 1, 18 | sylan 580 |
. . . 4
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N)
→ ¬ (𝐴
+o 𝐵) = 𝐴) |
20 | | addpiord 10640 |
. . . . 5
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N)
→ (𝐴
+N 𝐵) = (𝐴 +o 𝐵)) |
21 | 20 | eqeq1d 2740 |
. . . 4
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N)
→ ((𝐴
+N 𝐵) = 𝐴 ↔ (𝐴 +o 𝐵) = 𝐴)) |
22 | 19, 21 | mtbird 325 |
. . 3
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N)
→ ¬ (𝐴
+N 𝐵) = 𝐴) |
23 | 22 | a1d 25 |
. 2
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N)
→ (𝐴 ∈
N → ¬ (𝐴 +N 𝐵) = 𝐴)) |
24 | | dmaddpi 10646 |
. . . . . 6
⊢ dom
+N = (N ×
N) |
25 | 24 | ndmov 7456 |
. . . . 5
⊢ (¬
(𝐴 ∈ N
∧ 𝐵 ∈
N) → (𝐴
+N 𝐵) = ∅) |
26 | 25 | eqeq1d 2740 |
. . . 4
⊢ (¬
(𝐴 ∈ N
∧ 𝐵 ∈
N) → ((𝐴
+N 𝐵) = 𝐴 ↔ ∅ = 𝐴)) |
27 | | 0npi 10638 |
. . . . 5
⊢ ¬
∅ ∈ N |
28 | | eleq1 2826 |
. . . . 5
⊢ (∅
= 𝐴 → (∅ ∈
N ↔ 𝐴
∈ N)) |
29 | 27, 28 | mtbii 326 |
. . . 4
⊢ (∅
= 𝐴 → ¬ 𝐴 ∈
N) |
30 | 26, 29 | syl6bi 252 |
. . 3
⊢ (¬
(𝐴 ∈ N
∧ 𝐵 ∈
N) → ((𝐴
+N 𝐵) = 𝐴 → ¬ 𝐴 ∈ N)) |
31 | 30 | con2d 134 |
. 2
⊢ (¬
(𝐴 ∈ N
∧ 𝐵 ∈
N) → (𝐴
∈ N → ¬ (𝐴 +N 𝐵) = 𝐴)) |
32 | 23, 31 | pm2.61i 182 |
1
⊢ (𝐴 ∈ N →
¬ (𝐴
+N 𝐵) = 𝐴) |