This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) , ^◡ ≤ ⟩ )