Theorem isfunc 17821

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.

Step	Hyp	Ref	Expression
1		isfunc.d	. . . 4 ⊢ (𝜑 → 𝐷 ∈ Cat)
2		isfunc.e	. . . 4 ⊢ (𝜑 → 𝐸 ∈ Cat)
3		fvexd 6906	. . . . . . 7 ⊢ ((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) → (Base‘𝑑) ∈ V)
4		simpl 482	. . . . . . . . 9 ⊢ ((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) → 𝑑 = 𝐷)
5	4	fveq2d 6895	. . . . . . . 8 ⊢ ((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) → (Base‘𝑑) = (Base‘𝐷))
6		isfunc.b	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝐷)
7	5, 6	eqtr4di 2789	. . . . . . 7 ⊢ ((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) → (Base‘𝑑) = 𝐵)
8		simpr 484	. . . . . . . . . . 11 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵)
9		simplr 766	. . . . . . . . . . . . 13 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → 𝑒 = 𝐸)
10	9	fveq2d 6895	. . . . . . . . . . . 12 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Base‘𝑒) = (Base‘𝐸))
11		isfunc.c	. . . . . . . . . . . 12 ⊢ 𝐶 = (Base‘𝐸)
12	10, 11	eqtr4di 2789	. . . . . . . . . . 11 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Base‘𝑒) = 𝐶)
13	8, 12	feq23d 6712	. . . . . . . . . 10 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑓:𝑏⟶(Base‘𝑒) ↔ 𝑓:𝐵⟶𝐶))
14	11	fvexi 6905	. . . . . . . . . . 11 ⊢ 𝐶 ∈ V
15	6	fvexi 6905	. . . . . . . . . . 11 ⊢ 𝐵 ∈ V
16	14, 15	elmap 8871	. . . . . . . . . 10 ⊢ (𝑓 ∈ (𝐶 ↑m 𝐵) ↔ 𝑓:𝐵⟶𝐶)
17	13, 16	bitr4di 289	. . . . . . . . 9 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑓:𝑏⟶(Base‘𝑒) ↔ 𝑓 ∈ (𝐶 ↑m 𝐵)))
18	8	sqxpeqd 5708	. . . . . . . . . . . 12 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑏 × 𝑏) = (𝐵 × 𝐵))
19	18	ixpeq1d 8909	. . . . . . . . . . 11 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) = X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)))
20	9	fveq2d 6895	. . . . . . . . . . . . . . 15 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Hom ‘𝑒) = (Hom ‘𝐸))
21		isfunc.j	. . . . . . . . . . . . . . 15 ⊢ 𝐽 = (Hom ‘𝐸)
22	20, 21	eqtr4di 2789	. . . . . . . . . . . . . 14 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Hom ‘𝑒) = 𝐽)
23	22	oveqd 7429	. . . . . . . . . . . . 13 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) = ((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))))
24		simpll 764	. . . . . . . . . . . . . . . 16 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → 𝑑 = 𝐷)
25	24	fveq2d 6895	. . . . . . . . . . . . . . 15 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Hom ‘𝑑) = (Hom ‘𝐷))
26		isfunc.h	. . . . . . . . . . . . . . 15 ⊢ 𝐻 = (Hom ‘𝐷)
27	25, 26	eqtr4di 2789	. . . . . . . . . . . . . 14 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Hom ‘𝑑) = 𝐻)
28	27	fveq1d 6893	. . . . . . . . . . . . 13 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((Hom ‘𝑑)‘𝑧) = (𝐻‘𝑧))
29	23, 28	oveq12d 7430	. . . . . . . . . . . 12 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) = (((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))
30	29	ixpeq2dv 8913	. . . . . . . . . . 11 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) = X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))
31	19, 30	eqtrd 2771	. . . . . . . . . 10 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) = X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))
32	31	eleq2d 2818	. . . . . . . . 9 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) ↔ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))))
33	24	fveq2d 6895	. . . . . . . . . . . . . . 15 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Id‘𝑑) = (Id‘𝐷))
34		isfunc.1	. . . . . . . . . . . . . . 15 ⊢ 1 = (Id‘𝐷)
35	33, 34	eqtr4di 2789	. . . . . . . . . . . . . 14 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Id‘𝑑) = 1 )
36	35	fveq1d 6893	. . . . . . . . . . . . 13 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((Id‘𝑑)‘𝑥) = ( 1 ‘𝑥))
37	36	fveq2d 6895	. . . . . . . . . . . 12 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((𝑥𝑔𝑥)‘( 1 ‘𝑥)))
38	9	fveq2d 6895	. . . . . . . . . . . . . 14 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Id‘𝑒) = (Id‘𝐸))
39		isfunc.i	. . . . . . . . . . . . . 14 ⊢ 𝐼 = (Id‘𝐸)
40	38, 39	eqtr4di 2789	. . . . . . . . . . . . 13 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Id‘𝑒) = 𝐼)
41	40	fveq1d 6893	. . . . . . . . . . . 12 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((Id‘𝑒)‘(𝑓‘𝑥)) = (𝐼‘(𝑓‘𝑥)))
42	37, 41	eqeq12d 2747	. . . . . . . . . . 11 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓‘𝑥)) ↔ ((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥))))
43	27	oveqd 7429	. . . . . . . . . . . . . 14 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑥(Hom ‘𝑑)𝑦) = (𝑥𝐻𝑦))
44	27	oveqd 7429	. . . . . . . . . . . . . . 15 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑦(Hom ‘𝑑)𝑧) = (𝑦𝐻𝑧))
45	24	fveq2d 6895	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (comp‘𝑑) = (comp‘𝐷))
46		isfunc.x	. . . . . . . . . . . . . . . . . . . 20 ⊢ · = (comp‘𝐷)
47	45, 46	eqtr4di 2789	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (comp‘𝑑) = · )
48	47	oveqd 7429	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧) = (⟨𝑥, 𝑦⟩ · 𝑧))
49	48	oveqd 7429	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚) = (𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚))
50	49	fveq2d 6895	. . . . . . . . . . . . . . . 16 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)))
51	9	fveq2d 6895	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (comp‘𝑒) = (comp‘𝐸))
52		isfunc.o	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑂 = (comp‘𝐸)
53	51, 52	eqtr4di 2789	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (comp‘𝑒) = 𝑂)
54	53	oveqd 7429	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧)) = (⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧)))
55	54	oveqd 7429	. . . . . . . . . . . . . . . 16 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))
56	50, 55	eqeq12d 2747	. . . . . . . . . . . . . . 15 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
57	44, 56	raleqbidv 3341	. . . . . . . . . . . . . 14 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
58	43, 57	raleqbidv 3341	. . . . . . . . . . . . 13 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
59	8, 58	raleqbidv 3341	. . . . . . . . . . . 12 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
60	8, 59	raleqbidv 3341	. . . . . . . . . . 11 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
61	42, 60	anbi12d 630	. . . . . . . . . 10 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))
62	8, 61	raleqbidv 3341	. . . . . . . . 9 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))
63	17, 32, 62	3anbi123d 1435	. . . . . . . 8 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((𝑓:𝑏⟶(Base‘𝑒) ∧ 𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) ∧ ∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ (𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))))
64		df-3an 1088	. . . . . . . 8 ⊢ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))
65	63, 64	bitrdi 287	. . . . . . 7 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((𝑓:𝑏⟶(Base‘𝑒) ∧ 𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) ∧ ∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))))
66	3, 7, 65	sbcied2 3824	. . . . . 6 ⊢ ((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) → ([(Base‘𝑑) / 𝑏](𝑓:𝑏⟶(Base‘𝑒) ∧ 𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) ∧ ∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))))
67	66	opabbidv 5214	. . . . 5 ⊢ ((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) → {⟨𝑓, 𝑔⟩ ∣ [(Base‘𝑑) / 𝑏](𝑓:𝑏⟶(Base‘𝑒) ∧ 𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) ∧ ∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))} = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))})
68		df-func 17815	. . . . 5 ⊢ Func = (𝑑 ∈ Cat, 𝑒 ∈ Cat ↦ {⟨𝑓, 𝑔⟩ ∣ [(Base‘𝑑) / 𝑏](𝑓:𝑏⟶(Base‘𝑒) ∧ 𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) ∧ ∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))})
69		ovex 7445	. . . . . . 7 ⊢ (𝐶 ↑m 𝐵) ∈ V
70		vsnex 5429	. . . . . . . 8 ⊢ {𝑓} ∈ V
71		ovex 7445	. . . . . . . . . 10 ⊢ (((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∈ V
72	71	rgenw 3064	. . . . . . . . 9 ⊢ ∀𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∈ V
73		ixpexg 8922	. . . . . . . . 9 ⊢ (∀𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∈ V → X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∈ V)
74	72, 73	ax-mp 5	. . . . . . . 8 ⊢ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∈ V
75	70, 74	xpex 7744	. . . . . . 7 ⊢ ({𝑓} × X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∈ V
76	69, 75	iunex 7959	. . . . . 6 ⊢ ∪ 𝑓 ∈ (𝐶 ↑m 𝐵)({𝑓} × X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∈ V
77		simpl 482	. . . . . . . . . 10 ⊢ (((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) → (𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))))
78	77	anim2i 616	. . . . . . . . 9 ⊢ ((𝑑 = ⟨𝑓, 𝑔⟩ ∧ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))) → (𝑑 = ⟨𝑓, 𝑔⟩ ∧ (𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))))
79	78	2eximi 1837	. . . . . . . 8 ⊢ (∃𝑓∃𝑔(𝑑 = ⟨𝑓, 𝑔⟩ ∧ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))) → ∃𝑓∃𝑔(𝑑 = ⟨𝑓, 𝑔⟩ ∧ (𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))))
80		elopab 5527	. . . . . . . 8 ⊢ (𝑑 ∈ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))} ↔ ∃𝑓∃𝑔(𝑑 = ⟨𝑓, 𝑔⟩ ∧ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))))
81		eliunxp 5837	. . . . . . . 8 ⊢ (𝑑 ∈ ∪ 𝑓 ∈ (𝐶 ↑m 𝐵)({𝑓} × X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ↔ ∃𝑓∃𝑔(𝑑 = ⟨𝑓, 𝑔⟩ ∧ (𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))))
82	79, 80, 81	3imtr4i 292	. . . . . . 7 ⊢ (𝑑 ∈ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))} → 𝑑 ∈ ∪ 𝑓 ∈ (𝐶 ↑m 𝐵)({𝑓} × X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))))
83	82	ssriv 3986	. . . . . 6 ⊢ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))} ⊆ ∪ 𝑓 ∈ (𝐶 ↑m 𝐵)({𝑓} × X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))
84	76, 83	ssexi 5322	. . . . 5 ⊢ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))} ∈ V
85	67, 68, 84	ovmpoa 7566	. . . 4 ⊢ ((𝐷 ∈ Cat ∧ 𝐸 ∈ Cat) → (𝐷 Func 𝐸) = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))})
86	1, 2, 85	syl2anc 583	. . 3 ⊢ (𝜑 → (𝐷 Func 𝐸) = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))})
87	86	breqd 5159	. 2 ⊢ (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ 𝐹{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))}𝐺))
88		brabv 5569	. . . 4 ⊢ (𝐹{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))}𝐺 → (𝐹 ∈ V ∧ 𝐺 ∈ V))
89		elex 3492	. . . . . 6 ⊢ (𝐹 ∈ (𝐶 ↑m 𝐵) → 𝐹 ∈ V)
90		elex 3492	. . . . . 6 ⊢ (𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) → 𝐺 ∈ V)
91	89, 90	anim12i 612	. . . . 5 ⊢ ((𝐹 ∈ (𝐶 ↑m 𝐵) ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) → (𝐹 ∈ V ∧ 𝐺 ∈ V))
92	91	3adant3 1131	. . . 4 ⊢ ((𝐹 ∈ (𝐶 ↑m 𝐵) ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))) → (𝐹 ∈ V ∧ 𝐺 ∈ V))
93		simpl 482	. . . . . . . 8 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → 𝑓 = 𝐹)
94	93	eleq1d 2817	. . . . . . 7 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓 ∈ (𝐶 ↑m 𝐵) ↔ 𝐹 ∈ (𝐶 ↑m 𝐵)))
95		simpr 484	. . . . . . . 8 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺)
96	93	fveq1d 6893	. . . . . . . . . . 11 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓‘(1st ‘𝑧)) = (𝐹‘(1st ‘𝑧)))
97	93	fveq1d 6893	. . . . . . . . . . 11 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓‘(2nd ‘𝑧)) = (𝐹‘(2nd ‘𝑧)))
98	96, 97	oveq12d 7430	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) = ((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))))
99	98	oveq1d 7427	. . . . . . . . 9 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) = (((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))
100	99	ixpeq2dv 8913	. . . . . . . 8 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) = X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))
101	95, 100	eleq12d 2826	. . . . . . 7 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))))
102	95	oveqd 7429	. . . . . . . . . . 11 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑥𝑔𝑥) = (𝑥𝐺𝑥))
103	102	fveq1d 6893	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = ((𝑥𝐺𝑥)‘( 1 ‘𝑥)))
104	93	fveq1d 6893	. . . . . . . . . . 11 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓‘𝑥) = (𝐹‘𝑥))
105	104	fveq2d 6895	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝐼‘(𝑓‘𝑥)) = (𝐼‘(𝐹‘𝑥)))
106	103, 105	eqeq12d 2747	. . . . . . . . 9 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ↔ ((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥))))
107	95	oveqd 7429	. . . . . . . . . . . . 13 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑥𝑔𝑧) = (𝑥𝐺𝑧))
108	107	fveq1d 6893	. . . . . . . . . . . 12 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = ((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)))
109	93	fveq1d 6893	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓‘𝑦) = (𝐹‘𝑦))
110	104, 109	opeq12d 4881	. . . . . . . . . . . . . 14 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩ = ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)
111	93	fveq1d 6893	. . . . . . . . . . . . . 14 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓‘𝑧) = (𝐹‘𝑧))
112	110, 111	oveq12d 7430	. . . . . . . . . . . . 13 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧)) = (⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧)))
113	95	oveqd 7429	. . . . . . . . . . . . . 14 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑦𝑔𝑧) = (𝑦𝐺𝑧))
114	113	fveq1d 6893	. . . . . . . . . . . . 13 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑦𝑔𝑧)‘𝑛) = ((𝑦𝐺𝑧)‘𝑛))
115	95	oveqd 7429	. . . . . . . . . . . . . 14 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑥𝑔𝑦) = (𝑥𝐺𝑦))
116	115	fveq1d 6893	. . . . . . . . . . . . 13 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑥𝑔𝑦)‘𝑚) = ((𝑥𝐺𝑦)‘𝑚))
117	112, 114, 116	oveq123d 7433	. . . . . . . . . . . 12 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))
118	108, 117	eqeq12d 2747	. . . . . . . . . . 11 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))
119	118	2ralbidv 3217	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))
120	119	2ralbidv 3217	. . . . . . . . 9 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))
121	106, 120	anbi12d 630	. . . . . . . 8 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))))
122	121	ralbidv 3176	. . . . . . 7 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))))
123	94, 101, 122	3anbi123d 1435	. . . . . 6 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ (𝐹 ∈ (𝐶 ↑m 𝐵) ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))))
124	64, 123	bitr3id 285	. . . . 5 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ (𝐹 ∈ (𝐶 ↑m 𝐵) ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))))
125		eqid 2731	. . . . 5 ⊢ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))} = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))}
126	124, 125	brabga 5534	. . . 4 ⊢ ((𝐹 ∈ V ∧ 𝐺 ∈ V) → (𝐹{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))}𝐺 ↔ (𝐹 ∈ (𝐶 ↑m 𝐵) ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))))
127	88, 92, 126	pm5.21nii 378	. . 3 ⊢ (𝐹{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))}𝐺 ↔ (𝐹 ∈ (𝐶 ↑m 𝐵) ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))))
128	14, 15	elmap 8871	. . . 4 ⊢ (𝐹 ∈ (𝐶 ↑m 𝐵) ↔ 𝐹:𝐵⟶𝐶)
129	128	3anbi1i 1156	. . 3 ⊢ ((𝐹 ∈ (𝐶 ↑m 𝐵) ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))) ↔ (𝐹:𝐵⟶𝐶 ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))))
130	127, 129	bitri 275	. 2 ⊢ (𝐹{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))}𝐺 ↔ (𝐹:𝐵⟶𝐶 ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))))
131	87, 130	bitrdi 287	1 ⊢ (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ (𝐹:𝐵⟶𝐶 ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1086   = wceq 1540  ∃wex 1780   ∈ wcel 2105  ∀wral 3060  Vcvv 3473  [wsbc 3777  {csn 4628  ⟨cop 4634  ∪ ciun 4997   class class class wbr 5148  {copab 5210   × cxp 5674  ⟶wf 6539  ‘cfv 6543  (class class class)co 7412  1^st c1st 7977  2^nd c2nd 7978   ↑_m cmap 8826  Xcixp 8897  Basecbs 17151  Hom chom 17215  compcco 17216  Catccat 17615  Idccid 17616   Func cfunc 17811

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-ov 7415  df-oprab 7416  df-mpo 7417  df-map 8828  df-ixp 8898  df-func 17815

This theorem is referenced by:  isfuncd  17822  funcf1  17823  funcixp  17824  funcid  17827  funcco  17828  idfucl  17838  cofucl  17845  funcres2b  17854  funcpropd  17860  functhinc  47827