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		eqid	⊢ ( 𝐷 Nat 𝐸 ) = ( 𝐷 Nat 𝐸 )
14	13	natrcl	⊢ ( 𝑅 ∈ ( 𝐹 ( 𝐷 Nat 𝐸 ) 𝐾 ) → ( 𝐹 ∈ ( 𝐷 Func 𝐸 ) ∧ 𝐾 ∈ ( 𝐷 Func 𝐸 ) ) )
15	1 14	syl	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐷 Func 𝐸 ) ∧ 𝐾 ∈ ( 𝐷 Func 𝐸 ) ) )
16	15	simpld	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 Func 𝐸 ) )
17	16	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐹 ) )
18	17	funcrcl3	⊢ ( 𝜑 → 𝐸 ∈ Cat )
19		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
20	19 10 17	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) )
21		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
22		eqid	⊢ ( 𝐶 Nat 𝐷 ) = ( 𝐶 Nat 𝐷 )
23	22	natrcl	⊢ ( 𝑆 ∈ ( 𝐺 ( 𝐶 Nat 𝐷 ) 𝐿 ) → ( 𝐺 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐿 ∈ ( 𝐶 Func 𝐷 ) ) )
24	2 23	syl	⊢ ( 𝜑 → ( 𝐺 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝐿 ∈ ( 𝐶 Func 𝐷 ) ) )
25	24	simpld	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐷 ) )
26	25	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
27	21 19 26	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
28	27 5	ffvelcdmd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐷 ) )
29	20 28	ffvelcdmd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ∈ ( Base ‘ 𝐸 ) )
30	6	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ 𝑃 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝑃 ) )
31	19 10 30	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝑃 ) : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) )
32	7	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ 𝑄 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝑄 ) )
33	21 19 32	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝑄 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
34	33 5	ffvelcdmd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝑄 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐷 ) )
35	31 34	ffvelcdmd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝑃 ) ‘ ( ( 1^st ‘ 𝑄 ) ‘ 𝑋 ) ) ∈ ( Base ‘ 𝐸 ) )
36	15	simprd	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Func 𝐸 ) )
37	36	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ 𝐾 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐾 ) )
38	19 10 37	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐾 ) : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) )
39	22	natrcl	⊢ ( 𝑉 ∈ ( 𝐿 ( 𝐶 Nat 𝐷 ) 𝑁 ) → ( 𝐿 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑁 ∈ ( 𝐶 Func 𝐷 ) ) )
40	4 39	syl	⊢ ( 𝜑 → ( 𝐿 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑁 ∈ ( 𝐶 Func 𝐷 ) ) )
41	40	simprd	⊢ ( 𝜑 → 𝑁 ∈ ( 𝐶 Func 𝐷 ) )
42	41	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ 𝑁 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝑁 ) )
43	21 19 42	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝑁 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
44	43 5	ffvelcdmd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐷 ) )
45	38 44	ffvelcdmd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ∈ ( Base ‘ 𝐸 ) )
46	24	simprd	⊢ ( 𝜑 → 𝐿 ∈ ( 𝐶 Func 𝐷 ) )
47	46	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ 𝐿 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐿 ) )
48	21 19 47	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐿 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
49	48 5	ffvelcdmd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐷 ) )
50	20 49	ffvelcdmd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ∈ ( Base ‘ 𝐸 ) )
51		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
52	19 51 11 17 28 49	funcf2	⊢ ( 𝜑 → ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) : ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) )
53	22 2	nat1st2nd	⊢ ( 𝜑 → 𝑆 ∈ ( ⟨ ( 1^st ‘ 𝐺 ) , ( 2^nd ‘ 𝐺 ) ⟩ ( 𝐶 Nat 𝐷 ) ⟨ ( 1^st ‘ 𝐿 ) , ( 2^nd ‘ 𝐿 ) ⟩ ) )
54	22 53 21 51 5	natcl	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ∈ ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) )
55	52 54	ffvelcdmd	⊢ ( 𝜑 → ( ( ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ ( 𝑆 ‘ 𝑋 ) ) ∈ ( ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐺 ) ‘ 𝑋 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐹 ) ‘ ( ( 1^st ‘ 𝐿 ) ‘ 𝑋 ) ) ) )
56	10 11 12 18 29 50 35 55 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 ‘ 𝑄 ) ‘ 𝑋 ) ) ) )
57	13	natrcl	⊢ ( 𝑈 ∈ ( 𝐾 ( 𝐷 Nat 𝐸 ) 𝑀 ) → ( 𝐾 ∈ ( 𝐷 Func 𝐸 ) ∧ 𝑀 ∈ ( 𝐷 Func 𝐸 ) ) )
58	3 57	syl	⊢ ( 𝜑 → ( 𝐾 ∈ ( 𝐷 Func 𝐸 ) ∧ 𝑀 ∈ ( 𝐷 Func 𝐸 ) ) )
59	58	simprd	⊢ ( 𝜑 → 𝑀 ∈ ( 𝐷 Func 𝐸 ) )
60	59	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ 𝑀 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝑀 ) )
61	19 10 60	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝑀 ) : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) )
62	61 44	ffvelcdmd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ∈ ( Base ‘ 𝐸 ) )
63	13 3	nat1st2nd	⊢ ( 𝜑 → 𝑈 ∈ ( ⟨ ( 1^st ‘ 𝐾 ) , ( 2^nd ‘ 𝐾 ) ⟩ ( 𝐷 Nat 𝐸 ) ⟨ ( 1^st ‘ 𝑀 ) , ( 2^nd ‘ 𝑀 ) ⟩ ) )
64	13 63 19 11 44	natcl	⊢ ( 𝜑 → ( 𝑈 ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ∈ ( ( ( 1^st ‘ 𝐾 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝑀 ) ‘ ( ( 1^st ‘ 𝑁 ) ‘ 𝑋 ) ) ) )
65	10 11 12 18 29 35 45 56 8 62 64	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 ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ ( 𝑆 ‘ 𝑋 ) ) ) ) ) )
66	10 11 12 18 29 50 35 55 9 45 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 ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ ( 𝑆 ‘ 𝑋 ) ) ) ) )
67	66	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 ‘ 𝐿 ) ‘ 𝑋 ) ) ‘ ( 𝑆 ‘ 𝑋 ) ) ) ) ) )
68	65 67	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