# Metamath Proof Explorer

## 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 ) , ⟩ )