This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mrelatglbALT

Description: Greatest lower bounds in a Moore space are realized by intersections. (Contributed by Stefan O'Rear, 31-Jan-2015) (Proof shortened by Zhi Wang, 29-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses mreclatGOOD.i 
|- I = ( toInc ` C )
mrelatglbALT.g 
|- G = ( glb ` I )
Assertion mrelatglbALT 
|- ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) -> ( G ` U ) = |^| U )

Proof

Step Hyp Ref Expression
1 mreclatGOOD.i 
 |-  I = ( toInc ` C )
2 mrelatglbALT.g 
 |-  G = ( glb ` I )
3 simp1 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) -> C e. ( Moore ` X ) )
4 simp2 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) -> U C_ C )
5 2 a1i 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) -> G = ( glb ` I ) )
6 mreintcl 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) -> |^| U e. C )
7 unimax 
 |-  ( |^| U e. C -> U. { x e. C | x C_ |^| U } = |^| U )
8 7 eqcomd 
 |-  ( |^| U e. C -> |^| U = U. { x e. C | x C_ |^| U } )
9 6 8 syl 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) -> |^| U = U. { x e. C | x C_ |^| U } )
10 1 3 4 5 9 6 ipoglb 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ C /\ U =/= (/) ) -> ( G ` U ) = |^| U )