Theorem fucoppcffth

Description: A fully faithful functor from the opposite category of functors to the category of opposite functors. (Contributed by Zhi Wang, 19-Nov-2025)

	Ref	Expression
Hypotheses	fucoppc.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
	fucoppc.p	⊢ 𝑃 = ( oppCat ‘ 𝐷 )
	fucoppc.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
	fucoppc.r	⊢ 𝑅 = ( oppCat ‘ 𝑄 )
	fucoppc.s	⊢ 𝑆 = ( 𝑂 FuncCat 𝑃 )
	fucoppc.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
	fucoppc.f	⊢ ( 𝜑 → 𝐹 = ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) )
	fucoppc.g	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ ( 𝐶 Func 𝐷 ) , 𝑦 ∈ ( 𝐶 Func 𝐷 ) ↦ ( I ↾ ( 𝑦 𝑁 𝑥 ) ) ) )
	fucoppcffth.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	fucoppcffth.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
Assertion	fucoppcffth	⊢ ( 𝜑 → 𝐹 ( ( 𝑅 Full 𝑆 ) ∩ ( 𝑅 Faith 𝑆 ) ) 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		fucoppc.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2		fucoppc.p	⊢ 𝑃 = ( oppCat ‘ 𝐷 )
3		fucoppc.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
4		fucoppc.r	⊢ 𝑅 = ( oppCat ‘ 𝑄 )
5		fucoppc.s	⊢ 𝑆 = ( 𝑂 FuncCat 𝑃 )
6		fucoppc.n	⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
7		fucoppc.f	⊢ ( 𝜑 → 𝐹 = ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) )
8		fucoppc.g	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ ( 𝐶 Func 𝐷 ) , 𝑦 ∈ ( 𝐶 Func 𝐷 ) ↦ ( I ↾ ( 𝑦 𝑁 𝑥 ) ) ) )
9		fucoppcffth.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
10		fucoppcffth.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
11		eqid	⊢ ( CatCat ‘ { 𝑅 , 𝑆 } ) = ( CatCat ‘ { 𝑅 , 𝑆 } )
12		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
13		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
14		eqid	⊢ ( Iso ‘ ( CatCat ‘ { 𝑅 , 𝑆 } ) ) = ( Iso ‘ ( CatCat ‘ { 𝑅 , 𝑆 } ) )
15		eqid	⊢ ( Base ‘ ( CatCat ‘ { 𝑅 , 𝑆 } ) ) = ( Base ‘ ( CatCat ‘ { 𝑅 , 𝑆 } ) )
16	3 9 10	fuccat	⊢ ( 𝜑 → 𝑄 ∈ Cat )
17	4	oppccat	⊢ ( 𝑄 ∈ Cat → 𝑅 ∈ Cat )
18	16 17	syl	⊢ ( 𝜑 → 𝑅 ∈ Cat )
19		prid1g	⊢ ( 𝑅 ∈ Cat → 𝑅 ∈ { 𝑅 , 𝑆 } )
20	18 19	syl	⊢ ( 𝜑 → 𝑅 ∈ { 𝑅 , 𝑆 } )
21	20 18	elind	⊢ ( 𝜑 → 𝑅 ∈ ( { 𝑅 , 𝑆 } ∩ Cat ) )
22		prex	⊢ { 𝑅 , 𝑆 } ∈ V
23	22	a1i	⊢ ( 𝜑 → { 𝑅 , 𝑆 } ∈ V )
24	11 15 23	catcbas	⊢ ( 𝜑 → ( Base ‘ ( CatCat ‘ { 𝑅 , 𝑆 } ) ) = ( { 𝑅 , 𝑆 } ∩ Cat ) )
25	21 24	eleqtrrd	⊢ ( 𝜑 → 𝑅 ∈ ( Base ‘ ( CatCat ‘ { 𝑅 , 𝑆 } ) ) )
26	1	oppccat	⊢ ( 𝐶 ∈ Cat → 𝑂 ∈ Cat )
27	9 26	syl	⊢ ( 𝜑 → 𝑂 ∈ Cat )
28	2	oppccat	⊢ ( 𝐷 ∈ Cat → 𝑃 ∈ Cat )
29	10 28	syl	⊢ ( 𝜑 → 𝑃 ∈ Cat )
30	5 27 29	fuccat	⊢ ( 𝜑 → 𝑆 ∈ Cat )
31		prid2g	⊢ ( 𝑆 ∈ Cat → 𝑆 ∈ { 𝑅 , 𝑆 } )
32	30 31	syl	⊢ ( 𝜑 → 𝑆 ∈ { 𝑅 , 𝑆 } )
33	32 30	elind	⊢ ( 𝜑 → 𝑆 ∈ ( { 𝑅 , 𝑆 } ∩ Cat ) )
34	33 24	eleqtrrd	⊢ ( 𝜑 → 𝑆 ∈ ( Base ‘ ( CatCat ‘ { 𝑅 , 𝑆 } ) ) )
35	1 2 3 4 5 6 7 8 11 15 14 9 10 25 34	fucoppc	⊢ ( 𝜑 → 𝐹 ( 𝑅 ( Iso ‘ ( CatCat ‘ { 𝑅 , 𝑆 } ) ) 𝑆 ) 𝐺 )
36		df-br	⊢ ( 𝐹 ( 𝑅 ( Iso ‘ ( CatCat ‘ { 𝑅 , 𝑆 } ) ) 𝑆 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑅 ( Iso ‘ ( CatCat ‘ { 𝑅 , 𝑆 } ) ) 𝑆 ) )
37	35 36	sylib	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑅 ( Iso ‘ ( CatCat ‘ { 𝑅 , 𝑆 } ) ) 𝑆 ) )
38	11 12 13 14 37	catcisoi	⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( ( 𝑅 Full 𝑆 ) ∩ ( 𝑅 Faith 𝑆 ) ) ∧ ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ 𝑆 ) ) )
39	38	simpld	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( ( 𝑅 Full 𝑆 ) ∩ ( 𝑅 Faith 𝑆 ) ) )
40		df-br	⊢ ( 𝐹 ( ( 𝑅 Full 𝑆 ) ∩ ( 𝑅 Faith 𝑆 ) ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( ( 𝑅 Full 𝑆 ) ∩ ( 𝑅 Faith 𝑆 ) ) )
41	39 40	sylibr	⊢ ( 𝜑 → 𝐹 ( ( 𝑅 Full 𝑆 ) ∩ ( 𝑅 Faith 𝑆 ) ) 𝐺 )