Proof of Theorem nnaord
Step | Hyp | Ref
| Expression |
1 | | nnaordi 8268 |
. . 3
⊢ ((𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ∈ 𝐵 → (𝐶 +o 𝐴) ∈ (𝐶 +o 𝐵))) |
2 | 1 | 3adant1 1131 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ∈ 𝐵 → (𝐶 +o 𝐴) ∈ (𝐶 +o 𝐵))) |
3 | | oveq2 7172 |
. . . . . 6
⊢ (𝐴 = 𝐵 → (𝐶 +o 𝐴) = (𝐶 +o 𝐵)) |
4 | 3 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 = 𝐵 → (𝐶 +o 𝐴) = (𝐶 +o 𝐵))) |
5 | | nnaordi 8268 |
. . . . . 6
⊢ ((𝐴 ∈ ω ∧ 𝐶 ∈ ω) → (𝐵 ∈ 𝐴 → (𝐶 +o 𝐵) ∈ (𝐶 +o 𝐴))) |
6 | 5 | 3adant2 1132 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐵 ∈ 𝐴 → (𝐶 +o 𝐵) ∈ (𝐶 +o 𝐴))) |
7 | 4, 6 | orim12d 964 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴) → ((𝐶 +o 𝐴) = (𝐶 +o 𝐵) ∨ (𝐶 +o 𝐵) ∈ (𝐶 +o 𝐴)))) |
8 | 7 | con3d 155 |
. . 3
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (¬
((𝐶 +o 𝐴) = (𝐶 +o 𝐵) ∨ (𝐶 +o 𝐵) ∈ (𝐶 +o 𝐴)) → ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
9 | | df-3an 1090 |
. . . . . 6
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ↔ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐶 ∈
ω)) |
10 | | ancom 464 |
. . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐶 ∈ ω) ↔ (𝐶 ∈ ω ∧ (𝐴 ∈ ω ∧ 𝐵 ∈
ω))) |
11 | | anandi 676 |
. . . . . 6
⊢ ((𝐶 ∈ ω ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) ↔ ((𝐶 ∈ ω ∧ 𝐴 ∈ ω) ∧ (𝐶 ∈ ω ∧ 𝐵 ∈
ω))) |
12 | 9, 10, 11 | 3bitri 300 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ↔ ((𝐶 ∈ ω ∧ 𝐴 ∈ ω) ∧ (𝐶 ∈ ω ∧ 𝐵 ∈
ω))) |
13 | | nnacl 8261 |
. . . . . . 7
⊢ ((𝐶 ∈ ω ∧ 𝐴 ∈ ω) → (𝐶 +o 𝐴) ∈ ω) |
14 | | nnord 7601 |
. . . . . . 7
⊢ ((𝐶 +o 𝐴) ∈ ω → Ord (𝐶 +o 𝐴)) |
15 | 13, 14 | syl 17 |
. . . . . 6
⊢ ((𝐶 ∈ ω ∧ 𝐴 ∈ ω) → Ord
(𝐶 +o 𝐴)) |
16 | | nnacl 8261 |
. . . . . . 7
⊢ ((𝐶 ∈ ω ∧ 𝐵 ∈ ω) → (𝐶 +o 𝐵) ∈ ω) |
17 | | nnord 7601 |
. . . . . . 7
⊢ ((𝐶 +o 𝐵) ∈ ω → Ord (𝐶 +o 𝐵)) |
18 | 16, 17 | syl 17 |
. . . . . 6
⊢ ((𝐶 ∈ ω ∧ 𝐵 ∈ ω) → Ord
(𝐶 +o 𝐵)) |
19 | 15, 18 | anim12i 616 |
. . . . 5
⊢ (((𝐶 ∈ ω ∧ 𝐴 ∈ ω) ∧ (𝐶 ∈ ω ∧ 𝐵 ∈ ω)) → (Ord
(𝐶 +o 𝐴) ∧ Ord (𝐶 +o 𝐵))) |
20 | 12, 19 | sylbi 220 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (Ord
(𝐶 +o 𝐴) ∧ Ord (𝐶 +o 𝐵))) |
21 | | ordtri2 6201 |
. . . 4
⊢ ((Ord
(𝐶 +o 𝐴) ∧ Ord (𝐶 +o 𝐵)) → ((𝐶 +o 𝐴) ∈ (𝐶 +o 𝐵) ↔ ¬ ((𝐶 +o 𝐴) = (𝐶 +o 𝐵) ∨ (𝐶 +o 𝐵) ∈ (𝐶 +o 𝐴)))) |
22 | 20, 21 | syl 17 |
. . 3
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐶 +o 𝐴) ∈ (𝐶 +o 𝐵) ↔ ¬ ((𝐶 +o 𝐴) = (𝐶 +o 𝐵) ∨ (𝐶 +o 𝐵) ∈ (𝐶 +o 𝐴)))) |
23 | | nnord 7601 |
. . . . . 6
⊢ (𝐴 ∈ ω → Ord 𝐴) |
24 | | nnord 7601 |
. . . . . 6
⊢ (𝐵 ∈ ω → Ord 𝐵) |
25 | 23, 24 | anim12i 616 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (Ord
𝐴 ∧ Ord 𝐵)) |
26 | 25 | 3adant3 1133 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (Ord
𝐴 ∧ Ord 𝐵)) |
27 | | ordtri2 6201 |
. . . 4
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
28 | 26, 27 | syl 17 |
. . 3
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ∈ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
29 | 8, 22, 28 | 3imtr4d 297 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐶 +o 𝐴) ∈ (𝐶 +o 𝐵) → 𝐴 ∈ 𝐵)) |
30 | 2, 29 | impbid 215 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ∈ 𝐵 ↔ (𝐶 +o 𝐴) ∈ (𝐶 +o 𝐵))) |