Metamath Proof Explorer

Theorem mrelatglb0

Description: The empty intersection in a Moore space is realized by the base set. (Contributed by Stefan O'Rear, 31-Jan-2015)

Ref Expression
Hypotheses mreclat.i ⊢ I = toInc ⁡ C
mrelatglb.g ⊢ G = glb ⁡ I
Assertion mrelatglb0 ⊢ C ∈ Moore ⁡ X → G ⁡ ∅ = X

Proof

Step Hyp Ref Expression
1 mreclat.i ⊢ I = toInc ⁡ C
2 mrelatglb.g ⊢ G = glb ⁡ I
3 eqid ⊢ ≤ I = ≤ I
4 1 ipobas ⊢ C ∈ Moore ⁡ X → C = Base I
5 2 a1i ⊢ C ∈ Moore ⁡ X → G = glb ⁡ I
6 1 ipopos ⊢ I ∈ Poset
7 6 a1i ⊢ C ∈ Moore ⁡ X → I ∈ Poset
8 0ss ⊢ ∅ ⊆ C
9 8 a1i ⊢ C ∈ Moore ⁡ X → ∅ ⊆ C
10 mre1cl ⊢ C ∈ Moore ⁡ X → X ∈ C
11 ral0 ⊢ ∀ x ∈ ∅ X ≤ I x
12 11 rspec ⊢ x ∈ ∅ → X ≤ I x
13 12 adantl ⊢ C ∈ Moore ⁡ X ∧ x ∈ ∅ → X ≤ I x
14 mress ⊢ C ∈ Moore ⁡ X ∧ y ∈ C → y ⊆ X
15 10 adantr ⊢ C ∈ Moore ⁡ X ∧ y ∈ C → X ∈ C
16 1 3 ipole ⊢ C ∈ Moore ⁡ X ∧ y ∈ C ∧ X ∈ C → y ≤ I X ↔ y ⊆ X
17 15 16 mpd3an3 ⊢ C ∈ Moore ⁡ X ∧ y ∈ C → y ≤ I X ↔ y ⊆ X
18 14 17 mpbird ⊢ C ∈ Moore ⁡ X ∧ y ∈ C → y ≤ I X
19 18 3adant3 ⊢ C ∈ Moore ⁡ X ∧ y ∈ C ∧ ∀ x ∈ ∅ y ≤ I x → y ≤ I X
20 3 4 5 7 9 10 13 19 posglbdg ⊢ C ∈ Moore ⁡ X → G ⁡ ∅ = X