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		simpl	$⊢ (\{x, y\} \subseteq F \land x \subseteq y) \to \{x, y\} \subseteq F$
3		vex	$⊢ x \in V$
4		vex	$⊢ y \in V$
5	3 4	prss	$⊢ (x \in F \land y \in F) \leftrightarrow \{x, y\} \subseteq F$
6	2 5	sylibr	$⊢ (\{x, y\} \subseteq F \land x \subseteq y) \to (x \in F \land y \in F)$
7	6	ssopab2i	$⊢ \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\} \subseteq \{⟨x, y⟩ \| (x \in F \land y \in F)\}$
8		df-xp	$⊢ F \times F = \{⟨x, y⟩ \| (x \in F \land y \in F)\}$
9	7 8	sseqtrri	$⊢ \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\} \subseteq F \times F$
10		sqxpexg	$⊢ F \in V \to F \times F \in V$
11		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$
12	9 10 11	sylancr	$⊢ F \in V \to \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\} \in V$
13		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⟩$
14		pleid	$⊢ le = Slot \leq_{ndx}$
15		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\})⟩\}$
16		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\})⟩\}$
17	15 16	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\})⟩\}$
18	13 14 17	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\})⟩\})}$
19	12 18	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\})⟩\})}$
20		eqid	$⊢ \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\} = \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\}$
21	1 20	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\})⟩\}$
22	21	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\})⟩\})}$
23	19 22	eqtr4d	$⊢ F \in V \to \{⟨x, y⟩ \| (\{x, y\} \subseteq F \land x \subseteq y)\} = \leq_{I}$

Metamath Proof Explorer

Theorem ipolerval

Proof