2oppf

Description: The double opposite functor is the original functor. Remark 3.42 of Adamek p. 39. (Contributed by Zhi Wang, 14-Nov-2025)

	Ref	Expression
Hypotheses	oppfrcl.1	⊢ ( 𝜑 → 𝐺 ∈ 𝑅 )
	oppfrcl.2	⊢ Rel 𝑅
	oppfrcl.3	⊢ 𝐺 = ( oppFunc ‘ 𝐹 )
Assertion	2oppf	⊢ ( 𝜑 → ( oppFunc ‘ 𝐺 ) = 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		oppfrcl.1	⊢ ( 𝜑 → 𝐺 ∈ 𝑅 )
2		oppfrcl.2	⊢ Rel 𝑅
3		oppfrcl.3	⊢ 𝐺 = ( oppFunc ‘ 𝐹 )
4		fvex	⊢ ( 1^st ‘ 𝐹 ) ∈ V
5		fvex	⊢ ( 2^nd ‘ 𝐹 ) ∈ V
6	5	tposex	⊢ tpos ( 2^nd ‘ 𝐹 ) ∈ V
7		oppfvalg	⊢ ( ( ( 1^st ‘ 𝐹 ) ∈ V ∧ tpos ( 2^nd ‘ 𝐹 ) ∈ V ) → ( ( 1^st ‘ 𝐹 ) oppFunc tpos ( 2^nd ‘ 𝐹 ) ) = if ( ( Rel tpos ( 2^nd ‘ 𝐹 ) ∧ Rel dom tpos ( 2^nd ‘ 𝐹 ) ) , ⟨ ( 1^st ‘ 𝐹 ) , tpos tpos ( 2^nd ‘ 𝐹 ) ⟩ , ∅ ) )
8	4 6 7	mp2an	⊢ ( ( 1^st ‘ 𝐹 ) oppFunc tpos ( 2^nd ‘ 𝐹 ) ) = if ( ( Rel tpos ( 2^nd ‘ 𝐹 ) ∧ Rel dom tpos ( 2^nd ‘ 𝐹 ) ) , ⟨ ( 1^st ‘ 𝐹 ) , tpos tpos ( 2^nd ‘ 𝐹 ) ⟩ , ∅ )
9		df-ov	⊢ ( ( 1^st ‘ 𝐹 ) oppFunc tpos ( 2^nd ‘ 𝐹 ) ) = ( oppFunc ‘ ⟨ ( 1^st ‘ 𝐹 ) , tpos ( 2^nd ‘ 𝐹 ) ⟩ )
10	1 2 3	oppfrcl	⊢ ( 𝜑 → 𝐹 ∈ ( V × V ) )
11		1st2nd2	⊢ ( 𝐹 ∈ ( V × V ) → 𝐹 = ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
12	10 11	syl	⊢ ( 𝜑 → 𝐹 = ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
13	1 2 3 12	oppf1st2nd	⊢ ( 𝜑 → ( 𝐺 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝐺 ) = ( 1^st ‘ 𝐹 ) ∧ ( 2^nd ‘ 𝐺 ) = tpos ( 2^nd ‘ 𝐹 ) ) ) )
14		eqopi	⊢ ( ( 𝐺 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝐺 ) = ( 1^st ‘ 𝐹 ) ∧ ( 2^nd ‘ 𝐺 ) = tpos ( 2^nd ‘ 𝐹 ) ) ) → 𝐺 = ⟨ ( 1^st ‘ 𝐹 ) , tpos ( 2^nd ‘ 𝐹 ) ⟩ )
15	13 14	syl	⊢ ( 𝜑 → 𝐺 = ⟨ ( 1^st ‘ 𝐹 ) , tpos ( 2^nd ‘ 𝐹 ) ⟩ )
16	15	fveq2d	⊢ ( 𝜑 → ( oppFunc ‘ 𝐺 ) = ( oppFunc ‘ ⟨ ( 1^st ‘ 𝐹 ) , tpos ( 2^nd ‘ 𝐹 ) ⟩ ) )
17	9 16	eqtr4id	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐹 ) oppFunc tpos ( 2^nd ‘ 𝐹 ) ) = ( oppFunc ‘ 𝐺 ) )
18	1 2 3 12	oppfrcl3	⊢ ( 𝜑 → ( Rel ( 2^nd ‘ 𝐹 ) ∧ Rel dom ( 2^nd ‘ 𝐹 ) ) )
19		tpostpos2	⊢ ( ( Rel ( 2^nd ‘ 𝐹 ) ∧ Rel dom ( 2^nd ‘ 𝐹 ) ) → tpos tpos ( 2^nd ‘ 𝐹 ) = ( 2^nd ‘ 𝐹 ) )
20	18 19	syl	⊢ ( 𝜑 → tpos tpos ( 2^nd ‘ 𝐹 ) = ( 2^nd ‘ 𝐹 ) )
21	20	opeq2d	⊢ ( 𝜑 → ⟨ ( 1^st ‘ 𝐹 ) , tpos tpos ( 2^nd ‘ 𝐹 ) ⟩ = ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
22		0nelrel0	⊢ ( Rel dom ( 2^nd ‘ 𝐹 ) → ¬ ∅ ∈ dom ( 2^nd ‘ 𝐹 ) )
23	18 22	simpl2im	⊢ ( 𝜑 → ¬ ∅ ∈ dom ( 2^nd ‘ 𝐹 ) )
24		reldmtpos	⊢ ( Rel dom tpos ( 2^nd ‘ 𝐹 ) ↔ ¬ ∅ ∈ dom ( 2^nd ‘ 𝐹 ) )
25	23 24	sylibr	⊢ ( 𝜑 → Rel dom tpos ( 2^nd ‘ 𝐹 ) )
26		reltpos	⊢ Rel tpos ( 2^nd ‘ 𝐹 )
27	25 26	jctil	⊢ ( 𝜑 → ( Rel tpos ( 2^nd ‘ 𝐹 ) ∧ Rel dom tpos ( 2^nd ‘ 𝐹 ) ) )
28	27	iftrued	⊢ ( 𝜑 → if ( ( Rel tpos ( 2^nd ‘ 𝐹 ) ∧ Rel dom tpos ( 2^nd ‘ 𝐹 ) ) , ⟨ ( 1^st ‘ 𝐹 ) , tpos tpos ( 2^nd ‘ 𝐹 ) ⟩ , ∅ ) = ⟨ ( 1^st ‘ 𝐹 ) , tpos tpos ( 2^nd ‘ 𝐹 ) ⟩ )
29	21 28 12	3eqtr4d	⊢ ( 𝜑 → if ( ( Rel tpos ( 2^nd ‘ 𝐹 ) ∧ Rel dom tpos ( 2^nd ‘ 𝐹 ) ) , ⟨ ( 1^st ‘ 𝐹 ) , tpos tpos ( 2^nd ‘ 𝐹 ) ⟩ , ∅ ) = 𝐹 )
30	8 17 29	3eqtr3a	⊢ ( 𝜑 → ( oppFunc ‘ 𝐺 ) = 𝐹 )

Metamath Proof Explorer

Theorem 2oppf

Proof