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	⊢ 𝐼 = ( toInc ‘ 𝐶 )
	mrelatglb.g	⊢ 𝐺 = ( glb ‘ 𝐼 )
Assertion	mrelatglb0	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( 𝐺 ‘ ∅ ) = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		mreclat.i	⊢ 𝐼 = ( toInc ‘ 𝐶 )
2		mrelatglb.g	⊢ 𝐺 = ( glb ‘ 𝐼 )
3		eqid	⊢ ( le ‘ 𝐼 ) = ( le ‘ 𝐼 )
4	1	ipobas	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐶 = ( Base ‘ 𝐼 ) )
5	2	a1i	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐺 = ( glb ‘ 𝐼 ) )
6	1	ipopos	⊢ 𝐼 ∈ Poset
7	6	a1i	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐼 ∈ Poset )
8		0ss	⊢ ∅ ⊆ 𝐶
9	8	a1i	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ∅ ⊆ 𝐶 )
10		mre1cl	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝑋 ∈ 𝐶 )
11		ral0	⊢ ∀ 𝑥 ∈ ∅ 𝑋 ( le ‘ 𝐼 ) 𝑥
12	11	rspec	⊢ ( 𝑥 ∈ ∅ → 𝑋 ( le ‘ 𝐼 ) 𝑥 )
13	12	adantl	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ∈ ∅ ) → 𝑋 ( le ‘ 𝐼 ) 𝑥 )
14		mress	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐶 ) → 𝑦 ⊆ 𝑋 )
15	10	adantr	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐶 ) → 𝑋 ∈ 𝐶 )
16	1 3	ipole	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐶 ∧ 𝑋 ∈ 𝐶 ) → ( 𝑦 ( le ‘ 𝐼 ) 𝑋 ↔ 𝑦 ⊆ 𝑋 ) )
17	15 16	mpd3an3	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐶 ) → ( 𝑦 ( le ‘ 𝐼 ) 𝑋 ↔ 𝑦 ⊆ 𝑋 ) )
18	14 17	mpbird	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐶 ) → 𝑦 ( le ‘ 𝐼 ) 𝑋 )
19	18	3adant3	⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐶 ∧ ∀ 𝑥 ∈ ∅ 𝑦 ( le ‘ 𝐼 ) 𝑥 ) → 𝑦 ( le ‘ 𝐼 ) 𝑋 )
20	3 4 5 7 9 10 13 19	posglbd	⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( 𝐺 ‘ ∅ ) = 𝑋 )