This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ipobas

Description: Base set of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015) (Revised by Mario Carneiro, 25-Oct-2015)

		Ref	Expression
	Hypothesis	ipoval.i	$⊢ I = toInc (F)$
	Assertion	ipobas	$⊢ F \in V \to F = {Base}_{I}$

Proof

Step	Hyp	Ref	Expression
1		ipoval.i	$⊢ I = toInc (F)$
2		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⟩$
3		baseid	$⊢ Base = Slot {Base}_{ndx}$
4		snsspr1	$⊢ \{⟨{Base}_{ndx}, F⟩\} \subseteq \{⟨{Base}_{ndx}, F⟩, ⟨TopSet (ndx), ordTop (\{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\})⟩\}$
5		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\})⟩\}$
6	4 5	sstri	$⊢ \{⟨{Base}_{ndx}, F⟩\} \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\})⟩\}$
7	2 3 6	strfv	$⊢ F \in V \to F = {Base}_{(\{⟨{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		eqid	$⊢ \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\} = \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\}$
9	1 8	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\})⟩\}$
10	9	fveq2d	$⊢ F \in V \to {Base}_{I} = {Base}_{(\{⟨{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	7 10	eqtr4d	$⊢ F \in V \to F = {Base}_{I}$