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 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝐴 ⊆ 𝐵) |
6 | 5 | sselda 3917 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ 𝐵) |
7 | | toslub.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐾) |
8 | | toslub.e |
. . . . . 6
⊢ ≤ =
(le‘𝐾) |
9 | | toslub.l |
. . . . . 6
⊢ < =
(lt‘𝐾) |
10 | 7, 8, 9 | tltnle 17960 |
. . . . 5
⊢ ((𝐾 ∈ Toset ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑎 < 𝑏 ↔ ¬ 𝑏 ≤ 𝑎)) |
11 | 2, 3, 6, 10 | syl3anc 1373 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → (𝑎 < 𝑏 ↔ ¬ 𝑏 ≤ 𝑎)) |
12 | 11 | con2bid 358 |
. . 3
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → (𝑏 ≤ 𝑎 ↔ ¬ 𝑎 < 𝑏)) |
13 | 12 | ralbidva 3120 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑎 ↔ ∀𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏)) |
14 | 4 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → 𝐴 ⊆ 𝐵) |
15 | | simpr 488 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ 𝐴) |
16 | 14, 15 | sseldd 3918 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ 𝐵) |
17 | 7, 8, 9 | tltnle 17960 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ Toset ∧ 𝑐 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑐 < 𝑏 ↔ ¬ 𝑏 ≤ 𝑐)) |
18 | 1, 17 | syl3an1 1165 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑐 < 𝑏 ↔ ¬ 𝑏 ≤ 𝑐)) |
19 | 18 | 3expa 1120 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) → (𝑐 < 𝑏 ↔ ¬ 𝑏 ≤ 𝑐)) |
20 | 19 | con2bid 358 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) → (𝑏 ≤ 𝑐 ↔ ¬ 𝑐 < 𝑏)) |
21 | 16, 20 | syldan 594 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → (𝑏 ≤ 𝑐 ↔ ¬ 𝑐 < 𝑏)) |
22 | 21 | ralbidva 3120 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐵) → (∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 ↔ ∀𝑏 ∈ 𝐴 ¬ 𝑐 < 𝑏)) |
23 | | breq2 5073 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑑 → (𝑐 < 𝑏 ↔ 𝑐 < 𝑑)) |
24 | 23 | notbid 321 |
. . . . . . . . . 10
⊢ (𝑏 = 𝑑 → (¬ 𝑐 < 𝑏 ↔ ¬ 𝑐 < 𝑑)) |
25 | 24 | cbvralvw 3373 |
. . . . . . . . 9
⊢
(∀𝑏 ∈
𝐴 ¬ 𝑐 < 𝑏 ↔ ∀𝑑 ∈ 𝐴 ¬ 𝑐 < 𝑑) |
26 | | ralnex 3164 |
. . . . . . . . 9
⊢
(∀𝑑 ∈
𝐴 ¬ 𝑐 < 𝑑 ↔ ¬ ∃𝑑 ∈ 𝐴 𝑐 < 𝑑) |
27 | 25, 26 | bitri 278 |
. . . . . . . 8
⊢
(∀𝑏 ∈
𝐴 ¬ 𝑐 < 𝑏 ↔ ¬ ∃𝑑 ∈ 𝐴 𝑐 < 𝑑) |
28 | 22, 27 | bitrdi 290 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐵) → (∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 ↔ ¬ ∃𝑑 ∈ 𝐴 𝑐 < 𝑑)) |
29 | 28 | adantlr 715 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → (∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 ↔ ¬ ∃𝑑 ∈ 𝐴 𝑐 < 𝑑)) |
30 | 1 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → 𝐾 ∈ Toset) |
31 | | simpr 488 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → 𝑐 ∈ 𝐵) |
32 | | simplr 769 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → 𝑎 ∈ 𝐵) |
33 | 7, 8, 9 | tltnle 17960 |
. . . . . . . 8
⊢ ((𝐾 ∈ Toset ∧ 𝑐 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) → (𝑐 < 𝑎 ↔ ¬ 𝑎 ≤ 𝑐)) |
34 | 30, 31, 32, 33 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → (𝑐 < 𝑎 ↔ ¬ 𝑎 ≤ 𝑐)) |
35 | 34 | con2bid 358 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → (𝑎 ≤ 𝑐 ↔ ¬ 𝑐 < 𝑎)) |
36 | 29, 35 | imbi12d 348 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → ((∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐) ↔ (¬ ∃𝑑 ∈ 𝐴 𝑐 < 𝑑 → ¬ 𝑐 < 𝑎))) |
37 | | con34b 319 |
. . . . 5
⊢ ((𝑐 < 𝑎 → ∃𝑑 ∈ 𝐴 𝑐 < 𝑑) ↔ (¬ ∃𝑑 ∈ 𝐴 𝑐 < 𝑑 → ¬ 𝑐 < 𝑎)) |
38 | 36, 37 | bitr4di 292 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → ((∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐) ↔ (𝑐 < 𝑎 → ∃𝑑 ∈ 𝐴 𝑐 < 𝑑))) |
39 | 38 | ralbidva 3120 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (∀𝑐 ∈ 𝐵 (∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐) ↔ ∀𝑐 ∈ 𝐵 (𝑐 < 𝑎 → ∃𝑑 ∈ 𝐴 𝑐 < 𝑑))) |
40 | | breq1 5072 |
. . . . 5
⊢ (𝑏 = 𝑐 → (𝑏 < 𝑎 ↔ 𝑐 < 𝑎)) |
41 | | breq1 5072 |
. . . . . 6
⊢ (𝑏 = 𝑐 → (𝑏 < 𝑑 ↔ 𝑐 < 𝑑)) |
42 | 41 | rexbidv 3226 |
. . . . 5
⊢ (𝑏 = 𝑐 → (∃𝑑 ∈ 𝐴 𝑏 < 𝑑 ↔ ∃𝑑 ∈ 𝐴 𝑐 < 𝑑)) |
43 | 40, 42 | imbi12d 348 |
. . . 4
⊢ (𝑏 = 𝑐 → ((𝑏 < 𝑎 → ∃𝑑 ∈ 𝐴 𝑏 < 𝑑) ↔ (𝑐 < 𝑎 → ∃𝑑 ∈ 𝐴 𝑐 < 𝑑))) |
44 | 43 | cbvralvw 3373 |
. . 3
⊢
(∀𝑏 ∈
𝐵 (𝑏 < 𝑎 → ∃𝑑 ∈ 𝐴 𝑏 < 𝑑) ↔ ∀𝑐 ∈ 𝐵 (𝑐 < 𝑎 → ∃𝑑 ∈ 𝐴 𝑐 < 𝑑)) |
45 | 39, 44 | bitr4di 292 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (∀𝑐 ∈ 𝐵 (∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐) ↔ ∀𝑏 ∈ 𝐵 (𝑏 < 𝑎 → ∃𝑑 ∈ 𝐴 𝑏 < 𝑑))) |
46 | 13, 45 | anbi12d 634 |
1
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑎 ∧ ∀𝑐 ∈ 𝐵 (∀𝑏 ∈ 𝐴 𝑏 ≤ 𝑐 → 𝑎 ≤ 𝑐)) ↔ (∀𝑏 ∈ 𝐴 ¬ 𝑎 < 𝑏 ∧ ∀𝑏 ∈ 𝐵 (𝑏 < 𝑎 → ∃𝑑 ∈ 𝐴 𝑏 < 𝑑)))) |