Proof of Theorem nnaord
Step | Hyp | Ref
| Expression |
1 | | nnaordi 7698 |
. . 3
⊢ ((𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ∈ 𝐵 → (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵))) |
2 | 1 | 3adant1 1079 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ∈ 𝐵 → (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵))) |
3 | | oveq2 6658 |
. . . . . 6
⊢ (𝐴 = 𝐵 → (𝐶 +𝑜 𝐴) = (𝐶 +𝑜 𝐵)) |
4 | 3 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 = 𝐵 → (𝐶 +𝑜 𝐴) = (𝐶 +𝑜 𝐵))) |
5 | | nnaordi 7698 |
. . . . . 6
⊢ ((𝐴 ∈ ω ∧ 𝐶 ∈ ω) → (𝐵 ∈ 𝐴 → (𝐶 +𝑜 𝐵) ∈ (𝐶 +𝑜 𝐴))) |
6 | 5 | 3adant2 1080 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐵 ∈ 𝐴 → (𝐶 +𝑜 𝐵) ∈ (𝐶 +𝑜 𝐴))) |
7 | 4, 6 | orim12d 883 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴) → ((𝐶 +𝑜 𝐴) = (𝐶 +𝑜 𝐵) ∨ (𝐶 +𝑜 𝐵) ∈ (𝐶 +𝑜 𝐴)))) |
8 | 7 | con3d 148 |
. . 3
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (¬
((𝐶 +𝑜
𝐴) = (𝐶 +𝑜 𝐵) ∨ (𝐶 +𝑜 𝐵) ∈ (𝐶 +𝑜 𝐴)) → ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
9 | | df-3an 1039 |
. . . . . 6
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ↔ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐶 ∈
ω)) |
10 | | ancom 466 |
. . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐶 ∈ ω) ↔ (𝐶 ∈ ω ∧ (𝐴 ∈ ω ∧ 𝐵 ∈
ω))) |
11 | | anandi 871 |
. . . . . 6
⊢ ((𝐶 ∈ ω ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) ↔ ((𝐶 ∈ ω ∧ 𝐴 ∈ ω) ∧ (𝐶 ∈ ω ∧ 𝐵 ∈
ω))) |
12 | 9, 10, 11 | 3bitri 286 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ↔ ((𝐶 ∈ ω ∧ 𝐴 ∈ ω) ∧ (𝐶 ∈ ω ∧ 𝐵 ∈
ω))) |
13 | | nnacl 7691 |
. . . . . . 7
⊢ ((𝐶 ∈ ω ∧ 𝐴 ∈ ω) → (𝐶 +𝑜 𝐴) ∈
ω) |
14 | | nnord 7073 |
. . . . . . 7
⊢ ((𝐶 +𝑜 𝐴) ∈ ω → Ord
(𝐶 +𝑜
𝐴)) |
15 | 13, 14 | syl 17 |
. . . . . 6
⊢ ((𝐶 ∈ ω ∧ 𝐴 ∈ ω) → Ord
(𝐶 +𝑜
𝐴)) |
16 | | nnacl 7691 |
. . . . . . 7
⊢ ((𝐶 ∈ ω ∧ 𝐵 ∈ ω) → (𝐶 +𝑜 𝐵) ∈
ω) |
17 | | nnord 7073 |
. . . . . . 7
⊢ ((𝐶 +𝑜 𝐵) ∈ ω → Ord
(𝐶 +𝑜
𝐵)) |
18 | 16, 17 | syl 17 |
. . . . . 6
⊢ ((𝐶 ∈ ω ∧ 𝐵 ∈ ω) → Ord
(𝐶 +𝑜
𝐵)) |
19 | 15, 18 | anim12i 590 |
. . . . 5
⊢ (((𝐶 ∈ ω ∧ 𝐴 ∈ ω) ∧ (𝐶 ∈ ω ∧ 𝐵 ∈ ω)) → (Ord
(𝐶 +𝑜
𝐴) ∧ Ord (𝐶 +𝑜 𝐵))) |
20 | 12, 19 | sylbi 207 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (Ord
(𝐶 +𝑜
𝐴) ∧ Ord (𝐶 +𝑜 𝐵))) |
21 | | ordtri2 5758 |
. . . 4
⊢ ((Ord
(𝐶 +𝑜
𝐴) ∧ Ord (𝐶 +𝑜 𝐵)) → ((𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵) ↔ ¬ ((𝐶 +𝑜 𝐴) = (𝐶 +𝑜 𝐵) ∨ (𝐶 +𝑜 𝐵) ∈ (𝐶 +𝑜 𝐴)))) |
22 | 20, 21 | syl 17 |
. . 3
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵) ↔ ¬ ((𝐶 +𝑜 𝐴) = (𝐶 +𝑜 𝐵) ∨ (𝐶 +𝑜 𝐵) ∈ (𝐶 +𝑜 𝐴)))) |
23 | | nnord 7073 |
. . . . . 6
⊢ (𝐴 ∈ ω → Ord 𝐴) |
24 | | nnord 7073 |
. . . . . 6
⊢ (𝐵 ∈ ω → Ord 𝐵) |
25 | 23, 24 | anim12i 590 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (Ord
𝐴 ∧ Ord 𝐵)) |
26 | 25 | 3adant3 1081 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (Ord
𝐴 ∧ Ord 𝐵)) |
27 | | ordtri2 5758 |
. . . 4
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
28 | 26, 27 | syl 17 |
. . 3
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ∈ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
29 | 8, 22, 28 | 3imtr4d 283 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵) → 𝐴 ∈ 𝐵)) |
30 | 2, 29 | impbid 202 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ∈ 𝐵 ↔ (𝐶 +𝑜 𝐴) ∈ (𝐶 +𝑜 𝐵))) |