Metamath Proof Explorer

Theorem ipotset

Description: Topology of the inclusion poset. (Contributed by Mario Carneiro, 24-Oct-2015)

		Ref	Expression
	Hypotheses	ipoval.i	$⊢ I = toInc (F)$
		ipole.l	$⊢ \underset{˙}{\leq} = \leq_{I}$
	Assertion	ipotset	$⊢ F \in V \to ordTop (\underset{˙}{\leq}) = TopSet (I)$

Proof

Step	Hyp	Ref	Expression
1		ipoval.i	$⊢ I = toInc (F)$
2		ipole.l	$⊢ \underset{˙}{\leq} = \leq_{I}$
3		fvex	$⊢ ordTop (\{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\}) \in V$
4		ipostr	$⊢ (\{⟨{Base}_{ndx}, F⟩, ⟨TopSet (ndx), ordTop (\{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\})⟩\} \cup \{⟨\leq_{ndx}, \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\}⟩, ⟨oc (ndx), (x \in F ⟼ ⋃ \{y \in F \| y \cap x = \emptyset\})⟩\}) Struct ⟨1, 11⟩$
5		tsetid	$⊢ TopSet = Slot TopSet (ndx)$
6		snsspr2	$⊢ \{⟨TopSet (ndx), ordTop (\{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\})⟩\} \subseteq \{⟨{Base}_{ndx}, F⟩, ⟨TopSet (ndx), ordTop (\{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\})⟩\}$
7		ssun1	$⊢ \{⟨{Base}_{ndx}, F⟩, ⟨TopSet (ndx), ordTop (\{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\})⟩\} \subseteq \{⟨{Base}_{ndx}, F⟩, ⟨TopSet (ndx), ordTop (\{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\})⟩\} \cup \{⟨\leq_{ndx}, \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\}⟩, ⟨oc (ndx), (x \in F ⟼ ⋃ \{y \in F \| y \cap x = \emptyset\})⟩\}$
8	6 7	sstri	$⊢ \{⟨TopSet (ndx), ordTop (\{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\})⟩\} \subseteq \{⟨{Base}_{ndx}, F⟩, ⟨TopSet (ndx), ordTop (\{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\})⟩\} \cup \{⟨\leq_{ndx}, \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\}⟩, ⟨oc (ndx), (x \in F ⟼ ⋃ \{y \in F \| y \cap x = \emptyset\})⟩\}$
9	4 5 8	strfv	$⊢ ordTop (\{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\}) \in V \to ordTop (\{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\}) = TopSet (\{⟨{Base}_{ndx}, F⟩, ⟨TopSet (ndx), ordTop (\{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\})⟩\} \cup \{⟨\leq_{ndx}, \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\}⟩, ⟨oc (ndx), (x \in F ⟼ ⋃ \{y \in F \| y \cap x = \emptyset\})⟩\})$
10	3 9	ax-mp	$⊢ ordTop (\{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\}) = TopSet (\{⟨{Base}_{ndx}, F⟩, ⟨TopSet (ndx), ordTop (\{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\})⟩\} \cup \{⟨\leq_{ndx}, \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\}⟩, ⟨oc (ndx), (x \in F ⟼ ⋃ \{y \in F \| y \cap x = \emptyset\})⟩\})$
11	1	ipolerval	$⊢ F \in V \to \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\} = \leq_{I}$
12	2 11	eqtr4id	$⊢ F \in V \to \underset{˙}{\leq} = \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\}$
13	12	fveq2d	$⊢ F \in V \to ordTop (\underset{˙}{\leq}) = ordTop (\{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\})$
14		eqid	$⊢ \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\} = \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\}$
15	1 14	ipoval	$⊢ F \in V \to I = \{⟨{Base}_{ndx}, F⟩, ⟨TopSet (ndx), ordTop (\{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\})⟩\} \cup \{⟨\leq_{ndx}, \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\}⟩, ⟨oc (ndx), (x \in F ⟼ ⋃ \{y \in F \| y \cap x = \emptyset\})⟩\}$
16	15	fveq2d	$⊢ F \in V \to TopSet (I) = TopSet (\{⟨{Base}_{ndx}, F⟩, ⟨TopSet (ndx), ordTop (\{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\})⟩\} \cup \{⟨\leq_{ndx}, \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\}⟩, ⟨oc (ndx), (x \in F ⟼ ⋃ \{y \in F \| y \cap x = \emptyset\})⟩\})$
17	10 13 16	3eqtr4a	$⊢ F \in V \to ordTop (\underset{˙}{\leq}) = TopSet (I)$