Proof of Theorem tosglblem
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | tosglb.1 | . . . . . . 7
⊢ (𝜑 → 𝐾 ∈ Toset) | 
| 2 | 1 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → 𝐾 ∈ Toset) | 
| 3 |  | tosglb.2 | . . . . . . . 8
⊢ (𝜑 → 𝐴 ⊆ 𝐵) | 
| 4 | 3 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝐴 ⊆ 𝐵) | 
| 5 | 4 | sselda 3982 | . . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ 𝐵) | 
| 6 |  | simplr 768 | . . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → 𝑎 ∈ 𝐵) | 
| 7 |  | tosglb.b | . . . . . . 7
⊢ 𝐵 = (Base‘𝐾) | 
| 8 |  | tosglb.e | . . . . . . 7
⊢  ≤ =
(le‘𝐾) | 
| 9 |  | tosglb.l | . . . . . . 7
⊢  < =
(lt‘𝐾) | 
| 10 | 7, 8, 9 | tltnle 18468 | . . . . . 6
⊢ ((𝐾 ∈ Toset ∧ 𝑏 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵) → (𝑏 < 𝑎 ↔ ¬ 𝑎 ≤ 𝑏)) | 
| 11 | 2, 5, 6, 10 | syl3anc 1372 | . . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → (𝑏 < 𝑎 ↔ ¬ 𝑎 ≤ 𝑏)) | 
| 12 | 11 | con2bid 354 | . . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → (𝑎 ≤ 𝑏 ↔ ¬ 𝑏 < 𝑎)) | 
| 13 | 12 | ralbidva 3175 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (∀𝑏 ∈ 𝐴 𝑎 ≤ 𝑏 ↔ ∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎)) | 
| 14 | 3 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → 𝐴 ⊆ 𝐵) | 
| 15 |  | simpr 484 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ 𝐴) | 
| 16 | 14, 15 | sseldd 3983 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ 𝐵) | 
| 17 | 7, 8, 9 | tltnle 18468 | . . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ Toset ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) → (𝑏 < 𝑐 ↔ ¬ 𝑐 ≤ 𝑏)) | 
| 18 | 1, 17 | syl3an1 1163 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) → (𝑏 < 𝑐 ↔ ¬ 𝑐 ≤ 𝑏)) | 
| 19 | 18 | 3com23 1126 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑏 < 𝑐 ↔ ¬ 𝑐 ≤ 𝑏)) | 
| 20 | 19 | 3expa 1118 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) → (𝑏 < 𝑐 ↔ ¬ 𝑐 ≤ 𝑏)) | 
| 21 | 20 | con2bid 354 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) → (𝑐 ≤ 𝑏 ↔ ¬ 𝑏 < 𝑐)) | 
| 22 | 16, 21 | syldan 591 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐵) ∧ 𝑏 ∈ 𝐴) → (𝑐 ≤ 𝑏 ↔ ¬ 𝑏 < 𝑐)) | 
| 23 | 22 | ralbidva 3175 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐵) → (∀𝑏 ∈ 𝐴 𝑐 ≤ 𝑏 ↔ ∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑐)) | 
| 24 |  | breq1 5145 | . . . . . . . . . . . 12
⊢ (𝑏 = 𝑑 → (𝑏 < 𝑐 ↔ 𝑑 < 𝑐)) | 
| 25 | 24 | notbid 318 | . . . . . . . . . . 11
⊢ (𝑏 = 𝑑 → (¬ 𝑏 < 𝑐 ↔ ¬ 𝑑 < 𝑐)) | 
| 26 | 25 | cbvralvw 3236 | . . . . . . . . . 10
⊢
(∀𝑏 ∈
𝐴 ¬ 𝑏 < 𝑐 ↔ ∀𝑑 ∈ 𝐴 ¬ 𝑑 < 𝑐) | 
| 27 |  | ralnex 3071 | . . . . . . . . . 10
⊢
(∀𝑑 ∈
𝐴 ¬ 𝑑 < 𝑐 ↔ ¬ ∃𝑑 ∈ 𝐴 𝑑 < 𝑐) | 
| 28 | 26, 27 | bitri 275 | . . . . . . . . 9
⊢
(∀𝑏 ∈
𝐴 ¬ 𝑏 < 𝑐 ↔ ¬ ∃𝑑 ∈ 𝐴 𝑑 < 𝑐) | 
| 29 | 23, 28 | bitrdi 287 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐵) → (∀𝑏 ∈ 𝐴 𝑐 ≤ 𝑏 ↔ ¬ ∃𝑑 ∈ 𝐴 𝑑 < 𝑐)) | 
| 30 | 29 | adantlr 715 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → (∀𝑏 ∈ 𝐴 𝑐 ≤ 𝑏 ↔ ¬ ∃𝑑 ∈ 𝐴 𝑑 < 𝑐)) | 
| 31 | 1 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → 𝐾 ∈ Toset) | 
| 32 |  | simplr 768 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → 𝑎 ∈ 𝐵) | 
| 33 |  | simpr 484 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → 𝑐 ∈ 𝐵) | 
| 34 | 7, 8, 9 | tltnle 18468 | . . . . . . . . 9
⊢ ((𝐾 ∈ Toset ∧ 𝑎 ∈ 𝐵 ∧ 𝑐 ∈ 𝐵) → (𝑎 < 𝑐 ↔ ¬ 𝑐 ≤ 𝑎)) | 
| 35 | 31, 32, 33, 34 | syl3anc 1372 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → (𝑎 < 𝑐 ↔ ¬ 𝑐 ≤ 𝑎)) | 
| 36 | 35 | con2bid 354 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → (𝑐 ≤ 𝑎 ↔ ¬ 𝑎 < 𝑐)) | 
| 37 | 30, 36 | imbi12d 344 | . . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → ((∀𝑏 ∈ 𝐴 𝑐 ≤ 𝑏 → 𝑐 ≤ 𝑎) ↔ (¬ ∃𝑑 ∈ 𝐴 𝑑 < 𝑐 → ¬ 𝑎 < 𝑐))) | 
| 38 |  | con34b 316 | . . . . . 6
⊢ ((𝑎 < 𝑐 → ∃𝑑 ∈ 𝐴 𝑑 < 𝑐) ↔ (¬ ∃𝑑 ∈ 𝐴 𝑑 < 𝑐 → ¬ 𝑎 < 𝑐)) | 
| 39 | 37, 38 | bitr4di 289 | . . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → ((∀𝑏 ∈ 𝐴 𝑐 ≤ 𝑏 → 𝑐 ≤ 𝑎) ↔ (𝑎 < 𝑐 → ∃𝑑 ∈ 𝐴 𝑑 < 𝑐))) | 
| 40 | 39 | ralbidva 3175 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (∀𝑐 ∈ 𝐵 (∀𝑏 ∈ 𝐴 𝑐 ≤ 𝑏 → 𝑐 ≤ 𝑎) ↔ ∀𝑐 ∈ 𝐵 (𝑎 < 𝑐 → ∃𝑑 ∈ 𝐴 𝑑 < 𝑐))) | 
| 41 |  | breq2 5146 | . . . . . 6
⊢ (𝑏 = 𝑐 → (𝑎 < 𝑏 ↔ 𝑎 < 𝑐)) | 
| 42 |  | breq2 5146 | . . . . . . 7
⊢ (𝑏 = 𝑐 → (𝑑 < 𝑏 ↔ 𝑑 < 𝑐)) | 
| 43 | 42 | rexbidv 3178 | . . . . . 6
⊢ (𝑏 = 𝑐 → (∃𝑑 ∈ 𝐴 𝑑 < 𝑏 ↔ ∃𝑑 ∈ 𝐴 𝑑 < 𝑐)) | 
| 44 | 41, 43 | imbi12d 344 | . . . . 5
⊢ (𝑏 = 𝑐 → ((𝑎 < 𝑏 → ∃𝑑 ∈ 𝐴 𝑑 < 𝑏) ↔ (𝑎 < 𝑐 → ∃𝑑 ∈ 𝐴 𝑑 < 𝑐))) | 
| 45 | 44 | cbvralvw 3236 | . . . 4
⊢
(∀𝑏 ∈
𝐵 (𝑎 < 𝑏 → ∃𝑑 ∈ 𝐴 𝑑 < 𝑏) ↔ ∀𝑐 ∈ 𝐵 (𝑎 < 𝑐 → ∃𝑑 ∈ 𝐴 𝑑 < 𝑐)) | 
| 46 | 40, 45 | bitr4di 289 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (∀𝑐 ∈ 𝐵 (∀𝑏 ∈ 𝐴 𝑐 ≤ 𝑏 → 𝑐 ≤ 𝑎) ↔ ∀𝑏 ∈ 𝐵 (𝑎 < 𝑏 → ∃𝑑 ∈ 𝐴 𝑑 < 𝑏))) | 
| 47 | 13, 46 | anbi12d 632 | . 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((∀𝑏 ∈ 𝐴 𝑎 ≤ 𝑏 ∧ ∀𝑐 ∈ 𝐵 (∀𝑏 ∈ 𝐴 𝑐 ≤ 𝑏 → 𝑐 ≤ 𝑎)) ↔ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ 𝐵 (𝑎 < 𝑏 → ∃𝑑 ∈ 𝐴 𝑑 < 𝑏)))) | 
| 48 |  | vex 3483 | . . . . . 6
⊢ 𝑎 ∈ V | 
| 49 |  | vex 3483 | . . . . . 6
⊢ 𝑏 ∈ V | 
| 50 | 48, 49 | brcnv 5892 | . . . . 5
⊢ (𝑎◡ < 𝑏 ↔ 𝑏 < 𝑎) | 
| 51 | 50 | notbii 320 | . . . 4
⊢ (¬
𝑎◡ < 𝑏 ↔ ¬ 𝑏 < 𝑎) | 
| 52 | 51 | ralbii 3092 | . . 3
⊢
(∀𝑏 ∈
𝐴 ¬ 𝑎◡
<
𝑏 ↔ ∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎) | 
| 53 | 49, 48 | brcnv 5892 | . . . . 5
⊢ (𝑏◡ < 𝑎 ↔ 𝑎 < 𝑏) | 
| 54 |  | vex 3483 | . . . . . . 7
⊢ 𝑑 ∈ V | 
| 55 | 49, 54 | brcnv 5892 | . . . . . 6
⊢ (𝑏◡ < 𝑑 ↔ 𝑑 < 𝑏) | 
| 56 | 55 | rexbii 3093 | . . . . 5
⊢
(∃𝑑 ∈
𝐴 𝑏◡
<
𝑑 ↔ ∃𝑑 ∈ 𝐴 𝑑 < 𝑏) | 
| 57 | 53, 56 | imbi12i 350 | . . . 4
⊢ ((𝑏◡ < 𝑎 → ∃𝑑 ∈ 𝐴 𝑏◡
<
𝑑) ↔ (𝑎 < 𝑏 → ∃𝑑 ∈ 𝐴 𝑑 < 𝑏)) | 
| 58 | 57 | ralbii 3092 | . . 3
⊢
(∀𝑏 ∈
𝐵 (𝑏◡
<
𝑎 → ∃𝑑 ∈ 𝐴 𝑏◡
<
𝑑) ↔ ∀𝑏 ∈ 𝐵 (𝑎 < 𝑏 → ∃𝑑 ∈ 𝐴 𝑑 < 𝑏)) | 
| 59 | 52, 58 | anbi12i 628 | . 2
⊢
((∀𝑏 ∈
𝐴 ¬ 𝑎◡
<
𝑏 ∧ ∀𝑏 ∈ 𝐵 (𝑏◡
<
𝑎 → ∃𝑑 ∈ 𝐴 𝑏◡
<
𝑑)) ↔ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ 𝐵 (𝑎 < 𝑏 → ∃𝑑 ∈ 𝐴 𝑑 < 𝑏))) | 
| 60 | 47, 59 | bitr4di 289 | 1
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((∀𝑏 ∈ 𝐴 𝑎 ≤ 𝑏 ∧ ∀𝑐 ∈ 𝐵 (∀𝑏 ∈ 𝐴 𝑐 ≤ 𝑏 → 𝑐 ≤ 𝑎)) ↔ (∀𝑏 ∈ 𝐴 ¬ 𝑎◡
<
𝑏 ∧ ∀𝑏 ∈ 𝐵 (𝑏◡
<
𝑎 → ∃𝑑 ∈ 𝐴 𝑏◡
<
𝑑)))) |