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

Theorem isfunc 17129
Description: Value of the set of functors between two categories. (Contributed by Mario Carneiro, 2-Jan-2017.)
Hypotheses
Ref Expression
isfunc.b 𝐵 = (Base‘𝐷)
isfunc.c 𝐶 = (Base‘𝐸)
isfunc.h 𝐻 = (Hom ‘𝐷)
isfunc.j 𝐽 = (Hom ‘𝐸)
isfunc.1 1 = (Id‘𝐷)
isfunc.i 𝐼 = (Id‘𝐸)
isfunc.x · = (comp‘𝐷)
isfunc.o 𝑂 = (comp‘𝐸)
isfunc.d (𝜑𝐷 ∈ Cat)
isfunc.e (𝜑𝐸 ∈ Cat)
Assertion
Ref Expression
isfunc (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ (𝐹:𝐵𝐶𝐺X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))𝐽(𝐹‘(2nd𝑧))) ↑m (𝐻𝑧)) ∧ ∀𝑥𝐵 (((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚))))))
Distinct variable groups:   𝑚,𝑛,𝑥,𝑦,𝑧,𝐵   𝐷,𝑚,𝑛,𝑥,𝑦,𝑧   𝑚,𝐸,𝑛,𝑥,𝑦,𝑧   𝑚,𝐻,𝑛,𝑥,𝑦,𝑧   𝑚,𝐹,𝑛,𝑥,𝑦,𝑧   𝑚,𝐺,𝑛,𝑥,𝑦,𝑧   𝑥,𝐽,𝑦,𝑧   𝜑,𝑚,𝑛,𝑥,𝑦,𝑧
Allowed substitution hints:   𝐶(𝑥,𝑦,𝑧,𝑚,𝑛)   · (𝑥,𝑦,𝑧,𝑚,𝑛)   1 (𝑥,𝑦,𝑧,𝑚,𝑛)   𝐼(𝑥,𝑦,𝑧,𝑚,𝑛)   𝐽(𝑚,𝑛)   𝑂(𝑥,𝑦,𝑧,𝑚,𝑛)

Proof of Theorem isfunc
Dummy variables 𝑏 𝑑 𝑒 𝑓 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isfunc.d . . . 4 (𝜑𝐷 ∈ Cat)
2 isfunc.e . . . 4 (𝜑𝐸 ∈ Cat)
3 fvexd 6664 . . . . . . 7 ((𝑑 = 𝐷𝑒 = 𝐸) → (Base‘𝑑) ∈ V)
4 simpl 486 . . . . . . . . 9 ((𝑑 = 𝐷𝑒 = 𝐸) → 𝑑 = 𝐷)
54fveq2d 6653 . . . . . . . 8 ((𝑑 = 𝐷𝑒 = 𝐸) → (Base‘𝑑) = (Base‘𝐷))
6 isfunc.b . . . . . . . 8 𝐵 = (Base‘𝐷)
75, 6eqtr4di 2854 . . . . . . 7 ((𝑑 = 𝐷𝑒 = 𝐸) → (Base‘𝑑) = 𝐵)
8 simpr 488 . . . . . . . . . . 11 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵)
9 simplr 768 . . . . . . . . . . . . 13 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → 𝑒 = 𝐸)
109fveq2d 6653 . . . . . . . . . . . 12 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Base‘𝑒) = (Base‘𝐸))
11 isfunc.c . . . . . . . . . . . 12 𝐶 = (Base‘𝐸)
1210, 11eqtr4di 2854 . . . . . . . . . . 11 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Base‘𝑒) = 𝐶)
138, 12feq23d 6486 . . . . . . . . . 10 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑓:𝑏⟶(Base‘𝑒) ↔ 𝑓:𝐵𝐶))
1411fvexi 6663 . . . . . . . . . . 11 𝐶 ∈ V
156fvexi 6663 . . . . . . . . . . 11 𝐵 ∈ V
1614, 15elmap 8422 . . . . . . . . . 10 (𝑓 ∈ (𝐶m 𝐵) ↔ 𝑓:𝐵𝐶)
1713, 16syl6bbr 292 . . . . . . . . 9 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑓:𝑏⟶(Base‘𝑒) ↔ 𝑓 ∈ (𝐶m 𝐵)))
188sqxpeqd 5555 . . . . . . . . . . . 12 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑏 × 𝑏) = (𝐵 × 𝐵))
1918ixpeq1d 8460 . . . . . . . . . . 11 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st𝑧))(Hom ‘𝑒)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) = X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))(Hom ‘𝑒)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)))
209fveq2d 6653 . . . . . . . . . . . . . . 15 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Hom ‘𝑒) = (Hom ‘𝐸))
21 isfunc.j . . . . . . . . . . . . . . 15 𝐽 = (Hom ‘𝐸)
2220, 21eqtr4di 2854 . . . . . . . . . . . . . 14 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Hom ‘𝑒) = 𝐽)
2322oveqd 7156 . . . . . . . . . . . . 13 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((𝑓‘(1st𝑧))(Hom ‘𝑒)(𝑓‘(2nd𝑧))) = ((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))))
24 simpll 766 . . . . . . . . . . . . . . . 16 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → 𝑑 = 𝐷)
2524fveq2d 6653 . . . . . . . . . . . . . . 15 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Hom ‘𝑑) = (Hom ‘𝐷))
26 isfunc.h . . . . . . . . . . . . . . 15 𝐻 = (Hom ‘𝐷)
2725, 26eqtr4di 2854 . . . . . . . . . . . . . 14 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Hom ‘𝑑) = 𝐻)
2827fveq1d 6651 . . . . . . . . . . . . 13 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((Hom ‘𝑑)‘𝑧) = (𝐻𝑧))
2923, 28oveq12d 7157 . . . . . . . . . . . 12 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (((𝑓‘(1st𝑧))(Hom ‘𝑒)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) = (((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)))
3029ixpeq2dv 8464 . . . . . . . . . . 11 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))(Hom ‘𝑒)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) = X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)))
3119, 30eqtrd 2836 . . . . . . . . . 10 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st𝑧))(Hom ‘𝑒)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) = X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)))
3231eleq2d 2878 . . . . . . . . 9 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑔X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st𝑧))(Hom ‘𝑒)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) ↔ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))))
3324fveq2d 6653 . . . . . . . . . . . . . . 15 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Id‘𝑑) = (Id‘𝐷))
34 isfunc.1 . . . . . . . . . . . . . . 15 1 = (Id‘𝐷)
3533, 34eqtr4di 2854 . . . . . . . . . . . . . 14 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Id‘𝑑) = 1 )
3635fveq1d 6651 . . . . . . . . . . . . 13 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((Id‘𝑑)‘𝑥) = ( 1𝑥))
3736fveq2d 6653 . . . . . . . . . . . 12 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((𝑥𝑔𝑥)‘( 1𝑥)))
389fveq2d 6653 . . . . . . . . . . . . . 14 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Id‘𝑒) = (Id‘𝐸))
39 isfunc.i . . . . . . . . . . . . . 14 𝐼 = (Id‘𝐸)
4038, 39eqtr4di 2854 . . . . . . . . . . . . 13 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Id‘𝑒) = 𝐼)
4140fveq1d 6651 . . . . . . . . . . . 12 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((Id‘𝑒)‘(𝑓𝑥)) = (𝐼‘(𝑓𝑥)))
4237, 41eqeq12d 2817 . . . . . . . . . . 11 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓𝑥)) ↔ ((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥))))
4327oveqd 7156 . . . . . . . . . . . . . 14 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑥(Hom ‘𝑑)𝑦) = (𝑥𝐻𝑦))
4427oveqd 7156 . . . . . . . . . . . . . . 15 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑦(Hom ‘𝑑)𝑧) = (𝑦𝐻𝑧))
4524fveq2d 6653 . . . . . . . . . . . . . . . . . . . 20 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (comp‘𝑑) = (comp‘𝐷))
46 isfunc.x . . . . . . . . . . . . . . . . . . . 20 · = (comp‘𝐷)
4745, 46eqtr4di 2854 . . . . . . . . . . . . . . . . . . 19 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (comp‘𝑑) = · )
4847oveqd 7156 . . . . . . . . . . . . . . . . . 18 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧) = (⟨𝑥, 𝑦· 𝑧))
4948oveqd 7156 . . . . . . . . . . . . . . . . 17 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚) = (𝑛(⟨𝑥, 𝑦· 𝑧)𝑚))
5049fveq2d 6653 . . . . . . . . . . . . . . . 16 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)))
519fveq2d 6653 . . . . . . . . . . . . . . . . . . 19 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (comp‘𝑒) = (comp‘𝐸))
52 isfunc.o . . . . . . . . . . . . . . . . . . 19 𝑂 = (comp‘𝐸)
5351, 52eqtr4di 2854 . . . . . . . . . . . . . . . . . 18 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (comp‘𝑒) = 𝑂)
5453oveqd 7156 . . . . . . . . . . . . . . . . 17 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑒)(𝑓𝑧)) = (⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧)))
5554oveqd 7156 . . . . . . . . . . . . . . . 16 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑒)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))
5650, 55eqeq12d 2817 . . . . . . . . . . . . . . 15 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑒)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))
5744, 56raleqbidv 3357 . . . . . . . . . . . . . 14 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑒)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))
5843, 57raleqbidv 3357 . . . . . . . . . . . . 13 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑒)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))
598, 58raleqbidv 3357 . . . . . . . . . . . 12 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (∀𝑧𝑏𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑒)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))
608, 59raleqbidv 3357 . . . . . . . . . . 11 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (∀𝑦𝑏𝑧𝑏𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑒)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))
6142, 60anbi12d 633 . . . . . . . . . 10 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓𝑥)) ∧ ∀𝑦𝑏𝑧𝑏𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑒)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))))
628, 61raleqbidv 3357 . . . . . . . . 9 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (∀𝑥𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓𝑥)) ∧ ∀𝑦𝑏𝑧𝑏𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑒)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))))
6317, 32, 623anbi123d 1433 . . . . . . . 8 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((𝑓:𝑏⟶(Base‘𝑒) ∧ 𝑔X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st𝑧))(Hom ‘𝑒)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) ∧ ∀𝑥𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓𝑥)) ∧ ∀𝑦𝑏𝑧𝑏𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑒)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ (𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))))
64 df-3an 1086 . . . . . . . 8 ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))))
6563, 64syl6bb 290 . . . . . . 7 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((𝑓:𝑏⟶(Base‘𝑒) ∧ 𝑔X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st𝑧))(Hom ‘𝑒)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) ∧ ∀𝑥𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓𝑥)) ∧ ∀𝑦𝑏𝑧𝑏𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑒)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))))
663, 7, 65sbcied2 3766 . . . . . 6 ((𝑑 = 𝐷𝑒 = 𝐸) → ([(Base‘𝑑) / 𝑏](𝑓:𝑏⟶(Base‘𝑒) ∧ 𝑔X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st𝑧))(Hom ‘𝑒)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) ∧ ∀𝑥𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓𝑥)) ∧ ∀𝑦𝑏𝑧𝑏𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑒)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))))
6766opabbidv 5099 . . . . 5 ((𝑑 = 𝐷𝑒 = 𝐸) → {⟨𝑓, 𝑔⟩ ∣ [(Base‘𝑑) / 𝑏](𝑓:𝑏⟶(Base‘𝑒) ∧ 𝑔X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st𝑧))(Hom ‘𝑒)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) ∧ ∀𝑥𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓𝑥)) ∧ ∀𝑦𝑏𝑧𝑏𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑒)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))} = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))})
68 df-func 17123 . . . . 5 Func = (𝑑 ∈ Cat, 𝑒 ∈ Cat ↦ {⟨𝑓, 𝑔⟩ ∣ [(Base‘𝑑) / 𝑏](𝑓:𝑏⟶(Base‘𝑒) ∧ 𝑔X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st𝑧))(Hom ‘𝑒)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) ∧ ∀𝑥𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓𝑥)) ∧ ∀𝑦𝑏𝑧𝑏𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑒)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))})
69 ovex 7172 . . . . . . 7 (𝐶m 𝐵) ∈ V
70 snex 5300 . . . . . . . 8 {𝑓} ∈ V
71 ovex 7172 . . . . . . . . . 10 (((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)) ∈ V
7271rgenw 3121 . . . . . . . . 9 𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)) ∈ V
73 ixpexg 8473 . . . . . . . . 9 (∀𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)) ∈ V → X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)) ∈ V)
7472, 73ax-mp 5 . . . . . . . 8 X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)) ∈ V
7570, 74xpex 7460 . . . . . . 7 ({𝑓} × X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∈ V
7669, 75iunex 7655 . . . . . 6 𝑓 ∈ (𝐶m 𝐵)({𝑓} × X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∈ V
77 simpl 486 . . . . . . . . . 10 (((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))) → (𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))))
7877anim2i 619 . . . . . . . . 9 ((𝑑 = ⟨𝑓, 𝑔⟩ ∧ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))) → (𝑑 = ⟨𝑓, 𝑔⟩ ∧ (𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)))))
79782eximi 1837 . . . . . . . 8 (∃𝑓𝑔(𝑑 = ⟨𝑓, 𝑔⟩ ∧ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))) → ∃𝑓𝑔(𝑑 = ⟨𝑓, 𝑔⟩ ∧ (𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)))))
80 elopab 5382 . . . . . . . 8 (𝑑 ∈ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))} ↔ ∃𝑓𝑔(𝑑 = ⟨𝑓, 𝑔⟩ ∧ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))))
81 eliunxp 5676 . . . . . . . 8 (𝑑 𝑓 ∈ (𝐶m 𝐵)({𝑓} × X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ↔ ∃𝑓𝑔(𝑑 = ⟨𝑓, 𝑔⟩ ∧ (𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)))))
8279, 80, 813imtr4i 295 . . . . . . 7 (𝑑 ∈ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))} → 𝑑 𝑓 ∈ (𝐶m 𝐵)({𝑓} × X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))))
8382ssriv 3922 . . . . . 6 {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))} ⊆ 𝑓 ∈ (𝐶m 𝐵)({𝑓} × X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)))
8476, 83ssexi 5193 . . . . 5 {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))} ∈ V
8567, 68, 84ovmpoa 7288 . . . 4 ((𝐷 ∈ Cat ∧ 𝐸 ∈ Cat) → (𝐷 Func 𝐸) = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))})
861, 2, 85syl2anc 587 . . 3 (𝜑 → (𝐷 Func 𝐸) = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))})
8786breqd 5044 . 2 (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺𝐹{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))}𝐺))
88 brabv 5421 . . . 4 (𝐹{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))}𝐺 → (𝐹 ∈ V ∧ 𝐺 ∈ V))
89 elex 3462 . . . . . 6 (𝐹 ∈ (𝐶m 𝐵) → 𝐹 ∈ V)
90 elex 3462 . . . . . 6 (𝐺X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))𝐽(𝐹‘(2nd𝑧))) ↑m (𝐻𝑧)) → 𝐺 ∈ V)
9189, 90anim12i 615 . . . . 5 ((𝐹 ∈ (𝐶m 𝐵) ∧ 𝐺X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))𝐽(𝐹‘(2nd𝑧))) ↑m (𝐻𝑧))) → (𝐹 ∈ V ∧ 𝐺 ∈ V))
92913adant3 1129 . . . 4 ((𝐹 ∈ (𝐶m 𝐵) ∧ 𝐺X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))𝐽(𝐹‘(2nd𝑧))) ↑m (𝐻𝑧)) ∧ ∀𝑥𝐵 (((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚)))) → (𝐹 ∈ V ∧ 𝐺 ∈ V))
93 simpl 486 . . . . . . . 8 ((𝑓 = 𝐹𝑔 = 𝐺) → 𝑓 = 𝐹)
9493eleq1d 2877 . . . . . . 7 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑓 ∈ (𝐶m 𝐵) ↔ 𝐹 ∈ (𝐶m 𝐵)))
95 simpr 488 . . . . . . . 8 ((𝑓 = 𝐹𝑔 = 𝐺) → 𝑔 = 𝐺)
9693fveq1d 6651 . . . . . . . . . . 11 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑓‘(1st𝑧)) = (𝐹‘(1st𝑧)))
9793fveq1d 6651 . . . . . . . . . . 11 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑓‘(2nd𝑧)) = (𝐹‘(2nd𝑧)))
9896, 97oveq12d 7157 . . . . . . . . . 10 ((𝑓 = 𝐹𝑔 = 𝐺) → ((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) = ((𝐹‘(1st𝑧))𝐽(𝐹‘(2nd𝑧))))
9998oveq1d 7154 . . . . . . . . 9 ((𝑓 = 𝐹𝑔 = 𝐺) → (((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)) = (((𝐹‘(1st𝑧))𝐽(𝐹‘(2nd𝑧))) ↑m (𝐻𝑧)))
10099ixpeq2dv 8464 . . . . . . . 8 ((𝑓 = 𝐹𝑔 = 𝐺) → X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)) = X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))𝐽(𝐹‘(2nd𝑧))) ↑m (𝐻𝑧)))
10195, 100eleq12d 2887 . . . . . . 7 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)) ↔ 𝐺X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))𝐽(𝐹‘(2nd𝑧))) ↑m (𝐻𝑧))))
10295oveqd 7156 . . . . . . . . . . 11 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑥𝑔𝑥) = (𝑥𝐺𝑥))
103102fveq1d 6651 . . . . . . . . . 10 ((𝑓 = 𝐹𝑔 = 𝐺) → ((𝑥𝑔𝑥)‘( 1𝑥)) = ((𝑥𝐺𝑥)‘( 1𝑥)))
10493fveq1d 6651 . . . . . . . . . . 11 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑓𝑥) = (𝐹𝑥))
105104fveq2d 6653 . . . . . . . . . 10 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝐼‘(𝑓𝑥)) = (𝐼‘(𝐹𝑥)))
106103, 105eqeq12d 2817 . . . . . . . . 9 ((𝑓 = 𝐹𝑔 = 𝐺) → (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ↔ ((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥))))
10795oveqd 7156 . . . . . . . . . . . . 13 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑥𝑔𝑧) = (𝑥𝐺𝑧))
108107fveq1d 6651 . . . . . . . . . . . 12 ((𝑓 = 𝐹𝑔 = 𝐺) → ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = ((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)))
10993fveq1d 6651 . . . . . . . . . . . . . . 15 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑓𝑦) = (𝐹𝑦))
110104, 109opeq12d 4776 . . . . . . . . . . . . . 14 ((𝑓 = 𝐹𝑔 = 𝐺) → ⟨(𝑓𝑥), (𝑓𝑦)⟩ = ⟨(𝐹𝑥), (𝐹𝑦)⟩)
11193fveq1d 6651 . . . . . . . . . . . . . 14 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑓𝑧) = (𝐹𝑧))
112110, 111oveq12d 7157 . . . . . . . . . . . . 13 ((𝑓 = 𝐹𝑔 = 𝐺) → (⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧)) = (⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧)))
11395oveqd 7156 . . . . . . . . . . . . . 14 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑦𝑔𝑧) = (𝑦𝐺𝑧))
114113fveq1d 6651 . . . . . . . . . . . . 13 ((𝑓 = 𝐹𝑔 = 𝐺) → ((𝑦𝑔𝑧)‘𝑛) = ((𝑦𝐺𝑧)‘𝑛))
11595oveqd 7156 . . . . . . . . . . . . . 14 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑥𝑔𝑦) = (𝑥𝐺𝑦))
116115fveq1d 6651 . . . . . . . . . . . . 13 ((𝑓 = 𝐹𝑔 = 𝐺) → ((𝑥𝑔𝑦)‘𝑚) = ((𝑥𝐺𝑦)‘𝑚))
117112, 114, 116oveq123d 7160 . . . . . . . . . . . 12 ((𝑓 = 𝐹𝑔 = 𝐺) → (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚)))
118108, 117eqeq12d 2817 . . . . . . . . . . 11 ((𝑓 = 𝐹𝑔 = 𝐺) → (((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚))))
1191182ralbidv 3167 . . . . . . . . . 10 ((𝑓 = 𝐹𝑔 = 𝐺) → (∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚))))
1201192ralbidv 3167 . . . . . . . . 9 ((𝑓 = 𝐹𝑔 = 𝐺) → (∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚))))
121106, 120anbi12d 633 . . . . . . . 8 ((𝑓 = 𝐹𝑔 = 𝐺) → ((((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ (((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚)))))
122121ralbidv 3165 . . . . . . 7 ((𝑓 = 𝐹𝑔 = 𝐺) → (∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ ∀𝑥𝐵 (((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚)))))
12394, 101, 1223anbi123d 1433 . . . . . 6 ((𝑓 = 𝐹𝑔 = 𝐺) → ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ (𝐹 ∈ (𝐶m 𝐵) ∧ 𝐺X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))𝐽(𝐹‘(2nd𝑧))) ↑m (𝐻𝑧)) ∧ ∀𝑥𝐵 (((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚))))))
12464, 123bitr3id 288 . . . . 5 ((𝑓 = 𝐹𝑔 = 𝐺) → (((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ (𝐹 ∈ (𝐶m 𝐵) ∧ 𝐺X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))𝐽(𝐹‘(2nd𝑧))) ↑m (𝐻𝑧)) ∧ ∀𝑥𝐵 (((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚))))))
125 eqid 2801 . . . . 5 {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))} = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))}
126124, 125brabga 5389 . . . 4 ((𝐹 ∈ V ∧ 𝐺 ∈ V) → (𝐹{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))}𝐺 ↔ (𝐹 ∈ (𝐶m 𝐵) ∧ 𝐺X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))𝐽(𝐹‘(2nd𝑧))) ↑m (𝐻𝑧)) ∧ ∀𝑥𝐵 (((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚))))))
12788, 92, 126pm5.21nii 383 . . 3 (𝐹{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))}𝐺 ↔ (𝐹 ∈ (𝐶m 𝐵) ∧ 𝐺X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))𝐽(𝐹‘(2nd𝑧))) ↑m (𝐻𝑧)) ∧ ∀𝑥𝐵 (((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚)))))
12814, 15elmap 8422 . . . 4 (𝐹 ∈ (𝐶m 𝐵) ↔ 𝐹:𝐵𝐶)
1291283anbi1i 1154 . . 3 ((𝐹 ∈ (𝐶m 𝐵) ∧ 𝐺X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))𝐽(𝐹‘(2nd𝑧))) ↑m (𝐻𝑧)) ∧ ∀𝑥𝐵 (((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚)))) ↔ (𝐹:𝐵𝐶𝐺X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))𝐽(𝐹‘(2nd𝑧))) ↑m (𝐻𝑧)) ∧ ∀𝑥𝐵 (((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚)))))
130127, 129bitri 278 . 2 (𝐹{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))}𝐺 ↔ (𝐹:𝐵𝐶𝐺X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))𝐽(𝐹‘(2nd𝑧))) ↑m (𝐻𝑧)) ∧ ∀𝑥𝐵 (((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚)))))
13187, 130syl6bb 290 1 (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ (𝐹:𝐵𝐶𝐺X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))𝐽(𝐹‘(2nd𝑧))) ↑m (𝐻𝑧)) ∧ ∀𝑥𝐵 (((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wex 1781  wcel 2112  wral 3109  Vcvv 3444  [wsbc 3723  {csn 4528  cop 4534   ciun 4884   class class class wbr 5033  {copab 5095   × cxp 5521  wf 6324  cfv 6328  (class class class)co 7139  1st c1st 7673  2nd c2nd 7674  m cmap 8393  Xcixp 8448  Basecbs 16478  Hom chom 16571  compcco 16572  Catccat 16930  Idccid 16931   Func cfunc 17119
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7142  df-oprab 7143  df-mpo 7144  df-map 8395  df-ixp 8449  df-func 17123
This theorem is referenced by:  isfuncd  17130  funcf1  17131  funcixp  17132  funcid  17135  funcco  17136  idfucl  17146  cofucl  17153  funcres2b  17162  funcpropd  17165
  Copyright terms: Public domain W3C validator