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 ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ∧ 𝑈 ≠ ∅ ) → ( 𝐺 ‘ 𝑈 ) = ∩ 𝑈 )

Metamath Proof Explorer

Theorem mrelatglb

Proof