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

Metamath Proof Explorer

Theorem mrelatglb

Description: Greatest lower bounds in a Moore space are realized by intersections. (Contributed by Stefan O'Rear, 31-Jan-2015) See mrelatglbALT for an alternate proof.

Ref Expression
Hypotheses mreclat.i ⊢ 𝐼 = ( toInc ‘ 𝐶 )
mrelatglb.g ⊢ 𝐺 = ( glb ‘ 𝐼 )
Assertion mrelatglb ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) → ( 𝐺 ‘ 𝑈 ) = ∩ 𝑈 )

Proof

Step Hyp Ref Expression
1 mreclat.i ⊢ 𝐼 = ( toInc ‘ 𝐶 )
2 mrelatglb.g ⊢ 𝐺 = ( glb ‘ 𝐼 )
3 eqid ⊢ ( le ‘ 𝐼 ) = ( le ‘ 𝐼 )
4 1 ipobas ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐶 = ( Base ‘ 𝐼 ) )
5 4 3ad2ant1 ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) → 𝐶 = ( Base ‘ 𝐼 ) )
6 2 a1i ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) → 𝐺 = ( glb ‘ 𝐼 ) )
7 1 ipopos ⊢ 𝐼 ∈ Poset
8 7 a1i ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) → 𝐼 ∈ Poset )
9 simp2 ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) → 𝑈 ⊆ 𝐶 )
10 mreintcl ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) → ∩ 𝑈 ∈ 𝐶 )
11 intss1 ⊢ ( 𝑥 ∈ 𝑈 → ∩ 𝑈 ⊆ 𝑥 )
12 11 adantl ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) ∧ 𝑥 ∈ 𝑈 ) → ∩ 𝑈 ⊆ 𝑥 )
13 simpl1 ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) ∧ 𝑥 ∈ 𝑈 ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) )
14 10 adantr ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) ∧ 𝑥 ∈ 𝑈 ) → ∩ 𝑈 ∈ 𝐶 )
15 9 sselda ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ∈ 𝐶 )
16 1 3 ipole ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∩ 𝑈 ∈ 𝐶 ∧ 𝑥 ∈ 𝐶 ) → ( ∩ 𝑈 ( le ‘ 𝐼 ) 𝑥 ↔ ∩ 𝑈 ⊆ 𝑥 ) )
17 13 14 15 16 syl3anc ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) ∧ 𝑥 ∈ 𝑈 ) → ( ∩ 𝑈 ( le ‘ 𝐼 ) 𝑥 ↔ ∩ 𝑈 ⊆ 𝑥 ) )
18 12 17 mpbird ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) ∧ 𝑥 ∈ 𝑈 ) → ∩ 𝑈 ( le ‘ 𝐼 ) 𝑥 )
19 simpll1 ⊢ ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑥 ∈ 𝑈 ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) )
20 simplr ⊢ ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑥 ∈ 𝑈 ) → 𝑦 ∈ 𝐶 )
21 simpl2 ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) ∧ 𝑦 ∈ 𝐶 ) → 𝑈 ⊆ 𝐶 )
22 21 sselda ⊢ ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ∈ 𝐶 )
23 1 3 ipole ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐶 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑦 ( le ‘ 𝐼 ) 𝑥 ↔ 𝑦 ⊆ 𝑥 ) )
24 19 20 22 23 syl3anc ⊢ ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑥 ∈ 𝑈 ) → ( 𝑦 ( le ‘ 𝐼 ) 𝑥 ↔ 𝑦 ⊆ 𝑥 ) )
25 24 biimpd ⊢ ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) ∧ 𝑦 ∈ 𝐶 ) ∧ 𝑥 ∈ 𝑈 ) → ( 𝑦 ( le ‘ 𝐼 ) 𝑥 → 𝑦 ⊆ 𝑥 ) )
26 25 ralimdva ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) ∧ 𝑦 ∈ 𝐶 ) → ( ∀ 𝑥 ∈ 𝑈 𝑦 ( le ‘ 𝐼 ) 𝑥 → ∀ 𝑥 ∈ 𝑈 𝑦 ⊆ 𝑥 ) )
27 26 3impia ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) ∧ 𝑦 ∈ 𝐶 ∧ ∀ 𝑥 ∈ 𝑈 𝑦 ( le ‘ 𝐼 ) 𝑥 ) → ∀ 𝑥 ∈ 𝑈 𝑦 ⊆ 𝑥 )
28 ssint ⊢ ( 𝑦 ⊆ ∩ 𝑈 ↔ ∀ 𝑥 ∈ 𝑈 𝑦 ⊆ 𝑥 )
29 27 28 sylibr ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) ∧ 𝑦 ∈ 𝐶 ∧ ∀ 𝑥 ∈ 𝑈 𝑦 ( le ‘ 𝐼 ) 𝑥 ) → 𝑦 ⊆ ∩ 𝑈 )
30 simp11 ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) ∧ 𝑦 ∈ 𝐶 ∧ ∀ 𝑥 ∈ 𝑈 𝑦 ( le ‘ 𝐼 ) 𝑥 ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) )
31 simp2 ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) ∧ 𝑦 ∈ 𝐶 ∧ ∀ 𝑥 ∈ 𝑈 𝑦 ( le ‘ 𝐼 ) 𝑥 ) → 𝑦 ∈ 𝐶 )
32 10 3ad2ant1 ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) ∧ 𝑦 ∈ 𝐶 ∧ ∀ 𝑥 ∈ 𝑈 𝑦 ( le ‘ 𝐼 ) 𝑥 ) → ∩ 𝑈 ∈ 𝐶 )
33 1 3 ipole ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐶 ∧ ∩ 𝑈 ∈ 𝐶 ) → ( 𝑦 ( le ‘ 𝐼 ) ∩ 𝑈 ↔ 𝑦 ⊆ ∩ 𝑈 ) )
34 30 31 32 33 syl3anc ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) ∧ 𝑦 ∈ 𝐶 ∧ ∀ 𝑥 ∈ 𝑈 𝑦 ( le ‘ 𝐼 ) 𝑥 ) → ( 𝑦 ( le ‘ 𝐼 ) ∩ 𝑈 ↔ 𝑦 ⊆ ∩ 𝑈 ) )
35 29 34 mpbird ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) ∧ 𝑦 ∈ 𝐶 ∧ ∀ 𝑥 ∈ 𝑈 𝑦 ( le ‘ 𝐼 ) 𝑥 ) → 𝑦 ( le ‘ 𝐼 ) ∩ 𝑈 )
36 3 5 6 8 9 10 18 35 posglbdg ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) → ( 𝐺 ‘ 𝑈 ) = ∩ 𝑈 )