Proof of Theorem toslublem
| Step | Hyp | Ref
| Expression |
| 1 | | toslub.1 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ Toset) |
| 2 | 1 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → 𝐾 ∈ Toset) |
| 3 | | simplr 769 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → 𝑎 ∈ 𝐵) |
| 4 | | toslub.2 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
| 5 | 4 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝐴 ⊆ 𝐵) |
| 6 | 5 | sselda 3983 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ 𝐵) |
| 7 | | toslub.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐾) |
| 8 | | toslub.e |
. . . . . 6
⊢ ≤ =
(le‘𝐾) |
| 9 | | toslub.l |
. . . . . 6
⊢ < =
(lt‘𝐾) |
| 10 | 7, 8, 9 | tltnle 18467 |
. . . . 5
⊢ ((𝐾 ∈ Toset ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎 < 𝑏 ↔ ¬ 𝑏 ≤ 𝑎)) |
| 11 | 2, 3, 6, 10 | syl3anc 1373 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → (𝑎 < 𝑏 ↔ ¬ 𝑏 ≤ 𝑎)) |
| 12 | 11 | con2bid 354 |
. . 3
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → (𝑏 ≤ 𝑎 ↔ ¬ 𝑎 < 𝑏)) |
| 13 | 12 | ralbidva 3176 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑎 ↔ ∀𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏)) |
| 14 | 4 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → 𝐴 ⊆ 𝐵) |
| 15 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ 𝐴) |
| 16 | 14, 15 | sseldd 3984 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ 𝐵) |
| 17 | 7, 8, 9 | tltnle 18467 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ Toset ∧ 𝑐 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑐 < 𝑏 ↔ ¬ 𝑏 ≤ 𝑐)) |
| 18 | 1, 17 | syl3an1 1164 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑐 < 𝑏 ↔ ¬ 𝑏 ≤ 𝑐)) |
| 19 | 18 | 3expa 1119 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) → (𝑐 < 𝑏 ↔ ¬ 𝑏 ≤ 𝑐)) |
| 20 | 19 | con2bid 354 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) → (𝑏 ≤ 𝑐 ↔ ¬ 𝑐 < 𝑏)) |
| 21 | 16, 20 | syldan 591 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → (𝑏 ≤ 𝑐 ↔ ¬ 𝑐 < 𝑏)) |
| 22 | 21 | ralbidva 3176 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐵) → (∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 ↔ ∀𝑏 ∈ 𝐴 ¬ 𝑐 < 𝑏)) |
| 23 | | breq2 5147 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑑 → (𝑐 < 𝑏 ↔ 𝑐 < 𝑑)) |
| 24 | 23 | notbid 318 |
. . . . . . . . . 10
⊢ (𝑏 = 𝑑 → (¬ 𝑐 < 𝑏 ↔ ¬ 𝑐 < 𝑑)) |
| 25 | 24 | cbvralvw 3237 |
. . . . . . . . 9
⊢
(∀𝑏 ∈
𝐴 ¬ 𝑐 < 𝑏 ↔ ∀𝑑 ∈ 𝐴 ¬ 𝑐 < 𝑑) |
| 26 | | ralnex 3072 |
. . . . . . . . 9
⊢
(∀𝑑 ∈
𝐴 ¬ 𝑐 < 𝑑 ↔ ¬ ∃𝑑 ∈ 𝐴 𝑐 < 𝑑) |
| 27 | 25, 26 | bitri 275 |
. . . . . . . 8
⊢
(∀𝑏 ∈
𝐴 ¬ 𝑐 < 𝑏 ↔ ¬ ∃𝑑 ∈ 𝐴 𝑐 < 𝑑) |
| 28 | 22, 27 | bitrdi 287 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐵) → (∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 ↔ ¬ ∃𝑑 ∈ 𝐴 𝑐 < 𝑑)) |
| 29 | 28 | adantlr 715 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → (∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 ↔ ¬ ∃𝑑 ∈ 𝐴 𝑐 < 𝑑)) |
| 30 | 1 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → 𝐾 ∈ Toset) |
| 31 | | simpr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → 𝑐 ∈ 𝐵) |
| 32 | | simplr 769 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → 𝑎 ∈ 𝐵) |
| 33 | 7, 8, 9 | tltnle 18467 |
. . . . . . . 8
⊢ ((𝐾 ∈ Toset ∧ 𝑐 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) → (𝑐 < 𝑎 ↔ ¬ 𝑎 ≤ 𝑐)) |
| 34 | 30, 31, 32, 33 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → (𝑐 < 𝑎 ↔ ¬ 𝑎 ≤ 𝑐)) |
| 35 | 34 | con2bid 354 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → (𝑎 ≤ 𝑐 ↔ ¬ 𝑐 < 𝑎)) |
| 36 | 29, 35 | imbi12d 344 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → ((∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐) ↔ (¬ ∃𝑑 ∈ 𝐴 𝑐 < 𝑑 → ¬ 𝑐 < 𝑎))) |
| 37 | | con34b 316 |
. . . . 5
⊢ ((𝑐 < 𝑎 → ∃𝑑 ∈ 𝐴 𝑐 < 𝑑) ↔ (¬ ∃𝑑 ∈ 𝐴 𝑐 < 𝑑 → ¬ 𝑐 < 𝑎)) |
| 38 | 36, 37 | bitr4di 289 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → ((∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐) ↔ (𝑐 < 𝑎 → ∃𝑑 ∈ 𝐴 𝑐 < 𝑑))) |
| 39 | 38 | ralbidva 3176 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (∀𝑐 ∈ 𝐵 (∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐) ↔ ∀𝑐 ∈ 𝐵 (𝑐 < 𝑎 → ∃𝑑 ∈ 𝐴 𝑐 < 𝑑))) |
| 40 | | breq1 5146 |
. . . . 5
⊢ (𝑏 = 𝑐 → (𝑏 < 𝑎 ↔ 𝑐 < 𝑎)) |
| 41 | | breq1 5146 |
. . . . . 6
⊢ (𝑏 = 𝑐 → (𝑏 < 𝑑 ↔ 𝑐 < 𝑑)) |
| 42 | 41 | rexbidv 3179 |
. . . . 5
⊢ (𝑏 = 𝑐 → (∃𝑑 ∈ 𝐴 𝑏 < 𝑑 ↔ ∃𝑑 ∈ 𝐴 𝑐 < 𝑑)) |
| 43 | 40, 42 | imbi12d 344 |
. . . 4
⊢ (𝑏 = 𝑐 → ((𝑏 < 𝑎 → ∃𝑑 ∈ 𝐴 𝑏 < 𝑑) ↔ (𝑐 < 𝑎 → ∃𝑑 ∈ 𝐴 𝑐 < 𝑑))) |
| 44 | 43 | cbvralvw 3237 |
. . 3
⊢
(∀𝑏 ∈
𝐵 (𝑏 < 𝑎 → ∃𝑑 ∈ 𝐴 𝑏 < 𝑑) ↔ ∀𝑐 ∈ 𝐵 (𝑐 < 𝑎 → ∃𝑑 ∈ 𝐴 𝑐 < 𝑑)) |
| 45 | 39, 44 | bitr4di 289 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (∀𝑐 ∈ 𝐵 (∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐) ↔ ∀𝑏 ∈ 𝐵 (𝑏 < 𝑎 → ∃𝑑 ∈ 𝐴 𝑏 < 𝑑))) |
| 46 | 13, 45 | anbi12d 632 |
1
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑎 ∧ ∀𝑐 ∈ 𝐵 (∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐)) ↔ (∀𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏 ∧ ∀𝑏 ∈ 𝐵 (𝑏 < 𝑎 → ∃𝑑 ∈ 𝐴 𝑏 < 𝑑)))) |