Proof of Theorem addnidpi
| Step | Hyp | Ref
| Expression |
| 1 | | pinn 10918 |
. . . . 5
⊢ (𝐴 ∈ N →
𝐴 ∈
ω) |
| 2 | | elni2 10917 |
. . . . . 6
⊢ (𝐵 ∈ N ↔
(𝐵 ∈ ω ∧
∅ ∈ 𝐵)) |
| 3 | | nnaordi 8656 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ω ∧ 𝐴 ∈ ω) → (∅
∈ 𝐵 → (𝐴 +o ∅) ∈
(𝐴 +o 𝐵))) |
| 4 | | nna0 8642 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ω → (𝐴 +o ∅) = 𝐴) |
| 5 | 4 | eleq1d 2826 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ω → ((𝐴 +o ∅) ∈
(𝐴 +o 𝐵) ↔ 𝐴 ∈ (𝐴 +o 𝐵))) |
| 6 | | nnord 7895 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ω → Ord 𝐴) |
| 7 | | ordirr 6402 |
. . . . . . . . . . . . . 14
⊢ (Ord
𝐴 → ¬ 𝐴 ∈ 𝐴) |
| 8 | 6, 7 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ω → ¬
𝐴 ∈ 𝐴) |
| 9 | | eleq2 2830 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 +o 𝐵) = 𝐴 → (𝐴 ∈ (𝐴 +o 𝐵) ↔ 𝐴 ∈ 𝐴)) |
| 10 | 9 | notbid 318 |
. . . . . . . . . . . . 13
⊢ ((𝐴 +o 𝐵) = 𝐴 → (¬ 𝐴 ∈ (𝐴 +o 𝐵) ↔ ¬ 𝐴 ∈ 𝐴)) |
| 11 | 8, 10 | syl5ibrcom 247 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ω → ((𝐴 +o 𝐵) = 𝐴 → ¬ 𝐴 ∈ (𝐴 +o 𝐵))) |
| 12 | 11 | con2d 134 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ω → (𝐴 ∈ (𝐴 +o 𝐵) → ¬ (𝐴 +o 𝐵) = 𝐴)) |
| 13 | 5, 12 | sylbid 240 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ω → ((𝐴 +o ∅) ∈
(𝐴 +o 𝐵) → ¬ (𝐴 +o 𝐵) = 𝐴)) |
| 14 | 13 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ω ∧ 𝐴 ∈ ω) → ((𝐴 +o ∅) ∈
(𝐴 +o 𝐵) → ¬ (𝐴 +o 𝐵) = 𝐴)) |
| 15 | 3, 14 | syld 47 |
. . . . . . . 8
⊢ ((𝐵 ∈ ω ∧ 𝐴 ∈ ω) → (∅
∈ 𝐵 → ¬
(𝐴 +o 𝐵) = 𝐴)) |
| 16 | 15 | expcom 413 |
. . . . . . 7
⊢ (𝐴 ∈ ω → (𝐵 ∈ ω → (∅
∈ 𝐵 → ¬
(𝐴 +o 𝐵) = 𝐴))) |
| 17 | 16 | imp32 418 |
. . . . . 6
⊢ ((𝐴 ∈ ω ∧ (𝐵 ∈ ω ∧ ∅
∈ 𝐵)) → ¬
(𝐴 +o 𝐵) = 𝐴) |
| 18 | 2, 17 | sylan2b 594 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ N) →
¬ (𝐴 +o
𝐵) = 𝐴) |
| 19 | 1, 18 | sylan 580 |
. . . 4
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N)
→ ¬ (𝐴
+o 𝐵) = 𝐴) |
| 20 | | addpiord 10924 |
. . . . 5
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N)
→ (𝐴
+N 𝐵) = (𝐴 +o 𝐵)) |
| 21 | 20 | eqeq1d 2739 |
. . . 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 10930 |
. . . . . 6
⊢ dom
+N = (N ×
N) |
| 25 | 24 | ndmov 7617 |
. . . . 5
⊢ (¬
(𝐴 ∈ N
∧ 𝐵 ∈
N) → (𝐴
+N 𝐵) = ∅) |
| 26 | 25 | eqeq1d 2739 |
. . . 4
⊢ (¬
(𝐴 ∈ N
∧ 𝐵 ∈
N) → ((𝐴
+N 𝐵) = 𝐴 ↔ ∅ = 𝐴)) |
| 27 | | 0npi 10922 |
. . . . 5
⊢ ¬
∅ ∈ N |
| 28 | | eleq1 2829 |
. . . . 5
⊢ (∅
= 𝐴 → (∅ ∈
N ↔ 𝐴
∈ N)) |
| 29 | 27, 28 | mtbii 326 |
. . . 4
⊢ (∅
= 𝐴 → ¬ 𝐴 ∈
N) |
| 30 | 26, 29 | biimtrdi 253 |
. . 3
⊢ (¬
(𝐴 ∈ N
∧ 𝐵 ∈
N) → ((𝐴
+N 𝐵) = 𝐴 → ¬ 𝐴 ∈ N)) |
| 31 | 30 | con2d 134 |
. 2
⊢ (¬
(𝐴 ∈ N
∧ 𝐵 ∈
N) → (𝐴
∈ N → ¬ (𝐴 +N 𝐵) = 𝐴)) |
| 32 | 23, 31 | pm2.61i 182 |
1
⊢ (𝐴 ∈ N →
¬ (𝐴
+N 𝐵) = 𝐴) |