ipolerval

Description: Relation of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015)

		Ref	Expression
	Hypothesis	ipoval.i	$⊢ I = toInc (F)$
	Assertion	ipolerval	$⊢ F \in V \to \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\} = \leq_{I}$

Proof

Step	Hyp	Ref	Expression
1		ipoval.i	$⊢ I = toInc (F)$
2		vex	$⊢ x \in V$
3		vex	$⊢ y \in V$
4	2 3	prss	$⊢ (x \in F \land y \in F) \leftrightarrow \{x, y\} \subseteq F$
5	4	biranri	$⊢ (\{x, y\} \subseteq F \land x \subseteq y) \to (x \in F \land y \in F)$
6	5	ssopab2i	$⊢ \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\} \subseteq \{⟨x, y⟩ \| (x \in F \land y \in F)\}$
7		df-xp	$⊢ F \times F = \{⟨x, y⟩ \| (x \in F \land y \in F)\}$
8	6 7	sseqtrri	$⊢ \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\} \subseteq F \times F$
9		sqxpexg	$⊢ F \in V \to F \times F \in V$
10		ssexg	$⊢ (\{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\} \subseteq F \times F \land F \times F \in V) \to \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\} \in V$
11	8 9 10	sylancr	$⊢ F \in V \to \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\} \in V$
12		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⟩$
13		pleid	$⊢ le = Slot \leq_{ndx}$
14		snsspr1	$⊢ \{⟨\leq_{ndx}, \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\}⟩\} \subseteq \{⟨\leq_{ndx}, \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\}⟩, ⟨oc (ndx), (x \in F ⟼ ⋃ \{y \in F \| y \cap x = \emptyset\})⟩\}$
15		ssun2	$⊢ \{⟨\leq_{ndx}, \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\}⟩, ⟨oc (ndx), (x \in F ⟼ ⋃ \{y \in F \| y \cap x = \emptyset\})⟩\} \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\})⟩\}$
16	14 15	sstri	$⊢ \{⟨\leq_{ndx}, \{⟨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\})⟩\}$
17	12 13 16	strfv	$⊢ \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\} \in V \to \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\} = \leq_{(\{⟨{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\})⟩\})}$
18	11 17	syl	$⊢ F \in V \to \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\} = \leq_{(\{⟨{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\})⟩\})}$
19		eqid	$⊢ \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\} = \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\}$
20	1 19	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\})⟩\}$
21	20	fveq2d	$⊢ F \in V \to \leq_{I} = \leq_{(\{⟨{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\})⟩\})}$
22	18 21	eqtr4d	$⊢ F \in V \to \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\} = \leq_{I}$

Metamath Proof Explorer

Theorem ipolerval

Proof