Theorem isfunc 17833

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 6876	. . . . . . 7 ⊢ ((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) → (Base‘𝑑) ∈ V)
4		simpl 482	. . . . . . . . 9 ⊢ ((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) → 𝑑 = 𝐷)
5	4	fveq2d 6865	. . . . . . . 8 ⊢ ((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) → (Base‘𝑑) = (Base‘𝐷))
6		isfunc.b	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝐷)
7	5, 6	eqtr4di 2783	. . . . . . 7 ⊢ ((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) → (Base‘𝑑) = 𝐵)
8		simpr 484	. . . . . . . . . . 11 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵)
9		simplr 768	. . . . . . . . . . . . 13 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → 𝑒 = 𝐸)
10	9	fveq2d 6865	. . . . . . . . . . . 12 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Base‘𝑒) = (Base‘𝐸))
11		isfunc.c	. . . . . . . . . . . 12 ⊢ 𝐶 = (Base‘𝐸)
12	10, 11	eqtr4di 2783	. . . . . . . . . . 11 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Base‘𝑒) = 𝐶)
13	8, 12	feq23d 6686	. . . . . . . . . 10 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑓:𝑏⟶(Base‘𝑒) ↔ 𝑓:𝐵⟶𝐶))
14	11	fvexi 6875	. . . . . . . . . . 11 ⊢ 𝐶 ∈ V
15	6	fvexi 6875	. . . . . . . . . . 11 ⊢ 𝐵 ∈ V
16	14, 15	elmap 8847	. . . . . . . . . 10 ⊢ (𝑓 ∈ (𝐶 ↑m 𝐵) ↔ 𝑓:𝐵⟶𝐶)
17	13, 16	bitr4di 289	. . . . . . . . 9 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑓:𝑏⟶(Base‘𝑒) ↔ 𝑓 ∈ (𝐶 ↑m 𝐵)))
18	8	sqxpeqd 5673	. . . . . . . . . . . 12 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑏 × 𝑏) = (𝐵 × 𝐵))
19	18	ixpeq1d 8885	. . . . . . . . . . 11 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) = X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)))
20	9	fveq2d 6865	. . . . . . . . . . . . . . 15 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Hom ‘𝑒) = (Hom ‘𝐸))
21		isfunc.j	. . . . . . . . . . . . . . 15 ⊢ 𝐽 = (Hom ‘𝐸)
22	20, 21	eqtr4di 2783	. . . . . . . . . . . . . 14 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Hom ‘𝑒) = 𝐽)
23	22	oveqd 7407	. . . . . . . . . . . . 13 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) = ((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))))
24		simpll 766	. . . . . . . . . . . . . . . 16 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → 𝑑 = 𝐷)
25	24	fveq2d 6865	. . . . . . . . . . . . . . 15 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Hom ‘𝑑) = (Hom ‘𝐷))
26		isfunc.h	. . . . . . . . . . . . . . 15 ⊢ 𝐻 = (Hom ‘𝐷)
27	25, 26	eqtr4di 2783	. . . . . . . . . . . . . 14 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Hom ‘𝑑) = 𝐻)
28	27	fveq1d 6863	. . . . . . . . . . . . 13 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((Hom ‘𝑑)‘𝑧) = (𝐻‘𝑧))
29	23, 28	oveq12d 7408	. . . . . . . . . . . 12 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) = (((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))
30	29	ixpeq2dv 8889	. . . . . . . . . . 11 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) = X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))
31	19, 30	eqtrd 2765	. . . . . . . . . 10 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) = X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))
32	31	eleq2d 2815	. . . . . . . . 9 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) ↔ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))))
33	24	fveq2d 6865	. . . . . . . . . . . . . . 15 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Id‘𝑑) = (Id‘𝐷))
34		isfunc.1	. . . . . . . . . . . . . . 15 ⊢ 1 = (Id‘𝐷)
35	33, 34	eqtr4di 2783	. . . . . . . . . . . . . 14 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Id‘𝑑) = 1 )
36	35	fveq1d 6863	. . . . . . . . . . . . 13 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((Id‘𝑑)‘𝑥) = ( 1 ‘𝑥))
37	36	fveq2d 6865	. . . . . . . . . . . 12 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((𝑥𝑔𝑥)‘( 1 ‘𝑥)))
38	9	fveq2d 6865	. . . . . . . . . . . . . 14 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Id‘𝑒) = (Id‘𝐸))
39		isfunc.i	. . . . . . . . . . . . . 14 ⊢ 𝐼 = (Id‘𝐸)
40	38, 39	eqtr4di 2783	. . . . . . . . . . . . 13 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Id‘𝑒) = 𝐼)
41	40	fveq1d 6863	. . . . . . . . . . . 12 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((Id‘𝑒)‘(𝑓‘𝑥)) = (𝐼‘(𝑓‘𝑥)))
42	37, 41	eqeq12d 2746	. . . . . . . . . . 11 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓‘𝑥)) ↔ ((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥))))
43	27	oveqd 7407	. . . . . . . . . . . . . 14 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑥(Hom ‘𝑑)𝑦) = (𝑥𝐻𝑦))
44	27	oveqd 7407	. . . . . . . . . . . . . . 15 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑦(Hom ‘𝑑)𝑧) = (𝑦𝐻𝑧))
45	24	fveq2d 6865	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (comp‘𝑑) = (comp‘𝐷))
46		isfunc.x	. . . . . . . . . . . . . . . . . . . 20 ⊢ · = (comp‘𝐷)
47	45, 46	eqtr4di 2783	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (comp‘𝑑) = · )
48	47	oveqd 7407	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧) = (⟨𝑥, 𝑦⟩ · 𝑧))
49	48	oveqd 7407	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚) = (𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚))
50	49	fveq2d 6865	. . . . . . . . . . . . . . . 16 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)))
51	9	fveq2d 6865	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (comp‘𝑒) = (comp‘𝐸))
52		isfunc.o	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑂 = (comp‘𝐸)
53	51, 52	eqtr4di 2783	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (comp‘𝑒) = 𝑂)
54	53	oveqd 7407	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧)) = (⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧)))
55	54	oveqd 7407	. . . . . . . . . . . . . . . 16 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))
56	50, 55	eqeq12d 2746	. . . . . . . . . . . . . . 15 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
57	44, 56	raleqbidv 3321	. . . . . . . . . . . . . 14 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
58	43, 57	raleqbidv 3321	. . . . . . . . . . . . 13 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
59	8, 58	raleqbidv 3321	. . . . . . . . . . . 12 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
60	8, 59	raleqbidv 3321	. . . . . . . . . . 11 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
61	42, 60	anbi12d 632	. . . . . . . . . 10 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))
62	8, 61	raleqbidv 3321	. . . . . . . . 9 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))
63	17, 32, 62	3anbi123d 1438	. . . . . . . 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 3801	. . . . . 6 ⊢ ((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) → ([(Base‘𝑑) / 𝑏](𝑓:𝑏⟶(Base‘𝑒) ∧ 𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) ∧ ∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))))
67	66	opabbidv 5176	. . . . 5 ⊢ ((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) → {⟨𝑓, 𝑔⟩ ∣ [(Base‘𝑑) / 𝑏](𝑓:𝑏⟶(Base‘𝑒) ∧ 𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) ∧ ∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))} = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))})
68		df-func 17827	. . . . 5 ⊢ Func = (𝑑 ∈ Cat, 𝑒 ∈ Cat ↦ {⟨𝑓, 𝑔⟩ ∣ [(Base‘𝑑) / 𝑏](𝑓:𝑏⟶(Base‘𝑒) ∧ 𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) ∧ ∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))})
69		ovex 7423	. . . . . . 7 ⊢ (𝐶 ↑m 𝐵) ∈ V
70		vsnex 5392	. . . . . . . 8 ⊢ {𝑓} ∈ V
71		ovex 7423	. . . . . . . . . 10 ⊢ (((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∈ V
72	71	rgenw 3049	. . . . . . . . 9 ⊢ ∀𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∈ V
73		ixpexg 8898	. . . . . . . . 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 7732	. . . . . . 7 ⊢ ({𝑓} × X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∈ V
76	69, 75	iunex 7950	. . . . . 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 617	. . . . . . . . 9 ⊢ ((𝑑 = ⟨𝑓, 𝑔⟩ ∧ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))) → (𝑑 = ⟨𝑓, 𝑔⟩ ∧ (𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))))
79	78	2eximi 1836	. . . . . . . 8 ⊢ (∃𝑓∃𝑔(𝑑 = ⟨𝑓, 𝑔⟩ ∧ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))) → ∃𝑓∃𝑔(𝑑 = ⟨𝑓, 𝑔⟩ ∧ (𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))))
80		elopab 5490	. . . . . . . 8 ⊢ (𝑑 ∈ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))} ↔ ∃𝑓∃𝑔(𝑑 = ⟨𝑓, 𝑔⟩ ∧ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))))
81		eliunxp 5804	. . . . . . . 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 3953	. . . . . 6 ⊢ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))} ⊆ ∪ 𝑓 ∈ (𝐶 ↑m 𝐵)({𝑓} × X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))
84	76, 83	ssexi 5280	. . . . 5 ⊢ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))} ∈ V
85	67, 68, 84	ovmpoa 7547	. . . 4 ⊢ ((𝐷 ∈ Cat ∧ 𝐸 ∈ Cat) → (𝐷 Func 𝐸) = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))})
86	1, 2, 85	syl2anc 584	. . 3 ⊢ (𝜑 → (𝐷 Func 𝐸) = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))})
87	86	breqd 5121	. 2 ⊢ (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ 𝐹{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))}𝐺))
88		brabv 5531	. . . 4 ⊢ (𝐹{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))}𝐺 → (𝐹 ∈ V ∧ 𝐺 ∈ V))
89		elex 3471	. . . . . 6 ⊢ (𝐹 ∈ (𝐶 ↑m 𝐵) → 𝐹 ∈ V)
90		elex 3471	. . . . . 6 ⊢ (𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) → 𝐺 ∈ V)
91	89, 90	anim12i 613	. . . . 5 ⊢ ((𝐹 ∈ (𝐶 ↑m 𝐵) ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) → (𝐹 ∈ V ∧ 𝐺 ∈ V))
92	91	3adant3 1132	. . . 4 ⊢ ((𝐹 ∈ (𝐶 ↑m 𝐵) ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))) → (𝐹 ∈ V ∧ 𝐺 ∈ V))
93		simpl 482	. . . . . . . 8 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → 𝑓 = 𝐹)
94	93	eleq1d 2814	. . . . . . 7 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓 ∈ (𝐶 ↑m 𝐵) ↔ 𝐹 ∈ (𝐶 ↑m 𝐵)))
95		simpr 484	. . . . . . . 8 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺)
96	93	fveq1d 6863	. . . . . . . . . . 11 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓‘(1st ‘𝑧)) = (𝐹‘(1st ‘𝑧)))
97	93	fveq1d 6863	. . . . . . . . . . 11 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓‘(2nd ‘𝑧)) = (𝐹‘(2nd ‘𝑧)))
98	96, 97	oveq12d 7408	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) = ((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))))
99	98	oveq1d 7405	. . . . . . . . 9 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) = (((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))
100	99	ixpeq2dv 8889	. . . . . . . 8 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) = X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))
101	95, 100	eleq12d 2823	. . . . . . 7 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))))
102	95	oveqd 7407	. . . . . . . . . . 11 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑥𝑔𝑥) = (𝑥𝐺𝑥))
103	102	fveq1d 6863	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = ((𝑥𝐺𝑥)‘( 1 ‘𝑥)))
104	93	fveq1d 6863	. . . . . . . . . . 11 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓‘𝑥) = (𝐹‘𝑥))
105	104	fveq2d 6865	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝐼‘(𝑓‘𝑥)) = (𝐼‘(𝐹‘𝑥)))
106	103, 105	eqeq12d 2746	. . . . . . . . 9 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ↔ ((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥))))
107	95	oveqd 7407	. . . . . . . . . . . . 13 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑥𝑔𝑧) = (𝑥𝐺𝑧))
108	107	fveq1d 6863	. . . . . . . . . . . 12 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = ((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)))
109	93	fveq1d 6863	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓‘𝑦) = (𝐹‘𝑦))
110	104, 109	opeq12d 4848	. . . . . . . . . . . . . 14 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩ = ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)
111	93	fveq1d 6863	. . . . . . . . . . . . . 14 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓‘𝑧) = (𝐹‘𝑧))
112	110, 111	oveq12d 7408	. . . . . . . . . . . . 13 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧)) = (⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧)))
113	95	oveqd 7407	. . . . . . . . . . . . . 14 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑦𝑔𝑧) = (𝑦𝐺𝑧))
114	113	fveq1d 6863	. . . . . . . . . . . . 13 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑦𝑔𝑧)‘𝑛) = ((𝑦𝐺𝑧)‘𝑛))
115	95	oveqd 7407	. . . . . . . . . . . . . 14 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑥𝑔𝑦) = (𝑥𝐺𝑦))
116	115	fveq1d 6863	. . . . . . . . . . . . 13 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑥𝑔𝑦)‘𝑚) = ((𝑥𝐺𝑦)‘𝑚))
117	112, 114, 116	oveq123d 7411	. . . . . . . . . . . 12 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))
118	108, 117	eqeq12d 2746	. . . . . . . . . . 11 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))
119	118	2ralbidv 3202	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))
120	119	2ralbidv 3202	. . . . . . . . 9 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))
121	106, 120	anbi12d 632	. . . . . . . 8 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))))
122	121	ralbidv 3157	. . . . . . 7 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))))
123	94, 101, 122	3anbi123d 1438	. . . . . 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 2730	. . . . 5 ⊢ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))} = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))}
126	124, 125	brabga 5497	. . . 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 8847	. . . 4 ⊢ (𝐹 ∈ (𝐶 ↑m 𝐵) ↔ 𝐹:𝐵⟶𝐶)
129	128	3anbi1i 1157	. . 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 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ∀wral 3045  Vcvv 3450  [wsbc 3756  {csn 4592  ⟨cop 4598  ∪ ciun 4958   class class class wbr 5110  {copab 5172   × cxp 5639  ⟶wf 6510  ‘cfv 6514  (class class class)co 7390  1^st c1st 7969  2^nd c2nd 7970   ↑_m cmap 8802  Xcixp 8873  Basecbs 17186  Hom chom 17238  compcco 17239  Catccat 17632  Idccid 17633   Func cfunc 17823

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-fv 6522  df-ov 7393  df-oprab 7394  df-mpo 7395  df-map 8804  df-ixp 8874  df-func 17827

This theorem is referenced by:  isfuncd  17834  funcf1  17835  funcixp  17836  funcid  17839  funcco  17840  idfucl  17850  cofucl  17857  funcres2b  17866  funcpropd  17871  0funcg2  49077  0funcALT  49081  functhinc  49441