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

Theorem natfval 16372
Description: Value of the function giving natural transformations between two categories. (Contributed by Mario Carneiro, 6-Jan-2017.)
Hypotheses
Ref Expression
natfval.1 𝑁 = (𝐶 Nat 𝐷)
natfval.b 𝐵 = (Base‘𝐶)
natfval.h 𝐻 = (Hom ‘𝐶)
natfval.j 𝐽 = (Hom ‘𝐷)
natfval.o · = (comp‘𝐷)
Assertion
Ref Expression
natfval 𝑁 = (𝑓 ∈ (𝐶 Func 𝐷), 𝑔 ∈ (𝐶 Func 𝐷) ↦ (1st𝑓) / 𝑟(1st𝑔) / 𝑠{𝑎X𝑥𝐵 ((𝑟𝑥)𝐽(𝑠𝑥)) ∣ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩ · (𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩ · (𝑠𝑦))(𝑎𝑥))})
Distinct variable groups:   𝑓,𝑎,𝑔,,𝑟,𝑠,𝑥,𝑦   𝐵,𝑎,𝑓,𝑔,𝑟,𝑠,𝑥,𝑦   𝐶,𝑎,𝑓,𝑔,,𝑟,𝑠,𝑥,𝑦   𝐽,𝑎,𝑓,𝑔,𝑟,𝑠   𝐻,𝑎,𝑓,𝑔,,𝑟,𝑠   · ,𝑎,𝑓,𝑔,𝑟,𝑠   𝐷,𝑎,𝑓,𝑔,,𝑟,𝑠,𝑥,𝑦
Allowed substitution hints:   𝐵()   · (𝑥,𝑦,)   𝐻(𝑥,𝑦)   𝐽(𝑥,𝑦,)   𝑁(𝑥,𝑦,𝑓,𝑔,,𝑠,𝑟,𝑎)

Proof of Theorem natfval
Dummy variables 𝑡 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 natfval.1 . 2 𝑁 = (𝐶 Nat 𝐷)
2 oveq12 6533 . . . . 5 ((𝑡 = 𝐶𝑢 = 𝐷) → (𝑡 Func 𝑢) = (𝐶 Func 𝐷))
3 simpl 471 . . . . . . . . . . . 12 ((𝑡 = 𝐶𝑢 = 𝐷) → 𝑡 = 𝐶)
43fveq2d 6089 . . . . . . . . . . 11 ((𝑡 = 𝐶𝑢 = 𝐷) → (Base‘𝑡) = (Base‘𝐶))
5 natfval.b . . . . . . . . . . 11 𝐵 = (Base‘𝐶)
64, 5syl6eqr 2658 . . . . . . . . . 10 ((𝑡 = 𝐶𝑢 = 𝐷) → (Base‘𝑡) = 𝐵)
76ixpeq1d 7780 . . . . . . . . 9 ((𝑡 = 𝐶𝑢 = 𝐷) → X𝑥 ∈ (Base‘𝑡)((𝑟𝑥)(Hom ‘𝑢)(𝑠𝑥)) = X𝑥𝐵 ((𝑟𝑥)(Hom ‘𝑢)(𝑠𝑥)))
8 simpr 475 . . . . . . . . . . . . 13 ((𝑡 = 𝐶𝑢 = 𝐷) → 𝑢 = 𝐷)
98fveq2d 6089 . . . . . . . . . . . 12 ((𝑡 = 𝐶𝑢 = 𝐷) → (Hom ‘𝑢) = (Hom ‘𝐷))
10 natfval.j . . . . . . . . . . . 12 𝐽 = (Hom ‘𝐷)
119, 10syl6eqr 2658 . . . . . . . . . . 11 ((𝑡 = 𝐶𝑢 = 𝐷) → (Hom ‘𝑢) = 𝐽)
1211oveqd 6541 . . . . . . . . . 10 ((𝑡 = 𝐶𝑢 = 𝐷) → ((𝑟𝑥)(Hom ‘𝑢)(𝑠𝑥)) = ((𝑟𝑥)𝐽(𝑠𝑥)))
1312ixpeq2dv 7784 . . . . . . . . 9 ((𝑡 = 𝐶𝑢 = 𝐷) → X𝑥𝐵 ((𝑟𝑥)(Hom ‘𝑢)(𝑠𝑥)) = X𝑥𝐵 ((𝑟𝑥)𝐽(𝑠𝑥)))
147, 13eqtrd 2640 . . . . . . . 8 ((𝑡 = 𝐶𝑢 = 𝐷) → X𝑥 ∈ (Base‘𝑡)((𝑟𝑥)(Hom ‘𝑢)(𝑠𝑥)) = X𝑥𝐵 ((𝑟𝑥)𝐽(𝑠𝑥)))
153fveq2d 6089 . . . . . . . . . . . . 13 ((𝑡 = 𝐶𝑢 = 𝐷) → (Hom ‘𝑡) = (Hom ‘𝐶))
16 natfval.h . . . . . . . . . . . . 13 𝐻 = (Hom ‘𝐶)
1715, 16syl6eqr 2658 . . . . . . . . . . . 12 ((𝑡 = 𝐶𝑢 = 𝐷) → (Hom ‘𝑡) = 𝐻)
1817oveqd 6541 . . . . . . . . . . 11 ((𝑡 = 𝐶𝑢 = 𝐷) → (𝑥(Hom ‘𝑡)𝑦) = (𝑥𝐻𝑦))
198fveq2d 6089 . . . . . . . . . . . . . . 15 ((𝑡 = 𝐶𝑢 = 𝐷) → (comp‘𝑢) = (comp‘𝐷))
20 natfval.o . . . . . . . . . . . . . . 15 · = (comp‘𝐷)
2119, 20syl6eqr 2658 . . . . . . . . . . . . . 14 ((𝑡 = 𝐶𝑢 = 𝐷) → (comp‘𝑢) = · )
2221oveqd 6541 . . . . . . . . . . . . 13 ((𝑡 = 𝐶𝑢 = 𝐷) → (⟨(𝑟𝑥), (𝑟𝑦)⟩(comp‘𝑢)(𝑠𝑦)) = (⟨(𝑟𝑥), (𝑟𝑦)⟩ · (𝑠𝑦)))
2322oveqd 6541 . . . . . . . . . . . 12 ((𝑡 = 𝐶𝑢 = 𝐷) → ((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩(comp‘𝑢)(𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = ((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩ · (𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)))
2421oveqd 6541 . . . . . . . . . . . . 13 ((𝑡 = 𝐶𝑢 = 𝐷) → (⟨(𝑟𝑥), (𝑠𝑥)⟩(comp‘𝑢)(𝑠𝑦)) = (⟨(𝑟𝑥), (𝑠𝑥)⟩ · (𝑠𝑦)))
2524oveqd 6541 . . . . . . . . . . . 12 ((𝑡 = 𝐶𝑢 = 𝐷) → (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩(comp‘𝑢)(𝑠𝑦))(𝑎𝑥)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩ · (𝑠𝑦))(𝑎𝑥)))
2623, 25eqeq12d 2621 . . . . . . . . . . 11 ((𝑡 = 𝐶𝑢 = 𝐷) → (((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩(comp‘𝑢)(𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩(comp‘𝑢)(𝑠𝑦))(𝑎𝑥)) ↔ ((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩ · (𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩ · (𝑠𝑦))(𝑎𝑥))))
2718, 26raleqbidv 3125 . . . . . . . . . 10 ((𝑡 = 𝐶𝑢 = 𝐷) → (∀ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩(comp‘𝑢)(𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩(comp‘𝑢)(𝑠𝑦))(𝑎𝑥)) ↔ ∀ ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩ · (𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩ · (𝑠𝑦))(𝑎𝑥))))
286, 27raleqbidv 3125 . . . . . . . . 9 ((𝑡 = 𝐶𝑢 = 𝐷) → (∀𝑦 ∈ (Base‘𝑡)∀ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩(comp‘𝑢)(𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩(comp‘𝑢)(𝑠𝑦))(𝑎𝑥)) ↔ ∀𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩ · (𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩ · (𝑠𝑦))(𝑎𝑥))))
296, 28raleqbidv 3125 . . . . . . . 8 ((𝑡 = 𝐶𝑢 = 𝐷) → (∀𝑥 ∈ (Base‘𝑡)∀𝑦 ∈ (Base‘𝑡)∀ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩(comp‘𝑢)(𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩(comp‘𝑢)(𝑠𝑦))(𝑎𝑥)) ↔ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩ · (𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩ · (𝑠𝑦))(𝑎𝑥))))
3014, 29rabeqbidv 3164 . . . . . . 7 ((𝑡 = 𝐶𝑢 = 𝐷) → {𝑎X𝑥 ∈ (Base‘𝑡)((𝑟𝑥)(Hom ‘𝑢)(𝑠𝑥)) ∣ ∀𝑥 ∈ (Base‘𝑡)∀𝑦 ∈ (Base‘𝑡)∀ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩(comp‘𝑢)(𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩(comp‘𝑢)(𝑠𝑦))(𝑎𝑥))} = {𝑎X𝑥𝐵 ((𝑟𝑥)𝐽(𝑠𝑥)) ∣ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩ · (𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩ · (𝑠𝑦))(𝑎𝑥))})
3130csbeq2dv 3940 . . . . . 6 ((𝑡 = 𝐶𝑢 = 𝐷) → (1st𝑔) / 𝑠{𝑎X𝑥 ∈ (Base‘𝑡)((𝑟𝑥)(Hom ‘𝑢)(𝑠𝑥)) ∣ ∀𝑥 ∈ (Base‘𝑡)∀𝑦 ∈ (Base‘𝑡)∀ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩(comp‘𝑢)(𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩(comp‘𝑢)(𝑠𝑦))(𝑎𝑥))} = (1st𝑔) / 𝑠{𝑎X𝑥𝐵 ((𝑟𝑥)𝐽(𝑠𝑥)) ∣ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩ · (𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩ · (𝑠𝑦))(𝑎𝑥))})
3231csbeq2dv 3940 . . . . 5 ((𝑡 = 𝐶𝑢 = 𝐷) → (1st𝑓) / 𝑟(1st𝑔) / 𝑠{𝑎X𝑥 ∈ (Base‘𝑡)((𝑟𝑥)(Hom ‘𝑢)(𝑠𝑥)) ∣ ∀𝑥 ∈ (Base‘𝑡)∀𝑦 ∈ (Base‘𝑡)∀ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩(comp‘𝑢)(𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩(comp‘𝑢)(𝑠𝑦))(𝑎𝑥))} = (1st𝑓) / 𝑟(1st𝑔) / 𝑠{𝑎X𝑥𝐵 ((𝑟𝑥)𝐽(𝑠𝑥)) ∣ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩ · (𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩ · (𝑠𝑦))(𝑎𝑥))})
332, 2, 32mpt2eq123dv 6590 . . . 4 ((𝑡 = 𝐶𝑢 = 𝐷) → (𝑓 ∈ (𝑡 Func 𝑢), 𝑔 ∈ (𝑡 Func 𝑢) ↦ (1st𝑓) / 𝑟(1st𝑔) / 𝑠{𝑎X𝑥 ∈ (Base‘𝑡)((𝑟𝑥)(Hom ‘𝑢)(𝑠𝑥)) ∣ ∀𝑥 ∈ (Base‘𝑡)∀𝑦 ∈ (Base‘𝑡)∀ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩(comp‘𝑢)(𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩(comp‘𝑢)(𝑠𝑦))(𝑎𝑥))}) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑔 ∈ (𝐶 Func 𝐷) ↦ (1st𝑓) / 𝑟(1st𝑔) / 𝑠{𝑎X𝑥𝐵 ((𝑟𝑥)𝐽(𝑠𝑥)) ∣ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩ · (𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩ · (𝑠𝑦))(𝑎𝑥))}))
34 df-nat 16369 . . . 4 Nat = (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ (𝑓 ∈ (𝑡 Func 𝑢), 𝑔 ∈ (𝑡 Func 𝑢) ↦ (1st𝑓) / 𝑟(1st𝑔) / 𝑠{𝑎X𝑥 ∈ (Base‘𝑡)((𝑟𝑥)(Hom ‘𝑢)(𝑠𝑥)) ∣ ∀𝑥 ∈ (Base‘𝑡)∀𝑦 ∈ (Base‘𝑡)∀ ∈ (𝑥(Hom ‘𝑡)𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩(comp‘𝑢)(𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩(comp‘𝑢)(𝑠𝑦))(𝑎𝑥))}))
35 ovex 6552 . . . . 5 (𝐶 Func 𝐷) ∈ V
3635, 35mpt2ex 7110 . . . 4 (𝑓 ∈ (𝐶 Func 𝐷), 𝑔 ∈ (𝐶 Func 𝐷) ↦ (1st𝑓) / 𝑟(1st𝑔) / 𝑠{𝑎X𝑥𝐵 ((𝑟𝑥)𝐽(𝑠𝑥)) ∣ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩ · (𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩ · (𝑠𝑦))(𝑎𝑥))}) ∈ V
3733, 34, 36ovmpt2a 6664 . . 3 ((𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝐶 Nat 𝐷) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑔 ∈ (𝐶 Func 𝐷) ↦ (1st𝑓) / 𝑟(1st𝑔) / 𝑠{𝑎X𝑥𝐵 ((𝑟𝑥)𝐽(𝑠𝑥)) ∣ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩ · (𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩ · (𝑠𝑦))(𝑎𝑥))}))
3834mpt2ndm0 6747 . . . 4 (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝐶 Nat 𝐷) = ∅)
39 funcrcl 16289 . . . . . . . 8 (𝑓 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
4039con3i 148 . . . . . . 7 (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → ¬ 𝑓 ∈ (𝐶 Func 𝐷))
4140eq0rdv 3927 . . . . . 6 (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝐶 Func 𝐷) = ∅)
42 mpt2eq12 6588 . . . . . 6 (((𝐶 Func 𝐷) = ∅ ∧ (𝐶 Func 𝐷) = ∅) → (𝑓 ∈ (𝐶 Func 𝐷), 𝑔 ∈ (𝐶 Func 𝐷) ↦ (1st𝑓) / 𝑟(1st𝑔) / 𝑠{𝑎X𝑥𝐵 ((𝑟𝑥)𝐽(𝑠𝑥)) ∣ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩ · (𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩ · (𝑠𝑦))(𝑎𝑥))}) = (𝑓 ∈ ∅, 𝑔 ∈ ∅ ↦ (1st𝑓) / 𝑟(1st𝑔) / 𝑠{𝑎X𝑥𝐵 ((𝑟𝑥)𝐽(𝑠𝑥)) ∣ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩ · (𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩ · (𝑠𝑦))(𝑎𝑥))}))
4341, 41, 42syl2anc 690 . . . . 5 (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝑓 ∈ (𝐶 Func 𝐷), 𝑔 ∈ (𝐶 Func 𝐷) ↦ (1st𝑓) / 𝑟(1st𝑔) / 𝑠{𝑎X𝑥𝐵 ((𝑟𝑥)𝐽(𝑠𝑥)) ∣ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩ · (𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩ · (𝑠𝑦))(𝑎𝑥))}) = (𝑓 ∈ ∅, 𝑔 ∈ ∅ ↦ (1st𝑓) / 𝑟(1st𝑔) / 𝑠{𝑎X𝑥𝐵 ((𝑟𝑥)𝐽(𝑠𝑥)) ∣ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩ · (𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩ · (𝑠𝑦))(𝑎𝑥))}))
44 mpt20 6598 . . . . 5 (𝑓 ∈ ∅, 𝑔 ∈ ∅ ↦ (1st𝑓) / 𝑟(1st𝑔) / 𝑠{𝑎X𝑥𝐵 ((𝑟𝑥)𝐽(𝑠𝑥)) ∣ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩ · (𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩ · (𝑠𝑦))(𝑎𝑥))}) = ∅
4543, 44syl6eq 2656 . . . 4 (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝑓 ∈ (𝐶 Func 𝐷), 𝑔 ∈ (𝐶 Func 𝐷) ↦ (1st𝑓) / 𝑟(1st𝑔) / 𝑠{𝑎X𝑥𝐵 ((𝑟𝑥)𝐽(𝑠𝑥)) ∣ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩ · (𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩ · (𝑠𝑦))(𝑎𝑥))}) = ∅)
4638, 45eqtr4d 2643 . . 3 (¬ (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (𝐶 Nat 𝐷) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑔 ∈ (𝐶 Func 𝐷) ↦ (1st𝑓) / 𝑟(1st𝑔) / 𝑠{𝑎X𝑥𝐵 ((𝑟𝑥)𝐽(𝑠𝑥)) ∣ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩ · (𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩ · (𝑠𝑦))(𝑎𝑥))}))
4737, 46pm2.61i 174 . 2 (𝐶 Nat 𝐷) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑔 ∈ (𝐶 Func 𝐷) ↦ (1st𝑓) / 𝑟(1st𝑔) / 𝑠{𝑎X𝑥𝐵 ((𝑟𝑥)𝐽(𝑠𝑥)) ∣ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩ · (𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩ · (𝑠𝑦))(𝑎𝑥))})
481, 47eqtri 2628 1 𝑁 = (𝑓 ∈ (𝐶 Func 𝐷), 𝑔 ∈ (𝐶 Func 𝐷) ↦ (1st𝑓) / 𝑟(1st𝑔) / 𝑠{𝑎X𝑥𝐵 ((𝑟𝑥)𝐽(𝑠𝑥)) ∣ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩ · (𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩ · (𝑠𝑦))(𝑎𝑥))})
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 382   = wceq 1474  wcel 1976  wral 2892  {crab 2896  csb 3495  c0 3870  cop 4127  cfv 5787  (class class class)co 6524  cmpt2 6526  1st c1st 7031  2nd c2nd 7032  Xcixp 7768  Basecbs 15638  Hom chom 15722  compcco 15723  Catccat 16091   Func cfunc 16280   Nat cnat 16367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-rep 4690  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-ral 2897  df-rex 2898  df-reu 2899  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-op 4128  df-uni 4364  df-iun 4448  df-br 4575  df-opab 4635  df-mpt 4636  df-id 4940  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795  df-ov 6527  df-oprab 6528  df-mpt2 6529  df-1st 7033  df-2nd 7034  df-ixp 7769  df-func 16284  df-nat 16369
This theorem is referenced by:  isnat  16373  natffn  16375  natrcl  16376  wunnat  16382  natpropd  16402
  Copyright terms: Public domain W3C validator