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 e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) -> ( G ` U ) = |^| U )

Proof

Step Hyp Ref Expression
1 mreclat.i 
 |-  I = ( toInc ` C )
2 mrelatglb.g 
 |-  G = ( glb ` I )
3 eqid 
 |-  ( le ` I ) = ( le ` I )
4 1 ipobas 
 |-  ( C e. ( Moore ` X ) -> C = ( Base ` I ) )
5 4 3ad2ant1 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) -> C = ( Base ` I ) )
6 2 a1i 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) -> G = ( glb ` I ) )
7 1 ipopos 
 |-  I e. Poset
8 7 a1i 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) -> I e. Poset )
9 simp2 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) -> U C_ C )
10 mreintcl 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) -> |^| U e. C )
11 intss1 
 |-  ( x e. U -> |^| U C_ x )
12 11 adantl 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) /\ x e. U ) -> |^| U C_ x )
13 simpl1 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) /\ x e. U ) -> C e. ( Moore ` X ) )
14 10 adantr 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) /\ x e. U ) -> |^| U e. C )
15 9 sselda 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) /\ x e. U ) -> x e. C )
16 1 3 ipole 
 |-  ( ( C e. ( Moore ` X ) /\ |^| U e. C /\ x e. C ) -> ( |^| U ( le ` I ) x <-> |^| U C_ x ) )
17 13 14 15 16 syl3anc 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) /\ x e. U ) -> ( |^| U ( le ` I ) x <-> |^| U C_ x ) )
18 12 17 mpbird 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) /\ x e. U ) -> |^| U ( le ` I ) x )
19 simpll1 
 |-  ( ( ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) /\ y e. C ) /\ x e. U ) -> C e. ( Moore ` X ) )
20 simplr 
 |-  ( ( ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) /\ y e. C ) /\ x e. U ) -> y e. C )
21 simpl2 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) /\ y e. C ) -> U C_ C )
22 21 sselda 
 |-  ( ( ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) /\ y e. C ) /\ x e. U ) -> x e. C )
23 1 3 ipole 
 |-  ( ( C e. ( Moore ` X ) /\ y e. C /\ x e. C ) -> ( y ( le ` I ) x <-> y C_ x ) )
24 19 20 22 23 syl3anc 
 |-  ( ( ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) /\ y e. C ) /\ x e. U ) -> ( y ( le ` I ) x <-> y C_ x ) )
25 24 biimpd 
 |-  ( ( ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) /\ y e. C ) /\ x e. U ) -> ( y ( le ` I ) x -> y C_ x ) )
26 25 ralimdva 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) /\ y e. C ) -> ( A. x e. U y ( le ` I ) x -> A. x e. U y C_ x ) )
27 26 3impia 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) /\ y e. C /\ A. x e. U y ( le ` I ) x ) -> A. x e. U y C_ x )
28 ssint 
 |-  ( y C_ |^| U <-> A. x e. U y C_ x )
29 27 28 sylibr 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) /\ y e. C /\ A. x e. U y ( le ` I ) x ) -> y C_ |^| U )
30 simp11 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) /\ y e. C /\ A. x e. U y ( le ` I ) x ) -> C e. ( Moore ` X ) )
31 simp2 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) /\ y e. C /\ A. x e. U y ( le ` I ) x ) -> y e. C )
32 10 3ad2ant1 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) /\ y e. C /\ A. x e. U y ( le ` I ) x ) -> |^| U e. C )
33 1 3 ipole 
 |-  ( ( C e. ( Moore ` X ) /\ y e. C /\ |^| U e. C ) -> ( y ( le ` I ) |^| U <-> y C_ |^| U ) )
34 30 31 32 33 syl3anc 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) /\ y e. C /\ A. x e. U y ( le ` I ) x ) -> ( y ( le ` I ) |^| U <-> y C_ |^| U ) )
35 29 34 mpbird 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) /\ y e. C /\ A. x e. U y ( le ` I ) x ) -> y ( le ` I ) |^| U )
36 3 5 6 8 9 10 18 35 posglbdg 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) -> ( G ` U ) = |^| U )