Proof of Theorem nnmword
Step | Hyp | Ref
| Expression |
1 | | iba 528 |
. . . 4
⊢ (∅
∈ 𝐶 → (𝐵 ∈ 𝐴 ↔ (𝐵 ∈ 𝐴 ∧ ∅ ∈ 𝐶))) |
2 | | nnmord 8461 |
. . . . 5
⊢ ((𝐵 ∈ ω ∧ 𝐴 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐵 ∈ 𝐴 ∧ ∅ ∈ 𝐶) ↔ (𝐶 ·o 𝐵) ∈ (𝐶 ·o 𝐴))) |
3 | 2 | 3com12 1122 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐵 ∈ 𝐴 ∧ ∅ ∈ 𝐶) ↔ (𝐶 ·o 𝐵) ∈ (𝐶 ·o 𝐴))) |
4 | 1, 3 | sylan9bbr 511 |
. . 3
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → (𝐵 ∈ 𝐴 ↔ (𝐶 ·o 𝐵) ∈ (𝐶 ·o 𝐴))) |
5 | 4 | notbid 318 |
. 2
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → (¬
𝐵 ∈ 𝐴 ↔ ¬ (𝐶 ·o 𝐵) ∈ (𝐶 ·o 𝐴))) |
6 | | simpl1 1190 |
. . . 4
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → 𝐴 ∈
ω) |
7 | | nnon 7718 |
. . . 4
⊢ (𝐴 ∈ ω → 𝐴 ∈ On) |
8 | 6, 7 | syl 17 |
. . 3
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → 𝐴 ∈ On) |
9 | | simpl2 1191 |
. . . 4
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → 𝐵 ∈
ω) |
10 | | nnon 7718 |
. . . 4
⊢ (𝐵 ∈ ω → 𝐵 ∈ On) |
11 | 9, 10 | syl 17 |
. . 3
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → 𝐵 ∈ On) |
12 | | ontri1 6302 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴)) |
13 | 8, 11, 12 | syl2anc 584 |
. 2
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴)) |
14 | | simpl3 1192 |
. . . . 5
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → 𝐶 ∈
ω) |
15 | | nnmcl 8441 |
. . . . 5
⊢ ((𝐶 ∈ ω ∧ 𝐴 ∈ ω) → (𝐶 ·o 𝐴) ∈
ω) |
16 | 14, 6, 15 | syl2anc 584 |
. . . 4
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → (𝐶 ·o 𝐴) ∈
ω) |
17 | | nnon 7718 |
. . . 4
⊢ ((𝐶 ·o 𝐴) ∈ ω → (𝐶 ·o 𝐴) ∈ On) |
18 | 16, 17 | syl 17 |
. . 3
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → (𝐶 ·o 𝐴) ∈ On) |
19 | | nnmcl 8441 |
. . . . 5
⊢ ((𝐶 ∈ ω ∧ 𝐵 ∈ ω) → (𝐶 ·o 𝐵) ∈
ω) |
20 | 14, 9, 19 | syl2anc 584 |
. . . 4
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → (𝐶 ·o 𝐵) ∈
ω) |
21 | | nnon 7718 |
. . . 4
⊢ ((𝐶 ·o 𝐵) ∈ ω → (𝐶 ·o 𝐵) ∈ On) |
22 | 20, 21 | syl 17 |
. . 3
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → (𝐶 ·o 𝐵) ∈ On) |
23 | | ontri1 6302 |
. . 3
⊢ (((𝐶 ·o 𝐴) ∈ On ∧ (𝐶 ·o 𝐵) ∈ On) → ((𝐶 ·o 𝐴) ⊆ (𝐶 ·o 𝐵) ↔ ¬ (𝐶 ·o 𝐵) ∈ (𝐶 ·o 𝐴))) |
24 | 18, 22, 23 | syl2anc 584 |
. 2
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → ((𝐶 ·o 𝐴) ⊆ (𝐶 ·o 𝐵) ↔ ¬ (𝐶 ·o 𝐵) ∈ (𝐶 ·o 𝐴))) |
25 | 5, 13, 24 | 3bitr4d 311 |
1
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → (𝐴 ⊆ 𝐵 ↔ (𝐶 ·o 𝐴) ⊆ (𝐶 ·o 𝐵))) |