oppfdiag

Description: A diagonal functor for opposite categories is the opposite functor of the diagonal functor for original categories post-composed by an isomorphism ( fucoppc ). (Contributed by Zhi Wang, 19-Nov-2025)

	Ref	Expression
Hypotheses	oppfdiag.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
	oppfdiag.p	⊢ 𝑃 = ( oppCat ‘ 𝐷 )
	oppfdiag.l	⊢ 𝐿 = ( 𝐶 Δ_func 𝐷 )
	oppfdiag.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	oppfdiag.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	oppfdiag.f	⊢ ( 𝜑 → 𝐹 = ( oppFunc ↾ ( 𝐷 Func 𝐶 ) ) )
	oppfdiag.n	⊢ 𝑁 = ( 𝐷 Nat 𝐶 )
	oppfdiag.g	⊢ ( 𝜑 → 𝐺 = ( 𝑚 ∈ ( 𝐷 Func 𝐶 ) , 𝑛 ∈ ( 𝐷 Func 𝐶 ) ↦ ( I ↾ ( 𝑛 𝑁 𝑚 ) ) ) )
Assertion	oppfdiag	⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) = ( 𝑂 Δ_func 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		oppfdiag.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2		oppfdiag.p	⊢ 𝑃 = ( oppCat ‘ 𝐷 )
3		oppfdiag.l	⊢ 𝐿 = ( 𝐶 Δ_func 𝐷 )
4		oppfdiag.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
5		oppfdiag.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
6		oppfdiag.f	⊢ ( 𝜑 → 𝐹 = ( oppFunc ↾ ( 𝐷 Func 𝐶 ) ) )
7		oppfdiag.n	⊢ 𝑁 = ( 𝐷 Nat 𝐶 )
8		oppfdiag.g	⊢ ( 𝜑 → 𝐺 = ( 𝑚 ∈ ( 𝐷 Func 𝐶 ) , 𝑛 ∈ ( 𝐷 Func 𝐶 ) ↦ ( I ↾ ( 𝑛 𝑁 𝑚 ) ) ) )
9		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
10	1 9	oppcbas	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝑂 )
11		eqid	⊢ ( 𝑃 FuncCat 𝑂 ) = ( 𝑃 FuncCat 𝑂 )
12	11	fucbas	⊢ ( 𝑃 Func 𝑂 ) = ( Base ‘ ( 𝑃 FuncCat 𝑂 ) )
13		eqid	⊢ ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) = ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) )
14		eqid	⊢ ( 𝐷 FuncCat 𝐶 ) = ( 𝐷 FuncCat 𝐶 )
15	3 4 5 14	diagcl	⊢ ( 𝜑 → 𝐿 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐶 ) ) )
16	1 13 15	oppfoppc2	⊢ ( 𝜑 → ( oppFunc ‘ 𝐿 ) ∈ ( 𝑂 Func ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) )
17	2 1 14 13 11 7 6 8 5 4	fucoppcfunc	⊢ ( 𝜑 → 𝐹 ( ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) Func ( 𝑃 FuncCat 𝑂 ) ) 𝐺 )
18		df-br	⊢ ( 𝐹 ( ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) Func ( 𝑃 FuncCat 𝑂 ) ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) Func ( 𝑃 FuncCat 𝑂 ) ) )
19	17 18	sylib	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) Func ( 𝑃 FuncCat 𝑂 ) ) )
20	16 19	cofucl	⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ∈ ( 𝑂 Func ( 𝑃 FuncCat 𝑂 ) ) )
21	20	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) ( 𝑂 Func ( 𝑃 FuncCat 𝑂 ) ) ( 2^nd ‘ ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) )
22	10 12 21	funcf1	⊢ ( 𝜑 → ( 1^st ‘ ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) : ( Base ‘ 𝐶 ) ⟶ ( 𝑃 Func 𝑂 ) )
23	22	ffnd	⊢ ( 𝜑 → ( 1^st ‘ ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) Fn ( Base ‘ 𝐶 ) )
24		eqid	⊢ ( 𝑂 Δ_func 𝑃 ) = ( 𝑂 Δ_func 𝑃 )
25	1	oppccat	⊢ ( 𝐶 ∈ Cat → 𝑂 ∈ Cat )
26	4 25	syl	⊢ ( 𝜑 → 𝑂 ∈ Cat )
27	2	oppccat	⊢ ( 𝐷 ∈ Cat → 𝑃 ∈ Cat )
28	5 27	syl	⊢ ( 𝜑 → 𝑃 ∈ Cat )
29	24 26 28 11	diagcl	⊢ ( 𝜑 → ( 𝑂 Δ_func 𝑃 ) ∈ ( 𝑂 Func ( 𝑃 FuncCat 𝑂 ) ) )
30	29	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ( 𝑂 Func ( 𝑃 FuncCat 𝑂 ) ) ( 2^nd ‘ ( 𝑂 Δ_func 𝑃 ) ) )
31	10 12 30	funcf1	⊢ ( 𝜑 → ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) : ( Base ‘ 𝐶 ) ⟶ ( 𝑃 Func 𝑂 ) )
32	31	ffnd	⊢ ( 𝜑 → ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) Fn ( Base ‘ 𝐶 ) )
33	16	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( oppFunc ‘ 𝐿 ) ∈ ( 𝑂 Func ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) )
34	19	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) Func ( 𝑃 FuncCat 𝑂 ) ) )
35		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
36	10 33 34 35	cofu1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) ‘ 𝑥 ) = ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ ( ( 1^st ‘ ( oppFunc ‘ 𝐿 ) ) ‘ 𝑥 ) ) )
37	17	func1st	⊢ ( 𝜑 → ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
38	15	oppf1	⊢ ( 𝜑 → ( 1^st ‘ ( oppFunc ‘ 𝐿 ) ) = ( 1^st ‘ 𝐿 ) )
39	38	fveq1d	⊢ ( 𝜑 → ( ( 1^st ‘ ( oppFunc ‘ 𝐿 ) ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) )
40	37 39	fveq12d	⊢ ( 𝜑 → ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ ( ( 1^st ‘ ( oppFunc ‘ 𝐿 ) ) ‘ 𝑥 ) ) = ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) )
41	40	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ ( ( 1^st ‘ ( oppFunc ‘ 𝐿 ) ) ‘ 𝑥 ) ) = ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) )
42	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐶 ∈ Cat )
43	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐷 ∈ Cat )
44	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐹 = ( oppFunc ↾ ( 𝐷 Func 𝐶 ) ) )
45	1 2 3 42 43 44 9 35	oppfdiag1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) = ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑥 ) )
46	36 41 45	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) ‘ 𝑥 ) = ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑥 ) )
47	23 32 46	eqfnfvd	⊢ ( 𝜑 → ( 1^st ‘ ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) = ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) )
48	10 21	funcfn2	⊢ ( 𝜑 → ( 2^nd ‘ ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
49	10 30	funcfn2	⊢ ( 𝜑 → ( 2^nd ‘ ( 𝑂 Δ_func 𝑃 ) ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
50		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
51	50 1	oppchom	⊢ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) = ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 )
52	51	a1i	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) = ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) )
53		eqid	⊢ ( Hom ‘ 𝑂 ) = ( Hom ‘ 𝑂 )
54		eqid	⊢ ( 𝑃 Nat 𝑂 ) = ( 𝑃 Nat 𝑂 )
55	11 54	fuchom	⊢ ( 𝑃 Nat 𝑂 ) = ( Hom ‘ ( 𝑃 FuncCat 𝑂 ) )
56	21	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1^st ‘ ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) ( 𝑂 Func ( 𝑃 FuncCat 𝑂 ) ) ( 2^nd ‘ ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) )
57		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
58		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
59	10 53 55 56 57 58	funcf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2^nd ‘ ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) ‘ 𝑥 ) ( 𝑃 Nat 𝑂 ) ( ( 1^st ‘ ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) ‘ 𝑦 ) ) )
60	52 59	feq2dd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2^nd ‘ ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) 𝑦 ) : ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ⟶ ( ( ( 1^st ‘ ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) ‘ 𝑥 ) ( 𝑃 Nat 𝑂 ) ( ( 1^st ‘ ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) ‘ 𝑦 ) ) )
61	60	ffnd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2^nd ‘ ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) 𝑦 ) Fn ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) )
62	30	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ( 𝑂 Func ( 𝑃 FuncCat 𝑂 ) ) ( 2^nd ‘ ( 𝑂 Δ_func 𝑃 ) ) )
63	10 53 55 62 57 58	funcf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2^nd ‘ ( 𝑂 Δ_func 𝑃 ) ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑥 ) ( 𝑃 Nat 𝑂 ) ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑦 ) ) )
64	52 63	feq2dd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2^nd ‘ ( 𝑂 Δ_func 𝑃 ) ) 𝑦 ) : ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ⟶ ( ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑥 ) ( 𝑃 Nat 𝑂 ) ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑦 ) ) )
65	64	ffnd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2^nd ‘ ( 𝑂 Δ_func 𝑃 ) ) 𝑦 ) Fn ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) )
66	16	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) → ( oppFunc ‘ 𝐿 ) ∈ ( 𝑂 Func ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) )
67	19	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) Func ( 𝑃 FuncCat 𝑂 ) ) )
68	57	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
69	58	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
70		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) → 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) )
71	70 51	eleqtrrdi	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) )
72	10 66 67 68 69 53 71	cofu2	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) → ( ( 𝑥 ( 2^nd ‘ ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) 𝑦 ) ‘ 𝑓 ) = ( ( ( ( 1^st ‘ ( oppFunc ‘ 𝐿 ) ) ‘ 𝑥 ) ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ( ( 1^st ‘ ( oppFunc ‘ 𝐿 ) ) ‘ 𝑦 ) ) ‘ ( ( 𝑥 ( 2^nd ‘ ( oppFunc ‘ 𝐿 ) ) 𝑦 ) ‘ 𝑓 ) ) )
73	17	func2nd	⊢ ( 𝜑 → ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )
74	38	fveq1d	⊢ ( 𝜑 → ( ( 1^st ‘ ( oppFunc ‘ 𝐿 ) ) ‘ 𝑦 ) = ( ( 1^st ‘ 𝐿 ) ‘ 𝑦 ) )
75	73 39 74	oveq123d	⊢ ( 𝜑 → ( ( ( 1^st ‘ ( oppFunc ‘ 𝐿 ) ) ‘ 𝑥 ) ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ( ( 1^st ‘ ( oppFunc ‘ 𝐿 ) ) ‘ 𝑦 ) ) = ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝐺 ( ( 1^st ‘ 𝐿 ) ‘ 𝑦 ) ) )
76	15	oppf2	⊢ ( 𝜑 → ( 𝑥 ( 2^nd ‘ ( oppFunc ‘ 𝐿 ) ) 𝑦 ) = ( 𝑦 ( 2^nd ‘ 𝐿 ) 𝑥 ) )
77	76	fveq1d	⊢ ( 𝜑 → ( ( 𝑥 ( 2^nd ‘ ( oppFunc ‘ 𝐿 ) ) 𝑦 ) ‘ 𝑓 ) = ( ( 𝑦 ( 2^nd ‘ 𝐿 ) 𝑥 ) ‘ 𝑓 ) )
78	75 77	fveq12d	⊢ ( 𝜑 → ( ( ( ( 1^st ‘ ( oppFunc ‘ 𝐿 ) ) ‘ 𝑥 ) ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ( ( 1^st ‘ ( oppFunc ‘ 𝐿 ) ) ‘ 𝑦 ) ) ‘ ( ( 𝑥 ( 2^nd ‘ ( oppFunc ‘ 𝐿 ) ) 𝑦 ) ‘ 𝑓 ) ) = ( ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝐺 ( ( 1^st ‘ 𝐿 ) ‘ 𝑦 ) ) ‘ ( ( 𝑦 ( 2^nd ‘ 𝐿 ) 𝑥 ) ‘ 𝑓 ) ) )
79	78	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) → ( ( ( ( 1^st ‘ ( oppFunc ‘ 𝐿 ) ) ‘ 𝑥 ) ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ( ( 1^st ‘ ( oppFunc ‘ 𝐿 ) ) ‘ 𝑦 ) ) ‘ ( ( 𝑥 ( 2^nd ‘ ( oppFunc ‘ 𝐿 ) ) 𝑦 ) ‘ 𝑓 ) ) = ( ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝐺 ( ( 1^st ‘ 𝐿 ) ‘ 𝑦 ) ) ‘ ( ( 𝑦 ( 2^nd ‘ 𝐿 ) 𝑥 ) ‘ 𝑓 ) ) )
80	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) → 𝐺 = ( 𝑚 ∈ ( 𝐷 Func 𝐶 ) , 𝑛 ∈ ( 𝐷 Func 𝐶 ) ↦ ( I ↾ ( 𝑛 𝑁 𝑚 ) ) ) )
81	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) → 𝐶 ∈ Cat )
82	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) → 𝐷 ∈ Cat )
83		eqid	⊢ ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 )
84	3 81 82 9 68 83	diag1cl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) → ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ∈ ( 𝐷 Func 𝐶 ) )
85		eqid	⊢ ( ( 1^st ‘ 𝐿 ) ‘ 𝑦 ) = ( ( 1^st ‘ 𝐿 ) ‘ 𝑦 )
86	3 81 82 9 69 85	diag1cl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) → ( ( 1^st ‘ 𝐿 ) ‘ 𝑦 ) ∈ ( 𝐷 Func 𝐶 ) )
87		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
88	3 9 87 50 81 82 69 68 70	diag2	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) → ( ( 𝑦 ( 2^nd ‘ 𝐿 ) 𝑥 ) ‘ 𝑓 ) = ( ( Base ‘ 𝐷 ) × { 𝑓 } ) )
89	3 9 87 50 81 82 69 68 70 7	diag2cl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) → ( ( Base ‘ 𝐷 ) × { 𝑓 } ) ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑦 ) 𝑁 ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) ) )
90	80 84 86 88 89	opf2	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) → ( ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑥 ) 𝐺 ( ( 1^st ‘ 𝐿 ) ‘ 𝑦 ) ) ‘ ( ( 𝑦 ( 2^nd ‘ 𝐿 ) 𝑥 ) ‘ 𝑓 ) ) = ( ( Base ‘ 𝐷 ) × { 𝑓 } ) )
91	72 79 90	3eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) → ( ( 𝑥 ( 2^nd ‘ ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) 𝑦 ) ‘ 𝑓 ) = ( ( Base ‘ 𝐷 ) × { 𝑓 } ) )
92	2 87	oppcbas	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝑃 )
93	81 25	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) → 𝑂 ∈ Cat )
94	82 27	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) → 𝑃 ∈ Cat )
95	24 10 92 53 93 94 68 69 71	diag2	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) → ( ( 𝑥 ( 2^nd ‘ ( 𝑂 Δ_func 𝑃 ) ) 𝑦 ) ‘ 𝑓 ) = ( ( Base ‘ 𝐷 ) × { 𝑓 } ) )
96	91 95	eqtr4d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) → ( ( 𝑥 ( 2^nd ‘ ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) 𝑦 ) ‘ 𝑓 ) = ( ( 𝑥 ( 2^nd ‘ ( 𝑂 Δ_func 𝑃 ) ) 𝑦 ) ‘ 𝑓 ) )
97	61 65 96	eqfnfvd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2^nd ‘ ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) 𝑦 ) = ( 𝑥 ( 2^nd ‘ ( 𝑂 Δ_func 𝑃 ) ) 𝑦 ) )
98	48 49 97	eqfnovd	⊢ ( 𝜑 → ( 2^nd ‘ ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) = ( 2^nd ‘ ( 𝑂 Δ_func 𝑃 ) ) )
99	47 98	opeq12d	⊢ ( 𝜑 → ⟨ ( 1^st ‘ ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) , ( 2^nd ‘ ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) ⟩ = ⟨ ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) , ( 2^nd ‘ ( 𝑂 Δ_func 𝑃 ) ) ⟩ )
100		relfunc	⊢ Rel ( 𝑂 Func ( 𝑃 FuncCat 𝑂 ) )
101		1st2nd	⊢ ( ( Rel ( 𝑂 Func ( 𝑃 FuncCat 𝑂 ) ) ∧ ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ∈ ( 𝑂 Func ( 𝑃 FuncCat 𝑂 ) ) ) → ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) = ⟨ ( 1^st ‘ ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) , ( 2^nd ‘ ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) ⟩ )
102	100 20 101	sylancr	⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) = ⟨ ( 1^st ‘ ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) , ( 2^nd ‘ ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) ⟩ )
103		1st2nd	⊢ ( ( Rel ( 𝑂 Func ( 𝑃 FuncCat 𝑂 ) ) ∧ ( 𝑂 Δ_func 𝑃 ) ∈ ( 𝑂 Func ( 𝑃 FuncCat 𝑂 ) ) ) → ( 𝑂 Δ_func 𝑃 ) = ⟨ ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) , ( 2^nd ‘ ( 𝑂 Δ_func 𝑃 ) ) ⟩ )
104	100 29 103	sylancr	⊢ ( 𝜑 → ( 𝑂 Δ_func 𝑃 ) = ⟨ ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) , ( 2^nd ‘ ( 𝑂 Δ_func 𝑃 ) ) ⟩ )
105	99 102 104	3eqtr4d	⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝐺 ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) = ( 𝑂 Δ_func 𝑃 ) )

Metamath Proof Explorer

Theorem oppfdiag

Proof