Proof of Theorem oenord1
| Step | Hyp | Ref
| Expression |
| 1 | | oenord1ex 43328 |
. 2
⊢ ¬
(2o ∈ 3o ↔ (2o ↑o
ω) ∈ (3o ↑o ω)) |
| 2 | | 2on 8520 |
. . . 4
⊢
2o ∈ On |
| 3 | | 1oex 8516 |
. . . . . 6
⊢
1o ∈ V |
| 4 | 3 | prid2 4763 |
. . . . 5
⊢
1o ∈ {∅, 1o} |
| 5 | | df2o3 8514 |
. . . . 5
⊢
2o = {∅, 1o} |
| 6 | 4, 5 | eleqtrri 2840 |
. . . 4
⊢
1o ∈ 2o |
| 7 | | ondif2 8540 |
. . . 4
⊢
(2o ∈ (On ∖ 2o) ↔ (2o
∈ On ∧ 1o ∈ 2o)) |
| 8 | 2, 6, 7 | mpbir2an 711 |
. . 3
⊢
2o ∈ (On ∖ 2o) |
| 9 | | 3on 8524 |
. . . . 5
⊢
3o ∈ On |
| 10 | 3 | tpid2 4770 |
. . . . . 6
⊢
1o ∈ {∅, 1o,
2o} |
| 11 | | df3o2 43326 |
. . . . . 6
⊢
3o = {∅, 1o, 2o} |
| 12 | 10, 11 | eleqtrri 2840 |
. . . . 5
⊢
1o ∈ 3o |
| 13 | | ondif2 8540 |
. . . . 5
⊢
(3o ∈ (On ∖ 2o) ↔ (3o
∈ On ∧ 1o ∈ 3o)) |
| 14 | 9, 12, 13 | mpbir2an 711 |
. . . 4
⊢
3o ∈ (On ∖ 2o) |
| 15 | | omelon 9686 |
. . . . . 6
⊢ ω
∈ On |
| 16 | | peano1 7910 |
. . . . . 6
⊢ ∅
∈ ω |
| 17 | | ondif1 8539 |
. . . . . 6
⊢ (ω
∈ (On ∖ 1o) ↔ (ω ∈ On ∧ ∅
∈ ω)) |
| 18 | 15, 16, 17 | mpbir2an 711 |
. . . . 5
⊢ ω
∈ (On ∖ 1o) |
| 19 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑐 = ω → (2o
↑o 𝑐) =
(2o ↑o ω)) |
| 20 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑐 = ω → (3o
↑o 𝑐) =
(3o ↑o ω)) |
| 21 | 19, 20 | eleq12d 2835 |
. . . . . . . 8
⊢ (𝑐 = ω →
((2o ↑o 𝑐) ∈ (3o ↑o
𝑐) ↔ (2o
↑o ω) ∈ (3o ↑o
ω))) |
| 22 | 21 | bibi2d 342 |
. . . . . . 7
⊢ (𝑐 = ω →
((2o ∈ 3o ↔ (2o ↑o
𝑐) ∈ (3o
↑o 𝑐))
↔ (2o ∈ 3o ↔ (2o
↑o ω) ∈ (3o ↑o
ω)))) |
| 23 | 22 | notbid 318 |
. . . . . 6
⊢ (𝑐 = ω → (¬
(2o ∈ 3o ↔ (2o ↑o
𝑐) ∈ (3o
↑o 𝑐))
↔ ¬ (2o ∈ 3o ↔ (2o
↑o ω) ∈ (3o ↑o
ω)))) |
| 24 | 23 | rspcev 3622 |
. . . . 5
⊢ ((ω
∈ (On ∖ 1o) ∧ ¬ (2o ∈
3o ↔ (2o ↑o ω) ∈
(3o ↑o ω))) → ∃𝑐 ∈ (On ∖ 1o) ¬
(2o ∈ 3o ↔ (2o ↑o
𝑐) ∈ (3o
↑o 𝑐))) |
| 25 | 18, 24 | mpan 690 |
. . . 4
⊢ (¬
(2o ∈ 3o ↔ (2o ↑o
ω) ∈ (3o ↑o ω)) → ∃𝑐 ∈ (On ∖
1o) ¬ (2o ∈ 3o ↔ (2o
↑o 𝑐)
∈ (3o ↑o 𝑐))) |
| 26 | | eleq2 2830 |
. . . . . . . 8
⊢ (𝑏 = 3o →
(2o ∈ 𝑏
↔ 2o ∈ 3o)) |
| 27 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑏 = 3o → (𝑏 ↑o 𝑐) = (3o
↑o 𝑐)) |
| 28 | 27 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝑏 = 3o →
((2o ↑o 𝑐) ∈ (𝑏 ↑o 𝑐) ↔ (2o ↑o
𝑐) ∈ (3o
↑o 𝑐))) |
| 29 | 26, 28 | bibi12d 345 |
. . . . . . 7
⊢ (𝑏 = 3o →
((2o ∈ 𝑏
↔ (2o ↑o 𝑐) ∈ (𝑏 ↑o 𝑐)) ↔ (2o ∈ 3o
↔ (2o ↑o 𝑐) ∈ (3o ↑o
𝑐)))) |
| 30 | 29 | notbid 318 |
. . . . . 6
⊢ (𝑏 = 3o → (¬
(2o ∈ 𝑏
↔ (2o ↑o 𝑐) ∈ (𝑏 ↑o 𝑐)) ↔ ¬ (2o ∈
3o ↔ (2o ↑o 𝑐) ∈ (3o ↑o
𝑐)))) |
| 31 | 30 | rexbidv 3179 |
. . . . 5
⊢ (𝑏 = 3o →
(∃𝑐 ∈ (On
∖ 1o) ¬ (2o ∈ 𝑏 ↔ (2o ↑o
𝑐) ∈ (𝑏 ↑o 𝑐)) ↔ ∃𝑐 ∈ (On ∖
1o) ¬ (2o ∈ 3o ↔ (2o
↑o 𝑐)
∈ (3o ↑o 𝑐)))) |
| 32 | 31 | rspcev 3622 |
. . . 4
⊢
((3o ∈ (On ∖ 2o) ∧ ∃𝑐 ∈ (On ∖
1o) ¬ (2o ∈ 3o ↔ (2o
↑o 𝑐)
∈ (3o ↑o 𝑐))) → ∃𝑏 ∈ (On ∖
2o)∃𝑐
∈ (On ∖ 1o) ¬ (2o ∈ 𝑏 ↔ (2o
↑o 𝑐)
∈ (𝑏
↑o 𝑐))) |
| 33 | 14, 25, 32 | sylancr 587 |
. . 3
⊢ (¬
(2o ∈ 3o ↔ (2o ↑o
ω) ∈ (3o ↑o ω)) → ∃𝑏 ∈ (On ∖
2o)∃𝑐
∈ (On ∖ 1o) ¬ (2o ∈ 𝑏 ↔ (2o
↑o 𝑐)
∈ (𝑏
↑o 𝑐))) |
| 34 | | eleq1 2829 |
. . . . . . 7
⊢ (𝑎 = 2o → (𝑎 ∈ 𝑏 ↔ 2o ∈ 𝑏)) |
| 35 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑎 = 2o → (𝑎 ↑o 𝑐) = (2o
↑o 𝑐)) |
| 36 | 35 | eleq1d 2826 |
. . . . . . 7
⊢ (𝑎 = 2o → ((𝑎 ↑o 𝑐) ∈ (𝑏 ↑o 𝑐) ↔ (2o ↑o
𝑐) ∈ (𝑏 ↑o 𝑐))) |
| 37 | 34, 36 | bibi12d 345 |
. . . . . 6
⊢ (𝑎 = 2o → ((𝑎 ∈ 𝑏 ↔ (𝑎 ↑o 𝑐) ∈ (𝑏 ↑o 𝑐)) ↔ (2o ∈ 𝑏 ↔ (2o
↑o 𝑐)
∈ (𝑏
↑o 𝑐)))) |
| 38 | 37 | notbid 318 |
. . . . 5
⊢ (𝑎 = 2o → (¬
(𝑎 ∈ 𝑏 ↔ (𝑎 ↑o 𝑐) ∈ (𝑏 ↑o 𝑐)) ↔ ¬ (2o ∈ 𝑏 ↔ (2o
↑o 𝑐)
∈ (𝑏
↑o 𝑐)))) |
| 39 | 38 | 2rexbidv 3222 |
. . . 4
⊢ (𝑎 = 2o →
(∃𝑏 ∈ (On
∖ 2o)∃𝑐 ∈ (On ∖ 1o) ¬
(𝑎 ∈ 𝑏 ↔ (𝑎 ↑o 𝑐) ∈ (𝑏 ↑o 𝑐)) ↔ ∃𝑏 ∈ (On ∖
2o)∃𝑐
∈ (On ∖ 1o) ¬ (2o ∈ 𝑏 ↔ (2o
↑o 𝑐)
∈ (𝑏
↑o 𝑐)))) |
| 40 | 39 | rspcev 3622 |
. . 3
⊢
((2o ∈ (On ∖ 2o) ∧ ∃𝑏 ∈ (On ∖
2o)∃𝑐
∈ (On ∖ 1o) ¬ (2o ∈ 𝑏 ↔ (2o
↑o 𝑐)
∈ (𝑏
↑o 𝑐)))
→ ∃𝑎 ∈ (On
∖ 2o)∃𝑏 ∈ (On ∖
2o)∃𝑐
∈ (On ∖ 1o) ¬ (𝑎 ∈ 𝑏 ↔ (𝑎 ↑o 𝑐) ∈ (𝑏 ↑o 𝑐))) |
| 41 | 8, 33, 40 | sylancr 587 |
. 2
⊢ (¬
(2o ∈ 3o ↔ (2o ↑o
ω) ∈ (3o ↑o ω)) → ∃𝑎 ∈ (On ∖
2o)∃𝑏
∈ (On ∖ 2o)∃𝑐 ∈ (On ∖ 1o) ¬
(𝑎 ∈ 𝑏 ↔ (𝑎 ↑o 𝑐) ∈ (𝑏 ↑o 𝑐))) |
| 42 | 1, 41 | ax-mp 5 |
1
⊢
∃𝑎 ∈ (On
∖ 2o)∃𝑏 ∈ (On ∖
2o)∃𝑐
∈ (On ∖ 1o) ¬ (𝑎 ∈ 𝑏 ↔ (𝑎 ↑o 𝑐) ∈ (𝑏 ↑o 𝑐)) |