natoppf2

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

	Ref	Expression
Hypotheses	natoppf.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
	natoppf.p	⊢ 𝑃 = ( oppCat ‘ 𝐷 )
	natoppf.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
	natoppf.m	⊢ 𝑀 = ( 𝑂 Nat 𝑃 )
	natoppfb.k	⊢ ( 𝜑 → 𝐾 = ( oppFunc ‘ 𝐹 ) )
	natoppfb.l	⊢ ( 𝜑 → 𝐿 = ( oppFunc ‘ 𝐺 ) )
	natoppf2.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) )
Assertion	natoppf2	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐿 𝑀 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		natoppf.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2		natoppf.p	⊢ 𝑃 = ( oppCat ‘ 𝐷 )
3		natoppf.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
4		natoppf.m	⊢ 𝑀 = ( 𝑂 Nat 𝑃 )
5		natoppfb.k	⊢ ( 𝜑 → 𝐾 = ( oppFunc ‘ 𝐹 ) )
6		natoppfb.l	⊢ ( 𝜑 → 𝐿 = ( oppFunc ‘ 𝐺 ) )
7		natoppf2.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) )
8	3 7	nat1st2nd	⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ 𝑁 ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ ) )
9	1 2 3 4 8	natoppf	⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ ( 1^st ‘ 𝐺 ) , tpos ( 2^nd ‘ 𝐺 ) ⟩ 𝑀 ⟨ ( 1^st ‘ 𝐹 ) , tpos ( 2^nd ‘ 𝐹 ) ⟩ ) )
10	3	natrcl	⊢ ( 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) → ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) )
11	10	simprd	⊢ ( 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) → 𝐺 ∈ ( 𝐶 Func 𝐷 ) )
12		oppfval2	⊢ ( 𝐺 ∈ ( 𝐶 Func 𝐷 ) → ( oppFunc ‘ 𝐺 ) = ⟨ ( 1^st ‘ 𝐺 ) , tpos ( 2^nd ‘ 𝐺 ) ⟩ )
13	7 11 12	3syl	⊢ ( 𝜑 → ( oppFunc ‘ 𝐺 ) = ⟨ ( 1^st ‘ 𝐺 ) , tpos ( 2^nd ‘ 𝐺 ) ⟩ )
14	6 13	eqtrd	⊢ ( 𝜑 → 𝐿 = ⟨ ( 1^st ‘ 𝐺 ) , tpos ( 2^nd ‘ 𝐺 ) ⟩ )
15	10	simpld	⊢ ( 𝐴 ∈ ( 𝐹 𝑁 𝐺 ) → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
16		oppfval2	⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( oppFunc ‘ 𝐹 ) = ⟨ ( 1^st ‘ 𝐹 ) , tpos ( 2^nd ‘ 𝐹 ) ⟩ )
17	7 15 16	3syl	⊢ ( 𝜑 → ( oppFunc ‘ 𝐹 ) = ⟨ ( 1^st ‘ 𝐹 ) , tpos ( 2^nd ‘ 𝐹 ) ⟩ )
18	5 17	eqtrd	⊢ ( 𝜑 → 𝐾 = ⟨ ( 1^st ‘ 𝐹 ) , tpos ( 2^nd ‘ 𝐹 ) ⟩ )
19	14 18	oveq12d	⊢ ( 𝜑 → ( 𝐿 𝑀 𝐾 ) = ( ⟨ ( 1^st ‘ 𝐺 ) , tpos ( 2^nd ‘ 𝐺 ) ⟩ 𝑀 ⟨ ( 1^st ‘ 𝐹 ) , tpos ( 2^nd ‘ 𝐹 ) ⟩ ) )
20	9 19	eleqtrrd	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐿 𝑀 𝐾 ) )

Metamath Proof Explorer

Theorem natoppf2

Proof