Proof of Theorem addnidpi
Step | Hyp | Ref
| Expression |
1 | | pinn 10390 |
. . . . 5
⊢ (𝐴 ∈ N →
𝐴 ∈
ω) |
2 | | elni2 10389 |
. . . . . 6
⊢ (𝐵 ∈ N ↔
(𝐵 ∈ ω ∧
∅ ∈ 𝐵)) |
3 | | nnaordi 8287 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ω ∧ 𝐴 ∈ ω) → (∅
∈ 𝐵 → (𝐴 +o ∅) ∈
(𝐴 +o 𝐵))) |
4 | | nna0 8273 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ω → (𝐴 +o ∅) = 𝐴) |
5 | 4 | eleq1d 2818 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ω → ((𝐴 +o ∅) ∈
(𝐴 +o 𝐵) ↔ 𝐴 ∈ (𝐴 +o 𝐵))) |
6 | | nnord 7619 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ω → Ord 𝐴) |
7 | | ordirr 6200 |
. . . . . . . . . . . . . 14
⊢ (Ord
𝐴 → ¬ 𝐴 ∈ 𝐴) |
8 | 6, 7 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ω → ¬
𝐴 ∈ 𝐴) |
9 | | eleq2 2822 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 +o 𝐵) = 𝐴 → (𝐴 ∈ (𝐴 +o 𝐵) ↔ 𝐴 ∈ 𝐴)) |
10 | 9 | notbid 321 |
. . . . . . . . . . . . 13
⊢ ((𝐴 +o 𝐵) = 𝐴 → (¬ 𝐴 ∈ (𝐴 +o 𝐵) ↔ ¬ 𝐴 ∈ 𝐴)) |
11 | 8, 10 | syl5ibrcom 250 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ω → ((𝐴 +o 𝐵) = 𝐴 → ¬ 𝐴 ∈ (𝐴 +o 𝐵))) |
12 | 11 | con2d 136 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ω → (𝐴 ∈ (𝐴 +o 𝐵) → ¬ (𝐴 +o 𝐵) = 𝐴)) |
13 | 5, 12 | sylbid 243 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ω → ((𝐴 +o ∅) ∈
(𝐴 +o 𝐵) → ¬ (𝐴 +o 𝐵) = 𝐴)) |
14 | 13 | adantl 485 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ω ∧ 𝐴 ∈ ω) → ((𝐴 +o ∅) ∈
(𝐴 +o 𝐵) → ¬ (𝐴 +o 𝐵) = 𝐴)) |
15 | 3, 14 | syld 47 |
. . . . . . . 8
⊢ ((𝐵 ∈ ω ∧ 𝐴 ∈ ω) → (∅
∈ 𝐵 → ¬
(𝐴 +o 𝐵) = 𝐴)) |
16 | 15 | expcom 417 |
. . . . . . 7
⊢ (𝐴 ∈ ω → (𝐵 ∈ ω → (∅
∈ 𝐵 → ¬
(𝐴 +o 𝐵) = 𝐴))) |
17 | 16 | imp32 422 |
. . . . . 6
⊢ ((𝐴 ∈ ω ∧ (𝐵 ∈ ω ∧ ∅
∈ 𝐵)) → ¬
(𝐴 +o 𝐵) = 𝐴) |
18 | 2, 17 | sylan2b 597 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ N) →
¬ (𝐴 +o
𝐵) = 𝐴) |
19 | 1, 18 | sylan 583 |
. . . 4
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N)
→ ¬ (𝐴
+o 𝐵) = 𝐴) |
20 | | addpiord 10396 |
. . . . 5
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N)
→ (𝐴
+N 𝐵) = (𝐴 +o 𝐵)) |
21 | 20 | eqeq1d 2741 |
. . . 4
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N)
→ ((𝐴
+N 𝐵) = 𝐴 ↔ (𝐴 +o 𝐵) = 𝐴)) |
22 | 19, 21 | mtbird 328 |
. . 3
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N)
→ ¬ (𝐴
+N 𝐵) = 𝐴) |
23 | 22 | a1d 25 |
. 2
⊢ ((𝐴 ∈ N ∧
𝐵 ∈ N)
→ (𝐴 ∈
N → ¬ (𝐴 +N 𝐵) = 𝐴)) |
24 | | dmaddpi 10402 |
. . . . . 6
⊢ dom
+N = (N ×
N) |
25 | 24 | ndmov 7360 |
. . . . 5
⊢ (¬
(𝐴 ∈ N
∧ 𝐵 ∈
N) → (𝐴
+N 𝐵) = ∅) |
26 | 25 | eqeq1d 2741 |
. . . 4
⊢ (¬
(𝐴 ∈ N
∧ 𝐵 ∈
N) → ((𝐴
+N 𝐵) = 𝐴 ↔ ∅ = 𝐴)) |
27 | | 0npi 10394 |
. . . . 5
⊢ ¬
∅ ∈ N |
28 | | eleq1 2821 |
. . . . 5
⊢ (∅
= 𝐴 → (∅ ∈
N ↔ 𝐴
∈ N)) |
29 | 27, 28 | mtbii 329 |
. . . 4
⊢ (∅
= 𝐴 → ¬ 𝐴 ∈
N) |
30 | 26, 29 | syl6bi 256 |
. . 3
⊢ (¬
(𝐴 ∈ N
∧ 𝐵 ∈
N) → ((𝐴
+N 𝐵) = 𝐴 → ¬ 𝐴 ∈ N)) |
31 | 30 | con2d 136 |
. 2
⊢ (¬
(𝐴 ∈ N
∧ 𝐵 ∈
N) → (𝐴
∈ N → ¬ (𝐴 +N 𝐵) = 𝐴)) |
32 | 23, 31 | pm2.61i 185 |
1
⊢ (𝐴 ∈ N →
¬ (𝐴
+N 𝐵) = 𝐴) |