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 )