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	⊢ 𝐼 = ( toInc ‘ 𝐶 )
		mrelatglbALT.g	⊢ 𝐺 = ( glb ‘ 𝐼 )
	Assertion	mrelatglbALT	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) → ( 𝐺 ‘ 𝑈 ) = ∩ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		mreclatGOOD.i	⊢ 𝐼 = ( toInc ‘ 𝐶 )
2		mrelatglbALT.g	⊢ 𝐺 = ( glb ‘ 𝐼 )
3		simp1	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) )
4		simp2	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) → 𝑈 ⊆ 𝐶 )
5	2	a1i	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) → 𝐺 = ( glb ‘ 𝐼 ) )
6		mreintcl	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) → ∩ 𝑈 ∈ 𝐶 )
7		unimax	⊢ ( ∩ 𝑈 ∈ 𝐶 → ∪ { 𝑥 ∈ 𝐶 ∣ 𝑥 ⊆ ∩ 𝑈 } = ∩ 𝑈 )
8	7	eqcomd	⊢ ( ∩ 𝑈 ∈ 𝐶 → ∩ 𝑈 = ∪ { 𝑥 ∈ 𝐶 ∣ 𝑥 ⊆ ∩ 𝑈 } )
9	6 8	syl	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) → ∩ 𝑈 = ∪ { 𝑥 ∈ 𝐶 ∣ 𝑥 ⊆ ∩ 𝑈 } )
10	1 3 4 5 9 6	ipoglb	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) → ( 𝐺 ‘ 𝑈 ) = ∩ 𝑈 )