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 e. ( Moore ` X ) -> ( G ` (/) ) = X )

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 2 a1i 
 |-  ( C e. ( Moore ` X ) -> G = ( glb ` I ) )
6 1 ipopos 
 |-  I e. Poset
7 6 a1i 
 |-  ( C e. ( Moore ` X ) -> I e. Poset )
8 0ss 
 |-  (/) C_ C
9 8 a1i 
 |-  ( C e. ( Moore ` X ) -> (/) C_ C )
10 mre1cl 
 |-  ( C e. ( Moore ` X ) -> X e. C )
11 ral0 
 |-  A. x e. (/) X ( le ` I ) x
12 11 rspec 
 |-  ( x e. (/) -> X ( le ` I ) x )
13 12 adantl 
 |-  ( ( C e. ( Moore ` X ) /\ x e. (/) ) -> X ( le ` I ) x )
14 mress 
 |-  ( ( C e. ( Moore ` X ) /\ y e. C ) -> y C_ X )
15 10 adantr 
 |-  ( ( C e. ( Moore ` X ) /\ y e. C ) -> X e. C )
16 1 3 ipole 
 |-  ( ( C e. ( Moore ` X ) /\ y e. C /\ X e. C ) -> ( y ( le ` I ) X <-> y C_ X ) )
17 15 16 mpd3an3 
 |-  ( ( C e. ( Moore ` X ) /\ y e. C ) -> ( y ( le ` I ) X <-> y C_ X ) )
18 14 17 mpbird 
 |-  ( ( C e. ( Moore ` X ) /\ y e. C ) -> y ( le ` I ) X )
19 18 3adant3 
 |-  ( ( C e. ( Moore ` X ) /\ y e. C /\ A. x e. (/) y ( le ` I ) x ) -> y ( le ` I ) X )
20 3 4 5 7 9 10 13 19 posglbd 
 |-  ( C e. ( Moore ` X ) -> ( G ` (/) ) = X )