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	$⊢ I = toInc (C)$
	mrelatglb.g	$⊢ G = glb (I)$
Assertion	mrelatglb	$⊢ (C \in Moore (X) \land U \subseteq C \land U \neq \emptyset) \to G (U) = ⋂ U$

Proof

Step	Hyp	Ref	Expression
1		mreclat.i	$⊢ I = toInc (C)$
2		mrelatglb.g	$⊢ G = glb (I)$
3		eqid	$⊢ \leq_{I} = \leq_{I}$
4	1	ipobas	$⊢ C \in Moore (X) \to C = {Base}_{I}$
5	4	3ad2ant1	$⊢ (C \in Moore (X) \land U \subseteq C \land U \neq \emptyset) \to C = {Base}_{I}$
6	2	a1i	$⊢ (C \in Moore (X) \land U \subseteq C \land U \neq \emptyset) \to G = glb (I)$
7	1	ipopos	$⊢ I \in Poset$
8	7	a1i	$⊢ (C \in Moore (X) \land U \subseteq C \land U \neq \emptyset) \to I \in Poset$
9		simp2	$⊢ (C \in Moore (X) \land U \subseteq C \land U \neq \emptyset) \to U \subseteq C$
10		mreintcl	$⊢ (C \in Moore (X) \land U \subseteq C \land U \neq \emptyset) \to ⋂ U \in C$
11		intss1	$⊢ x \in U \to ⋂ U \subseteq x$
12	11	adantl	$⊢ ((C \in Moore (X) \land U \subseteq C \land U \neq \emptyset) \land x \in U) \to ⋂ U \subseteq x$
13		simpl1	$⊢ ((C \in Moore (X) \land U \subseteq C \land U \neq \emptyset) \land x \in U) \to C \in Moore (X)$
14	10	adantr	$⊢ ((C \in Moore (X) \land U \subseteq C \land U \neq \emptyset) \land x \in U) \to ⋂ U \in C$
15	9	sselda	$⊢ ((C \in Moore (X) \land U \subseteq C \land U \neq \emptyset) \land x \in U) \to x \in C$
16	1 3	ipole	$⊢ (C \in Moore (X) \land ⋂ U \in C \land x \in C) \to (⋂ U \leq_{I} x \leftrightarrow ⋂ U \subseteq x)$
17	13 14 15 16	syl3anc	$⊢ ((C \in Moore (X) \land U \subseteq C \land U \neq \emptyset) \land x \in U) \to (⋂ U \leq_{I} x \leftrightarrow ⋂ U \subseteq x)$
18	12 17	mpbird	$⊢ ((C \in Moore (X) \land U \subseteq C \land U \neq \emptyset) \land x \in U) \to ⋂ U \leq_{I} x$
19		simpll1	$⊢ (((C \in Moore (X) \land U \subseteq C \land U \neq \emptyset) \land y \in C) \land x \in U) \to C \in Moore (X)$
20		simplr	$⊢ (((C \in Moore (X) \land U \subseteq C \land U \neq \emptyset) \land y \in C) \land x \in U) \to y \in C$
21		simpl2	$⊢ ((C \in Moore (X) \land U \subseteq C \land U \neq \emptyset) \land y \in C) \to U \subseteq C$
22	21	sselda	$⊢ (((C \in Moore (X) \land U \subseteq C \land U \neq \emptyset) \land y \in C) \land x \in U) \to x \in C$
23	1 3	ipole	$⊢ (C \in Moore (X) \land y \in C \land x \in C) \to (y \leq_{I} x \leftrightarrow y \subseteq x)$
24	19 20 22 23	syl3anc	$⊢ (((C \in Moore (X) \land U \subseteq C \land U \neq \emptyset) \land y \in C) \land x \in U) \to (y \leq_{I} x \leftrightarrow y \subseteq x)$
25	24	biimpd	$⊢ (((C \in Moore (X) \land U \subseteq C \land U \neq \emptyset) \land y \in C) \land x \in U) \to (y \leq_{I} x \to y \subseteq x)$
26	25	ralimdva	$⊢ ((C \in Moore (X) \land U \subseteq C \land U \neq \emptyset) \land y \in C) \to (\forall x \in U y \leq_{I} x \to \forall x \in U y \subseteq x)$
27	26	3impia	$⊢ ((C \in Moore (X) \land U \subseteq C \land U \neq \emptyset) \land y \in C \land \forall x \in U y \leq_{I} x) \to \forall x \in U y \subseteq x$
28		ssint	$⊢ y \subseteq ⋂ U \leftrightarrow \forall x \in U y \subseteq x$
29	27 28	sylibr	$⊢ ((C \in Moore (X) \land U \subseteq C \land U \neq \emptyset) \land y \in C \land \forall x \in U y \leq_{I} x) \to y \subseteq ⋂ U$
30		simp11	$⊢ ((C \in Moore (X) \land U \subseteq C \land U \neq \emptyset) \land y \in C \land \forall x \in U y \leq_{I} x) \to C \in Moore (X)$
31		simp2	$⊢ ((C \in Moore (X) \land U \subseteq C \land U \neq \emptyset) \land y \in C \land \forall x \in U y \leq_{I} x) \to y \in C$
32	10	3ad2ant1	$⊢ ((C \in Moore (X) \land U \subseteq C \land U \neq \emptyset) \land y \in C \land \forall x \in U y \leq_{I} x) \to ⋂ U \in C$
33	1 3	ipole	$⊢ (C \in Moore (X) \land y \in C \land ⋂ U \in C) \to (y \leq_{I} ⋂ U \leftrightarrow y \subseteq ⋂ U)$
34	30 31 32 33	syl3anc	$⊢ ((C \in Moore (X) \land U \subseteq C \land U \neq \emptyset) \land y \in C \land \forall x \in U y \leq_{I} x) \to (y \leq_{I} ⋂ U \leftrightarrow y \subseteq ⋂ U)$
35	29 34	mpbird	$⊢ ((C \in Moore (X) \land U \subseteq C \land U \neq \emptyset) \land y \in C \land \forall x \in U y \leq_{I} x) \to y \leq_{I} ⋂ U$
36	3 5 6 8 9 10 18 35	posglbdg	$⊢ (C \in Moore (X) \land U \subseteq C \land U \neq \emptyset) \to G (U) = ⋂ U$

Metamath Proof Explorer

Theorem mrelatglb

Proof