Theorem natrcl2

Description: Reverse closure for a natural transformation. (Contributed by Zhi Wang, 1-Oct-2025)

	Ref	Expression
Hypotheses	natrcl2.n	$$⊢N=C\mathrm{Nat}D$$
	natrcl2.a	$$⊢\phi \to A\in \left(⟨F,G⟩N⟨K,L⟩\right)$$
Assertion	natrcl2	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$

Proof

Step	Hyp	Ref	Expression
1		natrcl2.n	$$⊢N=C\mathrm{Nat}D$$
2		natrcl2.a	$$⊢\phi \to A\in \left(⟨F,G⟩N⟨K,L⟩\right)$$
3	1	natrcl	$$⊢A\in \left(⟨F,G⟩N⟨K,L⟩\right)\to \left(⟨F,G⟩\in \left(C\mathrm{Func}D\right)\wedge ⟨K,L⟩\in \left(C\mathrm{Func}D\right)\right)$$
4	2 3	syl	$$⊢\phi \to \left(⟨F,G⟩\in \left(C\mathrm{Func}D\right)\wedge ⟨K,L⟩\in \left(C\mathrm{Func}D\right)\right)$$
5	4	simpld	$$⊢\phi \to ⟨F,G⟩\in \left(C\mathrm{Func}D\right)$$
6		df-br	$$⊢F\left(C\mathrm{Func}D\right)G\leftrightarrow ⟨F,G⟩\in \left(C\mathrm{Func}D\right)$$
7	5 6	sylibr	$$⊢\phi \to F\left(C\mathrm{Func}D\right)G$$