Theorem oppfval

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

	Ref	Expression
Assertion	oppfval	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → ( 𝐹 oppFunc 𝐺 ) = ⟨ 𝐹 , tpos 𝐺 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
2	1	brrelex12i	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) )
3		oppfvalg	⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 𝐹 oppFunc 𝐺 ) = if ( ( Rel 𝐺 ∧ Rel dom 𝐺 ) , ⟨ 𝐹 , tpos 𝐺 ⟩ , ∅ ) )
4	2 3	syl	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → ( 𝐹 oppFunc 𝐺 ) = if ( ( Rel 𝐺 ∧ Rel dom 𝐺 ) , ⟨ 𝐹 , tpos 𝐺 ⟩ , ∅ ) )
5		oppfvallem	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → ( Rel 𝐺 ∧ Rel dom 𝐺 ) )
6	5	iftrued	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → if ( ( Rel 𝐺 ∧ Rel dom 𝐺 ) , ⟨ 𝐹 , tpos 𝐺 ⟩ , ∅ ) = ⟨ 𝐹 , tpos 𝐺 ⟩ )
7	4 6	eqtrd	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → ( 𝐹 oppFunc 𝐺 ) = ⟨ 𝐹 , tpos 𝐺 ⟩ )