Proof of Theorem glbeldm2d
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2737 | . . 3
⊢
(Base‘𝐾) =
(Base‘𝐾) | 
| 2 |  | eqid 2737 | . . 3
⊢
(le‘𝐾) =
(le‘𝐾) | 
| 3 |  | eqid 2737 | . . 3
⊢
(glb‘𝐾) =
(glb‘𝐾) | 
| 4 |  | biid 261 | . . 3
⊢
((∀𝑦 ∈
𝑆 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑆 𝑧(le‘𝐾)𝑦 → 𝑧(le‘𝐾)𝑥)) ↔ (∀𝑦 ∈ 𝑆 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑆 𝑧(le‘𝐾)𝑦 → 𝑧(le‘𝐾)𝑥))) | 
| 5 |  | glbeldm2d.k | . . 3
⊢ (𝜑 → 𝐾 ∈ Poset) | 
| 6 | 1, 2, 3, 4, 5 | glbeldm2 48854 | . 2
⊢ (𝜑 → (𝑆 ∈ dom (glb‘𝐾) ↔ (𝑆 ⊆ (Base‘𝐾) ∧ ∃𝑥 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑆 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑆 𝑧(le‘𝐾)𝑦 → 𝑧(le‘𝐾)𝑥))))) | 
| 7 |  | glbeldm2d.g | . . . 4
⊢ (𝜑 → 𝐺 = (glb‘𝐾)) | 
| 8 | 7 | dmeqd 5916 | . . 3
⊢ (𝜑 → dom 𝐺 = dom (glb‘𝐾)) | 
| 9 | 8 | eleq2d 2827 | . 2
⊢ (𝜑 → (𝑆 ∈ dom 𝐺 ↔ 𝑆 ∈ dom (glb‘𝐾))) | 
| 10 |  | lubeldm2d.b | . . . 4
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) | 
| 11 | 10 | sseq2d 4016 | . . 3
⊢ (𝜑 → (𝑆 ⊆ 𝐵 ↔ 𝑆 ⊆ (Base‘𝐾))) | 
| 12 |  | glbeldm2d.p | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝜓 ↔ (∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥)))) | 
| 13 |  | lubeldm2d.l | . . . . . . . . . . 11
⊢ (𝜑 → ≤ = (le‘𝐾)) | 
| 14 | 13 | breqd 5154 | . . . . . . . . . 10
⊢ (𝜑 → (𝑥 ≤ 𝑦 ↔ 𝑥(le‘𝐾)𝑦)) | 
| 15 | 14 | ralbidv 3178 | . . . . . . . . 9
⊢ (𝜑 → (∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ↔ ∀𝑦 ∈ 𝑆 𝑥(le‘𝐾)𝑦)) | 
| 16 | 13 | breqd 5154 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑧 ≤ 𝑦 ↔ 𝑧(le‘𝐾)𝑦)) | 
| 17 | 16 | ralbidv 3178 | . . . . . . . . . . 11
⊢ (𝜑 → (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 ↔ ∀𝑦 ∈ 𝑆 𝑧(le‘𝐾)𝑦)) | 
| 18 | 13 | breqd 5154 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑧 ≤ 𝑥 ↔ 𝑧(le‘𝐾)𝑥)) | 
| 19 | 17, 18 | imbi12d 344 | . . . . . . . . . 10
⊢ (𝜑 → ((∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥) ↔ (∀𝑦 ∈ 𝑆 𝑧(le‘𝐾)𝑦 → 𝑧(le‘𝐾)𝑥))) | 
| 20 | 10, 19 | raleqbidv 3346 | . . . . . . . . 9
⊢ (𝜑 → (∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥) ↔ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑆 𝑧(le‘𝐾)𝑦 → 𝑧(le‘𝐾)𝑥))) | 
| 21 | 15, 20 | anbi12d 632 | . . . . . . . 8
⊢ (𝜑 → ((∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥)) ↔ (∀𝑦 ∈ 𝑆 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑆 𝑧(le‘𝐾)𝑦 → 𝑧(le‘𝐾)𝑥)))) | 
| 22 | 21 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((∀𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥)) ↔ (∀𝑦 ∈ 𝑆 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑆 𝑧(le‘𝐾)𝑦 → 𝑧(le‘𝐾)𝑥)))) | 
| 23 | 12, 22 | bitrd 279 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝜓 ↔ (∀𝑦 ∈ 𝑆 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑆 𝑧(le‘𝐾)𝑦 → 𝑧(le‘𝐾)𝑥)))) | 
| 24 | 23 | pm5.32da 579 | . . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ (∀𝑦 ∈ 𝑆 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑆 𝑧(le‘𝐾)𝑦 → 𝑧(le‘𝐾)𝑥))))) | 
| 25 | 10 | eleq2d 2827 | . . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ (Base‘𝐾))) | 
| 26 | 25 | anbi1d 631 | . . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ (∀𝑦 ∈ 𝑆 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑆 𝑧(le‘𝐾)𝑦 → 𝑧(le‘𝐾)𝑥))) ↔ (𝑥 ∈ (Base‘𝐾) ∧ (∀𝑦 ∈ 𝑆 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑆 𝑧(le‘𝐾)𝑦 → 𝑧(le‘𝐾)𝑥))))) | 
| 27 | 24, 26 | bitrd 279 | . . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝜓) ↔ (𝑥 ∈ (Base‘𝐾) ∧ (∀𝑦 ∈ 𝑆 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑆 𝑧(le‘𝐾)𝑦 → 𝑧(le‘𝐾)𝑥))))) | 
| 28 | 27 | rexbidv2 3175 | . . 3
⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑆 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑆 𝑧(le‘𝐾)𝑦 → 𝑧(le‘𝐾)𝑥)))) | 
| 29 | 11, 28 | anbi12d 632 | . 2
⊢ (𝜑 → ((𝑆 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐵 𝜓) ↔ (𝑆 ⊆ (Base‘𝐾) ∧ ∃𝑥 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑆 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑆 𝑧(le‘𝐾)𝑦 → 𝑧(le‘𝐾)𝑥))))) | 
| 30 | 6, 9, 29 | 3bitr4d 311 | 1
⊢ (𝜑 → (𝑆 ∈ dom 𝐺 ↔ (𝑆 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐵 𝜓))) |