Metamath Proof Explorer

Theorem mrelatglbALT

Description: Greatest lower bounds in a Moore space are realized by intersections. (Contributed by Stefan O'Rear, 31-Jan-2015) (Proof shortened by Zhi Wang, 29-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses mreclatGOOD.i ⊢ I = toInc ⁡ C
mrelatglbALT.g ⊢ G = glb ⁡ I
Assertion mrelatglbALT ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C ∧ U ≠ ∅ → G ⁡ U = ⋂ U

Proof

Step Hyp Ref Expression
1 mreclatGOOD.i ⊢ I = toInc ⁡ C
2 mrelatglbALT.g ⊢ G = glb ⁡ I
3 simp1 ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C ∧ U ≠ ∅ → C ∈ Moore ⁡ X
4 simp2 ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C ∧ U ≠ ∅ → U ⊆ C
5 2 a1i ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C ∧ U ≠ ∅ → G = glb ⁡ I
6 mreintcl ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C ∧ U ≠ ∅ → ⋂ U ∈ C
7 unimax ⊢ ⋂ U ∈ C → ⋃ x ∈ C | x ⊆ ⋂ U = ⋂ U
8 7 eqcomd ⊢ ⋂ U ∈ C → ⋂ U = ⋃ x ∈ C | x ⊆ ⋂ U
9 6 8 syl ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C ∧ U ≠ ∅ → ⋂ U = ⋃ x ∈ C | x ⊆ ⋂ U
10 1 3 4 5 9 6 ipoglb ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C ∧ U ≠ ∅ → G ⁡ U = ⋂ U