oduleval

Description: Value of the less-equal relation in an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015)

Step	Hyp	Ref	Expression
1		oduval.d	$⊢ D = ODual (O)$
2		oduval.l	$⊢ \underset{˙}{\leq} = \leq_{O}$
3		fvex	$⊢ \leq_{O} \in V$
4	3	cnvex	$⊢ {\leq_{O}}^{-1} \in V$
5		pleid	$⊢ le = Slot \leq_{ndx}$
6	5	setsid	$⊢ (O \in V \land {\leq_{O}}^{-1} \in V) \to {\leq_{O}}^{-1} = \leq_{(O sSet ⟨\leq_{ndx}, {\leq_{O}}^{-1}⟩)}$
7	4 6	mpan2	$⊢ O \in V \to {\leq_{O}}^{-1} = \leq_{(O sSet ⟨\leq_{ndx}, {\leq_{O}}^{-1}⟩)}$
8	5	str0	$⊢ \emptyset = \leq_{\emptyset}$
9		fvprc	$⊢ \neg O \in V \to \leq_{O} = \emptyset$
10	9	cnveqd	$⊢ \neg O \in V \to {\leq_{O}}^{-1} = \emptyset^{-1}$
11		cnv0	$⊢ \emptyset^{-1} = \emptyset$
12	10 11	eqtrdi	$⊢ \neg O \in V \to {\leq_{O}}^{-1} = \emptyset$
13		reldmsets	$⊢ Rel dom sSet$
14	13	ovprc1	$⊢ \neg O \in V \to O sSet ⟨\leq_{ndx}, {\leq_{O}}^{-1}⟩ = \emptyset$
15	14	fveq2d	$⊢ \neg O \in V \to \leq_{(O sSet ⟨\leq_{ndx}, {\leq_{O}}^{-1}⟩)} = \leq_{\emptyset}$
16	8 12 15	3eqtr4a	$⊢ \neg O \in V \to {\leq_{O}}^{-1} = \leq_{(O sSet ⟨\leq_{ndx}, {\leq_{O}}^{-1}⟩)}$
17	7 16	pm2.61i	$⊢ {\leq_{O}}^{-1} = \leq_{(O sSet ⟨\leq_{ndx}, {\leq_{O}}^{-1}⟩)}$
18	2	cnveqi	$⊢ {\underset{˙}{\leq}}^{-1} = {\leq_{O}}^{-1}$
19		eqid	$⊢ \leq_{O} = \leq_{O}$
20	1 19	oduval	$⊢ D = O sSet ⟨\leq_{ndx}, {\leq_{O}}^{-1}⟩$
21	20	fveq2i	$⊢ \leq_{D} = \leq_{(O sSet ⟨\leq_{ndx}, {\leq_{O}}^{-1}⟩)}$
22	17 18 21	3eqtr4i	$⊢ {\underset{˙}{\leq}}^{-1} = \leq_{D}$

Metamath Proof Explorer