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

Metamath Proof Explorer

Theorem oppfvalg

Description: Value of the opposite functor. (Contributed by Zhi Wang, 13-Nov-2025)

Ref Expression
Assertion oppfvalg ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 𝐹 oppFunc 𝐺 ) = if ( ( Rel 𝐺 ∧ Rel dom 𝐺 ) , ⟨ 𝐹 , tpos 𝐺 ⟩ , ∅ ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → 𝑔 = 𝐺 )
2 1 releqd ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( Rel 𝑔 ↔ Rel 𝐺 ) )
3 1 dmeqd ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → dom 𝑔 = dom 𝐺 )
4 3 releqd ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( Rel dom 𝑔 ↔ Rel dom 𝐺 ) )
5 2 4 anbi12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ( ( Rel 𝑔 ∧ Rel dom 𝑔 ) ↔ ( Rel 𝐺 ∧ Rel dom 𝐺 ) ) )
6 simpl ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → 𝑓 = 𝐹 )
7 1 tposeqd ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → tpos 𝑔 = tpos 𝐺 )
8 6 7 opeq12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → ⟨ 𝑓 , tpos 𝑔 ⟩ = ⟨ 𝐹 , tpos 𝐺 ⟩ )
9 5 8 ifbieq1d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑔 = 𝐺 ) → if ( ( Rel 𝑔 ∧ Rel dom 𝑔 ) , ⟨ 𝑓 , tpos 𝑔 ⟩ , ∅ ) = if ( ( Rel 𝐺 ∧ Rel dom 𝐺 ) , ⟨ 𝐹 , tpos 𝐺 ⟩ , ∅ ) )
10 df-oppf ⊢ oppFunc = ( 𝑓 ∈ V , 𝑔 ∈ V ↦ if ( ( Rel 𝑔 ∧ Rel dom 𝑔 ) , ⟨ 𝑓 , tpos 𝑔 ⟩ , ∅ ) )
11 opex ⊢ ⟨ 𝐹 , tpos 𝐺 ⟩ ∈ V
12 0ex ⊢ ∅ ∈ V
13 11 12 ifex ⊢ if ( ( Rel 𝐺 ∧ Rel dom 𝐺 ) , ⟨ 𝐹 , tpos 𝐺 ⟩ , ∅ ) ∈ V
14 9 10 13 ovmpoa ⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 𝐹 oppFunc 𝐺 ) = if ( ( Rel 𝐺 ∧ Rel dom 𝐺 ) , ⟨ 𝐹 , tpos 𝐺 ⟩ , ∅ ) )