Metamath Proof Explorer

Theorem mrelatlubALT

Description: Least upper bounds in a Moore space are realized by the closure of the union. (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
mrelatlubALT.f ⊢ F = mrCls ⁡ C
mrelatlubALT.l ⊢ L = lub ⁡ I
Assertion mrelatlubALT ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C → L ⁡ U = F ⁡ ⋃ U

Proof

Step Hyp Ref Expression
1 mreclatGOOD.i ⊢ I = toInc ⁡ C
2 mrelatlubALT.f ⊢ F = mrCls ⁡ C
3 mrelatlubALT.l ⊢ L = lub ⁡ I
4 simpl ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C → C ∈ Moore ⁡ X
5 simpr ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C → U ⊆ C
6 3 a1i ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C → L = lub ⁡ I
7 mreuniss ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C → ⋃ U ⊆ X
8 2 mrcval ⊢ C ∈ Moore ⁡ X ∧ ⋃ U ⊆ X → F ⁡ ⋃ U = ⋂ x ∈ C | ⋃ U ⊆ x
9 7 8 syldan ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C → F ⁡ ⋃ U = ⋂ x ∈ C | ⋃ U ⊆ x
10 2 mrccl ⊢ C ∈ Moore ⁡ X ∧ ⋃ U ⊆ X → F ⁡ ⋃ U ∈ C
11 7 10 syldan ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C → F ⁡ ⋃ U ∈ C
12 1 4 5 6 9 11 ipolub ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C → L ⁡ U = F ⁡ ⋃ U