Theorem 2oppf

Description: The double opposite functor is the original functor. (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 |-
Assertion	2oppf	Could not format assertion : No typesetting found for |- ( ph -> ( oppFunc ` G ) = F ) with typecode |-

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		fvex	$$⊢1^{st}\left(F\right)\in \mathrm{V}$$
5		fvex	$$⊢2^{nd}\left(F\right)\in \mathrm{V}$$
6	5	tposex	$$⊢tpos{2}^{nd}\left(F\right)\in \mathrm{V}$$
7		oppfvalg	Could not format ( ( ( 1st ` F ) e. _V /\ tpos ( 2nd ` F ) e. _V ) -> ( ( 1st ` F ) oppFunc tpos ( 2nd ` F ) ) = if ( ( Rel tpos ( 2nd ` F ) /\ Rel dom tpos ( 2nd ` F ) ) , <. ( 1st ` F ) , tpos tpos ( 2nd ` F ) >. , (/) ) ) : No typesetting found for |- ( ( ( 1st ` F ) e. _V /\ tpos ( 2nd ` F ) e. _V ) -> ( ( 1st ` F ) oppFunc tpos ( 2nd ` F ) ) = if ( ( Rel tpos ( 2nd ` F ) /\ Rel dom tpos ( 2nd ` F ) ) , <. ( 1st ` F ) , tpos tpos ( 2nd ` F ) >. , (/) ) ) with typecode |-
8	4 6 7	mp2an	Could not format ( ( 1st ` F ) oppFunc tpos ( 2nd ` F ) ) = if ( ( Rel tpos ( 2nd ` F ) /\ Rel dom tpos ( 2nd ` F ) ) , <. ( 1st ` F ) , tpos tpos ( 2nd ` F ) >. , (/) ) : No typesetting found for |- ( ( 1st ` F ) oppFunc tpos ( 2nd ` F ) ) = if ( ( Rel tpos ( 2nd ` F ) /\ Rel dom tpos ( 2nd ` F ) ) , <. ( 1st ` F ) , tpos tpos ( 2nd ` F ) >. , (/) ) with typecode |-
9		df-ov	Could not format ( ( 1st ` F ) oppFunc tpos ( 2nd ` F ) ) = ( oppFunc ` <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) : No typesetting found for |- ( ( 1st ` F ) oppFunc tpos ( 2nd ` F ) ) = ( oppFunc ` <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) with typecode |-
10	1 2 3	oppfrcl	$$⊢\phi \to F\in \left(\mathrm{V}\times \mathrm{V}\right)$$
11		1st2nd2	$$⊢F\in \left(\mathrm{V}\times \mathrm{V}\right)\to F=⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩$$
12	10 11	syl	$$⊢\phi \to F=⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩$$
13	1 2 3 12	oppf1st2nd	$$⊢\phi \to \left(G\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \left(1^{st}\left(G\right)=1^{st}\left(F\right)\wedge 2^{nd}\left(G\right)=tpos{2}^{nd}\left(F\right)\right)\right)$$
14		eqopi	$$⊢\left(G\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \left(1^{st}\left(G\right)=1^{st}\left(F\right)\wedge 2^{nd}\left(G\right)=tpos{2}^{nd}\left(F\right)\right)\right)\to G=⟨1^{st}\left(F\right),tpos{2}^{nd}\left(F\right)⟩$$
15	13 14	syl	$$⊢\phi \to G=⟨1^{st}\left(F\right),tpos{2}^{nd}\left(F\right)⟩$$
16	15	fveq2d	Could not format ( ph -> ( oppFunc ` G ) = ( oppFunc ` <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) ) : No typesetting found for |- ( ph -> ( oppFunc ` G ) = ( oppFunc ` <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) ) with typecode |-
17	9 16	eqtr4id	Could not format ( ph -> ( ( 1st ` F ) oppFunc tpos ( 2nd ` F ) ) = ( oppFunc ` G ) ) : No typesetting found for |- ( ph -> ( ( 1st ` F ) oppFunc tpos ( 2nd ` F ) ) = ( oppFunc ` G ) ) with typecode |-
18	1 2 3 12	oppfrcl3	$$⊢\phi \to \left(\mathrm{Rel}{2}^{nd}\left(F\right)\wedge \mathrm{Rel}\mathrm{dom}{2}^{nd}\left(F\right)\right)$$
19		tpostpos2	$$⊢\left(\mathrm{Rel}{2}^{nd}\left(F\right)\wedge \mathrm{Rel}\mathrm{dom}{2}^{nd}\left(F\right)\right)\to tpostpos{2}^{nd}\left(F\right)=2^{nd}\left(F\right)$$
20	18 19	syl	$$⊢\phi \to tpostpos{2}^{nd}\left(F\right)=2^{nd}\left(F\right)$$
21	20	opeq2d	$$⊢\phi \to ⟨1^{st}\left(F\right),tpostpos{2}^{nd}\left(F\right)⟩=⟨1^{st}\left(F\right),2^{nd}\left(F\right)⟩$$
22		0nelrel0	$$⊢\mathrm{Rel}\mathrm{dom}{2}^{nd}\left(F\right)\to \neg \varnothing \in \mathrm{dom}{2}^{nd}\left(F\right)$$
23	18 22	simpl2im	$$⊢\phi \to \neg \varnothing \in \mathrm{dom}{2}^{nd}\left(F\right)$$
24		reldmtpos	$$⊢\mathrm{Rel}\mathrm{dom}tpos{2}^{nd}\left(F\right)\leftrightarrow \neg \varnothing \in \mathrm{dom}{2}^{nd}\left(F\right)$$
25	23 24	sylibr	$$⊢\phi \to \mathrm{Rel}\mathrm{dom}tpos{2}^{nd}\left(F\right)$$
26		reltpos	$$⊢\mathrm{Rel}tpos{2}^{nd}\left(F\right)$$
27	25 26	jctil	$$⊢\phi \to \left(\mathrm{Rel}tpos{2}^{nd}\left(F\right)\wedge \mathrm{Rel}\mathrm{dom}tpos{2}^{nd}\left(F\right)\right)$$
28	27	iftrued	$$⊢\phi \to if\left(\left(\mathrm{Rel}tpos{2}^{nd}\left(F\right)\wedge \mathrm{Rel}\mathrm{dom}tpos{2}^{nd}\left(F\right)\right),⟨1^{st}\left(F\right),tpostpos{2}^{nd}\left(F\right)⟩,\varnothing \right)=⟨1^{st}\left(F\right),tpostpos{2}^{nd}\left(F\right)⟩$$
29	21 28 12	3eqtr4d	$$⊢\phi \to if\left(\left(\mathrm{Rel}tpos{2}^{nd}\left(F\right)\wedge \mathrm{Rel}\mathrm{dom}tpos{2}^{nd}\left(F\right)\right),⟨1^{st}\left(F\right),tpostpos{2}^{nd}\left(F\right)⟩,\varnothing \right)=F$$
30	8 17 29	3eqtr3a	Could not format ( ph -> ( oppFunc ` G ) = F ) : No typesetting found for |- ( ph -> ( oppFunc ` G ) = F ) with typecode |-