prcofdiag1

Description: A constant functor pre-composed by a functor is another constant functor. (Contributed by Zhi Wang, 25-Nov-2025)

	Ref	Expression
Hypotheses	prcofdiag.l	⊢ 𝐿 = ( 𝐶 Δ_func 𝐷 )
	prcofdiag.m	⊢ 𝑀 = ( 𝐶 Δ_func 𝐸 )
	prcofdiag.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐸 Func 𝐷 ) )
	prcofdiag.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	prcofdiag1.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	prcofdiag1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	prcofdiag1	⊢ ( 𝜑 → ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∘_func 𝐹 ) = ( ( 1^st ‘ 𝑀 ) ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		prcofdiag.l	⊢ 𝐿 = ( 𝐶 Δ_func 𝐷 )
2		prcofdiag.m	⊢ 𝑀 = ( 𝐶 Δ_func 𝐸 )
3		prcofdiag.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐸 Func 𝐷 ) )
4		prcofdiag.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
5		prcofdiag1.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
6		prcofdiag1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
8	3	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐸 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
9	8	funcrcl3	⊢ ( 𝜑 → 𝐷 ∈ Cat )
10		eqid	⊢ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) = ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 )
11	1 4 9 5 6 10	diag1cl	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∈ ( 𝐷 Func 𝐶 ) )
12	3 11	cofucl	⊢ ( 𝜑 → ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∘_func 𝐹 ) ∈ ( 𝐸 Func 𝐶 ) )
13	12	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∘_func 𝐹 ) ) ( 𝐸 Func 𝐶 ) ( 2^nd ‘ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∘_func 𝐹 ) ) )
14	7 5 13	funcf1	⊢ ( 𝜑 → ( 1^st ‘ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∘_func 𝐹 ) ) : ( Base ‘ 𝐸 ) ⟶ 𝐵 )
15	14	ffnd	⊢ ( 𝜑 → ( 1^st ‘ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∘_func 𝐹 ) ) Fn ( Base ‘ 𝐸 ) )
16	8	funcrcl2	⊢ ( 𝜑 → 𝐸 ∈ Cat )
17		eqid	⊢ ( ( 1^st ‘ 𝑀 ) ‘ 𝑋 ) = ( ( 1^st ‘ 𝑀 ) ‘ 𝑋 )
18	2 4 16 5 6 17	diag1cl	⊢ ( 𝜑 → ( ( 1^st ‘ 𝑀 ) ‘ 𝑋 ) ∈ ( 𝐸 Func 𝐶 ) )
19	18	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ ( ( 1^st ‘ 𝑀 ) ‘ 𝑋 ) ) ( 𝐸 Func 𝐶 ) ( 2^nd ‘ ( ( 1^st ‘ 𝑀 ) ‘ 𝑋 ) ) )
20	7 5 19	funcf1	⊢ ( 𝜑 → ( 1^st ‘ ( ( 1^st ‘ 𝑀 ) ‘ 𝑋 ) ) : ( Base ‘ 𝐸 ) ⟶ 𝐵 )
21	20	ffnd	⊢ ( 𝜑 → ( 1^st ‘ ( ( 1^st ‘ 𝑀 ) ‘ 𝑋 ) ) Fn ( Base ‘ 𝐸 ) )
22	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → 𝐶 ∈ Cat )
23	9	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → 𝐷 ∈ Cat )
24	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → 𝑋 ∈ 𝐵 )
25		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
26	7 25 8	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐸 ) ⟶ ( Base ‘ 𝐷 ) )
27	26	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
28	1 22 23 5 24 10 25 27	diag11	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) = 𝑋 )
29	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → 𝐹 ∈ ( 𝐸 Func 𝐷 ) )
30	11	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∈ ( 𝐷 Func 𝐶 ) )
31		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → 𝑥 ∈ ( Base ‘ 𝐸 ) )
32	7 29 30 31	cofu1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → ( ( 1^st ‘ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∘_func 𝐹 ) ) ‘ 𝑥 ) = ( ( 1^st ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
33	16	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → 𝐸 ∈ Cat )
34	2 22 33 5 24 17 7 31	diag11	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → ( ( 1^st ‘ ( ( 1^st ‘ 𝑀 ) ‘ 𝑋 ) ) ‘ 𝑥 ) = 𝑋 )
35	28 32 34	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐸 ) ) → ( ( 1^st ‘ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∘_func 𝐹 ) ) ‘ 𝑥 ) = ( ( 1^st ‘ ( ( 1^st ‘ 𝑀 ) ‘ 𝑋 ) ) ‘ 𝑥 ) )
36	15 21 35	eqfnfvd	⊢ ( 𝜑 → ( 1^st ‘ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∘_func 𝐹 ) ) = ( 1^st ‘ ( ( 1^st ‘ 𝑀 ) ‘ 𝑋 ) ) )
37	7 13	funcfn2	⊢ ( 𝜑 → ( 2^nd ‘ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∘_func 𝐹 ) ) Fn ( ( Base ‘ 𝐸 ) × ( Base ‘ 𝐸 ) ) )
38	7 19	funcfn2	⊢ ( 𝜑 → ( 2^nd ‘ ( ( 1^st ‘ 𝑀 ) ‘ 𝑋 ) ) Fn ( ( Base ‘ 𝐸 ) × ( Base ‘ 𝐸 ) ) )
39		eqid	⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
40		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
41	13	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ 𝑦 ∈ ( Base ‘ 𝐸 ) ) ) → ( 1^st ‘ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∘_func 𝐹 ) ) ( 𝐸 Func 𝐶 ) ( 2^nd ‘ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∘_func 𝐹 ) ) )
42		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ 𝑦 ∈ ( Base ‘ 𝐸 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐸 ) )
43		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ 𝑦 ∈ ( Base ‘ 𝐸 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐸 ) )
44	7 39 40 41 42 43	funcf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ 𝑦 ∈ ( Base ‘ 𝐸 ) ) ) → ( 𝑥 ( 2^nd ‘ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∘_func 𝐹 ) ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐸 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∘_func 𝐹 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( ( 1^st ‘ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∘_func 𝐹 ) ) ‘ 𝑦 ) ) )
45	44	ffnd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ 𝑦 ∈ ( Base ‘ 𝐸 ) ) ) → ( 𝑥 ( 2^nd ‘ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∘_func 𝐹 ) ) 𝑦 ) Fn ( 𝑥 ( Hom ‘ 𝐸 ) 𝑦 ) )
46	19	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ 𝑦 ∈ ( Base ‘ 𝐸 ) ) ) → ( 1^st ‘ ( ( 1^st ‘ 𝑀 ) ‘ 𝑋 ) ) ( 𝐸 Func 𝐶 ) ( 2^nd ‘ ( ( 1^st ‘ 𝑀 ) ‘ 𝑋 ) ) )
47	7 39 40 46 42 43	funcf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ 𝑦 ∈ ( Base ‘ 𝐸 ) ) ) → ( 𝑥 ( 2^nd ‘ ( ( 1^st ‘ 𝑀 ) ‘ 𝑋 ) ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐸 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ ( ( 1^st ‘ 𝑀 ) ‘ 𝑋 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( ( 1^st ‘ ( ( 1^st ‘ 𝑀 ) ‘ 𝑋 ) ) ‘ 𝑦 ) ) )
48	47	ffnd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ 𝑦 ∈ ( Base ‘ 𝐸 ) ) ) → ( 𝑥 ( 2^nd ‘ ( ( 1^st ‘ 𝑀 ) ‘ 𝑋 ) ) 𝑦 ) Fn ( 𝑥 ( Hom ‘ 𝐸 ) 𝑦 ) )
49	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ 𝑦 ∈ ( Base ‘ 𝐸 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐸 ) 𝑦 ) ) → 𝐶 ∈ Cat )
50	9	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ 𝑦 ∈ ( Base ‘ 𝐸 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐸 ) 𝑦 ) ) → 𝐷 ∈ Cat )
51	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ 𝑦 ∈ ( Base ‘ 𝐸 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐸 ) 𝑦 ) ) → 𝑋 ∈ 𝐵 )
52	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ 𝑦 ∈ ( Base ‘ 𝐸 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐸 ) 𝑦 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐸 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
53	7 25 52	funcf1	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ 𝑦 ∈ ( Base ‘ 𝐸 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐸 ) 𝑦 ) ) → ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐸 ) ⟶ ( Base ‘ 𝐷 ) )
54	42	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ 𝑦 ∈ ( Base ‘ 𝐸 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐸 ) 𝑦 ) ) → 𝑥 ∈ ( Base ‘ 𝐸 ) )
55	53 54	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ 𝑦 ∈ ( Base ‘ 𝐸 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐸 ) 𝑦 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
56		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
57		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
58	43	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ 𝑦 ∈ ( Base ‘ 𝐸 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐸 ) 𝑦 ) ) → 𝑦 ∈ ( Base ‘ 𝐸 ) )
59	53 58	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ 𝑦 ∈ ( Base ‘ 𝐸 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐸 ) 𝑦 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐷 ) )
60	7 39 56 52 54 58	funcf2	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ 𝑦 ∈ ( Base ‘ 𝐸 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐸 ) 𝑦 ) ) → ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐸 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
61		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ 𝑦 ∈ ( Base ‘ 𝐸 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐸 ) 𝑦 ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐸 ) 𝑦 ) )
62	60 61	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ 𝑦 ∈ ( Base ‘ 𝐸 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐸 ) 𝑦 ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
63	1 49 50 5 51 10 25 55 56 57 59 62	diag12	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ 𝑦 ∈ ( Base ‘ 𝐸 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐸 ) 𝑦 ) ) → ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ‘ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) )
64	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ 𝑦 ∈ ( Base ‘ 𝐸 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐸 ) 𝑦 ) ) → 𝐹 ∈ ( 𝐸 Func 𝐷 ) )
65	11	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ 𝑦 ∈ ( Base ‘ 𝐸 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐸 ) 𝑦 ) ) → ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∈ ( 𝐷 Func 𝐶 ) )
66	7 64 65 54 58 39 61	cofu2	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ 𝑦 ∈ ( Base ‘ 𝐸 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐸 ) 𝑦 ) ) → ( ( 𝑥 ( 2^nd ‘ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∘_func 𝐹 ) ) 𝑦 ) ‘ 𝑓 ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ‘ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) )
67	16	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ 𝑦 ∈ ( Base ‘ 𝐸 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐸 ) 𝑦 ) ) → 𝐸 ∈ Cat )
68	2 49 67 5 51 17 7 54 39 57 58 61	diag12	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ 𝑦 ∈ ( Base ‘ 𝐸 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐸 ) 𝑦 ) ) → ( ( 𝑥 ( 2^nd ‘ ( ( 1^st ‘ 𝑀 ) ‘ 𝑋 ) ) 𝑦 ) ‘ 𝑓 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) )
69	63 66 68	3eqtr4d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ 𝑦 ∈ ( Base ‘ 𝐸 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐸 ) 𝑦 ) ) → ( ( 𝑥 ( 2^nd ‘ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∘_func 𝐹 ) ) 𝑦 ) ‘ 𝑓 ) = ( ( 𝑥 ( 2^nd ‘ ( ( 1^st ‘ 𝑀 ) ‘ 𝑋 ) ) 𝑦 ) ‘ 𝑓 ) )
70	45 48 69	eqfnfvd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐸 ) ∧ 𝑦 ∈ ( Base ‘ 𝐸 ) ) ) → ( 𝑥 ( 2^nd ‘ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∘_func 𝐹 ) ) 𝑦 ) = ( 𝑥 ( 2^nd ‘ ( ( 1^st ‘ 𝑀 ) ‘ 𝑋 ) ) 𝑦 ) )
71	37 38 70	eqfnovd	⊢ ( 𝜑 → ( 2^nd ‘ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∘_func 𝐹 ) ) = ( 2^nd ‘ ( ( 1^st ‘ 𝑀 ) ‘ 𝑋 ) ) )
72	36 71	opeq12d	⊢ ( 𝜑 → ⟨ ( 1^st ‘ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∘_func 𝐹 ) ) , ( 2^nd ‘ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∘_func 𝐹 ) ) ⟩ = ⟨ ( 1^st ‘ ( ( 1^st ‘ 𝑀 ) ‘ 𝑋 ) ) , ( 2^nd ‘ ( ( 1^st ‘ 𝑀 ) ‘ 𝑋 ) ) ⟩ )
73		relfunc	⊢ Rel ( 𝐸 Func 𝐶 )
74		1st2nd	⊢ ( ( Rel ( 𝐸 Func 𝐶 ) ∧ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∘_func 𝐹 ) ∈ ( 𝐸 Func 𝐶 ) ) → ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∘_func 𝐹 ) = ⟨ ( 1^st ‘ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∘_func 𝐹 ) ) , ( 2^nd ‘ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∘_func 𝐹 ) ) ⟩ )
75	73 12 74	sylancr	⊢ ( 𝜑 → ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∘_func 𝐹 ) = ⟨ ( 1^st ‘ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∘_func 𝐹 ) ) , ( 2^nd ‘ ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∘_func 𝐹 ) ) ⟩ )
76		1st2nd	⊢ ( ( Rel ( 𝐸 Func 𝐶 ) ∧ ( ( 1^st ‘ 𝑀 ) ‘ 𝑋 ) ∈ ( 𝐸 Func 𝐶 ) ) → ( ( 1^st ‘ 𝑀 ) ‘ 𝑋 ) = ⟨ ( 1^st ‘ ( ( 1^st ‘ 𝑀 ) ‘ 𝑋 ) ) , ( 2^nd ‘ ( ( 1^st ‘ 𝑀 ) ‘ 𝑋 ) ) ⟩ )
77	73 18 76	sylancr	⊢ ( 𝜑 → ( ( 1^st ‘ 𝑀 ) ‘ 𝑋 ) = ⟨ ( 1^st ‘ ( ( 1^st ‘ 𝑀 ) ‘ 𝑋 ) ) , ( 2^nd ‘ ( ( 1^st ‘ 𝑀 ) ‘ 𝑋 ) ) ⟩ )
78	72 75 77	3eqtr4d	⊢ ( 𝜑 → ( ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∘_func 𝐹 ) = ( ( 1^st ‘ 𝑀 ) ‘ 𝑋 ) )

Metamath Proof Explorer

Theorem prcofdiag1

Proof