topclat

Description: A topology is a complete lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024)

		Ref	Expression
	Hypothesis	topclat.i	$⊢ I = toInc (J)$
	Assertion	topclat	$⊢ J \in Top \to I \in CLat$

Proof

Step	Hyp	Ref	Expression
1		topclat.i	$⊢ I = toInc (J)$
2	1	ipobas	$⊢ J \in Top \to J = {Base}_{I}$
3		eqidd	$⊢ J \in Top \to lub (I) = lub (I)$
4		eqidd	$⊢ J \in Top \to glb (I) = glb (I)$
5	1	ipopos	$⊢ I \in Poset$
6	5	a1i	$⊢ J \in Top \to I \in Poset$
7		uniopn	$⊢ (J \in Top \land x \subseteq J) \to ⋃ x \in J$
8		simpl	$⊢ (J \in Top \land x \subseteq J) \to J \in Top$
9		simpr	$⊢ (J \in Top \land x \subseteq J) \to x \subseteq J$
10		eqidd	$⊢ (J \in Top \land x \subseteq J) \to lub (I) = lub (I)$
11		intmin	$⊢ ⋃ x \in J \to ⋂ \{y \in J \| ⋃ x \subseteq y\} = ⋃ x$
12	11	eqcomd	$⊢ ⋃ x \in J \to ⋃ x = ⋂ \{y \in J \| ⋃ x \subseteq y\}$
13	7 12	syl	$⊢ (J \in Top \land x \subseteq J) \to ⋃ x = ⋂ \{y \in J \| ⋃ x \subseteq y\}$
14	1 8 9 10 13	ipolubdm	$⊢ (J \in Top \land x \subseteq J) \to (x \in dom lub (I) \leftrightarrow ⋃ x \in J)$
15	7 14	mpbird	$⊢ (J \in Top \land x \subseteq J) \to x \in dom lub (I)$
16		ssrab2	$⊢ \{y \in J \| y \subseteq ⋂ x\} \subseteq J$
17		uniopn	$⊢ (J \in Top \land \{y \in J \| y \subseteq ⋂ x\} \subseteq J) \to ⋃ \{y \in J \| y \subseteq ⋂ x\} \in J$
18	8 16 17	sylancl	$⊢ (J \in Top \land x \subseteq J) \to ⋃ \{y \in J \| y \subseteq ⋂ x\} \in J$
19		eqidd	$⊢ (J \in Top \land x \subseteq J) \to glb (I) = glb (I)$
20		eqidd	$⊢ (J \in Top \land x \subseteq J) \to ⋃ \{y \in J \| y \subseteq ⋂ x\} = ⋃ \{y \in J \| y \subseteq ⋂ x\}$
21	1 8 9 19 20	ipoglbdm	$⊢ (J \in Top \land x \subseteq J) \to (x \in dom glb (I) \leftrightarrow ⋃ \{y \in J \| y \subseteq ⋂ x\} \in J)$
22	18 21	mpbird	$⊢ (J \in Top \land x \subseteq J) \to x \in dom glb (I)$
23	2 3 4 6 15 22	isclatd	$⊢ J \in Top \to I \in CLat$

Metamath Proof Explorer

Theorem topclat

Proof