fucpropd

Description: If two categories have the same set of objects, morphisms, and compositions, then they have the same functor categories. (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	fucpropd	⊢ ( 𝜑 → ( 𝐴 FuncCat 𝐶 ) = ( 𝐵 FuncCat 𝐷 ) )

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	opeq2d	⊢ ( 𝜑 → ⟨ ( Base ‘ ndx ) , ( 𝐴 Func 𝐶 ) ⟩ = ⟨ ( Base ‘ ndx ) , ( 𝐵 Func 𝐷 ) ⟩ )
11	1 2 3 4 5 6 7 8	natpropd	⊢ ( 𝜑 → ( 𝐴 Nat 𝐶 ) = ( 𝐵 Nat 𝐷 ) )
12	11	opeq2d	⊢ ( 𝜑 → ⟨ ( Hom ‘ ndx ) , ( 𝐴 Nat 𝐶 ) ⟩ = ⟨ ( Hom ‘ ndx ) , ( 𝐵 Nat 𝐷 ) ⟩ )
13	9	sqxpeqd	⊢ ( 𝜑 → ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) = ( ( 𝐵 Func 𝐷 ) × ( 𝐵 Func 𝐷 ) ) )
14	9	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ) → ( 𝐴 Func 𝐶 ) = ( 𝐵 Func 𝐷 ) )
15		nfv	⊢ Ⅎ 𝑓 ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) )
16		nfcsb1v	⊢ Ⅎ 𝑓 ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝐵 Nat 𝐷 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐵 Nat 𝐷 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐵 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) )
17	16	a1i	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) → Ⅎ 𝑓 ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝐵 Nat 𝐷 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐵 Nat 𝐷 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐵 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) )
18		fvexd	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) → ( 1^st ‘ 𝑣 ) ∈ V )
19		nfv	⊢ Ⅎ 𝑔 ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) )
20		nfcsb1v	⊢ Ⅎ 𝑔 ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝐵 Nat 𝐷 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐵 Nat 𝐷 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐵 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) )
21	20	a1i	⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) → Ⅎ 𝑔 ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝐵 Nat 𝐷 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐵 Nat 𝐷 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐵 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) )
22		fvexd	⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) → ( 2^nd ‘ 𝑣 ) ∈ V )
23	11	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) → ( 𝐴 Nat 𝐶 ) = ( 𝐵 Nat 𝐷 ) )
24	23	oveqd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) → ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) = ( 𝑔 ( 𝐵 Nat 𝐷 ) ℎ ) )
25	23	oveqdr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) ∧ 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) ) → ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) = ( 𝑓 ( 𝐵 Nat 𝐷 ) 𝑔 ) )
26	1	homfeqbas	⊢ ( 𝜑 → ( Base ‘ 𝐴 ) = ( Base ‘ 𝐵 ) )
27	26	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) ∧ 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ) ) → ( Base ‘ 𝐴 ) = ( Base ‘ 𝐵 ) )
28		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
29		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
30		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
31		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
32	3	ad5antr	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) ∧ 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
33	4	ad5antr	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) ∧ 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( comp_f ‘ 𝐶 ) = ( comp_f ‘ 𝐷 ) )
34		eqid	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
35		relfunc	⊢ Rel ( 𝐴 Func 𝐶 )
36		simpllr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) ∧ 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ) ) → 𝑓 = ( 1^st ‘ 𝑣 ) )
37		simp-4r	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) ∧ 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ) ) → ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) )
38	37	simpld	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) ∧ 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ) ) → 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) )
39		xp1st	⊢ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) → ( 1^st ‘ 𝑣 ) ∈ ( 𝐴 Func 𝐶 ) )
40	38 39	syl	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) ∧ 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ) ) → ( 1^st ‘ 𝑣 ) ∈ ( 𝐴 Func 𝐶 ) )
41	36 40	eqeltrd	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) ∧ 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ) ) → 𝑓 ∈ ( 𝐴 Func 𝐶 ) )
42		1st2ndbr	⊢ ( ( Rel ( 𝐴 Func 𝐶 ) ∧ 𝑓 ∈ ( 𝐴 Func 𝐶 ) ) → ( 1^st ‘ 𝑓 ) ( 𝐴 Func 𝐶 ) ( 2^nd ‘ 𝑓 ) )
43	35 41 42	sylancr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) ∧ 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ) ) → ( 1^st ‘ 𝑓 ) ( 𝐴 Func 𝐶 ) ( 2^nd ‘ 𝑓 ) )
44	34 28 43	funcf1	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) ∧ 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ) ) → ( 1^st ‘ 𝑓 ) : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) )
45	44	ffvelrnda	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) ∧ 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐶 ) )
46		simplr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) ∧ 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ) ) → 𝑔 = ( 2^nd ‘ 𝑣 ) )
47		xp2nd	⊢ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) → ( 2^nd ‘ 𝑣 ) ∈ ( 𝐴 Func 𝐶 ) )
48	38 47	syl	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) ∧ 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ) ) → ( 2^nd ‘ 𝑣 ) ∈ ( 𝐴 Func 𝐶 ) )
49	46 48	eqeltrd	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) ∧ 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ) ) → 𝑔 ∈ ( 𝐴 Func 𝐶 ) )
50		1st2ndbr	⊢ ( ( Rel ( 𝐴 Func 𝐶 ) ∧ 𝑔 ∈ ( 𝐴 Func 𝐶 ) ) → ( 1^st ‘ 𝑔 ) ( 𝐴 Func 𝐶 ) ( 2^nd ‘ 𝑔 ) )
51	35 49 50	sylancr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) ∧ 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ) ) → ( 1^st ‘ 𝑔 ) ( 𝐴 Func 𝐶 ) ( 2^nd ‘ 𝑔 ) )
52	34 28 51	funcf1	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) ∧ 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ) ) → ( 1^st ‘ 𝑔 ) : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) )
53	52	ffvelrnda	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) ∧ 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐶 ) )
54	37	simprd	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) ∧ 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ) ) → ℎ ∈ ( 𝐴 Func 𝐶 ) )
55		1st2ndbr	⊢ ( ( Rel ( 𝐴 Func 𝐶 ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) → ( 1^st ‘ ℎ ) ( 𝐴 Func 𝐶 ) ( 2^nd ‘ ℎ ) )
56	35 54 55	sylancr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) ∧ 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ) ) → ( 1^st ‘ ℎ ) ( 𝐴 Func 𝐶 ) ( 2^nd ‘ ℎ ) )
57	34 28 56	funcf1	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) ∧ 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ) ) → ( 1^st ‘ ℎ ) : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) )
58	57	ffvelrnda	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) ∧ 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐶 ) )
59		eqid	⊢ ( 𝐴 Nat 𝐶 ) = ( 𝐴 Nat 𝐶 )
60		simplrr	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) ∧ 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) )
61	59 60	nat1st2nd	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) ∧ 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → 𝑎 ∈ ( ⟨ ( 1^st ‘ 𝑓 ) , ( 2^nd ‘ 𝑓 ) ⟩ ( 𝐴 Nat 𝐶 ) ⟨ ( 1^st ‘ 𝑔 ) , ( 2^nd ‘ 𝑔 ) ⟩ ) )
62		simpr	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) ∧ 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → 𝑥 ∈ ( Base ‘ 𝐴 ) )
63	59 61 34 29 62	natcl	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) ∧ 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑎 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ) )
64		simplrl	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) ∧ 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) )
65	59 64	nat1st2nd	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) ∧ 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → 𝑏 ∈ ( ⟨ ( 1^st ‘ 𝑔 ) , ( 2^nd ‘ 𝑔 ) ⟩ ( 𝐴 Nat 𝐶 ) ⟨ ( 1^st ‘ ℎ ) , ( 2^nd ‘ ℎ ) ⟩ ) )
66	59 65 34 29 62	natcl	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) ∧ 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑏 ‘ 𝑥 ) ∈ ( ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) )
67	28 29 30 31 32 33 45 53 58 63 66	comfeqval	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) ∧ 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) = ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) )
68	27 67	mpteq12dva	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) ∧ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) ∧ 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ) ) → ( 𝑥 ∈ ( Base ‘ 𝐴 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐵 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) )
69	24 25 68	mpoeq123dva	⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) → ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) = ( 𝑏 ∈ ( 𝑔 ( 𝐵 Nat 𝐷 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐵 Nat 𝐷 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐵 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) )
70		csbeq1a	⊢ ( 𝑔 = ( 2^nd ‘ 𝑣 ) → ( 𝑏 ∈ ( 𝑔 ( 𝐵 Nat 𝐷 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐵 Nat 𝐷 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐵 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) = ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝐵 Nat 𝐷 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐵 Nat 𝐷 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐵 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) )
71	70	adantl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) → ( 𝑏 ∈ ( 𝑔 ( 𝐵 Nat 𝐷 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐵 Nat 𝐷 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐵 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) = ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝐵 Nat 𝐷 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐵 Nat 𝐷 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐵 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) )
72	69 71	eqtrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) ∧ 𝑔 = ( 2^nd ‘ 𝑣 ) ) → ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) = ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝐵 Nat 𝐷 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐵 Nat 𝐷 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐵 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) )
73	19 21 22 72	csbiedf	⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) → ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) = ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝐵 Nat 𝐷 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐵 Nat 𝐷 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐵 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) )
74		csbeq1a	⊢ ( 𝑓 = ( 1^st ‘ 𝑣 ) → ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝐵 Nat 𝐷 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐵 Nat 𝐷 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐵 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) = ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝐵 Nat 𝐷 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐵 Nat 𝐷 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐵 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) )
75	74	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) → ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝐵 Nat 𝐷 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐵 Nat 𝐷 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐵 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) = ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝐵 Nat 𝐷 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐵 Nat 𝐷 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐵 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) )
76	73 75	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) ∧ 𝑓 = ( 1^st ‘ 𝑣 ) ) → ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) = ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝐵 Nat 𝐷 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐵 Nat 𝐷 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐵 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) )
77	15 17 18 76	csbiedf	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) ∧ ℎ ∈ ( 𝐴 Func 𝐶 ) ) ) → ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) = ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝐵 Nat 𝐷 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐵 Nat 𝐷 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐵 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) )
78	13 14 77	mpoeq123dva	⊢ ( 𝜑 → ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) , ℎ ∈ ( 𝐴 Func 𝐶 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) = ( 𝑣 ∈ ( ( 𝐵 Func 𝐷 ) × ( 𝐵 Func 𝐷 ) ) , ℎ ∈ ( 𝐵 Func 𝐷 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝐵 Nat 𝐷 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐵 Nat 𝐷 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐵 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
79	78	opeq2d	⊢ ( 𝜑 → ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) , ℎ ∈ ( 𝐴 Func 𝐶 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ = ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( ( 𝐵 Func 𝐷 ) × ( 𝐵 Func 𝐷 ) ) , ℎ ∈ ( 𝐵 Func 𝐷 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝐵 Nat 𝐷 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐵 Nat 𝐷 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐵 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ )
80	10 12 79	tpeq123d	⊢ ( 𝜑 → { ⟨ ( Base ‘ ndx ) , ( 𝐴 Func 𝐶 ) ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝐴 Nat 𝐶 ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) , ℎ ∈ ( 𝐴 Func 𝐶 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , ( 𝐵 Func 𝐷 ) ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝐵 Nat 𝐷 ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( ( 𝐵 Func 𝐷 ) × ( 𝐵 Func 𝐷 ) ) , ℎ ∈ ( 𝐵 Func 𝐷 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝐵 Nat 𝐷 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐵 Nat 𝐷 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐵 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ } )
81		eqid	⊢ ( 𝐴 FuncCat 𝐶 ) = ( 𝐴 FuncCat 𝐶 )
82		eqid	⊢ ( 𝐴 Func 𝐶 ) = ( 𝐴 Func 𝐶 )
83		eqidd	⊢ ( 𝜑 → ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) , ℎ ∈ ( 𝐴 Func 𝐶 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) = ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) , ℎ ∈ ( 𝐴 Func 𝐶 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
84	81 82 59 34 30 5 7 83	fucval	⊢ ( 𝜑 → ( 𝐴 FuncCat 𝐶 ) = { ⟨ ( Base ‘ ndx ) , ( 𝐴 Func 𝐶 ) ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝐴 Nat 𝐶 ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( ( 𝐴 Func 𝐶 ) × ( 𝐴 Func 𝐶 ) ) , ℎ ∈ ( 𝐴 Func 𝐶 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝐴 Nat 𝐶 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐴 Nat 𝐶 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ } )
85		eqid	⊢ ( 𝐵 FuncCat 𝐷 ) = ( 𝐵 FuncCat 𝐷 )
86		eqid	⊢ ( 𝐵 Func 𝐷 ) = ( 𝐵 Func 𝐷 )
87		eqid	⊢ ( 𝐵 Nat 𝐷 ) = ( 𝐵 Nat 𝐷 )
88		eqid	⊢ ( Base ‘ 𝐵 ) = ( Base ‘ 𝐵 )
89		eqidd	⊢ ( 𝜑 → ( 𝑣 ∈ ( ( 𝐵 Func 𝐷 ) × ( 𝐵 Func 𝐷 ) ) , ℎ ∈ ( 𝐵 Func 𝐷 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝐵 Nat 𝐷 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐵 Nat 𝐷 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐵 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) = ( 𝑣 ∈ ( ( 𝐵 Func 𝐷 ) × ( 𝐵 Func 𝐷 ) ) , ℎ ∈ ( 𝐵 Func 𝐷 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝐵 Nat 𝐷 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐵 Nat 𝐷 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐵 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
90	85 86 87 88 31 6 8 89	fucval	⊢ ( 𝜑 → ( 𝐵 FuncCat 𝐷 ) = { ⟨ ( Base ‘ ndx ) , ( 𝐵 Func 𝐷 ) ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝐵 Nat 𝐷 ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( ( 𝐵 Func 𝐷 ) × ( 𝐵 Func 𝐷 ) ) , ℎ ∈ ( 𝐵 Func 𝐷 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝐵 Nat 𝐷 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐵 Nat 𝐷 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐵 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ } )
91	80 84 90	3eqtr4d	⊢ ( 𝜑 → ( 𝐴 FuncCat 𝐶 ) = ( 𝐵 FuncCat 𝐷 ) )

Metamath Proof Explorer

Theorem fucpropd

Proof