Theorem oppf1st2nd

Description: Rewrite the opposite functor into its components ( eqopi ). (Contributed by Zhi Wang, 14-Nov-2025)

	Ref	Expression
Hypotheses	oppfrcl.1	⊢ ( 𝜑 → 𝐺 ∈ 𝑅 )
	oppfrcl.2	⊢ Rel 𝑅
	oppfrcl.3	⊢ 𝐺 = ( oppFunc ‘ 𝐹 )
	oppfrcl2.4	⊢ ( 𝜑 → 𝐹 = ⟨ 𝐴 , 𝐵 ⟩ )
Assertion	oppf1st2nd	⊢ ( 𝜑 → ( 𝐺 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝐺 ) = 𝐴 ∧ ( 2nd ‘ 𝐺 ) = tpos 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		oppfrcl.1	⊢ ( 𝜑 → 𝐺 ∈ 𝑅 )
2		oppfrcl.2	⊢ Rel 𝑅
3		oppfrcl.3	⊢ 𝐺 = ( oppFunc ‘ 𝐹 )
4		oppfrcl2.4	⊢ ( 𝜑 → 𝐹 = ⟨ 𝐴 , 𝐵 ⟩ )
5	4	fveq2d	⊢ ( 𝜑 → ( oppFunc ‘ 𝐹 ) = ( oppFunc ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
6		df-ov	⊢ ( 𝐴 oppFunc 𝐵 ) = ( oppFunc ‘ ⟨ 𝐴 , 𝐵 ⟩ )
7	5 3 6	3eqtr4g	⊢ ( 𝜑 → 𝐺 = ( 𝐴 oppFunc 𝐵 ) )
8	1 2 3 4	oppfrcl2	⊢ ( 𝜑 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
9		oppfvalg	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 oppFunc 𝐵 ) = if ( ( Rel 𝐵 ∧ Rel dom 𝐵 ) , ⟨ 𝐴 , tpos 𝐵 ⟩ , ∅ ) )
10	8 9	syl	⊢ ( 𝜑 → ( 𝐴 oppFunc 𝐵 ) = if ( ( Rel 𝐵 ∧ Rel dom 𝐵 ) , ⟨ 𝐴 , tpos 𝐵 ⟩ , ∅ ) )
11	7 10	eqtrd	⊢ ( 𝜑 → 𝐺 = if ( ( Rel 𝐵 ∧ Rel dom 𝐵 ) , ⟨ 𝐴 , tpos 𝐵 ⟩ , ∅ ) )
12	1 2 3 4	oppfrcl3	⊢ ( 𝜑 → ( Rel 𝐵 ∧ Rel dom 𝐵 ) )
13	12	iftrued	⊢ ( 𝜑 → if ( ( Rel 𝐵 ∧ Rel dom 𝐵 ) , ⟨ 𝐴 , tpos 𝐵 ⟩ , ∅ ) = ⟨ 𝐴 , tpos 𝐵 ⟩ )
14	11 13	eqtrd	⊢ ( 𝜑 → 𝐺 = ⟨ 𝐴 , tpos 𝐵 ⟩ )
15	8	simpld	⊢ ( 𝜑 → 𝐴 ∈ V )
16		tposexg	⊢ ( 𝐵 ∈ V → tpos 𝐵 ∈ V )
17	8 16	simpl2im	⊢ ( 𝜑 → tpos 𝐵 ∈ V )
18	15 17	opelxpd	⊢ ( 𝜑 → ⟨ 𝐴 , tpos 𝐵 ⟩ ∈ ( V × V ) )
19	14 18	eqeltrd	⊢ ( 𝜑 → 𝐺 ∈ ( V × V ) )
20	14	fveq2d	⊢ ( 𝜑 → ( 1st ‘ 𝐺 ) = ( 1st ‘ ⟨ 𝐴 , tpos 𝐵 ⟩ ) )
21		op1stg	⊢ ( ( 𝐴 ∈ V ∧ tpos 𝐵 ∈ V ) → ( 1st ‘ ⟨ 𝐴 , tpos 𝐵 ⟩ ) = 𝐴 )
22	15 17 21	syl2anc	⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐴 , tpos 𝐵 ⟩ ) = 𝐴 )
23	20 22	eqtrd	⊢ ( 𝜑 → ( 1st ‘ 𝐺 ) = 𝐴 )
24	14	fveq2d	⊢ ( 𝜑 → ( 2nd ‘ 𝐺 ) = ( 2nd ‘ ⟨ 𝐴 , tpos 𝐵 ⟩ ) )
25		op2ndg	⊢ ( ( 𝐴 ∈ V ∧ tpos 𝐵 ∈ V ) → ( 2nd ‘ ⟨ 𝐴 , tpos 𝐵 ⟩ ) = tpos 𝐵 )
26	15 17 25	syl2anc	⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝐴 , tpos 𝐵 ⟩ ) = tpos 𝐵 )
27	24 26	eqtrd	⊢ ( 𝜑 → ( 2nd ‘ 𝐺 ) = tpos 𝐵 )
28	19 23 27	jca32	⊢ ( 𝜑 → ( 𝐺 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝐺 ) = 𝐴 ∧ ( 2nd ‘ 𝐺 ) = tpos 𝐵 ) ) )