MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fucpropd Structured version   Visualization version   GIF version

Theorem fucpropd 17226
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.)
Hypotheses
Ref Expression
fucpropd.1 (𝜑 → (Homf𝐴) = (Homf𝐵))
fucpropd.2 (𝜑 → (compf𝐴) = (compf𝐵))
fucpropd.3 (𝜑 → (Homf𝐶) = (Homf𝐷))
fucpropd.4 (𝜑 → (compf𝐶) = (compf𝐷))
fucpropd.a (𝜑𝐴 ∈ Cat)
fucpropd.b (𝜑𝐵 ∈ Cat)
fucpropd.c (𝜑𝐶 ∈ Cat)
fucpropd.d (𝜑𝐷 ∈ Cat)
Assertion
Ref Expression
fucpropd (𝜑 → (𝐴 FuncCat 𝐶) = (𝐵 FuncCat 𝐷))

Proof of Theorem fucpropd
Dummy variables 𝑎 𝑏 𝑓 𝑔 𝑣 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fucpropd.1 . . . . 5 (𝜑 → (Homf𝐴) = (Homf𝐵))
2 fucpropd.2 . . . . 5 (𝜑 → (compf𝐴) = (compf𝐵))
3 fucpropd.3 . . . . 5 (𝜑 → (Homf𝐶) = (Homf𝐷))
4 fucpropd.4 . . . . 5 (𝜑 → (compf𝐶) = (compf𝐷))
5 fucpropd.a . . . . 5 (𝜑𝐴 ∈ Cat)
6 fucpropd.b . . . . 5 (𝜑𝐵 ∈ Cat)
7 fucpropd.c . . . . 5 (𝜑𝐶 ∈ Cat)
8 fucpropd.d . . . . 5 (𝜑𝐷 ∈ Cat)
91, 2, 3, 4, 5, 6, 7, 8funcpropd 17149 . . . 4 (𝜑 → (𝐴 Func 𝐶) = (𝐵 Func 𝐷))
109opeq2d 4786 . . 3 (𝜑 → ⟨(Base‘ndx), (𝐴 Func 𝐶)⟩ = ⟨(Base‘ndx), (𝐵 Func 𝐷)⟩)
111, 2, 3, 4, 5, 6, 7, 8natpropd 17225 . . . 4 (𝜑 → (𝐴 Nat 𝐶) = (𝐵 Nat 𝐷))
1211opeq2d 4786 . . 3 (𝜑 → ⟨(Hom ‘ndx), (𝐴 Nat 𝐶)⟩ = ⟨(Hom ‘ndx), (𝐵 Nat 𝐷)⟩)
139sqxpeqd 5563 . . . . 5 (𝜑 → ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) = ((𝐵 Func 𝐷) × (𝐵 Func 𝐷)))
149adantr 483 . . . . 5 ((𝜑𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶))) → (𝐴 Func 𝐶) = (𝐵 Func 𝐷))
15 nfv 1915 . . . . . 6 𝑓(𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶)))
16 nfcsb1v 3884 . . . . . . 7 𝑓(1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝐵 Nat 𝐷)), 𝑎 ∈ (𝑓(𝐵 Nat 𝐷)𝑔) ↦ (𝑥 ∈ (Base‘𝐵) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐷)((1st)‘𝑥))(𝑎𝑥))))
1716a1i 11 . . . . . 6 ((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) → 𝑓(1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝐵 Nat 𝐷)), 𝑎 ∈ (𝑓(𝐵 Nat 𝐷)𝑔) ↦ (𝑥 ∈ (Base‘𝐵) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐷)((1st)‘𝑥))(𝑎𝑥)))))
18 fvexd 6661 . . . . . 6 ((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) → (1st𝑣) ∈ V)
19 nfv 1915 . . . . . . . 8 𝑔((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣))
20 nfcsb1v 3884 . . . . . . . . 9 𝑔(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝐵 Nat 𝐷)), 𝑎 ∈ (𝑓(𝐵 Nat 𝐷)𝑔) ↦ (𝑥 ∈ (Base‘𝐵) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐷)((1st)‘𝑥))(𝑎𝑥))))
2120a1i 11 . . . . . . . 8 (((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) → 𝑔(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝐵 Nat 𝐷)), 𝑎 ∈ (𝑓(𝐵 Nat 𝐷)𝑔) ↦ (𝑥 ∈ (Base‘𝐵) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐷)((1st)‘𝑥))(𝑎𝑥)))))
22 fvexd 6661 . . . . . . . 8 (((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) → (2nd𝑣) ∈ V)
2311ad3antrrr 728 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) → (𝐴 Nat 𝐶) = (𝐵 Nat 𝐷))
2423oveqd 7150 . . . . . . . . . 10 ((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) → (𝑔(𝐴 Nat 𝐶)) = (𝑔(𝐵 Nat 𝐷)))
2523oveqdr 7161 . . . . . . . . . 10 (((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) ∧ 𝑏 ∈ (𝑔(𝐴 Nat 𝐶))) → (𝑓(𝐴 Nat 𝐶)𝑔) = (𝑓(𝐵 Nat 𝐷)𝑔))
261homfeqbas 16945 . . . . . . . . . . . 12 (𝜑 → (Base‘𝐴) = (Base‘𝐵))
2726ad4antr 730 . . . . . . . . . . 11 (((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) ∧ (𝑏 ∈ (𝑔(𝐴 Nat 𝐶)) ∧ 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔))) → (Base‘𝐴) = (Base‘𝐵))
28 eqid 2820 . . . . . . . . . . . 12 (Base‘𝐶) = (Base‘𝐶)
29 eqid 2820 . . . . . . . . . . . 12 (Hom ‘𝐶) = (Hom ‘𝐶)
30 eqid 2820 . . . . . . . . . . . 12 (comp‘𝐶) = (comp‘𝐶)
31 eqid 2820 . . . . . . . . . . . 12 (comp‘𝐷) = (comp‘𝐷)
323ad5antr 732 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) ∧ (𝑏 ∈ (𝑔(𝐴 Nat 𝐶)) ∧ 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔))) ∧ 𝑥 ∈ (Base‘𝐴)) → (Homf𝐶) = (Homf𝐷))
334ad5antr 732 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) ∧ (𝑏 ∈ (𝑔(𝐴 Nat 𝐶)) ∧ 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔))) ∧ 𝑥 ∈ (Base‘𝐴)) → (compf𝐶) = (compf𝐷))
34 eqid 2820 . . . . . . . . . . . . . 14 (Base‘𝐴) = (Base‘𝐴)
35 relfunc 17111 . . . . . . . . . . . . . . 15 Rel (𝐴 Func 𝐶)
36 simpllr 774 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) ∧ (𝑏 ∈ (𝑔(𝐴 Nat 𝐶)) ∧ 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔))) → 𝑓 = (1st𝑣))
37 simp-4r 782 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) ∧ (𝑏 ∈ (𝑔(𝐴 Nat 𝐶)) ∧ 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔))) → (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶)))
3837simpld 497 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) ∧ (𝑏 ∈ (𝑔(𝐴 Nat 𝐶)) ∧ 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔))) → 𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)))
39 xp1st 7699 . . . . . . . . . . . . . . . . 17 (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) → (1st𝑣) ∈ (𝐴 Func 𝐶))
4038, 39syl 17 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) ∧ (𝑏 ∈ (𝑔(𝐴 Nat 𝐶)) ∧ 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔))) → (1st𝑣) ∈ (𝐴 Func 𝐶))
4136, 40eqeltrd 2911 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) ∧ (𝑏 ∈ (𝑔(𝐴 Nat 𝐶)) ∧ 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔))) → 𝑓 ∈ (𝐴 Func 𝐶))
42 1st2ndbr 7719 . . . . . . . . . . . . . . 15 ((Rel (𝐴 Func 𝐶) ∧ 𝑓 ∈ (𝐴 Func 𝐶)) → (1st𝑓)(𝐴 Func 𝐶)(2nd𝑓))
4335, 41, 42sylancr 589 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) ∧ (𝑏 ∈ (𝑔(𝐴 Nat 𝐶)) ∧ 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔))) → (1st𝑓)(𝐴 Func 𝐶)(2nd𝑓))
4434, 28, 43funcf1 17115 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) ∧ (𝑏 ∈ (𝑔(𝐴 Nat 𝐶)) ∧ 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔))) → (1st𝑓):(Base‘𝐴)⟶(Base‘𝐶))
4544ffvelrnda 6827 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) ∧ (𝑏 ∈ (𝑔(𝐴 Nat 𝐶)) ∧ 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔))) ∧ 𝑥 ∈ (Base‘𝐴)) → ((1st𝑓)‘𝑥) ∈ (Base‘𝐶))
46 simplr 767 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) ∧ (𝑏 ∈ (𝑔(𝐴 Nat 𝐶)) ∧ 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔))) → 𝑔 = (2nd𝑣))
47 xp2nd 7700 . . . . . . . . . . . . . . . . 17 (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) → (2nd𝑣) ∈ (𝐴 Func 𝐶))
4838, 47syl 17 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) ∧ (𝑏 ∈ (𝑔(𝐴 Nat 𝐶)) ∧ 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔))) → (2nd𝑣) ∈ (𝐴 Func 𝐶))
4946, 48eqeltrd 2911 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) ∧ (𝑏 ∈ (𝑔(𝐴 Nat 𝐶)) ∧ 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔))) → 𝑔 ∈ (𝐴 Func 𝐶))
50 1st2ndbr 7719 . . . . . . . . . . . . . . 15 ((Rel (𝐴 Func 𝐶) ∧ 𝑔 ∈ (𝐴 Func 𝐶)) → (1st𝑔)(𝐴 Func 𝐶)(2nd𝑔))
5135, 49, 50sylancr 589 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) ∧ (𝑏 ∈ (𝑔(𝐴 Nat 𝐶)) ∧ 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔))) → (1st𝑔)(𝐴 Func 𝐶)(2nd𝑔))
5234, 28, 51funcf1 17115 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) ∧ (𝑏 ∈ (𝑔(𝐴 Nat 𝐶)) ∧ 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔))) → (1st𝑔):(Base‘𝐴)⟶(Base‘𝐶))
5352ffvelrnda 6827 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) ∧ (𝑏 ∈ (𝑔(𝐴 Nat 𝐶)) ∧ 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔))) ∧ 𝑥 ∈ (Base‘𝐴)) → ((1st𝑔)‘𝑥) ∈ (Base‘𝐶))
5437simprd 498 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) ∧ (𝑏 ∈ (𝑔(𝐴 Nat 𝐶)) ∧ 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔))) → ∈ (𝐴 Func 𝐶))
55 1st2ndbr 7719 . . . . . . . . . . . . . . 15 ((Rel (𝐴 Func 𝐶) ∧ ∈ (𝐴 Func 𝐶)) → (1st)(𝐴 Func 𝐶)(2nd))
5635, 54, 55sylancr 589 . . . . . . . . . . . . . 14 (((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) ∧ (𝑏 ∈ (𝑔(𝐴 Nat 𝐶)) ∧ 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔))) → (1st)(𝐴 Func 𝐶)(2nd))
5734, 28, 56funcf1 17115 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) ∧ (𝑏 ∈ (𝑔(𝐴 Nat 𝐶)) ∧ 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔))) → (1st):(Base‘𝐴)⟶(Base‘𝐶))
5857ffvelrnda 6827 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) ∧ (𝑏 ∈ (𝑔(𝐴 Nat 𝐶)) ∧ 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔))) ∧ 𝑥 ∈ (Base‘𝐴)) → ((1st)‘𝑥) ∈ (Base‘𝐶))
59 eqid 2820 . . . . . . . . . . . . 13 (𝐴 Nat 𝐶) = (𝐴 Nat 𝐶)
60 simplrr 776 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) ∧ (𝑏 ∈ (𝑔(𝐴 Nat 𝐶)) ∧ 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔))) ∧ 𝑥 ∈ (Base‘𝐴)) → 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔))
6159, 60nat1st2nd 17200 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) ∧ (𝑏 ∈ (𝑔(𝐴 Nat 𝐶)) ∧ 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔))) ∧ 𝑥 ∈ (Base‘𝐴)) → 𝑎 ∈ (⟨(1st𝑓), (2nd𝑓)⟩(𝐴 Nat 𝐶)⟨(1st𝑔), (2nd𝑔)⟩))
62 simpr 487 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) ∧ (𝑏 ∈ (𝑔(𝐴 Nat 𝐶)) ∧ 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔))) ∧ 𝑥 ∈ (Base‘𝐴)) → 𝑥 ∈ (Base‘𝐴))
6359, 61, 34, 29, 62natcl 17202 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) ∧ (𝑏 ∈ (𝑔(𝐴 Nat 𝐶)) ∧ 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔))) ∧ 𝑥 ∈ (Base‘𝐴)) → (𝑎𝑥) ∈ (((1st𝑓)‘𝑥)(Hom ‘𝐶)((1st𝑔)‘𝑥)))
64 simplrl 775 . . . . . . . . . . . . . 14 ((((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) ∧ (𝑏 ∈ (𝑔(𝐴 Nat 𝐶)) ∧ 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔))) ∧ 𝑥 ∈ (Base‘𝐴)) → 𝑏 ∈ (𝑔(𝐴 Nat 𝐶)))
6559, 64nat1st2nd 17200 . . . . . . . . . . . . 13 ((((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) ∧ (𝑏 ∈ (𝑔(𝐴 Nat 𝐶)) ∧ 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔))) ∧ 𝑥 ∈ (Base‘𝐴)) → 𝑏 ∈ (⟨(1st𝑔), (2nd𝑔)⟩(𝐴 Nat 𝐶)⟨(1st), (2nd)⟩))
6659, 65, 34, 29, 62natcl 17202 . . . . . . . . . . . 12 ((((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) ∧ (𝑏 ∈ (𝑔(𝐴 Nat 𝐶)) ∧ 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔))) ∧ 𝑥 ∈ (Base‘𝐴)) → (𝑏𝑥) ∈ (((1st𝑔)‘𝑥)(Hom ‘𝐶)((1st)‘𝑥)))
6728, 29, 30, 31, 32, 33, 45, 53, 58, 63, 66comfeqval 16957 . . . . . . . . . . 11 ((((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) ∧ (𝑏 ∈ (𝑔(𝐴 Nat 𝐶)) ∧ 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔))) ∧ 𝑥 ∈ (Base‘𝐴)) → ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐶)((1st)‘𝑥))(𝑎𝑥)) = ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐷)((1st)‘𝑥))(𝑎𝑥)))
6827, 67mpteq12dva 5126 . . . . . . . . . 10 (((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) ∧ (𝑏 ∈ (𝑔(𝐴 Nat 𝐶)) ∧ 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔))) → (𝑥 ∈ (Base‘𝐴) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐶)((1st)‘𝑥))(𝑎𝑥))) = (𝑥 ∈ (Base‘𝐵) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐷)((1st)‘𝑥))(𝑎𝑥))))
6924, 25, 68mpoeq123dva 7205 . . . . . . . . 9 ((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) → (𝑏 ∈ (𝑔(𝐴 Nat 𝐶)), 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔) ↦ (𝑥 ∈ (Base‘𝐴) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐶)((1st)‘𝑥))(𝑎𝑥)))) = (𝑏 ∈ (𝑔(𝐵 Nat 𝐷)), 𝑎 ∈ (𝑓(𝐵 Nat 𝐷)𝑔) ↦ (𝑥 ∈ (Base‘𝐵) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐷)((1st)‘𝑥))(𝑎𝑥)))))
70 csbeq1a 3874 . . . . . . . . . 10 (𝑔 = (2nd𝑣) → (𝑏 ∈ (𝑔(𝐵 Nat 𝐷)), 𝑎 ∈ (𝑓(𝐵 Nat 𝐷)𝑔) ↦ (𝑥 ∈ (Base‘𝐵) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐷)((1st)‘𝑥))(𝑎𝑥)))) = (2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝐵 Nat 𝐷)), 𝑎 ∈ (𝑓(𝐵 Nat 𝐷)𝑔) ↦ (𝑥 ∈ (Base‘𝐵) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐷)((1st)‘𝑥))(𝑎𝑥)))))
7170adantl 484 . . . . . . . . 9 ((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) → (𝑏 ∈ (𝑔(𝐵 Nat 𝐷)), 𝑎 ∈ (𝑓(𝐵 Nat 𝐷)𝑔) ↦ (𝑥 ∈ (Base‘𝐵) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐷)((1st)‘𝑥))(𝑎𝑥)))) = (2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝐵 Nat 𝐷)), 𝑎 ∈ (𝑓(𝐵 Nat 𝐷)𝑔) ↦ (𝑥 ∈ (Base‘𝐵) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐷)((1st)‘𝑥))(𝑎𝑥)))))
7269, 71eqtrd 2855 . . . . . . . 8 ((((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) ∧ 𝑔 = (2nd𝑣)) → (𝑏 ∈ (𝑔(𝐴 Nat 𝐶)), 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔) ↦ (𝑥 ∈ (Base‘𝐴) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐶)((1st)‘𝑥))(𝑎𝑥)))) = (2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝐵 Nat 𝐷)), 𝑎 ∈ (𝑓(𝐵 Nat 𝐷)𝑔) ↦ (𝑥 ∈ (Base‘𝐵) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐷)((1st)‘𝑥))(𝑎𝑥)))))
7319, 21, 22, 72csbiedf 3890 . . . . . . 7 (((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) → (2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝐴 Nat 𝐶)), 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔) ↦ (𝑥 ∈ (Base‘𝐴) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐶)((1st)‘𝑥))(𝑎𝑥)))) = (2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝐵 Nat 𝐷)), 𝑎 ∈ (𝑓(𝐵 Nat 𝐷)𝑔) ↦ (𝑥 ∈ (Base‘𝐵) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐷)((1st)‘𝑥))(𝑎𝑥)))))
74 csbeq1a 3874 . . . . . . . 8 (𝑓 = (1st𝑣) → (2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝐵 Nat 𝐷)), 𝑎 ∈ (𝑓(𝐵 Nat 𝐷)𝑔) ↦ (𝑥 ∈ (Base‘𝐵) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐷)((1st)‘𝑥))(𝑎𝑥)))) = (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝐵 Nat 𝐷)), 𝑎 ∈ (𝑓(𝐵 Nat 𝐷)𝑔) ↦ (𝑥 ∈ (Base‘𝐵) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐷)((1st)‘𝑥))(𝑎𝑥)))))
7574adantl 484 . . . . . . 7 (((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) → (2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝐵 Nat 𝐷)), 𝑎 ∈ (𝑓(𝐵 Nat 𝐷)𝑔) ↦ (𝑥 ∈ (Base‘𝐵) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐷)((1st)‘𝑥))(𝑎𝑥)))) = (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝐵 Nat 𝐷)), 𝑎 ∈ (𝑓(𝐵 Nat 𝐷)𝑔) ↦ (𝑥 ∈ (Base‘𝐵) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐷)((1st)‘𝑥))(𝑎𝑥)))))
7673, 75eqtrd 2855 . . . . . 6 (((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) ∧ 𝑓 = (1st𝑣)) → (2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝐴 Nat 𝐶)), 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔) ↦ (𝑥 ∈ (Base‘𝐴) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐶)((1st)‘𝑥))(𝑎𝑥)))) = (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝐵 Nat 𝐷)), 𝑎 ∈ (𝑓(𝐵 Nat 𝐷)𝑔) ↦ (𝑥 ∈ (Base‘𝐵) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐷)((1st)‘𝑥))(𝑎𝑥)))))
7715, 17, 18, 76csbiedf 3890 . . . . 5 ((𝜑 ∧ (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)) ∧ ∈ (𝐴 Func 𝐶))) → (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝐴 Nat 𝐶)), 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔) ↦ (𝑥 ∈ (Base‘𝐴) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐶)((1st)‘𝑥))(𝑎𝑥)))) = (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝐵 Nat 𝐷)), 𝑎 ∈ (𝑓(𝐵 Nat 𝐷)𝑔) ↦ (𝑥 ∈ (Base‘𝐵) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐷)((1st)‘𝑥))(𝑎𝑥)))))
7813, 14, 77mpoeq123dva 7205 . . . 4 (𝜑 → (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)), ∈ (𝐴 Func 𝐶) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝐴 Nat 𝐶)), 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔) ↦ (𝑥 ∈ (Base‘𝐴) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐶)((1st)‘𝑥))(𝑎𝑥))))) = (𝑣 ∈ ((𝐵 Func 𝐷) × (𝐵 Func 𝐷)), ∈ (𝐵 Func 𝐷) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝐵 Nat 𝐷)), 𝑎 ∈ (𝑓(𝐵 Nat 𝐷)𝑔) ↦ (𝑥 ∈ (Base‘𝐵) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐷)((1st)‘𝑥))(𝑎𝑥))))))
7978opeq2d 4786 . . 3 (𝜑 → ⟨(comp‘ndx), (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)), ∈ (𝐴 Func 𝐶) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝐴 Nat 𝐶)), 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔) ↦ (𝑥 ∈ (Base‘𝐴) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐶)((1st)‘𝑥))(𝑎𝑥)))))⟩ = ⟨(comp‘ndx), (𝑣 ∈ ((𝐵 Func 𝐷) × (𝐵 Func 𝐷)), ∈ (𝐵 Func 𝐷) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝐵 Nat 𝐷)), 𝑎 ∈ (𝑓(𝐵 Nat 𝐷)𝑔) ↦ (𝑥 ∈ (Base‘𝐵) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐷)((1st)‘𝑥))(𝑎𝑥)))))⟩)
8010, 12, 79tpeq123d 4660 . 2 (𝜑 → {⟨(Base‘ndx), (𝐴 Func 𝐶)⟩, ⟨(Hom ‘ndx), (𝐴 Nat 𝐶)⟩, ⟨(comp‘ndx), (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)), ∈ (𝐴 Func 𝐶) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝐴 Nat 𝐶)), 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔) ↦ (𝑥 ∈ (Base‘𝐴) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐶)((1st)‘𝑥))(𝑎𝑥)))))⟩} = {⟨(Base‘ndx), (𝐵 Func 𝐷)⟩, ⟨(Hom ‘ndx), (𝐵 Nat 𝐷)⟩, ⟨(comp‘ndx), (𝑣 ∈ ((𝐵 Func 𝐷) × (𝐵 Func 𝐷)), ∈ (𝐵 Func 𝐷) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝐵 Nat 𝐷)), 𝑎 ∈ (𝑓(𝐵 Nat 𝐷)𝑔) ↦ (𝑥 ∈ (Base‘𝐵) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐷)((1st)‘𝑥))(𝑎𝑥)))))⟩})
81 eqid 2820 . . 3 (𝐴 FuncCat 𝐶) = (𝐴 FuncCat 𝐶)
82 eqid 2820 . . 3 (𝐴 Func 𝐶) = (𝐴 Func 𝐶)
83 eqidd 2821 . . 3 (𝜑 → (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)), ∈ (𝐴 Func 𝐶) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝐴 Nat 𝐶)), 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔) ↦ (𝑥 ∈ (Base‘𝐴) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐶)((1st)‘𝑥))(𝑎𝑥))))) = (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)), ∈ (𝐴 Func 𝐶) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝐴 Nat 𝐶)), 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔) ↦ (𝑥 ∈ (Base‘𝐴) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐶)((1st)‘𝑥))(𝑎𝑥))))))
8481, 82, 59, 34, 30, 5, 7, 83fucval 17207 . 2 (𝜑 → (𝐴 FuncCat 𝐶) = {⟨(Base‘ndx), (𝐴 Func 𝐶)⟩, ⟨(Hom ‘ndx), (𝐴 Nat 𝐶)⟩, ⟨(comp‘ndx), (𝑣 ∈ ((𝐴 Func 𝐶) × (𝐴 Func 𝐶)), ∈ (𝐴 Func 𝐶) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝐴 Nat 𝐶)), 𝑎 ∈ (𝑓(𝐴 Nat 𝐶)𝑔) ↦ (𝑥 ∈ (Base‘𝐴) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐶)((1st)‘𝑥))(𝑎𝑥)))))⟩})
85 eqid 2820 . . 3 (𝐵 FuncCat 𝐷) = (𝐵 FuncCat 𝐷)
86 eqid 2820 . . 3 (𝐵 Func 𝐷) = (𝐵 Func 𝐷)
87 eqid 2820 . . 3 (𝐵 Nat 𝐷) = (𝐵 Nat 𝐷)
88 eqid 2820 . . 3 (Base‘𝐵) = (Base‘𝐵)
89 eqidd 2821 . . 3 (𝜑 → (𝑣 ∈ ((𝐵 Func 𝐷) × (𝐵 Func 𝐷)), ∈ (𝐵 Func 𝐷) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝐵 Nat 𝐷)), 𝑎 ∈ (𝑓(𝐵 Nat 𝐷)𝑔) ↦ (𝑥 ∈ (Base‘𝐵) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐷)((1st)‘𝑥))(𝑎𝑥))))) = (𝑣 ∈ ((𝐵 Func 𝐷) × (𝐵 Func 𝐷)), ∈ (𝐵 Func 𝐷) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝐵 Nat 𝐷)), 𝑎 ∈ (𝑓(𝐵 Nat 𝐷)𝑔) ↦ (𝑥 ∈ (Base‘𝐵) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐷)((1st)‘𝑥))(𝑎𝑥))))))
9085, 86, 87, 88, 31, 6, 8, 89fucval 17207 . 2 (𝜑 → (𝐵 FuncCat 𝐷) = {⟨(Base‘ndx), (𝐵 Func 𝐷)⟩, ⟨(Hom ‘ndx), (𝐵 Nat 𝐷)⟩, ⟨(comp‘ndx), (𝑣 ∈ ((𝐵 Func 𝐷) × (𝐵 Func 𝐷)), ∈ (𝐵 Func 𝐷) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝐵 Nat 𝐷)), 𝑎 ∈ (𝑓(𝐵 Nat 𝐷)𝑔) ↦ (𝑥 ∈ (Base‘𝐵) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝐷)((1st)‘𝑥))(𝑎𝑥)))))⟩})
9180, 84, 903eqtr4d 2865 1 (𝜑 → (𝐴 FuncCat 𝐶) = (𝐵 FuncCat 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398   = wceq 1537  wcel 2114  wnfc 2957  Vcvv 3473  csb 3860  {ctp 4547  cop 4549   class class class wbr 5042  cmpt 5122   × cxp 5529  Rel wrel 5536  cfv 6331  (class class class)co 7133  cmpo 7135  1st c1st 7665  2nd c2nd 7666  ndxcnx 16459  Basecbs 16462  Hom chom 16555  compcco 16556  Catccat 16914  Homf chomf 16916  compfccomf 16917   Func cfunc 17103   Nat cnat 17190   FuncCat cfuc 17191
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5242  ax-pr 5306  ax-un 7439
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-fal 1550  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-ral 3130  df-rex 3131  df-reu 3132  df-rab 3134  df-v 3475  df-sbc 3753  df-csb 3861  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4270  df-if 4444  df-pw 4517  df-sn 4544  df-pr 4546  df-tp 4548  df-op 4550  df-uni 4815  df-iun 4897  df-br 5043  df-opab 5105  df-mpt 5123  df-id 5436  df-xp 5537  df-rel 5538  df-cnv 5539  df-co 5540  df-dm 5541  df-rn 5542  df-res 5543  df-ima 5544  df-iota 6290  df-fun 6333  df-fn 6334  df-f 6335  df-f1 6336  df-fo 6337  df-f1o 6338  df-fv 6339  df-riota 7091  df-ov 7136  df-oprab 7137  df-mpo 7138  df-1st 7667  df-2nd 7668  df-map 8386  df-ixp 8440  df-cat 16918  df-cid 16919  df-homf 16920  df-comf 16921  df-func 17107  df-nat 17192  df-fuc 17193
This theorem is referenced by:  oyoncl  17499
  Copyright terms: Public domain W3C validator