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

Theorem isfunc 17750
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 6857 . . . . . . 7 ((𝑑 = 𝐷𝑒 = 𝐸) → (Base‘𝑑) ∈ V)
4 simpl 483 . . . . . . . . 9 ((𝑑 = 𝐷𝑒 = 𝐸) → 𝑑 = 𝐷)
54fveq2d 6846 . . . . . . . 8 ((𝑑 = 𝐷𝑒 = 𝐸) → (Base‘𝑑) = (Base‘𝐷))
6 isfunc.b . . . . . . . 8 𝐵 = (Base‘𝐷)
75, 6eqtr4di 2794 . . . . . . 7 ((𝑑 = 𝐷𝑒 = 𝐸) → (Base‘𝑑) = 𝐵)
8 simpr 485 . . . . . . . . . . 11 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵)
9 simplr 767 . . . . . . . . . . . . 13 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → 𝑒 = 𝐸)
109fveq2d 6846 . . . . . . . . . . . 12 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Base‘𝑒) = (Base‘𝐸))
11 isfunc.c . . . . . . . . . . . 12 𝐶 = (Base‘𝐸)
1210, 11eqtr4di 2794 . . . . . . . . . . 11 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Base‘𝑒) = 𝐶)
138, 12feq23d 6663 . . . . . . . . . 10 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑓:𝑏⟶(Base‘𝑒) ↔ 𝑓:𝐵𝐶))
1411fvexi 6856 . . . . . . . . . . 11 𝐶 ∈ V
156fvexi 6856 . . . . . . . . . . 11 𝐵 ∈ V
1614, 15elmap 8809 . . . . . . . . . 10 (𝑓 ∈ (𝐶m 𝐵) ↔ 𝑓:𝐵𝐶)
1713, 16bitr4di 288 . . . . . . . . 9 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑓:𝑏⟶(Base‘𝑒) ↔ 𝑓 ∈ (𝐶m 𝐵)))
188sqxpeqd 5665 . . . . . . . . . . . 12 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑏 × 𝑏) = (𝐵 × 𝐵))
1918ixpeq1d 8847 . . . . . . . . . . 11 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st𝑧))(Hom ‘𝑒)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) = X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))(Hom ‘𝑒)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)))
209fveq2d 6846 . . . . . . . . . . . . . . 15 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Hom ‘𝑒) = (Hom ‘𝐸))
21 isfunc.j . . . . . . . . . . . . . . 15 𝐽 = (Hom ‘𝐸)
2220, 21eqtr4di 2794 . . . . . . . . . . . . . 14 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Hom ‘𝑒) = 𝐽)
2322oveqd 7374 . . . . . . . . . . . . 13 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((𝑓‘(1st𝑧))(Hom ‘𝑒)(𝑓‘(2nd𝑧))) = ((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))))
24 simpll 765 . . . . . . . . . . . . . . . 16 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → 𝑑 = 𝐷)
2524fveq2d 6846 . . . . . . . . . . . . . . 15 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Hom ‘𝑑) = (Hom ‘𝐷))
26 isfunc.h . . . . . . . . . . . . . . 15 𝐻 = (Hom ‘𝐷)
2725, 26eqtr4di 2794 . . . . . . . . . . . . . 14 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Hom ‘𝑑) = 𝐻)
2827fveq1d 6844 . . . . . . . . . . . . 13 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((Hom ‘𝑑)‘𝑧) = (𝐻𝑧))
2923, 28oveq12d 7375 . . . . . . . . . . . 12 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (((𝑓‘(1st𝑧))(Hom ‘𝑒)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) = (((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)))
3029ixpeq2dv 8851 . . . . . . . . . . 11 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))(Hom ‘𝑒)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) = X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)))
3119, 30eqtrd 2776 . . . . . . . . . 10 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st𝑧))(Hom ‘𝑒)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) = X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)))
3231eleq2d 2823 . . . . . . . . 9 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑔X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st𝑧))(Hom ‘𝑒)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) ↔ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))))
3324fveq2d 6846 . . . . . . . . . . . . . . 15 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Id‘𝑑) = (Id‘𝐷))
34 isfunc.1 . . . . . . . . . . . . . . 15 1 = (Id‘𝐷)
3533, 34eqtr4di 2794 . . . . . . . . . . . . . 14 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Id‘𝑑) = 1 )
3635fveq1d 6844 . . . . . . . . . . . . 13 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((Id‘𝑑)‘𝑥) = ( 1𝑥))
3736fveq2d 6846 . . . . . . . . . . . 12 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((𝑥𝑔𝑥)‘( 1𝑥)))
389fveq2d 6846 . . . . . . . . . . . . . 14 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Id‘𝑒) = (Id‘𝐸))
39 isfunc.i . . . . . . . . . . . . . 14 𝐼 = (Id‘𝐸)
4038, 39eqtr4di 2794 . . . . . . . . . . . . 13 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Id‘𝑒) = 𝐼)
4140fveq1d 6844 . . . . . . . . . . . 12 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((Id‘𝑒)‘(𝑓𝑥)) = (𝐼‘(𝑓𝑥)))
4237, 41eqeq12d 2752 . . . . . . . . . . 11 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓𝑥)) ↔ ((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥))))
4327oveqd 7374 . . . . . . . . . . . . . 14 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑥(Hom ‘𝑑)𝑦) = (𝑥𝐻𝑦))
4427oveqd 7374 . . . . . . . . . . . . . . 15 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑦(Hom ‘𝑑)𝑧) = (𝑦𝐻𝑧))
4524fveq2d 6846 . . . . . . . . . . . . . . . . . . . 20 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (comp‘𝑑) = (comp‘𝐷))
46 isfunc.x . . . . . . . . . . . . . . . . . . . 20 · = (comp‘𝐷)
4745, 46eqtr4di 2794 . . . . . . . . . . . . . . . . . . 19 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (comp‘𝑑) = · )
4847oveqd 7374 . . . . . . . . . . . . . . . . . 18 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧) = (⟨𝑥, 𝑦· 𝑧))
4948oveqd 7374 . . . . . . . . . . . . . . . . 17 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚) = (𝑛(⟨𝑥, 𝑦· 𝑧)𝑚))
5049fveq2d 6846 . . . . . . . . . . . . . . . 16 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)))
519fveq2d 6846 . . . . . . . . . . . . . . . . . . 19 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (comp‘𝑒) = (comp‘𝐸))
52 isfunc.o . . . . . . . . . . . . . . . . . . 19 𝑂 = (comp‘𝐸)
5351, 52eqtr4di 2794 . . . . . . . . . . . . . . . . . 18 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (comp‘𝑒) = 𝑂)
5453oveqd 7374 . . . . . . . . . . . . . . . . 17 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑒)(𝑓𝑧)) = (⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧)))
5554oveqd 7374 . . . . . . . . . . . . . . . 16 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑒)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))
5650, 55eqeq12d 2752 . . . . . . . . . . . . . . 15 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑒)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))
5744, 56raleqbidv 3319 . . . . . . . . . . . . . 14 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑒)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))
5843, 57raleqbidv 3319 . . . . . . . . . . . . 13 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑒)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))
598, 58raleqbidv 3319 . . . . . . . . . . . 12 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (∀𝑧𝑏𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑒)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))
608, 59raleqbidv 3319 . . . . . . . . . . 11 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (∀𝑦𝑏𝑧𝑏𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑒)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))
6142, 60anbi12d 631 . . . . . . . . . 10 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓𝑥)) ∧ ∀𝑦𝑏𝑧𝑏𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑒)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))))
628, 61raleqbidv 3319 . . . . . . . . 9 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (∀𝑥𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓𝑥)) ∧ ∀𝑦𝑏𝑧𝑏𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑒)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))))
6317, 32, 623anbi123d 1436 . . . . . . . 8 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((𝑓:𝑏⟶(Base‘𝑒) ∧ 𝑔X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st𝑧))(Hom ‘𝑒)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) ∧ ∀𝑥𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓𝑥)) ∧ ∀𝑦𝑏𝑧𝑏𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑒)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ (𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))))
64 df-3an 1089 . . . . . . . 8 ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))))
6563, 64bitrdi 286 . . . . . . 7 (((𝑑 = 𝐷𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((𝑓:𝑏⟶(Base‘𝑒) ∧ 𝑔X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st𝑧))(Hom ‘𝑒)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) ∧ ∀𝑥𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓𝑥)) ∧ ∀𝑦𝑏𝑧𝑏𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑒)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))))
663, 7, 65sbcied2 3786 . . . . . 6 ((𝑑 = 𝐷𝑒 = 𝐸) → ([(Base‘𝑑) / 𝑏](𝑓:𝑏⟶(Base‘𝑒) ∧ 𝑔X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st𝑧))(Hom ‘𝑒)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) ∧ ∀𝑥𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓𝑥)) ∧ ∀𝑦𝑏𝑧𝑏𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑒)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))))
6766opabbidv 5171 . . . . 5 ((𝑑 = 𝐷𝑒 = 𝐸) → {⟨𝑓, 𝑔⟩ ∣ [(Base‘𝑑) / 𝑏](𝑓:𝑏⟶(Base‘𝑒) ∧ 𝑔X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st𝑧))(Hom ‘𝑒)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) ∧ ∀𝑥𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓𝑥)) ∧ ∀𝑦𝑏𝑧𝑏𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑒)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))} = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))})
68 df-func 17744 . . . . 5 Func = (𝑑 ∈ Cat, 𝑒 ∈ Cat ↦ {⟨𝑓, 𝑔⟩ ∣ [(Base‘𝑑) / 𝑏](𝑓:𝑏⟶(Base‘𝑒) ∧ 𝑔X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st𝑧))(Hom ‘𝑒)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) ∧ ∀𝑥𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓𝑥)) ∧ ∀𝑦𝑏𝑧𝑏𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑒)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))})
69 ovex 7390 . . . . . . 7 (𝐶m 𝐵) ∈ V
70 vsnex 5386 . . . . . . . 8 {𝑓} ∈ V
71 ovex 7390 . . . . . . . . . 10 (((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)) ∈ V
7271rgenw 3068 . . . . . . . . 9 𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)) ∈ V
73 ixpexg 8860 . . . . . . . . 9 (∀𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)) ∈ V → X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)) ∈ V)
7472, 73ax-mp 5 . . . . . . . 8 X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)) ∈ V
7570, 74xpex 7687 . . . . . . 7 ({𝑓} × X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∈ V
7669, 75iunex 7901 . . . . . 6 𝑓 ∈ (𝐶m 𝐵)({𝑓} × X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∈ V
77 simpl 483 . . . . . . . . . 10 (((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))) → (𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))))
7877anim2i 617 . . . . . . . . 9 ((𝑑 = ⟨𝑓, 𝑔⟩ ∧ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))) → (𝑑 = ⟨𝑓, 𝑔⟩ ∧ (𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)))))
79782eximi 1838 . . . . . . . 8 (∃𝑓𝑔(𝑑 = ⟨𝑓, 𝑔⟩ ∧ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))) → ∃𝑓𝑔(𝑑 = ⟨𝑓, 𝑔⟩ ∧ (𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)))))
80 elopab 5484 . . . . . . . 8 (𝑑 ∈ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))} ↔ ∃𝑓𝑔(𝑑 = ⟨𝑓, 𝑔⟩ ∧ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))))
81 eliunxp 5793 . . . . . . . 8 (𝑑 𝑓 ∈ (𝐶m 𝐵)({𝑓} × X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ↔ ∃𝑓𝑔(𝑑 = ⟨𝑓, 𝑔⟩ ∧ (𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)))))
8279, 80, 813imtr4i 291 . . . . . . 7 (𝑑 ∈ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))} → 𝑑 𝑓 ∈ (𝐶m 𝐵)({𝑓} × X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))))
8382ssriv 3948 . . . . . 6 {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))} ⊆ 𝑓 ∈ (𝐶m 𝐵)({𝑓} × X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)))
8476, 83ssexi 5279 . . . . 5 {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))} ∈ V
8567, 68, 84ovmpoa 7510 . . . 4 ((𝐷 ∈ Cat ∧ 𝐸 ∈ Cat) → (𝐷 Func 𝐸) = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))})
861, 2, 85syl2anc 584 . . 3 (𝜑 → (𝐷 Func 𝐸) = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))})
8786breqd 5116 . 2 (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺𝐹{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))}𝐺))
88 brabv 5526 . . . 4 (𝐹{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))}𝐺 → (𝐹 ∈ V ∧ 𝐺 ∈ V))
89 elex 3463 . . . . . 6 (𝐹 ∈ (𝐶m 𝐵) → 𝐹 ∈ V)
90 elex 3463 . . . . . 6 (𝐺X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))𝐽(𝐹‘(2nd𝑧))) ↑m (𝐻𝑧)) → 𝐺 ∈ V)
9189, 90anim12i 613 . . . . 5 ((𝐹 ∈ (𝐶m 𝐵) ∧ 𝐺X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))𝐽(𝐹‘(2nd𝑧))) ↑m (𝐻𝑧))) → (𝐹 ∈ V ∧ 𝐺 ∈ V))
92913adant3 1132 . . . 4 ((𝐹 ∈ (𝐶m 𝐵) ∧ 𝐺X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))𝐽(𝐹‘(2nd𝑧))) ↑m (𝐻𝑧)) ∧ ∀𝑥𝐵 (((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚)))) → (𝐹 ∈ V ∧ 𝐺 ∈ V))
93 simpl 483 . . . . . . . 8 ((𝑓 = 𝐹𝑔 = 𝐺) → 𝑓 = 𝐹)
9493eleq1d 2822 . . . . . . 7 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑓 ∈ (𝐶m 𝐵) ↔ 𝐹 ∈ (𝐶m 𝐵)))
95 simpr 485 . . . . . . . 8 ((𝑓 = 𝐹𝑔 = 𝐺) → 𝑔 = 𝐺)
9693fveq1d 6844 . . . . . . . . . . 11 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑓‘(1st𝑧)) = (𝐹‘(1st𝑧)))
9793fveq1d 6844 . . . . . . . . . . 11 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑓‘(2nd𝑧)) = (𝐹‘(2nd𝑧)))
9896, 97oveq12d 7375 . . . . . . . . . 10 ((𝑓 = 𝐹𝑔 = 𝐺) → ((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) = ((𝐹‘(1st𝑧))𝐽(𝐹‘(2nd𝑧))))
9998oveq1d 7372 . . . . . . . . 9 ((𝑓 = 𝐹𝑔 = 𝐺) → (((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)) = (((𝐹‘(1st𝑧))𝐽(𝐹‘(2nd𝑧))) ↑m (𝐻𝑧)))
10099ixpeq2dv 8851 . . . . . . . 8 ((𝑓 = 𝐹𝑔 = 𝐺) → X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)) = X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))𝐽(𝐹‘(2nd𝑧))) ↑m (𝐻𝑧)))
10195, 100eleq12d 2832 . . . . . . 7 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)) ↔ 𝐺X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))𝐽(𝐹‘(2nd𝑧))) ↑m (𝐻𝑧))))
10295oveqd 7374 . . . . . . . . . . 11 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑥𝑔𝑥) = (𝑥𝐺𝑥))
103102fveq1d 6844 . . . . . . . . . 10 ((𝑓 = 𝐹𝑔 = 𝐺) → ((𝑥𝑔𝑥)‘( 1𝑥)) = ((𝑥𝐺𝑥)‘( 1𝑥)))
10493fveq1d 6844 . . . . . . . . . . 11 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑓𝑥) = (𝐹𝑥))
105104fveq2d 6846 . . . . . . . . . 10 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝐼‘(𝑓𝑥)) = (𝐼‘(𝐹𝑥)))
106103, 105eqeq12d 2752 . . . . . . . . 9 ((𝑓 = 𝐹𝑔 = 𝐺) → (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ↔ ((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥))))
10795oveqd 7374 . . . . . . . . . . . . 13 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑥𝑔𝑧) = (𝑥𝐺𝑧))
108107fveq1d 6844 . . . . . . . . . . . 12 ((𝑓 = 𝐹𝑔 = 𝐺) → ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = ((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)))
10993fveq1d 6844 . . . . . . . . . . . . . . 15 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑓𝑦) = (𝐹𝑦))
110104, 109opeq12d 4838 . . . . . . . . . . . . . 14 ((𝑓 = 𝐹𝑔 = 𝐺) → ⟨(𝑓𝑥), (𝑓𝑦)⟩ = ⟨(𝐹𝑥), (𝐹𝑦)⟩)
11193fveq1d 6844 . . . . . . . . . . . . . 14 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑓𝑧) = (𝐹𝑧))
112110, 111oveq12d 7375 . . . . . . . . . . . . 13 ((𝑓 = 𝐹𝑔 = 𝐺) → (⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧)) = (⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧)))
11395oveqd 7374 . . . . . . . . . . . . . 14 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑦𝑔𝑧) = (𝑦𝐺𝑧))
114113fveq1d 6844 . . . . . . . . . . . . 13 ((𝑓 = 𝐹𝑔 = 𝐺) → ((𝑦𝑔𝑧)‘𝑛) = ((𝑦𝐺𝑧)‘𝑛))
11595oveqd 7374 . . . . . . . . . . . . . 14 ((𝑓 = 𝐹𝑔 = 𝐺) → (𝑥𝑔𝑦) = (𝑥𝐺𝑦))
116115fveq1d 6844 . . . . . . . . . . . . 13 ((𝑓 = 𝐹𝑔 = 𝐺) → ((𝑥𝑔𝑦)‘𝑚) = ((𝑥𝐺𝑦)‘𝑚))
117112, 114, 116oveq123d 7378 . . . . . . . . . . . 12 ((𝑓 = 𝐹𝑔 = 𝐺) → (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚)))
118108, 117eqeq12d 2752 . . . . . . . . . . 11 ((𝑓 = 𝐹𝑔 = 𝐺) → (((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚))))
1191182ralbidv 3212 . . . . . . . . . 10 ((𝑓 = 𝐹𝑔 = 𝐺) → (∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚))))
1201192ralbidv 3212 . . . . . . . . 9 ((𝑓 = 𝐹𝑔 = 𝐺) → (∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚))))
121106, 120anbi12d 631 . . . . . . . 8 ((𝑓 = 𝐹𝑔 = 𝐺) → ((((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ (((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚)))))
122121ralbidv 3174 . . . . . . 7 ((𝑓 = 𝐹𝑔 = 𝐺) → (∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ ∀𝑥𝐵 (((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚)))))
12394, 101, 1223anbi123d 1436 . . . . . 6 ((𝑓 = 𝐹𝑔 = 𝐺) → ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧)) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ (𝐹 ∈ (𝐶m 𝐵) ∧ 𝐺X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))𝐽(𝐹‘(2nd𝑧))) ↑m (𝐻𝑧)) ∧ ∀𝑥𝐵 (((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚))))))
12464, 123bitr3id 284 . . . . 5 ((𝑓 = 𝐹𝑔 = 𝐺) → (((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ (𝐹 ∈ (𝐶m 𝐵) ∧ 𝐺X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))𝐽(𝐹‘(2nd𝑧))) ↑m (𝐻𝑧)) ∧ ∀𝑥𝐵 (((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚))))))
125 eqid 2736 . . . . 5 {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))} = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))}
126124, 125brabga 5491 . . . 4 ((𝐹 ∈ V ∧ 𝐺 ∈ V) → (𝐹{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))}𝐺 ↔ (𝐹 ∈ (𝐶m 𝐵) ∧ 𝐺X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))𝐽(𝐹‘(2nd𝑧))) ↑m (𝐻𝑧)) ∧ ∀𝑥𝐵 (((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚))))))
12788, 92, 126pm5.21nii 379 . . 3 (𝐹{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))}𝐺 ↔ (𝐹 ∈ (𝐶m 𝐵) ∧ 𝐺X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))𝐽(𝐹‘(2nd𝑧))) ↑m (𝐻𝑧)) ∧ ∀𝑥𝐵 (((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚)))))
12814, 15elmap 8809 . . . 4 (𝐹 ∈ (𝐶m 𝐵) ↔ 𝐹:𝐵𝐶)
1291283anbi1i 1157 . . 3 ((𝐹 ∈ (𝐶m 𝐵) ∧ 𝐺X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))𝐽(𝐹‘(2nd𝑧))) ↑m (𝐻𝑧)) ∧ ∀𝑥𝐵 (((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚)))) ↔ (𝐹:𝐵𝐶𝐺X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))𝐽(𝐹‘(2nd𝑧))) ↑m (𝐻𝑧)) ∧ ∀𝑥𝐵 (((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚)))))
130127, 129bitri 274 . 2 (𝐹{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶m 𝐵) ∧ 𝑔X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st𝑧))𝐽(𝑓‘(2nd𝑧))) ↑m (𝐻𝑧))) ∧ ∀𝑥𝐵 (((𝑥𝑔𝑥)‘( 1𝑥)) = (𝐼‘(𝑓𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩𝑂(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))}𝐺 ↔ (𝐹:𝐵𝐶𝐺X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))𝐽(𝐹‘(2nd𝑧))) ↑m (𝐻𝑧)) ∧ ∀𝑥𝐵 (((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚)))))
13187, 130bitrdi 286 1 (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ (𝐹:𝐵𝐶𝐺X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st𝑧))𝐽(𝐹‘(2nd𝑧))) ↑m (𝐻𝑧)) ∧ ∀𝑥𝐵 (((𝑥𝐺𝑥)‘( 1𝑥)) = (𝐼‘(𝐹𝑥)) ∧ ∀𝑦𝐵𝑧𝐵𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦· 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹𝑥), (𝐹𝑦)⟩𝑂(𝐹𝑧))((𝑥𝐺𝑦)‘𝑚))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wex 1781  wcel 2106  wral 3064  Vcvv 3445  [wsbc 3739  {csn 4586  cop 4592   ciun 4954   class class class wbr 5105  {copab 5167   × cxp 5631  wf 6492  cfv 6496  (class class class)co 7357  1st c1st 7919  2nd c2nd 7920  m cmap 8765  Xcixp 8835  Basecbs 17083  Hom chom 17144  compcco 17145  Catccat 17544  Idccid 17545   Func cfunc 17740
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-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-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-map 8767  df-ixp 8836  df-func 17744
This theorem is referenced by:  isfuncd  17751  funcf1  17752  funcixp  17753  funcid  17756  funcco  17757  idfucl  17767  cofucl  17774  funcres2b  17783  funcpropd  17787  functhinc  47055
  Copyright terms: Public domain W3C validator