Metamath Proof Explorer

Theorem oduleval

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

Ref Expression
Hypotheses oduval.d ⊢ 𝐷 = ( ODual ‘ 𝑂 )
oduval.l ⊢ ≤ = ( le ‘ 𝑂 )
Assertion oduleval ◡ ≤ = ( le ‘ 𝐷 )

Proof

Step Hyp Ref Expression
1 oduval.d ⊢ 𝐷 = ( ODual ‘ 𝑂 )
2 oduval.l ⊢ ≤ = ( le ‘ 𝑂 )
3 fvex ⊢ ( le ‘ 𝑂 ) ∈ V
4 3 cnvex ⊢ ◡ ( le ‘ 𝑂 ) ∈ V
5 pleid ⊢ le = Slot ( le ‘ ndx )
6 5 setsid ⊢ ( ( 𝑂 ∈ V ∧ ◡ ( le ‘ 𝑂 ) ∈ V ) → ◡ ( le ‘ 𝑂 ) = ( le ‘ ( 𝑂 sSet ⟨ ( le ‘ ndx ) , ◡ ( le ‘ 𝑂 ) ⟩ ) ) )
7 4 6 mpan2 ⊢ ( 𝑂 ∈ V → ◡ ( le ‘ 𝑂 ) = ( le ‘ ( 𝑂 sSet ⟨ ( le ‘ ndx ) , ◡ ( le ‘ 𝑂 ) ⟩ ) ) )
8 5 str0 ⊢ ∅ = ( le ‘ ∅ )
9 fvprc ⊢ ( ¬ 𝑂 ∈ V → ( le ‘ 𝑂 ) = ∅ )
10 9 cnveqd ⊢ ( ¬ 𝑂 ∈ V → ◡ ( le ‘ 𝑂 ) = ◡ ∅ )
11 cnv0 ⊢ ◡ ∅ = ∅
12 10 11 eqtrdi ⊢ ( ¬ 𝑂 ∈ V → ◡ ( le ‘ 𝑂 ) = ∅ )
13 reldmsets ⊢ Rel dom sSet
14 13 ovprc1 ⊢ ( ¬ 𝑂 ∈ V → ( 𝑂 sSet ⟨ ( le ‘ ndx ) , ◡ ( le ‘ 𝑂 ) ⟩ ) = ∅ )
15 14 fveq2d ⊢ ( ¬ 𝑂 ∈ V → ( le ‘ ( 𝑂 sSet ⟨ ( le ‘ ndx ) , ◡ ( le ‘ 𝑂 ) ⟩ ) ) = ( le ‘ ∅ ) )
16 8 12 15 3eqtr4a ⊢ ( ¬ 𝑂 ∈ V → ◡ ( le ‘ 𝑂 ) = ( le ‘ ( 𝑂 sSet ⟨ ( le ‘ ndx ) , ◡ ( le ‘ 𝑂 ) ⟩ ) ) )
17 7 16 pm2.61i ⊢ ◡ ( le ‘ 𝑂 ) = ( le ‘ ( 𝑂 sSet ⟨ ( le ‘ ndx ) , ◡ ( le ‘ 𝑂 ) ⟩ ) )
18 2 cnveqi ⊢ ◡ ≤ = ◡ ( le ‘ 𝑂 )
19 eqid ⊢ ( le ‘ 𝑂 ) = ( le ‘ 𝑂 )
20 1 19 oduval ⊢ 𝐷 = ( 𝑂 sSet ⟨ ( le ‘ ndx ) , ◡ ( le ‘ 𝑂 ) ⟩ )
21 20 fveq2i ⊢ ( le ‘ 𝐷 ) = ( le ‘ ( 𝑂 sSet ⟨ ( le ‘ ndx ) , ◡ ( le ‘ 𝑂 ) ⟩ ) )
22 17 18 21 3eqtr4i ⊢ ◡ ≤ = ( le ‘ 𝐷 )