natoppf2

Description: A natural transformation is natural between opposite functors. (Contributed by Zhi Wang, 18-Nov-2025)

	Ref	Expression
Hypotheses	natoppf.o	$⊢ O = oppCat (C)$
	natoppf.p	$⊢ P = oppCat (D)$
	natoppf.n	$⊢ N = C Nat D$
	natoppf.m	$⊢ M = O Nat P$
	natoppfb.k	No typesetting found for \|- ( ph -> K = ( oppFunc ` F ) ) with typecode \|-
	natoppfb.l	No typesetting found for \|- ( ph -> L = ( oppFunc ` G ) ) with typecode \|-
	natoppf2.a	$⊢ φ \to A \in (F N G)$
Assertion	natoppf2	$⊢ φ \to A \in (L M K)$

Proof

Step	Hyp	Ref	Expression
1		natoppf.o	$⊢ O = oppCat (C)$
2		natoppf.p	$⊢ P = oppCat (D)$
3		natoppf.n	$⊢ N = C Nat D$
4		natoppf.m	$⊢ M = O Nat P$
5		natoppfb.k	Could not format ( ph -> K = ( oppFunc ` F ) ) : No typesetting found for \|- ( ph -> K = ( oppFunc ` F ) ) with typecode \|-
6		natoppfb.l	Could not format ( ph -> L = ( oppFunc ` G ) ) : No typesetting found for \|- ( ph -> L = ( oppFunc ` G ) ) with typecode \|-
7		natoppf2.a	$⊢ φ \to A \in (F N G)$
8	3 7	nat1st2nd	$⊢ φ \to A \in (⟨1^{st} (F), 2^{nd} (F)⟩ N ⟨1^{st} (G), 2^{nd} (G)⟩)$
9	1 2 3 4 8	natoppf	$⊢ φ \to A \in (⟨1^{st} (G), tpos 2^{nd} (G)⟩ M ⟨1^{st} (F), tpos 2^{nd} (F)⟩)$
10	3	natrcl	$⊢ A \in (F N G) \to (F \in (C Func D) \land G \in (C Func D))$
11	10	simprd	$⊢ A \in (F N G) \to G \in (C Func D)$
12		oppfval2	Could not format ( G e. ( C Func D ) -> ( oppFunc ` G ) = <. ( 1st ` G ) , tpos ( 2nd ` G ) >. ) : No typesetting found for \|- ( G e. ( C Func D ) -> ( oppFunc ` G ) = <. ( 1st ` G ) , tpos ( 2nd ` G ) >. ) with typecode \|-
13	7 11 12	3syl	Could not format ( ph -> ( oppFunc ` G ) = <. ( 1st ` G ) , tpos ( 2nd ` G ) >. ) : No typesetting found for \|- ( ph -> ( oppFunc ` G ) = <. ( 1st ` G ) , tpos ( 2nd ` G ) >. ) with typecode \|-
14	6 13	eqtrd	$⊢ φ \to L = ⟨1^{st} (G), tpos 2^{nd} (G)⟩$
15	10	simpld	$⊢ A \in (F N G) \to F \in (C Func D)$
16		oppfval2	Could not format ( F e. ( C Func D ) -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) : No typesetting found for \|- ( F e. ( C Func D ) -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) with typecode \|-
17	7 15 16	3syl	Could not format ( ph -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) : No typesetting found for \|- ( ph -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) with typecode \|-
18	5 17	eqtrd	$⊢ φ \to K = ⟨1^{st} (F), tpos 2^{nd} (F)⟩$
19	14 18	oveq12d	$⊢ φ \to L M K = ⟨1^{st} (G), tpos 2^{nd} (G)⟩ M ⟨1^{st} (F), tpos 2^{nd} (F)⟩$
20	9 19	eleqtrrd	$⊢ φ \to A \in (L M K)$

Metamath Proof Explorer

Theorem natoppf2

Proof