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 𝐺 ⟩ , ∅ ) )