oppfdiag1

Description: A constant functor for opposite categories is the opposite functor of the constant functor for original categories. (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 )
	oppfdiag1.f	⊢ ( 𝜑 → 𝐹 = ( oppFunc ↾ ( 𝐷 Func 𝐶 ) ) )
	oppfdiag1.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
	oppfdiag1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
Assertion	oppfdiag1	⊢ ( 𝜑 → ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) = ( ( 1^st ‘ ( 𝑂 Δ_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		oppfdiag1.f	⊢ ( 𝜑 → 𝐹 = ( oppFunc ↾ ( 𝐷 Func 𝐶 ) ) )
7		oppfdiag1.a	⊢ 𝐴 = ( Base ‘ 𝐶 )
8		oppfdiag1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
9		eqid	⊢ ( 𝐷 FuncCat 𝐶 ) = ( 𝐷 FuncCat 𝐶 )
10	9	fucbas	⊢ ( 𝐷 Func 𝐶 ) = ( Base ‘ ( 𝐷 FuncCat 𝐶 ) )
11	3 4 5 9	diagcl	⊢ ( 𝜑 → 𝐿 ∈ ( 𝐶 Func ( 𝐷 FuncCat 𝐶 ) ) )
12	11	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ 𝐿 ) ( 𝐶 Func ( 𝐷 FuncCat 𝐶 ) ) ( 2^nd ‘ 𝐿 ) )
13	7 10 12	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐿 ) : 𝐴 ⟶ ( 𝐷 Func 𝐶 ) )
14	13 8	ffvelcdmd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∈ ( 𝐷 Func 𝐶 ) )
15	6 14	opf11	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) = ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) )
16		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
17	2 16	oppcbas	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝑃 )
18	1 7	oppcbas	⊢ 𝐴 = ( Base ‘ 𝑂 )
19		eqid	⊢ ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) = ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) )
20	1 19 11	oppfoppc2	⊢ ( 𝜑 → ( oppFunc ‘ 𝐿 ) ∈ ( 𝑂 Func ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) ) )
21		eqid	⊢ ( 𝑃 FuncCat 𝑂 ) = ( 𝑃 FuncCat 𝑂 )
22		eqid	⊢ ( 𝐷 Nat 𝐶 ) = ( 𝐷 Nat 𝐶 )
23		eqidd	⊢ ( 𝜑 → ( 𝑚 ∈ ( 𝐷 Func 𝐶 ) , 𝑛 ∈ ( 𝐷 Func 𝐶 ) ↦ ( I ↾ ( 𝑛 ( 𝐷 Nat 𝐶 ) 𝑚 ) ) ) = ( 𝑚 ∈ ( 𝐷 Func 𝐶 ) , 𝑛 ∈ ( 𝐷 Func 𝐶 ) ↦ ( I ↾ ( 𝑛 ( 𝐷 Nat 𝐶 ) 𝑚 ) ) ) )
24	2 1 9 19 21 22 6 23 5 4	fucoppcfunc	⊢ ( 𝜑 → 𝐹 ( ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) Func ( 𝑃 FuncCat 𝑂 ) ) ( 𝑚 ∈ ( 𝐷 Func 𝐶 ) , 𝑛 ∈ ( 𝐷 Func 𝐶 ) ↦ ( I ↾ ( 𝑛 ( 𝐷 Nat 𝐶 ) 𝑚 ) ) ) )
25		df-br	⊢ ( 𝐹 ( ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) Func ( 𝑃 FuncCat 𝑂 ) ) ( 𝑚 ∈ ( 𝐷 Func 𝐶 ) , 𝑛 ∈ ( 𝐷 Func 𝐶 ) ↦ ( I ↾ ( 𝑛 ( 𝐷 Nat 𝐶 ) 𝑚 ) ) ) ↔ ⟨ 𝐹 , ( 𝑚 ∈ ( 𝐷 Func 𝐶 ) , 𝑛 ∈ ( 𝐷 Func 𝐶 ) ↦ ( I ↾ ( 𝑛 ( 𝐷 Nat 𝐶 ) 𝑚 ) ) ) ⟩ ∈ ( ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) Func ( 𝑃 FuncCat 𝑂 ) ) )
26	24 25	sylib	⊢ ( 𝜑 → ⟨ 𝐹 , ( 𝑚 ∈ ( 𝐷 Func 𝐶 ) , 𝑛 ∈ ( 𝐷 Func 𝐶 ) ↦ ( I ↾ ( 𝑛 ( 𝐷 Nat 𝐶 ) 𝑚 ) ) ) ⟩ ∈ ( ( oppCat ‘ ( 𝐷 FuncCat 𝐶 ) ) Func ( 𝑃 FuncCat 𝑂 ) ) )
27	18 20 26 8	cofu1	⊢ ( 𝜑 → ( ( 1^st ‘ ( ⟨ 𝐹 , ( 𝑚 ∈ ( 𝐷 Func 𝐶 ) , 𝑛 ∈ ( 𝐷 Func 𝐶 ) ↦ ( I ↾ ( 𝑛 ( 𝐷 Nat 𝐶 ) 𝑚 ) ) ) ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) ‘ 𝑋 ) = ( ( 1^st ‘ ⟨ 𝐹 , ( 𝑚 ∈ ( 𝐷 Func 𝐶 ) , 𝑛 ∈ ( 𝐷 Func 𝐶 ) ↦ ( I ↾ ( 𝑛 ( 𝐷 Nat 𝐶 ) 𝑚 ) ) ) ⟩ ) ‘ ( ( 1^st ‘ ( oppFunc ‘ 𝐿 ) ) ‘ 𝑋 ) ) )
28	24	func1st	⊢ ( 𝜑 → ( 1^st ‘ ⟨ 𝐹 , ( 𝑚 ∈ ( 𝐷 Func 𝐶 ) , 𝑛 ∈ ( 𝐷 Func 𝐶 ) ↦ ( I ↾ ( 𝑛 ( 𝐷 Nat 𝐶 ) 𝑚 ) ) ) ⟩ ) = 𝐹 )
29	11	oppf1	⊢ ( 𝜑 → ( 1^st ‘ ( oppFunc ‘ 𝐿 ) ) = ( 1^st ‘ 𝐿 ) )
30	29	fveq1d	⊢ ( 𝜑 → ( ( 1^st ‘ ( oppFunc ‘ 𝐿 ) ) ‘ 𝑋 ) = ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) )
31	28 30	fveq12d	⊢ ( 𝜑 → ( ( 1^st ‘ ⟨ 𝐹 , ( 𝑚 ∈ ( 𝐷 Func 𝐶 ) , 𝑛 ∈ ( 𝐷 Func 𝐶 ) ↦ ( I ↾ ( 𝑛 ( 𝐷 Nat 𝐶 ) 𝑚 ) ) ) ⟩ ) ‘ ( ( 1^st ‘ ( oppFunc ‘ 𝐿 ) ) ‘ 𝑋 ) ) = ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) )
32	27 31	eqtrd	⊢ ( 𝜑 → ( ( 1^st ‘ ( ⟨ 𝐹 , ( 𝑚 ∈ ( 𝐷 Func 𝐶 ) , 𝑛 ∈ ( 𝐷 Func 𝐶 ) ↦ ( I ↾ ( 𝑛 ( 𝐷 Nat 𝐶 ) 𝑚 ) ) ) ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) ‘ 𝑋 ) = ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) )
33	21	fucbas	⊢ ( 𝑃 Func 𝑂 ) = ( Base ‘ ( 𝑃 FuncCat 𝑂 ) )
34	20 26	cofucl	⊢ ( 𝜑 → ( ⟨ 𝐹 , ( 𝑚 ∈ ( 𝐷 Func 𝐶 ) , 𝑛 ∈ ( 𝐷 Func 𝐶 ) ↦ ( I ↾ ( 𝑛 ( 𝐷 Nat 𝐶 ) 𝑚 ) ) ) ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ∈ ( 𝑂 Func ( 𝑃 FuncCat 𝑂 ) ) )
35	34	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ ( ⟨ 𝐹 , ( 𝑚 ∈ ( 𝐷 Func 𝐶 ) , 𝑛 ∈ ( 𝐷 Func 𝐶 ) ↦ ( I ↾ ( 𝑛 ( 𝐷 Nat 𝐶 ) 𝑚 ) ) ) ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) ( 𝑂 Func ( 𝑃 FuncCat 𝑂 ) ) ( 2^nd ‘ ( ⟨ 𝐹 , ( 𝑚 ∈ ( 𝐷 Func 𝐶 ) , 𝑛 ∈ ( 𝐷 Func 𝐶 ) ↦ ( I ↾ ( 𝑛 ( 𝐷 Nat 𝐶 ) 𝑚 ) ) ) ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) )
36	18 33 35	funcf1	⊢ ( 𝜑 → ( 1^st ‘ ( ⟨ 𝐹 , ( 𝑚 ∈ ( 𝐷 Func 𝐶 ) , 𝑛 ∈ ( 𝐷 Func 𝐶 ) ↦ ( I ↾ ( 𝑛 ( 𝐷 Nat 𝐶 ) 𝑚 ) ) ) ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) : 𝐴 ⟶ ( 𝑃 Func 𝑂 ) )
37	36 8	ffvelcdmd	⊢ ( 𝜑 → ( ( 1^st ‘ ( ⟨ 𝐹 , ( 𝑚 ∈ ( 𝐷 Func 𝐶 ) , 𝑛 ∈ ( 𝐷 Func 𝐶 ) ↦ ( I ↾ ( 𝑛 ( 𝐷 Nat 𝐶 ) 𝑚 ) ) ) ⟩ ∘_func ( oppFunc ‘ 𝐿 ) ) ) ‘ 𝑋 ) ∈ ( 𝑃 Func 𝑂 ) )
38	32 37	eqeltrrd	⊢ ( 𝜑 → ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ∈ ( 𝑃 Func 𝑂 ) )
39	38	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ( 𝑃 Func 𝑂 ) ( 2^nd ‘ ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) )
40	17 18 39	funcf1	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) : ( Base ‘ 𝐷 ) ⟶ 𝐴 )
41	15 40	feq1dd	⊢ ( 𝜑 → ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) : ( Base ‘ 𝐷 ) ⟶ 𝐴 )
42	41	ffnd	⊢ ( 𝜑 → ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) Fn ( Base ‘ 𝐷 ) )
43		eqid	⊢ ( 𝑂 Δ_func 𝑃 ) = ( 𝑂 Δ_func 𝑃 )
44	1	oppccat	⊢ ( 𝐶 ∈ Cat → 𝑂 ∈ Cat )
45	4 44	syl	⊢ ( 𝜑 → 𝑂 ∈ Cat )
46	2	oppccat	⊢ ( 𝐷 ∈ Cat → 𝑃 ∈ Cat )
47	5 46	syl	⊢ ( 𝜑 → 𝑃 ∈ Cat )
48	43 45 47 21	diagcl	⊢ ( 𝜑 → ( 𝑂 Δ_func 𝑃 ) ∈ ( 𝑂 Func ( 𝑃 FuncCat 𝑂 ) ) )
49	48	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ( 𝑂 Func ( 𝑃 FuncCat 𝑂 ) ) ( 2^nd ‘ ( 𝑂 Δ_func 𝑃 ) ) )
50	18 33 49	funcf1	⊢ ( 𝜑 → ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) : 𝐴 ⟶ ( 𝑃 Func 𝑂 ) )
51	50 8	ffvelcdmd	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) ∈ ( 𝑃 Func 𝑂 ) )
52	51	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) ) ( 𝑃 Func 𝑂 ) ( 2^nd ‘ ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) ) )
53	17 18 52	funcf1	⊢ ( 𝜑 → ( 1^st ‘ ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) ) : ( Base ‘ 𝐷 ) ⟶ 𝐴 )
54	53	ffnd	⊢ ( 𝜑 → ( 1^st ‘ ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) ) Fn ( Base ‘ 𝐷 ) )
55	4	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → 𝐶 ∈ Cat )
56	5	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → 𝐷 ∈ Cat )
57	8	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → 𝑋 ∈ 𝐴 )
58		eqid	⊢ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) = ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 )
59		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → 𝑦 ∈ ( Base ‘ 𝐷 ) )
60	3 55 56 7 57 58 16 59	diag11	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ 𝑦 ) = 𝑋 )
61	45	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → 𝑂 ∈ Cat )
62	47	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → 𝑃 ∈ Cat )
63		eqid	⊢ ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) = ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 )
64	43 61 62 18 57 63 17 59	diag11	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ( ( 1^st ‘ ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) ) ‘ 𝑦 ) = 𝑋 )
65	60 64	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐷 ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ 𝑦 ) = ( ( 1^st ‘ ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) ) ‘ 𝑦 ) )
66	42 54 65	eqfnfvd	⊢ ( 𝜑 → ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) = ( 1^st ‘ ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) ) )
67	15 66	eqtrd	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) = ( 1^st ‘ ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) ) )
68	17 39	funcfn2	⊢ ( 𝜑 → ( 2^nd ‘ ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) Fn ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) )
69	17 52	funcfn2	⊢ ( 𝜑 → ( 2^nd ‘ ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) ) Fn ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) )
70	6 14	opf12	⊢ ( 𝜑 → ( 𝑦 ( 2^nd ‘ ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) 𝑧 ) = ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) 𝑦 ) )
71	70	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) → ( 𝑦 ( 2^nd ‘ ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) 𝑧 ) = ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) 𝑦 ) )
72		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
73	72 2	oppchom	⊢ ( 𝑦 ( Hom ‘ 𝑃 ) 𝑧 ) = ( 𝑧 ( Hom ‘ 𝐷 ) 𝑦 )
74	73	a1i	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) → ( 𝑦 ( Hom ‘ 𝑃 ) 𝑧 ) = ( 𝑧 ( Hom ‘ 𝐷 ) 𝑦 ) )
75		eqid	⊢ ( Hom ‘ 𝑃 ) = ( Hom ‘ 𝑃 )
76		eqid	⊢ ( Hom ‘ 𝑂 ) = ( Hom ‘ 𝑂 )
77	39	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) → ( 1^st ‘ ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ( 𝑃 Func 𝑂 ) ( 2^nd ‘ ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) )
78		simprl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐷 ) )
79		simprr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) → 𝑧 ∈ ( Base ‘ 𝐷 ) )
80	17 75 76 77 78 79	funcf2	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) → ( 𝑦 ( 2^nd ‘ ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) 𝑧 ) : ( 𝑦 ( Hom ‘ 𝑃 ) 𝑧 ) ⟶ ( ( ( 1^st ‘ ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ‘ 𝑦 ) ( Hom ‘ 𝑂 ) ( ( 1^st ‘ ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ‘ 𝑧 ) ) )
81	74 80	feq2dd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) → ( 𝑦 ( 2^nd ‘ ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) 𝑧 ) : ( 𝑧 ( Hom ‘ 𝐷 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ‘ 𝑦 ) ( Hom ‘ 𝑂 ) ( ( 1^st ‘ ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ‘ 𝑧 ) ) )
82	71 81	feq1dd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) → ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) 𝑦 ) : ( 𝑧 ( Hom ‘ 𝐷 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ‘ 𝑦 ) ( Hom ‘ 𝑂 ) ( ( 1^st ‘ ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ‘ 𝑧 ) ) )
83	82	ffnd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) → ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) 𝑦 ) Fn ( 𝑧 ( Hom ‘ 𝐷 ) 𝑦 ) )
84	52	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) → ( 1^st ‘ ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) ) ( 𝑃 Func 𝑂 ) ( 2^nd ‘ ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) ) )
85	17 75 76 84 78 79	funcf2	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) → ( 𝑦 ( 2^nd ‘ ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) ) 𝑧 ) : ( 𝑦 ( Hom ‘ 𝑃 ) 𝑧 ) ⟶ ( ( ( 1^st ‘ ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) ) ‘ 𝑦 ) ( Hom ‘ 𝑂 ) ( ( 1^st ‘ ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) ) ‘ 𝑧 ) ) )
86	74 85	feq2dd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) → ( 𝑦 ( 2^nd ‘ ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) ) 𝑧 ) : ( 𝑧 ( Hom ‘ 𝐷 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) ) ‘ 𝑦 ) ( Hom ‘ 𝑂 ) ( ( 1^st ‘ ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) ) ‘ 𝑧 ) ) )
87	86	ffnd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) → ( 𝑦 ( 2^nd ‘ ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) ) 𝑧 ) Fn ( 𝑧 ( Hom ‘ 𝐷 ) 𝑦 ) )
88		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
89	1 88	oppcid	⊢ ( 𝐶 ∈ Cat → ( Id ‘ 𝑂 ) = ( Id ‘ 𝐶 ) )
90	4 89	syl	⊢ ( 𝜑 → ( Id ‘ 𝑂 ) = ( Id ‘ 𝐶 ) )
91	90	fveq1d	⊢ ( 𝜑 → ( ( Id ‘ 𝑂 ) ‘ 𝑋 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) )
92	91	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑦 ) ) → ( ( Id ‘ 𝑂 ) ‘ 𝑋 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) )
93	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑦 ) ) → 𝐶 ∈ Cat )
94	93 44	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑦 ) ) → 𝑂 ∈ Cat )
95	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑦 ) ) → 𝐷 ∈ Cat )
96	95 46	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑦 ) ) → 𝑃 ∈ Cat )
97	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑦 ) ) → 𝑋 ∈ 𝐴 )
98	78	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑦 ) ) → 𝑦 ∈ ( Base ‘ 𝐷 ) )
99		eqid	⊢ ( Id ‘ 𝑂 ) = ( Id ‘ 𝑂 )
100	79	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑦 ) ) → 𝑧 ∈ ( Base ‘ 𝐷 ) )
101		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑦 ) ) → 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑦 ) )
102	101 73	eleqtrrdi	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑦 ) ) → 𝑓 ∈ ( 𝑦 ( Hom ‘ 𝑃 ) 𝑧 ) )
103	43 94 96 18 97 63 17 98 75 99 100 102	diag12	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑦 ) ) → ( ( 𝑦 ( 2^nd ‘ ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) ) 𝑧 ) ‘ 𝑓 ) = ( ( Id ‘ 𝑂 ) ‘ 𝑋 ) )
104	3 93 95 7 97 58 16 100 72 88 98 101	diag12	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑦 ) ) → ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) 𝑦 ) ‘ 𝑓 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) )
105	92 103 104	3eqtr4rd	⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) ∧ 𝑓 ∈ ( 𝑧 ( Hom ‘ 𝐷 ) 𝑦 ) ) → ( ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) 𝑦 ) ‘ 𝑓 ) = ( ( 𝑦 ( 2^nd ‘ ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) ) 𝑧 ) ‘ 𝑓 ) )
106	83 87 105	eqfnfvd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) → ( 𝑧 ( 2^nd ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) 𝑦 ) = ( 𝑦 ( 2^nd ‘ ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) ) 𝑧 ) )
107	71 106	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( Base ‘ 𝐷 ) ∧ 𝑧 ∈ ( Base ‘ 𝐷 ) ) ) → ( 𝑦 ( 2^nd ‘ ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) 𝑧 ) = ( 𝑦 ( 2^nd ‘ ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) ) 𝑧 ) )
108	68 69 107	eqfnovd	⊢ ( 𝜑 → ( 2^nd ‘ ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) = ( 2^nd ‘ ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) ) )
109	67 108	opeq12d	⊢ ( 𝜑 → ⟨ ( 1^st ‘ ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) , ( 2^nd ‘ ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ⟩ = ⟨ ( 1^st ‘ ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) ) , ( 2^nd ‘ ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) ) ⟩ )
110		relfunc	⊢ Rel ( 𝑃 Func 𝑂 )
111		1st2nd	⊢ ( ( Rel ( 𝑃 Func 𝑂 ) ∧ ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ∈ ( 𝑃 Func 𝑂 ) ) → ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) , ( 2^nd ‘ ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ⟩ )
112	110 38 111	sylancr	⊢ ( 𝜑 → ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) , ( 2^nd ‘ ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) ⟩ )
113		1st2nd	⊢ ( ( Rel ( 𝑃 Func 𝑂 ) ∧ ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) ∈ ( 𝑃 Func 𝑂 ) ) → ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) = ⟨ ( 1^st ‘ ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) ) , ( 2^nd ‘ ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) ) ⟩ )
114	110 51 113	sylancr	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) = ⟨ ( 1^st ‘ ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) ) , ( 2^nd ‘ ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) ) ⟩ )
115	109 112 114	3eqtr4d	⊢ ( 𝜑 → ( 𝐹 ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) = ( ( 1^st ‘ ( 𝑂 Δ_func 𝑃 ) ) ‘ 𝑋 ) )

Metamath Proof Explorer

Theorem oppfdiag1

Proof