mrelatlub

Description: Least upper bounds in a Moore space are realized by the closure of the union. (Contributed by Stefan O'Rear, 31-Jan-2015)

	Ref	Expression
Hypotheses	mreclat.i	$⊢ I = toInc (C)$
	mrelatlub.f	$⊢ F = mrCls (C)$
	mrelatlub.l	$⊢ L = lub (I)$
Assertion	mrelatlub	$⊢ (C \in Moore (X) \land U \subseteq C) \to L (U) = F (⋃ U)$

Proof

Step	Hyp	Ref	Expression
1		mreclat.i	$⊢ I = toInc (C)$
2		mrelatlub.f	$⊢ F = mrCls (C)$
3		mrelatlub.l	$⊢ L = lub (I)$
4		eqid	$⊢ \leq_{I} = \leq_{I}$
5	1	ipobas	$⊢ C \in Moore (X) \to C = {Base}_{I}$
6	5	adantr	$⊢ (C \in Moore (X) \land U \subseteq C) \to C = {Base}_{I}$
7	3	a1i	$⊢ (C \in Moore (X) \land U \subseteq C) \to L = lub (I)$
8	1	ipopos	$⊢ I \in Poset$
9	8	a1i	$⊢ (C \in Moore (X) \land U \subseteq C) \to I \in Poset$
10		simpr	$⊢ (C \in Moore (X) \land U \subseteq C) \to U \subseteq C$
11		uniss	$⊢ U \subseteq C \to ⋃ U \subseteq ⋃ C$
12	11	adantl	$⊢ (C \in Moore (X) \land U \subseteq C) \to ⋃ U \subseteq ⋃ C$
13		mreuni	$⊢ C \in Moore (X) \to ⋃ C = X$
14	13	adantr	$⊢ (C \in Moore (X) \land U \subseteq C) \to ⋃ C = X$
15	12 14	sseqtrd	$⊢ (C \in Moore (X) \land U \subseteq C) \to ⋃ U \subseteq X$
16	2	mrccl	$⊢ (C \in Moore (X) \land ⋃ U \subseteq X) \to F (⋃ U) \in C$
17	15 16	syldan	$⊢ (C \in Moore (X) \land U \subseteq C) \to F (⋃ U) \in C$
18		elssuni	$⊢ x \in U \to x \subseteq ⋃ U$
19	2	mrcssid	$⊢ (C \in Moore (X) \land ⋃ U \subseteq X) \to ⋃ U \subseteq F (⋃ U)$
20	15 19	syldan	$⊢ (C \in Moore (X) \land U \subseteq C) \to ⋃ U \subseteq F (⋃ U)$
21	18 20	sylan9ssr	$⊢ ((C \in Moore (X) \land U \subseteq C) \land x \in U) \to x \subseteq F (⋃ U)$
22		simpll	$⊢ ((C \in Moore (X) \land U \subseteq C) \land x \in U) \to C \in Moore (X)$
23	10	sselda	$⊢ ((C \in Moore (X) \land U \subseteq C) \land x \in U) \to x \in C$
24	17	adantr	$⊢ ((C \in Moore (X) \land U \subseteq C) \land x \in U) \to F (⋃ U) \in C$
25	1 4	ipole	$⊢ (C \in Moore (X) \land x \in C \land F (⋃ U) \in C) \to (x \leq_{I} F (⋃ U) \leftrightarrow x \subseteq F (⋃ U))$
26	22 23 24 25	syl3anc	$⊢ ((C \in Moore (X) \land U \subseteq C) \land x \in U) \to (x \leq_{I} F (⋃ U) \leftrightarrow x \subseteq F (⋃ U))$
27	21 26	mpbird	$⊢ ((C \in Moore (X) \land U \subseteq C) \land x \in U) \to x \leq_{I} F (⋃ U)$
28		simp1l	$⊢ ((C \in Moore (X) \land U \subseteq C) \land y \in C \land \forall x \in U x \leq_{I} y) \to C \in Moore (X)$
29		simplll	$⊢ (((C \in Moore (X) \land U \subseteq C) \land y \in C) \land x \in U) \to C \in Moore (X)$
30		simplr	$⊢ ((C \in Moore (X) \land U \subseteq C) \land y \in C) \to U \subseteq C$
31	30	sselda	$⊢ (((C \in Moore (X) \land U \subseteq C) \land y \in C) \land x \in U) \to x \in C$
32		simplr	$⊢ (((C \in Moore (X) \land U \subseteq C) \land y \in C) \land x \in U) \to y \in C$
33	1 4	ipole	$⊢ (C \in Moore (X) \land x \in C \land y \in C) \to (x \leq_{I} y \leftrightarrow x \subseteq y)$
34	29 31 32 33	syl3anc	$⊢ (((C \in Moore (X) \land U \subseteq C) \land y \in C) \land x \in U) \to (x \leq_{I} y \leftrightarrow x \subseteq y)$
35	34	biimpd	$⊢ (((C \in Moore (X) \land U \subseteq C) \land y \in C) \land x \in U) \to (x \leq_{I} y \to x \subseteq y)$
36	35	ralimdva	$⊢ ((C \in Moore (X) \land U \subseteq C) \land y \in C) \to (\forall x \in U x \leq_{I} y \to \forall x \in U x \subseteq y)$
37	36	3impia	$⊢ ((C \in Moore (X) \land U \subseteq C) \land y \in C \land \forall x \in U x \leq_{I} y) \to \forall x \in U x \subseteq y$
38		unissb	$⊢ ⋃ U \subseteq y \leftrightarrow \forall x \in U x \subseteq y$
39	37 38	sylibr	$⊢ ((C \in Moore (X) \land U \subseteq C) \land y \in C \land \forall x \in U x \leq_{I} y) \to ⋃ U \subseteq y$
40		simp2	$⊢ ((C \in Moore (X) \land U \subseteq C) \land y \in C \land \forall x \in U x \leq_{I} y) \to y \in C$
41	2	mrcsscl	$⊢ (C \in Moore (X) \land ⋃ U \subseteq y \land y \in C) \to F (⋃ U) \subseteq y$
42	28 39 40 41	syl3anc	$⊢ ((C \in Moore (X) \land U \subseteq C) \land y \in C \land \forall x \in U x \leq_{I} y) \to F (⋃ U) \subseteq y$
43	17	3ad2ant1	$⊢ ((C \in Moore (X) \land U \subseteq C) \land y \in C \land \forall x \in U x \leq_{I} y) \to F (⋃ U) \in C$
44	1 4	ipole	$⊢ (C \in Moore (X) \land F (⋃ U) \in C \land y \in C) \to (F (⋃ U) \leq_{I} y \leftrightarrow F (⋃ U) \subseteq y)$
45	28 43 40 44	syl3anc	$⊢ ((C \in Moore (X) \land U \subseteq C) \land y \in C \land \forall x \in U x \leq_{I} y) \to (F (⋃ U) \leq_{I} y \leftrightarrow F (⋃ U) \subseteq y)$
46	42 45	mpbird	$⊢ ((C \in Moore (X) \land U \subseteq C) \land y \in C \land \forall x \in U x \leq_{I} y) \to F (⋃ U) \leq_{I} y$
47	4 6 7 9 10 17 27 46	poslubdg	$⊢ (C \in Moore (X) \land U \subseteq C) \to L (U) = F (⋃ U)$

Metamath Proof Explorer

Theorem mrelatlub

Proof