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

Theorem isnat 17834
Description: Property of being a natural transformation. (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‘𝐷)
isnat.f (𝜑𝐹(𝐶 Func 𝐷)𝐺)
isnat.g (𝜑𝐾(𝐶 Func 𝐷)𝐿)
Assertion
Ref Expression
isnat (𝜑 → (𝐴 ∈ (⟨𝐹, 𝐺𝑁𝐾, 𝐿⟩) ↔ (𝐴X𝑥𝐵 ((𝐹𝑥)𝐽(𝐾𝑥)) ∧ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝐴𝑦)(⟨(𝐹𝑥), (𝐹𝑦)⟩ · (𝐾𝑦))((𝑥𝐺𝑦)‘)) = (((𝑥𝐿𝑦)‘)(⟨(𝐹𝑥), (𝐾𝑥)⟩ · (𝐾𝑦))(𝐴𝑥)))))
Distinct variable groups:   𝑥,,𝑦,𝐴   𝑥,𝐵,𝑦   𝐶,,𝑥,𝑦   ,𝐹,𝑥,𝑦   ,𝐺,𝑥,𝑦   ,𝐻   𝜑,,𝑥,𝑦   ,𝐾,𝑥,𝑦   ,𝐿,𝑥,𝑦   𝐷,,𝑥,𝑦
Allowed substitution hints:   𝐵()   · (𝑥,𝑦,)   𝐻(𝑥,𝑦)   𝐽(𝑥,𝑦,)   𝑁(𝑥,𝑦,)

Proof of Theorem isnat
Dummy variables 𝑎 𝑓 𝑔 𝑟 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 natfval.1 . . . . . 6 𝑁 = (𝐶 Nat 𝐷)
2 natfval.b . . . . . 6 𝐵 = (Base‘𝐶)
3 natfval.h . . . . . 6 𝐻 = (Hom ‘𝐶)
4 natfval.j . . . . . 6 𝐽 = (Hom ‘𝐷)
5 natfval.o . . . . . 6 · = (comp‘𝐷)
61, 2, 3, 4, 5natfval 17833 . . . . 5 𝑁 = (𝑓 ∈ (𝐶 Func 𝐷), 𝑔 ∈ (𝐶 Func 𝐷) ↦ (1st𝑓) / 𝑟(1st𝑔) / 𝑠{𝑎X𝑥𝐵 ((𝑟𝑥)𝐽(𝑠𝑥)) ∣ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩ · (𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩ · (𝑠𝑦))(𝑎𝑥))})
76a1i 11 . . . 4 (𝜑𝑁 = (𝑓 ∈ (𝐶 Func 𝐷), 𝑔 ∈ (𝐶 Func 𝐷) ↦ (1st𝑓) / 𝑟(1st𝑔) / 𝑠{𝑎X𝑥𝐵 ((𝑟𝑥)𝐽(𝑠𝑥)) ∣ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩ · (𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩ · (𝑠𝑦))(𝑎𝑥))}))
8 fvexd 6857 . . . . 5 ((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) → (1st𝑓) ∈ V)
9 simprl 769 . . . . . . 7 ((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) → 𝑓 = ⟨𝐹, 𝐺⟩)
109fveq2d 6846 . . . . . 6 ((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) → (1st𝑓) = (1st ‘⟨𝐹, 𝐺⟩))
11 relfunc 17748 . . . . . . . . 9 Rel (𝐶 Func 𝐷)
12 isnat.f . . . . . . . . 9 (𝜑𝐹(𝐶 Func 𝐷)𝐺)
13 brrelex12 5684 . . . . . . . . 9 ((Rel (𝐶 Func 𝐷) ∧ 𝐹(𝐶 Func 𝐷)𝐺) → (𝐹 ∈ V ∧ 𝐺 ∈ V))
1411, 12, 13sylancr 587 . . . . . . . 8 (𝜑 → (𝐹 ∈ V ∧ 𝐺 ∈ V))
15 op1stg 7933 . . . . . . . 8 ((𝐹 ∈ V ∧ 𝐺 ∈ V) → (1st ‘⟨𝐹, 𝐺⟩) = 𝐹)
1614, 15syl 17 . . . . . . 7 (𝜑 → (1st ‘⟨𝐹, 𝐺⟩) = 𝐹)
1716adantr 481 . . . . . 6 ((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) → (1st ‘⟨𝐹, 𝐺⟩) = 𝐹)
1810, 17eqtrd 2776 . . . . 5 ((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) → (1st𝑓) = 𝐹)
19 fvexd 6857 . . . . . 6 (((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) → (1st𝑔) ∈ V)
20 simplrr 776 . . . . . . . 8 (((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) → 𝑔 = ⟨𝐾, 𝐿⟩)
2120fveq2d 6846 . . . . . . 7 (((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) → (1st𝑔) = (1st ‘⟨𝐾, 𝐿⟩))
22 isnat.g . . . . . . . . . 10 (𝜑𝐾(𝐶 Func 𝐷)𝐿)
23 brrelex12 5684 . . . . . . . . . 10 ((Rel (𝐶 Func 𝐷) ∧ 𝐾(𝐶 Func 𝐷)𝐿) → (𝐾 ∈ V ∧ 𝐿 ∈ V))
2411, 22, 23sylancr 587 . . . . . . . . 9 (𝜑 → (𝐾 ∈ V ∧ 𝐿 ∈ V))
25 op1stg 7933 . . . . . . . . 9 ((𝐾 ∈ V ∧ 𝐿 ∈ V) → (1st ‘⟨𝐾, 𝐿⟩) = 𝐾)
2624, 25syl 17 . . . . . . . 8 (𝜑 → (1st ‘⟨𝐾, 𝐿⟩) = 𝐾)
2726ad2antrr 724 . . . . . . 7 (((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) → (1st ‘⟨𝐾, 𝐿⟩) = 𝐾)
2821, 27eqtrd 2776 . . . . . 6 (((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) → (1st𝑔) = 𝐾)
29 simplr 767 . . . . . . . . . 10 ((((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → 𝑟 = 𝐹)
3029fveq1d 6844 . . . . . . . . 9 ((((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (𝑟𝑥) = (𝐹𝑥))
31 simpr 485 . . . . . . . . . 10 ((((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → 𝑠 = 𝐾)
3231fveq1d 6844 . . . . . . . . 9 ((((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (𝑠𝑥) = (𝐾𝑥))
3330, 32oveq12d 7375 . . . . . . . 8 ((((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → ((𝑟𝑥)𝐽(𝑠𝑥)) = ((𝐹𝑥)𝐽(𝐾𝑥)))
3433ixpeq2dv 8851 . . . . . . 7 ((((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → X𝑥𝐵 ((𝑟𝑥)𝐽(𝑠𝑥)) = X𝑥𝐵 ((𝐹𝑥)𝐽(𝐾𝑥)))
3529fveq1d 6844 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (𝑟𝑦) = (𝐹𝑦))
3630, 35opeq12d 4838 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → ⟨(𝑟𝑥), (𝑟𝑦)⟩ = ⟨(𝐹𝑥), (𝐹𝑦)⟩)
3731fveq1d 6844 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (𝑠𝑦) = (𝐾𝑦))
3836, 37oveq12d 7375 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (⟨(𝑟𝑥), (𝑟𝑦)⟩ · (𝑠𝑦)) = (⟨(𝐹𝑥), (𝐹𝑦)⟩ · (𝐾𝑦)))
39 eqidd 2737 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (𝑎𝑦) = (𝑎𝑦))
409ad2antrr 724 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → 𝑓 = ⟨𝐹, 𝐺⟩)
4140fveq2d 6846 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (2nd𝑓) = (2nd ‘⟨𝐹, 𝐺⟩))
42 op2ndg 7934 . . . . . . . . . . . . . . . 16 ((𝐹 ∈ V ∧ 𝐺 ∈ V) → (2nd ‘⟨𝐹, 𝐺⟩) = 𝐺)
4314, 42syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (2nd ‘⟨𝐹, 𝐺⟩) = 𝐺)
4443ad3antrrr 728 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (2nd ‘⟨𝐹, 𝐺⟩) = 𝐺)
4541, 44eqtrd 2776 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (2nd𝑓) = 𝐺)
4645oveqd 7374 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (𝑥(2nd𝑓)𝑦) = (𝑥𝐺𝑦))
4746fveq1d 6844 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → ((𝑥(2nd𝑓)𝑦)‘) = ((𝑥𝐺𝑦)‘))
4838, 39, 47oveq123d 7378 . . . . . . . . . 10 ((((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → ((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩ · (𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = ((𝑎𝑦)(⟨(𝐹𝑥), (𝐹𝑦)⟩ · (𝐾𝑦))((𝑥𝐺𝑦)‘)))
4930, 32opeq12d 4838 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → ⟨(𝑟𝑥), (𝑠𝑥)⟩ = ⟨(𝐹𝑥), (𝐾𝑥)⟩)
5049, 37oveq12d 7375 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (⟨(𝑟𝑥), (𝑠𝑥)⟩ · (𝑠𝑦)) = (⟨(𝐹𝑥), (𝐾𝑥)⟩ · (𝐾𝑦)))
5120adantr 481 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → 𝑔 = ⟨𝐾, 𝐿⟩)
5251fveq2d 6846 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (2nd𝑔) = (2nd ‘⟨𝐾, 𝐿⟩))
53 op2ndg 7934 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ V ∧ 𝐿 ∈ V) → (2nd ‘⟨𝐾, 𝐿⟩) = 𝐿)
5424, 53syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (2nd ‘⟨𝐾, 𝐿⟩) = 𝐿)
5554ad3antrrr 728 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (2nd ‘⟨𝐾, 𝐿⟩) = 𝐿)
5652, 55eqtrd 2776 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (2nd𝑔) = 𝐿)
5756oveqd 7374 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (𝑥(2nd𝑔)𝑦) = (𝑥𝐿𝑦))
5857fveq1d 6844 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → ((𝑥(2nd𝑔)𝑦)‘) = ((𝑥𝐿𝑦)‘))
59 eqidd 2737 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (𝑎𝑥) = (𝑎𝑥))
6050, 58, 59oveq123d 7378 . . . . . . . . . 10 ((((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩ · (𝑠𝑦))(𝑎𝑥)) = (((𝑥𝐿𝑦)‘)(⟨(𝐹𝑥), (𝐾𝑥)⟩ · (𝐾𝑦))(𝑎𝑥)))
6148, 60eqeq12d 2752 . . . . . . . . 9 ((((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩ · (𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩ · (𝑠𝑦))(𝑎𝑥)) ↔ ((𝑎𝑦)(⟨(𝐹𝑥), (𝐹𝑦)⟩ · (𝐾𝑦))((𝑥𝐺𝑦)‘)) = (((𝑥𝐿𝑦)‘)(⟨(𝐹𝑥), (𝐾𝑥)⟩ · (𝐾𝑦))(𝑎𝑥))))
6261ralbidv 3174 . . . . . . . 8 ((((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (∀ ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩ · (𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩ · (𝑠𝑦))(𝑎𝑥)) ↔ ∀ ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝐹𝑥), (𝐹𝑦)⟩ · (𝐾𝑦))((𝑥𝐺𝑦)‘)) = (((𝑥𝐿𝑦)‘)(⟨(𝐹𝑥), (𝐾𝑥)⟩ · (𝐾𝑦))(𝑎𝑥))))
63622ralbidv 3212 . . . . . . 7 ((((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → (∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩ · (𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩ · (𝑠𝑦))(𝑎𝑥)) ↔ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝐹𝑥), (𝐹𝑦)⟩ · (𝐾𝑦))((𝑥𝐺𝑦)‘)) = (((𝑥𝐿𝑦)‘)(⟨(𝐹𝑥), (𝐾𝑥)⟩ · (𝐾𝑦))(𝑎𝑥))))
6434, 63rabeqbidv 3424 . . . . . 6 ((((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) ∧ 𝑠 = 𝐾) → {𝑎X𝑥𝐵 ((𝑟𝑥)𝐽(𝑠𝑥)) ∣ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩ · (𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩ · (𝑠𝑦))(𝑎𝑥))} = {𝑎X𝑥𝐵 ((𝐹𝑥)𝐽(𝐾𝑥)) ∣ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝐹𝑥), (𝐹𝑦)⟩ · (𝐾𝑦))((𝑥𝐺𝑦)‘)) = (((𝑥𝐿𝑦)‘)(⟨(𝐹𝑥), (𝐾𝑥)⟩ · (𝐾𝑦))(𝑎𝑥))})
6519, 28, 64csbied2 3895 . . . . 5 (((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) ∧ 𝑟 = 𝐹) → (1st𝑔) / 𝑠{𝑎X𝑥𝐵 ((𝑟𝑥)𝐽(𝑠𝑥)) ∣ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩ · (𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩ · (𝑠𝑦))(𝑎𝑥))} = {𝑎X𝑥𝐵 ((𝐹𝑥)𝐽(𝐾𝑥)) ∣ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝐹𝑥), (𝐹𝑦)⟩ · (𝐾𝑦))((𝑥𝐺𝑦)‘)) = (((𝑥𝐿𝑦)‘)(⟨(𝐹𝑥), (𝐾𝑥)⟩ · (𝐾𝑦))(𝑎𝑥))})
668, 18, 65csbied2 3895 . . . 4 ((𝜑 ∧ (𝑓 = ⟨𝐹, 𝐺⟩ ∧ 𝑔 = ⟨𝐾, 𝐿⟩)) → (1st𝑓) / 𝑟(1st𝑔) / 𝑠{𝑎X𝑥𝐵 ((𝑟𝑥)𝐽(𝑠𝑥)) ∣ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝑟𝑥), (𝑟𝑦)⟩ · (𝑠𝑦))((𝑥(2nd𝑓)𝑦)‘)) = (((𝑥(2nd𝑔)𝑦)‘)(⟨(𝑟𝑥), (𝑠𝑥)⟩ · (𝑠𝑦))(𝑎𝑥))} = {𝑎X𝑥𝐵 ((𝐹𝑥)𝐽(𝐾𝑥)) ∣ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝐹𝑥), (𝐹𝑦)⟩ · (𝐾𝑦))((𝑥𝐺𝑦)‘)) = (((𝑥𝐿𝑦)‘)(⟨(𝐹𝑥), (𝐾𝑥)⟩ · (𝐾𝑦))(𝑎𝑥))})
67 df-br 5106 . . . . 5 (𝐹(𝐶 Func 𝐷)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝐶 Func 𝐷))
6812, 67sylib 217 . . . 4 (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝐶 Func 𝐷))
69 df-br 5106 . . . . 5 (𝐾(𝐶 Func 𝐷)𝐿 ↔ ⟨𝐾, 𝐿⟩ ∈ (𝐶 Func 𝐷))
7022, 69sylib 217 . . . 4 (𝜑 → ⟨𝐾, 𝐿⟩ ∈ (𝐶 Func 𝐷))
71 ovex 7390 . . . . . . . 8 ((𝐹𝑥)𝐽(𝐾𝑥)) ∈ V
7271rgenw 3068 . . . . . . 7 𝑥𝐵 ((𝐹𝑥)𝐽(𝐾𝑥)) ∈ V
73 ixpexg 8860 . . . . . . 7 (∀𝑥𝐵 ((𝐹𝑥)𝐽(𝐾𝑥)) ∈ V → X𝑥𝐵 ((𝐹𝑥)𝐽(𝐾𝑥)) ∈ V)
7472, 73ax-mp 5 . . . . . 6 X𝑥𝐵 ((𝐹𝑥)𝐽(𝐾𝑥)) ∈ V
7574rabex 5289 . . . . 5 {𝑎X𝑥𝐵 ((𝐹𝑥)𝐽(𝐾𝑥)) ∣ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝐹𝑥), (𝐹𝑦)⟩ · (𝐾𝑦))((𝑥𝐺𝑦)‘)) = (((𝑥𝐿𝑦)‘)(⟨(𝐹𝑥), (𝐾𝑥)⟩ · (𝐾𝑦))(𝑎𝑥))} ∈ V
7675a1i 11 . . . 4 (𝜑 → {𝑎X𝑥𝐵 ((𝐹𝑥)𝐽(𝐾𝑥)) ∣ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝐹𝑥), (𝐹𝑦)⟩ · (𝐾𝑦))((𝑥𝐺𝑦)‘)) = (((𝑥𝐿𝑦)‘)(⟨(𝐹𝑥), (𝐾𝑥)⟩ · (𝐾𝑦))(𝑎𝑥))} ∈ V)
777, 66, 68, 70, 76ovmpod 7507 . . 3 (𝜑 → (⟨𝐹, 𝐺𝑁𝐾, 𝐿⟩) = {𝑎X𝑥𝐵 ((𝐹𝑥)𝐽(𝐾𝑥)) ∣ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝐹𝑥), (𝐹𝑦)⟩ · (𝐾𝑦))((𝑥𝐺𝑦)‘)) = (((𝑥𝐿𝑦)‘)(⟨(𝐹𝑥), (𝐾𝑥)⟩ · (𝐾𝑦))(𝑎𝑥))})
7877eleq2d 2823 . 2 (𝜑 → (𝐴 ∈ (⟨𝐹, 𝐺𝑁𝐾, 𝐿⟩) ↔ 𝐴 ∈ {𝑎X𝑥𝐵 ((𝐹𝑥)𝐽(𝐾𝑥)) ∣ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝐹𝑥), (𝐹𝑦)⟩ · (𝐾𝑦))((𝑥𝐺𝑦)‘)) = (((𝑥𝐿𝑦)‘)(⟨(𝐹𝑥), (𝐾𝑥)⟩ · (𝐾𝑦))(𝑎𝑥))}))
79 fveq1 6841 . . . . . . 7 (𝑎 = 𝐴 → (𝑎𝑦) = (𝐴𝑦))
8079oveq1d 7372 . . . . . 6 (𝑎 = 𝐴 → ((𝑎𝑦)(⟨(𝐹𝑥), (𝐹𝑦)⟩ · (𝐾𝑦))((𝑥𝐺𝑦)‘)) = ((𝐴𝑦)(⟨(𝐹𝑥), (𝐹𝑦)⟩ · (𝐾𝑦))((𝑥𝐺𝑦)‘)))
81 fveq1 6841 . . . . . . 7 (𝑎 = 𝐴 → (𝑎𝑥) = (𝐴𝑥))
8281oveq2d 7373 . . . . . 6 (𝑎 = 𝐴 → (((𝑥𝐿𝑦)‘)(⟨(𝐹𝑥), (𝐾𝑥)⟩ · (𝐾𝑦))(𝑎𝑥)) = (((𝑥𝐿𝑦)‘)(⟨(𝐹𝑥), (𝐾𝑥)⟩ · (𝐾𝑦))(𝐴𝑥)))
8380, 82eqeq12d 2752 . . . . 5 (𝑎 = 𝐴 → (((𝑎𝑦)(⟨(𝐹𝑥), (𝐹𝑦)⟩ · (𝐾𝑦))((𝑥𝐺𝑦)‘)) = (((𝑥𝐿𝑦)‘)(⟨(𝐹𝑥), (𝐾𝑥)⟩ · (𝐾𝑦))(𝑎𝑥)) ↔ ((𝐴𝑦)(⟨(𝐹𝑥), (𝐹𝑦)⟩ · (𝐾𝑦))((𝑥𝐺𝑦)‘)) = (((𝑥𝐿𝑦)‘)(⟨(𝐹𝑥), (𝐾𝑥)⟩ · (𝐾𝑦))(𝐴𝑥))))
8483ralbidv 3174 . . . 4 (𝑎 = 𝐴 → (∀ ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝐹𝑥), (𝐹𝑦)⟩ · (𝐾𝑦))((𝑥𝐺𝑦)‘)) = (((𝑥𝐿𝑦)‘)(⟨(𝐹𝑥), (𝐾𝑥)⟩ · (𝐾𝑦))(𝑎𝑥)) ↔ ∀ ∈ (𝑥𝐻𝑦)((𝐴𝑦)(⟨(𝐹𝑥), (𝐹𝑦)⟩ · (𝐾𝑦))((𝑥𝐺𝑦)‘)) = (((𝑥𝐿𝑦)‘)(⟨(𝐹𝑥), (𝐾𝑥)⟩ · (𝐾𝑦))(𝐴𝑥))))
85842ralbidv 3212 . . 3 (𝑎 = 𝐴 → (∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝐹𝑥), (𝐹𝑦)⟩ · (𝐾𝑦))((𝑥𝐺𝑦)‘)) = (((𝑥𝐿𝑦)‘)(⟨(𝐹𝑥), (𝐾𝑥)⟩ · (𝐾𝑦))(𝑎𝑥)) ↔ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝐴𝑦)(⟨(𝐹𝑥), (𝐹𝑦)⟩ · (𝐾𝑦))((𝑥𝐺𝑦)‘)) = (((𝑥𝐿𝑦)‘)(⟨(𝐹𝑥), (𝐾𝑥)⟩ · (𝐾𝑦))(𝐴𝑥))))
8685elrab 3645 . 2 (𝐴 ∈ {𝑎X𝑥𝐵 ((𝐹𝑥)𝐽(𝐾𝑥)) ∣ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝑎𝑦)(⟨(𝐹𝑥), (𝐹𝑦)⟩ · (𝐾𝑦))((𝑥𝐺𝑦)‘)) = (((𝑥𝐿𝑦)‘)(⟨(𝐹𝑥), (𝐾𝑥)⟩ · (𝐾𝑦))(𝑎𝑥))} ↔ (𝐴X𝑥𝐵 ((𝐹𝑥)𝐽(𝐾𝑥)) ∧ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝐴𝑦)(⟨(𝐹𝑥), (𝐹𝑦)⟩ · (𝐾𝑦))((𝑥𝐺𝑦)‘)) = (((𝑥𝐿𝑦)‘)(⟨(𝐹𝑥), (𝐾𝑥)⟩ · (𝐾𝑦))(𝐴𝑥))))
8778, 86bitrdi 286 1 (𝜑 → (𝐴 ∈ (⟨𝐹, 𝐺𝑁𝐾, 𝐿⟩) ↔ (𝐴X𝑥𝐵 ((𝐹𝑥)𝐽(𝐾𝑥)) ∧ ∀𝑥𝐵𝑦𝐵 ∈ (𝑥𝐻𝑦)((𝐴𝑦)(⟨(𝐹𝑥), (𝐹𝑦)⟩ · (𝐾𝑦))((𝑥𝐺𝑦)‘)) = (((𝑥𝐿𝑦)‘)(⟨(𝐹𝑥), (𝐾𝑥)⟩ · (𝐾𝑦))(𝐴𝑥)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wral 3064  {crab 3407  Vcvv 3445  csb 3855  cop 4592   class class class wbr 5105  Rel wrel 5638  cfv 6496  (class class class)co 7357  cmpo 7359  1st c1st 7919  2nd c2nd 7920  Xcixp 8835  Basecbs 17083  Hom chom 17144  compcco 17145   Func cfunc 17740   Nat cnat 17828
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-1st 7921  df-2nd 7922  df-ixp 8836  df-func 17744  df-nat 17830
This theorem is referenced by:  isnat2  17835  natixp  17839  nati  17842
  Copyright terms: Public domain W3C validator