Metamath Proof Explorer

Theorem mrelatlub

Description: Least upper bounds in a Moore space are realized by the closure of the union. (Contributed by Stefan O'Rear, 31-Jan-2015) See mrelatlubALT for an alternate proof.

Ref Expression
Hypotheses mreclat.i ⊢ I = toInc ⁡ C
mrelatlub.f ⊢ F = mrCls ⁡ C
mrelatlub.l ⊢ L = lub ⁡ I
Assertion mrelatlub ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C → L ⁡ U = F ⁡ ⋃ U

Proof

Step Hyp Ref Expression
1 mreclat.i ⊢ I = toInc ⁡ C
2 mrelatlub.f ⊢ F = mrCls ⁡ C
3 mrelatlub.l ⊢ L = lub ⁡ I
4 eqid ⊢ ≤ I = ≤ I
5 1 ipobas ⊢ C ∈ Moore ⁡ X → C = Base I
6 5 adantr ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C → C = Base I
7 3 a1i ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C → L = lub ⁡ I
8 1 ipopos ⊢ I ∈ Poset
9 8 a1i ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C → I ∈ Poset
10 simpr ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C → U ⊆ C
11 uniss ⊢ U ⊆ C → ⋃ U ⊆ ⋃ C
12 11 adantl ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C → ⋃ U ⊆ ⋃ C
13 mreuni ⊢ C ∈ Moore ⁡ X → ⋃ C = X
14 13 adantr ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C → ⋃ C = X
15 12 14 sseqtrd ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C → ⋃ U ⊆ X
16 2 mrccl ⊢ C ∈ Moore ⁡ X ∧ ⋃ U ⊆ X → F ⁡ ⋃ U ∈ C
17 15 16 syldan ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C → F ⁡ ⋃ U ∈ C
18 elssuni ⊢ x ∈ U → x ⊆ ⋃ U
19 2 mrcssid ⊢ C ∈ Moore ⁡ X ∧ ⋃ U ⊆ X → ⋃ U ⊆ F ⁡ ⋃ U
20 15 19 syldan ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C → ⋃ U ⊆ F ⁡ ⋃ U
21 18 20 sylan9ssr ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C ∧ x ∈ U → x ⊆ F ⁡ ⋃ U
22 simpll ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C ∧ x ∈ U → C ∈ Moore ⁡ X
23 10 sselda ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C ∧ x ∈ U → x ∈ C
24 17 adantr ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C ∧ x ∈ U → F ⁡ ⋃ U ∈ C
25 1 4 ipole ⊢ C ∈ Moore ⁡ X ∧ x ∈ C ∧ F ⁡ ⋃ U ∈ C → x ≤ I F ⁡ ⋃ U ↔ x ⊆ F ⁡ ⋃ U
26 22 23 24 25 syl3anc ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C ∧ x ∈ U → x ≤ I F ⁡ ⋃ U ↔ x ⊆ F ⁡ ⋃ U
27 21 26 mpbird ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C ∧ x ∈ U → x ≤ I F ⁡ ⋃ U
28 simp1l ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C ∧ y ∈ C ∧ ∀ x ∈ U x ≤ I y → C ∈ Moore ⁡ X
29 simplll ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C ∧ y ∈ C ∧ x ∈ U → C ∈ Moore ⁡ X
30 simplr ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C ∧ y ∈ C → U ⊆ C
31 30 sselda ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C ∧ y ∈ C ∧ x ∈ U → x ∈ C
32 simplr ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C ∧ y ∈ C ∧ x ∈ U → y ∈ C
33 1 4 ipole ⊢ C ∈ Moore ⁡ X ∧ x ∈ C ∧ y ∈ C → x ≤ I y ↔ x ⊆ y
34 29 31 32 33 syl3anc ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C ∧ y ∈ C ∧ x ∈ U → x ≤ I y ↔ x ⊆ y
35 34 biimpd ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C ∧ y ∈ C ∧ x ∈ U → x ≤ I y → x ⊆ y
36 35 ralimdva ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C ∧ y ∈ C → ∀ x ∈ U x ≤ I y → ∀ x ∈ U x ⊆ y
37 36 3impia ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C ∧ y ∈ C ∧ ∀ x ∈ U x ≤ I y → ∀ x ∈ U x ⊆ y
38 unissb ⊢ ⋃ U ⊆ y ↔ ∀ x ∈ U x ⊆ y
39 37 38 sylibr ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C ∧ y ∈ C ∧ ∀ x ∈ U x ≤ I y → ⋃ U ⊆ y
40 simp2 ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C ∧ y ∈ C ∧ ∀ x ∈ U x ≤ I y → y ∈ C
41 2 mrcsscl ⊢ C ∈ Moore ⁡ X ∧ ⋃ U ⊆ y ∧ y ∈ C → F ⁡ ⋃ U ⊆ y
42 28 39 40 41 syl3anc ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C ∧ y ∈ C ∧ ∀ x ∈ U x ≤ I y → F ⁡ ⋃ U ⊆ y
43 17 3ad2ant1 ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C ∧ y ∈ C ∧ ∀ x ∈ U x ≤ I y → F ⁡ ⋃ U ∈ C
44 1 4 ipole ⊢ C ∈ Moore ⁡ X ∧ F ⁡ ⋃ U ∈ C ∧ y ∈ C → F ⁡ ⋃ U ≤ I y ↔ F ⁡ ⋃ U ⊆ y
45 28 43 40 44 syl3anc ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C ∧ y ∈ C ∧ ∀ x ∈ U x ≤ I y → F ⁡ ⋃ U ≤ I y ↔ F ⁡ ⋃ U ⊆ y
46 42 45 mpbird ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C ∧ y ∈ C ∧ ∀ x ∈ U x ≤ I y → F ⁡ ⋃ U ≤ I y
47 4 6 7 9 10 17 27 46 poslubdg ⊢ C ∈ Moore ⁡ X ∧ U ⊆ C → L ⁡ U = F ⁡ ⋃ U