Theorem oppf1st2nd

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

	Ref	Expression
Hypotheses	oppfrcl.1	$$⊢\phi \to G\in R$$
	oppfrcl.2	$$⊢\mathrm{Rel}R$$
	oppfrcl.3	No typesetting found for |- G = ( oppFunc ` F ) with typecode |-
	oppfrcl2.4	$$⊢\phi \to F=⟨A,B⟩$$
Assertion	oppf1st2nd	$$⊢\phi \to \left(G\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \left(1^{st}\left(G\right)=A\wedge 2^{nd}\left(G\right)=tposB\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		oppfrcl.1	$$⊢\phi \to G\in R$$
2		oppfrcl.2	$$⊢\mathrm{Rel}R$$
3		oppfrcl.3	Could not format G = ( oppFunc ` F ) : No typesetting found for |- G = ( oppFunc ` F ) with typecode |-
4		oppfrcl2.4	$$⊢\phi \to F=⟨A,B⟩$$
5	4	fveq2d	Could not format ( ph -> ( oppFunc ` F ) = ( oppFunc ` <. A , B >. ) ) : No typesetting found for |- ( ph -> ( oppFunc ` F ) = ( oppFunc ` <. A , B >. ) ) with typecode |-
6		df-ov	Could not format ( A oppFunc B ) = ( oppFunc ` <. A , B >. ) : No typesetting found for |- ( A oppFunc B ) = ( oppFunc ` <. A , B >. ) with typecode |-
7	5 3 6	3eqtr4g	Could not format ( ph -> G = ( A oppFunc B ) ) : No typesetting found for |- ( ph -> G = ( A oppFunc B ) ) with typecode |-
8	1 2 3 4	oppfrcl2	$$⊢\phi \to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$
9		oppfvalg	Could not format ( ( A e. _V /\ B e. _V ) -> ( A oppFunc B ) = if ( ( Rel B /\ Rel dom B ) , <. A , tpos B >. , (/) ) ) : No typesetting found for |- ( ( A e. _V /\ B e. _V ) -> ( A oppFunc B ) = if ( ( Rel B /\ Rel dom B ) , <. A , tpos B >. , (/) ) ) with typecode |-
10	8 9	syl	Could not format ( ph -> ( A oppFunc B ) = if ( ( Rel B /\ Rel dom B ) , <. A , tpos B >. , (/) ) ) : No typesetting found for |- ( ph -> ( A oppFunc B ) = if ( ( Rel B /\ Rel dom B ) , <. A , tpos B >. , (/) ) ) with typecode |-
11	7 10	eqtrd	$$⊢\phi \to G=if\left(\left(\mathrm{Rel}B\wedge \mathrm{Rel}\mathrm{dom}B\right),⟨A,tposB⟩,\varnothing \right)$$
12	1 2 3 4	oppfrcl3	$$⊢\phi \to \left(\mathrm{Rel}B\wedge \mathrm{Rel}\mathrm{dom}B\right)$$
13	12	iftrued	$$⊢\phi \to if\left(\left(\mathrm{Rel}B\wedge \mathrm{Rel}\mathrm{dom}B\right),⟨A,tposB⟩,\varnothing \right)=⟨A,tposB⟩$$
14	11 13	eqtrd	$$⊢\phi \to G=⟨A,tposB⟩$$
15	8	simpld	$$⊢\phi \to A\in \mathrm{V}$$
16		tposexg	$$⊢B\in \mathrm{V}\to tposB\in \mathrm{V}$$
17	8 16	simpl2im	$$⊢\phi \to tposB\in \mathrm{V}$$
18	15 17	opelxpd	$$⊢\phi \to ⟨A,tposB⟩\in \left(\mathrm{V}\times \mathrm{V}\right)$$
19	14 18	eqeltrd	$$⊢\phi \to G\in \left(\mathrm{V}\times \mathrm{V}\right)$$
20	14	fveq2d	$$⊢\phi \to 1^{st}\left(G\right)=1^{st}\left(⟨A,tposB⟩\right)$$
21		op1stg	$$⊢\left(A\in \mathrm{V}\wedge tposB\in \mathrm{V}\right)\to 1^{st}\left(⟨A,tposB⟩\right)=A$$
22	15 17 21	syl2anc	$$⊢\phi \to 1^{st}\left(⟨A,tposB⟩\right)=A$$
23	20 22	eqtrd	$$⊢\phi \to 1^{st}\left(G\right)=A$$
24	14	fveq2d	$$⊢\phi \to 2^{nd}\left(G\right)=2^{nd}\left(⟨A,tposB⟩\right)$$
25		op2ndg	$$⊢\left(A\in \mathrm{V}\wedge tposB\in \mathrm{V}\right)\to 2^{nd}\left(⟨A,tposB⟩\right)=tposB$$
26	15 17 25	syl2anc	$$⊢\phi \to 2^{nd}\left(⟨A,tposB⟩\right)=tposB$$
27	24 26	eqtrd	$$⊢\phi \to 2^{nd}\left(G\right)=tposB$$
28	19 23 27	jca32	$$⊢\phi \to \left(G\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \left(1^{st}\left(G\right)=A\wedge 2^{nd}\left(G\right)=tposB\right)\right)$$