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=BaseI
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≤Ix
12 11 rspec ⊢x∈∅→X≤Ix
13 12 adantl ⊢C∈Moore⁡X∧x∈∅→X≤Ix
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≤IX↔y⊆X
17 15 16 mpd3an3 ⊢C∈Moore⁡X∧y∈C→y≤IX↔y⊆X
18 14 17 mpbird ⊢C∈Moore⁡X∧y∈C→y≤IX
19 18 3adant3 ⊢C∈Moore⁡X∧y∈C∧∀x∈∅y≤Ix→y≤IX
20 3 4 5 7 9 10 13 19 posglbdg ⊢C∈Moore⁡X→G⁡∅=X