Theorem oduval

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

	Ref	Expression
Hypotheses	oduval.d	⊢ 𝐷 = ( ODual ‘ 𝑂 )
	oduval.l	⊢ ≤ = ( le ‘ 𝑂 )
Assertion	oduval	⊢ 𝐷 = ( 𝑂 sSet ⟨ ( le ‘ ndx ) , ◡ ≤ ⟩ )

Proof

Step	Hyp	Ref	Expression
1		oduval.d	⊢ 𝐷 = ( ODual ‘ 𝑂 )
2		oduval.l	⊢ ≤ = ( le ‘ 𝑂 )
3		id	⊢ ( 𝑎 = 𝑂 → 𝑎 = 𝑂 )
4		fveq2	⊢ ( 𝑎 = 𝑂 → ( le ‘ 𝑎 ) = ( le ‘ 𝑂 ) )
5	4	cnveqd	⊢ ( 𝑎 = 𝑂 → ◡ ( le ‘ 𝑎 ) = ◡ ( le ‘ 𝑂 ) )
6	5	opeq2d	⊢ ( 𝑎 = 𝑂 → ⟨ ( le ‘ ndx ) , ◡ ( le ‘ 𝑎 ) ⟩ = ⟨ ( le ‘ ndx ) , ◡ ( le ‘ 𝑂 ) ⟩ )
7	3 6	oveq12d	⊢ ( 𝑎 = 𝑂 → ( 𝑎 sSet ⟨ ( le ‘ ndx ) , ◡ ( le ‘ 𝑎 ) ⟩ ) = ( 𝑂 sSet ⟨ ( le ‘ ndx ) , ◡ ( le ‘ 𝑂 ) ⟩ ) )
8		df-odu	⊢ ODual = ( 𝑎 ∈ V ↦ ( 𝑎 sSet ⟨ ( le ‘ ndx ) , ◡ ( le ‘ 𝑎 ) ⟩ ) )
9		ovex	⊢ ( 𝑂 sSet ⟨ ( le ‘ ndx ) , ◡ ( le ‘ 𝑂 ) ⟩ ) ∈ V
10	7 8 9	fvmpt	⊢ ( 𝑂 ∈ V → ( ODual ‘ 𝑂 ) = ( 𝑂 sSet ⟨ ( le ‘ ndx ) , ◡ ( le ‘ 𝑂 ) ⟩ ) )
11		fvprc	⊢ ( ¬ 𝑂 ∈ V → ( ODual ‘ 𝑂 ) = ∅ )
12		reldmsets	⊢ Rel dom sSet
13	12	ovprc1	⊢ ( ¬ 𝑂 ∈ V → ( 𝑂 sSet ⟨ ( le ‘ ndx ) , ◡ ( le ‘ 𝑂 ) ⟩ ) = ∅ )
14	11 13	eqtr4d	⊢ ( ¬ 𝑂 ∈ V → ( ODual ‘ 𝑂 ) = ( 𝑂 sSet ⟨ ( le ‘ ndx ) , ◡ ( le ‘ 𝑂 ) ⟩ ) )
15	10 14	pm2.61i	⊢ ( ODual ‘ 𝑂 ) = ( 𝑂 sSet ⟨ ( le ‘ ndx ) , ◡ ( le ‘ 𝑂 ) ⟩ )
16	2	cnveqi	⊢ ◡ ≤ = ◡ ( le ‘ 𝑂 )
17	16	opeq2i	⊢ ⟨ ( le ‘ ndx ) , ◡ ≤ ⟩ = ⟨ ( le ‘ ndx ) , ◡ ( le ‘ 𝑂 ) ⟩
18	17	oveq2i	⊢ ( 𝑂 sSet ⟨ ( le ‘ ndx ) , ◡ ≤ ⟩ ) = ( 𝑂 sSet ⟨ ( le ‘ ndx ) , ◡ ( le ‘ 𝑂 ) ⟩ )
19	15 1 18	3eqtr4i	⊢ 𝐷 = ( 𝑂 sSet ⟨ ( le ‘ ndx ) , ◡ ≤ ⟩ )