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

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 ⊢ 𝐼 = ( 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 posglbdg ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( 𝐺 ‘ ∅ ) = 𝑋 )