natpropd

Description: If two categories have the same set of objects, morphisms, and compositions, then they have the same natural transformations. (Contributed by Mario Carneiro, 26-Jan-2017)

	Ref	Expression
Hypotheses	fucpropd.1	⊢ ( 𝜑 → ( Hom_f ‘ 𝐴 ) = ( Hom_f ‘ 𝐵 ) )
	fucpropd.2	⊢ ( 𝜑 → ( comp_f ‘ 𝐴 ) = ( comp_f ‘ 𝐵 ) )
	fucpropd.3	⊢ ( 𝜑 → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
	fucpropd.4	⊢ ( 𝜑 → ( comp_f ‘ 𝐶 ) = ( comp_f ‘ 𝐷 ) )
	fucpropd.a	⊢ ( 𝜑 → 𝐴 ∈ Cat )
	fucpropd.b	⊢ ( 𝜑 → 𝐵 ∈ Cat )
	fucpropd.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	fucpropd.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
Assertion	natpropd	⊢ ( 𝜑 → ( 𝐴 Nat 𝐶 ) = ( 𝐵 Nat 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		fucpropd.1	⊢ ( 𝜑 → ( Hom_f ‘ 𝐴 ) = ( Hom_f ‘ 𝐵 ) )
2		fucpropd.2	⊢ ( 𝜑 → ( comp_f ‘ 𝐴 ) = ( comp_f ‘ 𝐵 ) )
3		fucpropd.3	⊢ ( 𝜑 → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
4		fucpropd.4	⊢ ( 𝜑 → ( comp_f ‘ 𝐶 ) = ( comp_f ‘ 𝐷 ) )
5		fucpropd.a	⊢ ( 𝜑 → 𝐴 ∈ Cat )
6		fucpropd.b	⊢ ( 𝜑 → 𝐵 ∈ Cat )
7		fucpropd.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
8		fucpropd.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
9	1 2 3 4 5 6 7 8	funcpropd	⊢ ( 𝜑 → ( 𝐴 Func 𝐶 ) = ( 𝐵 Func 𝐷 ) )
10	9	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 Func 𝐶 ) ) → ( 𝐴 Func 𝐶 ) = ( 𝐵 Func 𝐷 ) )
11		nfv	⊢ Ⅎ 𝑟 ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) )
12		nfcsb1v	⊢ Ⅎ 𝑟 ⦋ ( 1^st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐵 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) }
13	12	a1i	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) → Ⅎ 𝑟 ⦋ ( 1^st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐵 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } )
14		fvexd	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) → ( 1^st ‘ 𝑓 ) ∈ V )
15		nfv	⊢ Ⅎ 𝑠 ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) )
16		nfcsb1v	⊢ Ⅎ 𝑠 ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐵 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) }
17	16	a1i	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) → Ⅎ 𝑠 ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐵 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } )
18		fvexd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) → ( 1^st ‘ 𝑔 ) ∈ V )
19		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
20		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
21		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
22	3	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
23		eqid	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
24		simplr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) → 𝑟 = ( 1^st ‘ 𝑓 ) )
25		relfunc	⊢ Rel ( 𝐴 Func 𝐶 )
26		simpllr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) → ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) )
27	26	simpld	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) → 𝑓 ∈ ( 𝐴 Func 𝐶 ) )
28		1st2ndbr	⊢ ( ( Rel ( 𝐴 Func 𝐶 ) ∧ 𝑓 ∈ ( 𝐴 Func 𝐶 ) ) → ( 1^st ‘ 𝑓 ) ( 𝐴 Func 𝐶 ) ( 2^nd ‘ 𝑓 ) )
29	25 27 28	sylancr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) → ( 1^st ‘ 𝑓 ) ( 𝐴 Func 𝐶 ) ( 2^nd ‘ 𝑓 ) )
30	24 29	eqbrtrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) → 𝑟 ( 𝐴 Func 𝐶 ) ( 2^nd ‘ 𝑓 ) )
31	23 19 30	funcf1	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) → 𝑟 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) )
32	31	ffvelcdmda	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑟 ‘ 𝑥 ) ∈ ( Base ‘ 𝐶 ) )
33		simpr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) → 𝑠 = ( 1^st ‘ 𝑔 ) )
34	26	simprd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) → 𝑔 ∈ ( 𝐴 Func 𝐶 ) )
35		1st2ndbr	⊢ ( ( Rel ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) → ( 1^st ‘ 𝑔 ) ( 𝐴 Func 𝐶 ) ( 2^nd ‘ 𝑔 ) )
36	25 34 35	sylancr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) → ( 1^st ‘ 𝑔 ) ( 𝐴 Func 𝐶 ) ( 2^nd ‘ 𝑔 ) )
37	33 36	eqbrtrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) → 𝑠 ( 𝐴 Func 𝐶 ) ( 2^nd ‘ 𝑔 ) )
38	23 19 37	funcf1	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) → 𝑠 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) )
39	38	ffvelcdmda	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑠 ‘ 𝑥 ) ∈ ( Base ‘ 𝐶 ) )
40	19 20 21 22 32 39	homfeqval	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑥 ) ) = ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) )
41	40	ixpeq2dva	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) → X 𝑥 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑥 ) ) = X 𝑥 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) )
42	1	homfeqbas	⊢ ( 𝜑 → ( Base ‘ 𝐴 ) = ( Base ‘ 𝐵 ) )
43	42	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) → ( Base ‘ 𝐴 ) = ( Base ‘ 𝐵 ) )
44	43	ixpeq1d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) → X 𝑥 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) = X 𝑥 ∈ ( Base ‘ 𝐵 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) )
45	41 44	eqtrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) → X 𝑥 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑥 ) ) = X 𝑥 ∈ ( Base ‘ 𝐵 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) )
46		fveq2	⊢ ( 𝑥 = 𝑧 → ( 𝑟 ‘ 𝑥 ) = ( 𝑟 ‘ 𝑧 ) )
47		fveq2	⊢ ( 𝑥 = 𝑧 → ( 𝑠 ‘ 𝑥 ) = ( 𝑠 ‘ 𝑧 ) )
48	46 47	oveq12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑥 ) ) = ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) )
49	48	cbvixpv	⊢ X 𝑥 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑥 ) ) = X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) )
50	49	eleq2i	⊢ ( 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑥 ) ) ↔ 𝑎 ∈ X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) )
51	43	adantr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑎 ∈ X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) ) → ( Base ‘ 𝐴 ) = ( Base ‘ 𝐵 ) )
52	51	adantr	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑎 ∈ X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( Base ‘ 𝐴 ) = ( Base ‘ 𝐵 ) )
53		eqid	⊢ ( Hom ‘ 𝐴 ) = ( Hom ‘ 𝐴 )
54		eqid	⊢ ( Hom ‘ 𝐵 ) = ( Hom ‘ 𝐵 )
55	1	ad6antr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑎 ∈ X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → ( Hom_f ‘ 𝐴 ) = ( Hom_f ‘ 𝐵 ) )
56		simplr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑎 ∈ X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → 𝑥 ∈ ( Base ‘ 𝐴 ) )
57		simpr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑎 ∈ X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → 𝑦 ∈ ( Base ‘ 𝐴 ) )
58	23 53 54 55 56 57	homfeqval	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑎 ∈ X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) )
59		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
60		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
61	3	ad7antr	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑎 ∈ X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
62	4	ad7antr	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑎 ∈ X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) → ( comp_f ‘ 𝐶 ) = ( comp_f ‘ 𝐷 ) )
63	32	ad5ant13	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑎 ∈ X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) → ( 𝑟 ‘ 𝑥 ) ∈ ( Base ‘ 𝐶 ) )
64	31	ad2antrr	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑎 ∈ X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → 𝑟 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) )
65	64	ffvelcdmda	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑎 ∈ X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑟 ‘ 𝑦 ) ∈ ( Base ‘ 𝐶 ) )
66	65	adantr	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑎 ∈ X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) → ( 𝑟 ‘ 𝑦 ) ∈ ( Base ‘ 𝐶 ) )
67	38	ad2antrr	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑎 ∈ X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → 𝑠 : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) )
68	67	ffvelcdmda	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑎 ∈ X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑠 ‘ 𝑦 ) ∈ ( Base ‘ 𝐶 ) )
69	68	adantr	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑎 ∈ X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) → ( 𝑠 ‘ 𝑦 ) ∈ ( Base ‘ 𝐶 ) )
70	30	ad3antrrr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑎 ∈ X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → 𝑟 ( 𝐴 Func 𝐶 ) ( 2^nd ‘ 𝑓 ) )
71	23 53 20 70 56 57	funcf2	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑎 ∈ X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ⟶ ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑟 ‘ 𝑦 ) ) )
72	71	ffvelcdmda	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑎 ∈ X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) → ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ∈ ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑟 ‘ 𝑦 ) ) )
73		fveq2	⊢ ( 𝑧 = 𝑦 → ( 𝑟 ‘ 𝑧 ) = ( 𝑟 ‘ 𝑦 ) )
74		fveq2	⊢ ( 𝑧 = 𝑦 → ( 𝑠 ‘ 𝑧 ) = ( 𝑠 ‘ 𝑦 ) )
75	73 74	oveq12d	⊢ ( 𝑧 = 𝑦 → ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) = ( ( 𝑟 ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑦 ) ) )
76	75	fvixp	⊢ ( ( 𝑎 ∈ X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑎 ‘ 𝑦 ) ∈ ( ( 𝑟 ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑦 ) ) )
77	76	ad5ant24	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑎 ∈ X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) → ( 𝑎 ‘ 𝑦 ) ∈ ( ( 𝑟 ‘ 𝑦 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑦 ) ) )
78	19 20 59 60 61 62 63 66 69 72 77	comfeqval	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑎 ∈ X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) → ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) )
79	39	ad5ant13	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑎 ∈ X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) → ( 𝑠 ‘ 𝑥 ) ∈ ( Base ‘ 𝐶 ) )
80		fveq2	⊢ ( 𝑧 = 𝑥 → ( 𝑟 ‘ 𝑧 ) = ( 𝑟 ‘ 𝑥 ) )
81		fveq2	⊢ ( 𝑧 = 𝑥 → ( 𝑠 ‘ 𝑧 ) = ( 𝑠 ‘ 𝑥 ) )
82	80 81	oveq12d	⊢ ( 𝑧 = 𝑥 → ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) = ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑥 ) ) )
83	82	fvixp	⊢ ( ( 𝑎 ∈ X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑎 ‘ 𝑥 ) ∈ ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑥 ) ) )
84	83	ad5ant23	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑎 ∈ X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) → ( 𝑎 ‘ 𝑥 ) ∈ ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑥 ) ) )
85	37	ad3antrrr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑎 ∈ X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → 𝑠 ( 𝐴 Func 𝐶 ) ( 2^nd ‘ 𝑔 ) )
86	23 53 20 85 56 57	funcf2	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑎 ∈ X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ⟶ ( ( 𝑠 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑦 ) ) )
87	86	ffvelcdmda	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑎 ∈ X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) → ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ∈ ( ( 𝑠 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑦 ) ) )
88	19 20 59 60 61 62 63 79 69 84 87	comfeqval	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑎 ∈ X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) → ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) )
89	78 88	eqeq12d	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑎 ∈ X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) → ( ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) ↔ ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) ) )
90	58 89	raleqbidva	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑎 ∈ X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → ( ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) ↔ ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) ) )
91	52 90	raleqbidva	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑎 ∈ X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) ) )
92	51 91	raleqbidva	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑎 ∈ X 𝑧 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑧 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑧 ) ) ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) ) )
93	50 92	sylan2b	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) ∧ 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑥 ) ) ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) ) )
94	45 93	rabeqbidva	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) → { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } = { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐵 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } )
95		csbeq1a	⊢ ( 𝑠 = ( 1^st ‘ 𝑔 ) → { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐵 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } = ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐵 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } )
96	95	adantl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) → { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐵 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } = ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐵 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } )
97	94 96	eqtrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) ∧ 𝑠 = ( 1^st ‘ 𝑔 ) ) → { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } = ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐵 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } )
98	15 17 18 97	csbiedf	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) → ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } = ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐵 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } )
99		csbeq1a	⊢ ( 𝑟 = ( 1^st ‘ 𝑓 ) → ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐵 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } = ⦋ ( 1^st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐵 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } )
100	99	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) → ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐵 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } = ⦋ ( 1^st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐵 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } )
101	98 100	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑟 = ( 1^st ‘ 𝑓 ) ) → ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } = ⦋ ( 1^st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐵 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } )
102	11 13 14 101	csbiedf	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) ) → ⦋ ( 1^st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } = ⦋ ( 1^st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐵 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } )
103	9 10 102	mpoeq123dva	⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) , 𝑔 ∈ ( 𝐴 Func 𝐶 ) ↦ ⦋ ( 1^st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } ) = ( 𝑓 ∈ ( 𝐵 Func 𝐷 ) , 𝑔 ∈ ( 𝐵 Func 𝐷 ) ↦ ⦋ ( 1^st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐵 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } ) )
104		eqid	⊢ ( 𝐴 Nat 𝐶 ) = ( 𝐴 Nat 𝐶 )
105	104 23 53 20 59	natfval	⊢ ( 𝐴 Nat 𝐶 ) = ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) , 𝑔 ∈ ( 𝐴 Func 𝐶 ) ↦ ⦋ ( 1^st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐴 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐴 ) ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } )
106		eqid	⊢ ( 𝐵 Nat 𝐷 ) = ( 𝐵 Nat 𝐷 )
107		eqid	⊢ ( Base ‘ 𝐵 ) = ( Base ‘ 𝐵 )
108	106 107 54 21 60	natfval	⊢ ( 𝐵 Nat 𝐷 ) = ( 𝑓 ∈ ( 𝐵 Func 𝐷 ) , 𝑔 ∈ ( 𝐵 Func 𝐷 ) ↦ ⦋ ( 1^st ‘ 𝑓 ) / 𝑟 ⦌ ⦋ ( 1^st ‘ 𝑔 ) / 𝑠 ⦌ { 𝑎 ∈ X 𝑥 ∈ ( Base ‘ 𝐵 ) ( ( 𝑟 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝑠 ‘ 𝑥 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝐵 ) ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ ℎ ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) ( ( 𝑎 ‘ 𝑦 ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑟 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ ℎ ) ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑔 ) 𝑦 ) ‘ ℎ ) ( ⟨ ( 𝑟 ‘ 𝑥 ) , ( 𝑠 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝑠 ‘ 𝑦 ) ) ( 𝑎 ‘ 𝑥 ) ) } )
109	103 105 108	3eqtr4g	⊢ ( 𝜑 → ( 𝐴 Nat 𝐶 ) = ( 𝐵 Nat 𝐷 ) )

Metamath Proof Explorer

Theorem natpropd

Proof