fucocolem1

Description: Lemma for fucoco . Associativity for morphisms in category E . To simply put, ( ( a .x. b ) .x. ( c .x. d ) ) = ( a .x. ( ( b .x. c ) .x. d ) ) for morphism compositions. (Contributed by Zhi Wang, 2-Oct-2025)

	Ref	Expression
Hypotheses	fucoco.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝐹 ( 𝐷 Nat 𝐸 ) 𝐾 ) )
	fucoco.s	⊢ ( 𝜑 → 𝑆 ∈ ( 𝐺 ( 𝐶 Nat 𝐷 ) 𝐿 ) )
	fucoco.u	⊢ ( 𝜑 → 𝑈 ∈ ( 𝐾 ( 𝐷 Nat 𝐸 ) 𝑀 ) )
	fucoco.v	⊢ ( 𝜑 → 𝑉 ∈ ( 𝐿 ( 𝐶 Nat 𝐷 ) 𝑁 ) )
	fucocolem1.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
	fucocolem1.p	⊢ ( 𝜑 → 𝑃 ∈ ( 𝐷 Func 𝐸 ) )
	fucocolem1.q	⊢ ( 𝜑 → 𝑄 ∈ ( 𝐶 Func 𝐷 ) )
	fucocolem1.a	⊢ ( 𝜑 → 𝐴 ∈ ( ( ( 1^st ‘ 𝑃 ) ‘ ( ( 1^st ‘ 𝑄 ) ‘ 𝑋 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ) )
	fucocolem1.b	⊢ ( 𝜑 → 𝐵 ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝑃 ) ‘ ( ( 1^st ‘ 𝑄 ) ‘ 𝑋 ) ) ) )
Assertion	fucocolem1	⊢ ( 𝜑 → ( ( ( 𝑈 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ( ⟨ ( ( 1^st ‘ 𝑃 ) ‘ ( ( 1^st ‘ 𝑄 ) ‘ 𝑋 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ) 𝐴 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) , ( ( 1^st ‘ 𝑃 ) ‘ ( ( 1^st ‘ 𝑄 ) ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ) ( 𝐵 ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑃 ) ‘ ( ( 1^st ‘ 𝑄 ) ‘ 𝑋 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ ( 𝑆 ‘ 𝑋 ) ) ) ) = ( ( 𝑈 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ) ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) , ( ( 1^st ‘ 𝑃 ) ‘ ( ( 1^st ‘ 𝑄 ) ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ) 𝐵 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ ( 𝑆 ‘ 𝑋 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fucoco.r	⊢ ( 𝜑 → 𝑅 ∈ ( 𝐹 ( 𝐷 Nat 𝐸 ) 𝐾 ) )
2		fucoco.s	⊢ ( 𝜑 → 𝑆 ∈ ( 𝐺 ( 𝐶 Nat 𝐷 ) 𝐿 ) )
3		fucoco.u	⊢ ( 𝜑 → 𝑈 ∈ ( 𝐾 ( 𝐷 Nat 𝐸 ) 𝑀 ) )
4		fucoco.v	⊢ ( 𝜑 → 𝑉 ∈ ( 𝐿 ( 𝐶 Nat 𝐷 ) 𝑁 ) )
5		fucocolem1.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
6		fucocolem1.p	⊢ ( 𝜑 → 𝑃 ∈ ( 𝐷 Func 𝐸 ) )
7		fucocolem1.q	⊢ ( 𝜑 → 𝑄 ∈ ( 𝐶 Func 𝐷 ) )
8		fucocolem1.a	⊢ ( 𝜑 → 𝐴 ∈ ( ( ( 1^st ‘ 𝑃 ) ‘ ( ( 1^st ‘ 𝑄 ) ‘ 𝑋 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ) )
9		fucocolem1.b	⊢ ( 𝜑 → 𝐵 ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝑃 ) ‘ ( ( 1^st ‘ 𝑄 ) ‘ 𝑋 ) ) ) )
10		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
11		eqid	⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
12		eqid	⊢ ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
13		relfunc	⊢ Rel ( 𝐷 Func 𝐸 )
14		eqid	⊢ ( 𝐷 Nat 𝐸 ) = ( 𝐷 Nat 𝐸 )
15	14	natrcl	⊢ ( 𝑅 ∈ ( 𝐹 ( 𝐷 Nat 𝐸 ) 𝐾 ) → ( 𝐹 ∈ ( 𝐷 Func 𝐸 ) ∧ 𝐾 ∈ ( 𝐷 Func 𝐸 ) ) )
16	1 15	syl	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐷 Func 𝐸 ) ∧ 𝐾 ∈ ( 𝐷 Func 𝐸 ) ) )
17	16	simpld	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 Func 𝐸 ) )
18		1st2ndbr	⊢ ( ( Rel ( 𝐷 Func 𝐸 ) ∧ 𝐹 ∈ ( 𝐷 Func 𝐸 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐹 ) )
19	13 17 18	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐹 ) )
20	19	funcrcl3	⊢ ( 𝜑 → 𝐸 ∈ Cat )
21		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
22	21 10 19	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) )
23		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
24		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
25		eqid	⊢ ( 𝐶 Nat 𝐷 ) = ( 𝐶 Nat 𝐷 )
26	25	natrcl	⊢ ( 𝑆 ∈ ( 𝐺 ( 𝐶 Nat 𝐷 ) 𝐿 ) → ( 𝐺 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐿 ∈ ( 𝐶 Func 𝐷 ) ) )
27	2 26	syl	⊢ ( 𝜑 → ( 𝐺 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐿 ∈ ( 𝐶 Func 𝐷 ) ) )
28	27	simpld	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐷 ) )
29		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
30	24 28 29	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
31	23 21 30	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
32	31 5	ffvelcdmd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐷 ) )
33	22 32	ffvelcdmd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ∈ ( Base ‘ 𝐸 ) )
34		1st2ndbr	⊢ ( ( Rel ( 𝐷 Func 𝐸 ) ∧ 𝑃 ∈ ( 𝐷 Func 𝐸 ) ) → ( 1^st ‘ 𝑃 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝑃 ) )
35	13 6 34	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝑃 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝑃 ) )
36	21 10 35	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝑃 ) : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) )
37		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝑄 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝑄 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝑄 ) )
38	24 7 37	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝑄 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝑄 ) )
39	23 21 38	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝑄 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
40	39 5	ffvelcdmd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝑄 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐷 ) )
41	36 40	ffvelcdmd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝑃 ) ‘ ( ( 1^st ‘ 𝑄 ) ‘ 𝑋 ) ) ∈ ( Base ‘ 𝐸 ) )
42	16	simprd	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Func 𝐸 ) )
43		1st2ndbr	⊢ ( ( Rel ( 𝐷 Func 𝐸 ) ∧ 𝐾 ∈ ( 𝐷 Func 𝐸 ) ) → ( 1^st ‘ 𝐾 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐾 ) )
44	13 42 43	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐾 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐾 ) )
45	21 10 44	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐾 ) : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) )
46	25	natrcl	⊢ ( 𝑉 ∈ ( 𝐿 ( 𝐶 Nat 𝐷 ) 𝑁 ) → ( 𝐿 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑁 ∈ ( 𝐶 Func 𝐷 ) ) )
47	4 46	syl	⊢ ( 𝜑 → ( 𝐿 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑁 ∈ ( 𝐶 Func 𝐷 ) ) )
48	47	simprd	⊢ ( 𝜑 → 𝑁 ∈ ( 𝐶 Func 𝐷 ) )
49		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝑁 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝑁 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝑁 ) )
50	24 48 49	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝑁 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝑁 ) )
51	23 21 50	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝑁 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
52	51 5	ffvelcdmd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐷 ) )
53	45 52	ffvelcdmd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ∈ ( Base ‘ 𝐸 ) )
54	27	simprd	⊢ ( 𝜑 → 𝐿 ∈ ( 𝐶 Func 𝐷 ) )
55		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐿 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐿 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐿 ) )
56	24 54 55	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐿 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐿 ) )
57	23 21 56	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐿 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
58	57 5	ffvelcdmd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐷 ) )
59	22 58	ffvelcdmd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ∈ ( Base ‘ 𝐸 ) )
60		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
61	21 60 11 19 32 58	funcf2	⊢ ( 𝜑 → ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) : ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) )
62	25 2	nat1st2nd	⊢ ( 𝜑 → 𝑆 ∈ ( ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ ( 𝐶 Nat 𝐷 ) ⟨ ( 1^st ‘ 𝐿 ) , ( 2^nd ‘ 𝐿 ) ⟩ ) )
63	25 62 23 60 5	natcl	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) )
64	61 63	ffvelcdmd	⊢ ( 𝜑 → ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ ( 𝑆 ‘ 𝑋 ) ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) )
65	10 11 12 20 33 59 41 64 9	catcocl	⊢ ( 𝜑 → ( 𝐵 ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑃 ) ‘ ( ( 1^st ‘ 𝑄 ) ‘ 𝑋 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ ( 𝑆 ‘ 𝑋 ) ) ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝑃 ) ‘ ( ( 1^st ‘ 𝑄 ) ‘ 𝑋 ) ) ) )
66	14	natrcl	⊢ ( 𝑈 ∈ ( 𝐾 ( 𝐷 Nat 𝐸 ) 𝑀 ) → ( 𝐾 ∈ ( 𝐷 Func 𝐸 ) ∧ 𝑀 ∈ ( 𝐷 Func 𝐸 ) ) )
67	3 66	syl	⊢ ( 𝜑 → ( 𝐾 ∈ ( 𝐷 Func 𝐸 ) ∧ 𝑀 ∈ ( 𝐷 Func 𝐸 ) ) )
68	67	simprd	⊢ ( 𝜑 → 𝑀 ∈ ( 𝐷 Func 𝐸 ) )
69		1st2ndbr	⊢ ( ( Rel ( 𝐷 Func 𝐸 ) ∧ 𝑀 ∈ ( 𝐷 Func 𝐸 ) ) → ( 1^st ‘ 𝑀 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝑀 ) )
70	13 68 69	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝑀 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝑀 ) )
71	21 10 70	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝑀 ) : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) )
72	71 52	ffvelcdmd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ∈ ( Base ‘ 𝐸 ) )
73	14 3	nat1st2nd	⊢ ( 𝜑 → 𝑈 ∈ ( ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ ( 𝐷 Nat 𝐸 ) ⟨ ( 1^st ‘ 𝑀 ) , ( 2^nd ‘ 𝑀 ) ⟩ ) )
74	14 73 21 11 52	natcl	⊢ ( 𝜑 → ( 𝑈 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ∈ ( ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ) )
75	10 11 12 20 33 41 53 65 8 72 74	catass	⊢ ( 𝜑 → ( ( ( 𝑈 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ( ⟨ ( ( 1^st ‘ 𝑃 ) ‘ ( ( 1^st ‘ 𝑄 ) ‘ 𝑋 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ) 𝐴 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) , ( ( 1^st ‘ 𝑃 ) ‘ ( ( 1^st ‘ 𝑄 ) ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ) ( 𝐵 ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑃 ) ‘ ( ( 1^st ‘ 𝑄 ) ‘ 𝑋 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ ( 𝑆 ‘ 𝑋 ) ) ) ) = ( ( 𝑈 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ) ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) , ( ( 1^st ‘ 𝑃 ) ‘ ( ( 1^st ‘ 𝑄 ) ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ) ( 𝐵 ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑃 ) ‘ ( ( 1^st ‘ 𝑄 ) ‘ 𝑋 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ ( 𝑆 ‘ 𝑋 ) ) ) ) ) )
76	10 11 12 20 33 59 41 64 9 53 8	catass	⊢ ( 𝜑 → ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) , ( ( 1^st ‘ 𝑃 ) ‘ ( ( 1^st ‘ 𝑄 ) ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ) 𝐵 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ ( 𝑆 ‘ 𝑋 ) ) ) = ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) , ( ( 1^st ‘ 𝑃 ) ‘ ( ( 1^st ‘ 𝑄 ) ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ) ( 𝐵 ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑃 ) ‘ ( ( 1^st ‘ 𝑄 ) ‘ 𝑋 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ ( 𝑆 ‘ 𝑋 ) ) ) ) )
77	76	oveq2d	⊢ ( 𝜑 → ( ( 𝑈 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ) ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) , ( ( 1^st ‘ 𝑃 ) ‘ ( ( 1^st ‘ 𝑄 ) ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ) 𝐵 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ ( 𝑆 ‘ 𝑋 ) ) ) ) = ( ( 𝑈 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ) ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) , ( ( 1^st ‘ 𝑃 ) ‘ ( ( 1^st ‘ 𝑄 ) ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ) ( 𝐵 ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑃 ) ‘ ( ( 1^st ‘ 𝑄 ) ‘ 𝑋 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ ( 𝑆 ‘ 𝑋 ) ) ) ) ) )
78	75 77	eqtr4d	⊢ ( 𝜑 → ( ( ( 𝑈 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ( ⟨ ( ( 1^st ‘ 𝑃 ) ‘ ( ( 1^st ‘ 𝑄 ) ‘ 𝑋 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ) 𝐴 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) , ( ( 1^st ‘ 𝑃 ) ‘ ( ( 1^st ‘ 𝑄 ) ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ) ( 𝐵 ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑃 ) ‘ ( ( 1^st ‘ 𝑄 ) ‘ 𝑋 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ ( 𝑆 ‘ 𝑋 ) ) ) ) = ( ( 𝑈 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) , ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ) ( ( 𝐴 ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) , ( ( 1^st ‘ 𝑃 ) ‘ ( ( 1^st ‘ 𝑄 ) ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ) 𝐵 ) ( ⟨ ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) , ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ) ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ ( 𝑆 ‘ 𝑋 ) ) ) ) )

Metamath Proof Explorer

Theorem fucocolem1

Proof