Metamath Proof Explorer


Theorem mrelatglb

Description: Greatest lower bounds in a Moore space are realized by intersections. (Contributed by Stefan O'Rear, 31-Jan-2015) See mrelatglbALT for an alternate proof.

Ref Expression
Hypotheses mreclat.i I = toInc C
mrelatglb.g G = glb I
Assertion mrelatglb C Moore X U C U G U = U

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 4 3ad2ant1 C Moore X U C U C = Base I
6 2 a1i C Moore X U C U G = glb I
7 1 ipopos I Poset
8 7 a1i C Moore X U C U I Poset
9 simp2 C Moore X U C U U C
10 mreintcl C Moore X U C U U C
11 intss1 x U U x
12 11 adantl C Moore X U C U x U U x
13 simpl1 C Moore X U C U x U C Moore X
14 10 adantr C Moore X U C U x U U C
15 9 sselda C Moore X U C U x U x C
16 1 3 ipole C Moore X U C x C U I x U x
17 13 14 15 16 syl3anc C Moore X U C U x U U I x U x
18 12 17 mpbird C Moore X U C U x U U I x
19 simpll1 C Moore X U C U y C x U C Moore X
20 simplr C Moore X U C U y C x U y C
21 simpl2 C Moore X U C U y C U C
22 21 sselda C Moore X U C U y C x U x C
23 1 3 ipole C Moore X y C x C y I x y x
24 19 20 22 23 syl3anc C Moore X U C U y C x U y I x y x
25 24 biimpd C Moore X U C U y C x U y I x y x
26 25 ralimdva C Moore X U C U y C x U y I x x U y x
27 26 3impia C Moore X U C U y C x U y I x x U y x
28 ssint y U x U y x
29 27 28 sylibr C Moore X U C U y C x U y I x y U
30 simp11 C Moore X U C U y C x U y I x C Moore X
31 simp2 C Moore X U C U y C x U y I x y C
32 10 3ad2ant1 C Moore X U C U y C x U y I x U C
33 1 3 ipole C Moore X y C U C y I U y U
34 30 31 32 33 syl3anc C Moore X U C U y C x U y I x y I U y U
35 29 34 mpbird C Moore X U C U y C x U y I x y I U
36 3 5 6 8 9 10 18 35 posglbdg C Moore X U C U G U = U