Proof of Theorem omnord1
Step | Hyp | Ref
| Expression |
1 | | omnord1ex 41889 |
. 2
⊢ ¬
(1o ∈ 2o ↔ (1o ·o
ω) ∈ (2o ·o ω)) |
2 | | 1on 8462 |
. . 3
⊢
1o ∈ On |
3 | | 2on 8464 |
. . . 4
⊢
2o ∈ On |
4 | | omelon 9625 |
. . . . . 6
⊢ ω
∈ On |
5 | | peano1 7863 |
. . . . . 6
⊢ ∅
∈ ω |
6 | | ondif1 8485 |
. . . . . 6
⊢ (ω
∈ (On ∖ 1o) ↔ (ω ∈ On ∧ ∅
∈ ω)) |
7 | 4, 5, 6 | mpbir2an 709 |
. . . . 5
⊢ ω
∈ (On ∖ 1o) |
8 | | oveq2 7402 |
. . . . . . . . 9
⊢ (𝑐 = ω → (1o
·o 𝑐) =
(1o ·o ω)) |
9 | | oveq2 7402 |
. . . . . . . . 9
⊢ (𝑐 = ω → (2o
·o 𝑐) =
(2o ·o ω)) |
10 | 8, 9 | eleq12d 2827 |
. . . . . . . 8
⊢ (𝑐 = ω →
((1o ·o 𝑐) ∈ (2o ·o
𝑐) ↔ (1o
·o ω) ∈ (2o ·o
ω))) |
11 | 10 | bibi2d 342 |
. . . . . . 7
⊢ (𝑐 = ω →
((1o ∈ 2o ↔ (1o ·o
𝑐) ∈ (2o
·o 𝑐))
↔ (1o ∈ 2o ↔ (1o
·o ω) ∈ (2o ·o
ω)))) |
12 | 11 | notbid 317 |
. . . . . 6
⊢ (𝑐 = ω → (¬
(1o ∈ 2o ↔ (1o ·o
𝑐) ∈ (2o
·o 𝑐))
↔ ¬ (1o ∈ 2o ↔ (1o
·o ω) ∈ (2o ·o
ω)))) |
13 | 12 | rspcev 3610 |
. . . . 5
⊢ ((ω
∈ (On ∖ 1o) ∧ ¬ (1o ∈
2o ↔ (1o ·o ω) ∈
(2o ·o ω))) → ∃𝑐 ∈ (On ∖ 1o) ¬
(1o ∈ 2o ↔ (1o ·o
𝑐) ∈ (2o
·o 𝑐))) |
14 | 7, 13 | mpan 688 |
. . . 4
⊢ (¬
(1o ∈ 2o ↔ (1o ·o
ω) ∈ (2o ·o ω)) →
∃𝑐 ∈ (On ∖
1o) ¬ (1o ∈ 2o ↔ (1o
·o 𝑐)
∈ (2o ·o 𝑐))) |
15 | | eleq2 2822 |
. . . . . . . 8
⊢ (𝑏 = 2o →
(1o ∈ 𝑏
↔ 1o ∈ 2o)) |
16 | | oveq1 7401 |
. . . . . . . . 9
⊢ (𝑏 = 2o → (𝑏 ·o 𝑐) = (2o
·o 𝑐)) |
17 | 16 | eleq2d 2819 |
. . . . . . . 8
⊢ (𝑏 = 2o →
((1o ·o 𝑐) ∈ (𝑏 ·o 𝑐) ↔ (1o ·o
𝑐) ∈ (2o
·o 𝑐))) |
18 | 15, 17 | bibi12d 345 |
. . . . . . 7
⊢ (𝑏 = 2o →
((1o ∈ 𝑏
↔ (1o ·o 𝑐) ∈ (𝑏 ·o 𝑐)) ↔ (1o ∈ 2o
↔ (1o ·o 𝑐) ∈ (2o ·o
𝑐)))) |
19 | 18 | notbid 317 |
. . . . . 6
⊢ (𝑏 = 2o → (¬
(1o ∈ 𝑏
↔ (1o ·o 𝑐) ∈ (𝑏 ·o 𝑐)) ↔ ¬ (1o ∈
2o ↔ (1o ·o 𝑐) ∈ (2o ·o
𝑐)))) |
20 | 19 | rexbidv 3178 |
. . . . 5
⊢ (𝑏 = 2o →
(∃𝑐 ∈ (On
∖ 1o) ¬ (1o ∈ 𝑏 ↔ (1o ·o
𝑐) ∈ (𝑏 ·o 𝑐)) ↔ ∃𝑐 ∈ (On ∖
1o) ¬ (1o ∈ 2o ↔ (1o
·o 𝑐)
∈ (2o ·o 𝑐)))) |
21 | 20 | rspcev 3610 |
. . . 4
⊢
((2o ∈ On ∧ ∃𝑐 ∈ (On ∖ 1o) ¬
(1o ∈ 2o ↔ (1o ·o
𝑐) ∈ (2o
·o 𝑐)))
→ ∃𝑏 ∈ On
∃𝑐 ∈ (On ∖
1o) ¬ (1o ∈ 𝑏 ↔ (1o ·o
𝑐) ∈ (𝑏 ·o 𝑐))) |
22 | 3, 14, 21 | sylancr 587 |
. . 3
⊢ (¬
(1o ∈ 2o ↔ (1o ·o
ω) ∈ (2o ·o ω)) →
∃𝑏 ∈ On
∃𝑐 ∈ (On ∖
1o) ¬ (1o ∈ 𝑏 ↔ (1o ·o
𝑐) ∈ (𝑏 ·o 𝑐))) |
23 | | eleq1 2821 |
. . . . . . . 8
⊢ (𝑎 = 1o → (𝑎 ∈ 𝑏 ↔ 1o ∈ 𝑏)) |
24 | | oveq1 7401 |
. . . . . . . . 9
⊢ (𝑎 = 1o → (𝑎 ·o 𝑐) = (1o
·o 𝑐)) |
25 | 24 | eleq1d 2818 |
. . . . . . . 8
⊢ (𝑎 = 1o → ((𝑎 ·o 𝑐) ∈ (𝑏 ·o 𝑐) ↔ (1o ·o
𝑐) ∈ (𝑏 ·o 𝑐))) |
26 | 23, 25 | bibi12d 345 |
. . . . . . 7
⊢ (𝑎 = 1o → ((𝑎 ∈ 𝑏 ↔ (𝑎 ·o 𝑐) ∈ (𝑏 ·o 𝑐)) ↔ (1o ∈ 𝑏 ↔ (1o
·o 𝑐)
∈ (𝑏
·o 𝑐)))) |
27 | 26 | notbid 317 |
. . . . . 6
⊢ (𝑎 = 1o → (¬
(𝑎 ∈ 𝑏 ↔ (𝑎 ·o 𝑐) ∈ (𝑏 ·o 𝑐)) ↔ ¬ (1o ∈ 𝑏 ↔ (1o
·o 𝑐)
∈ (𝑏
·o 𝑐)))) |
28 | 27 | rexbidv 3178 |
. . . . 5
⊢ (𝑎 = 1o →
(∃𝑐 ∈ (On
∖ 1o) ¬ (𝑎 ∈ 𝑏 ↔ (𝑎 ·o 𝑐) ∈ (𝑏 ·o 𝑐)) ↔ ∃𝑐 ∈ (On ∖ 1o) ¬
(1o ∈ 𝑏
↔ (1o ·o 𝑐) ∈ (𝑏 ·o 𝑐)))) |
29 | 28 | rexbidv 3178 |
. . . 4
⊢ (𝑎 = 1o →
(∃𝑏 ∈ On
∃𝑐 ∈ (On ∖
1o) ¬ (𝑎
∈ 𝑏 ↔ (𝑎 ·o 𝑐) ∈ (𝑏 ·o 𝑐)) ↔ ∃𝑏 ∈ On ∃𝑐 ∈ (On ∖ 1o) ¬
(1o ∈ 𝑏
↔ (1o ·o 𝑐) ∈ (𝑏 ·o 𝑐)))) |
30 | 29 | rspcev 3610 |
. . 3
⊢
((1o ∈ On ∧ ∃𝑏 ∈ On ∃𝑐 ∈ (On ∖ 1o) ¬
(1o ∈ 𝑏
↔ (1o ·o 𝑐) ∈ (𝑏 ·o 𝑐))) → ∃𝑎 ∈ On ∃𝑏 ∈ On ∃𝑐 ∈ (On ∖ 1o) ¬
(𝑎 ∈ 𝑏 ↔ (𝑎 ·o 𝑐) ∈ (𝑏 ·o 𝑐))) |
31 | 2, 22, 30 | sylancr 587 |
. 2
⊢ (¬
(1o ∈ 2o ↔ (1o ·o
ω) ∈ (2o ·o ω)) →
∃𝑎 ∈ On
∃𝑏 ∈ On
∃𝑐 ∈ (On ∖
1o) ¬ (𝑎
∈ 𝑏 ↔ (𝑎 ·o 𝑐) ∈ (𝑏 ·o 𝑐))) |
32 | 1, 31 | ax-mp 5 |
1
⊢
∃𝑎 ∈ On
∃𝑏 ∈ On
∃𝑐 ∈ (On ∖
1o) ¬ (𝑎
∈ 𝑏 ↔ (𝑎 ·o 𝑐) ∈ (𝑏 ·o 𝑐)) |