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.

Step	Hyp	Ref	Expression
1		isfunc.d	. . . 4 ⊢ (𝜑 → 𝐷 ∈ Cat)
2		isfunc.e	. . . 4 ⊢ (𝜑 → 𝐸 ∈ Cat)
3		fvexd 6857	. . . . . . 7 ⊢ ((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) → (Base‘𝑑) ∈ V)
4		simpl 483	. . . . . . . . 9 ⊢ ((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) → 𝑑 = 𝐷)
5	4	fveq2d 6846	. . . . . . . 8 ⊢ ((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) → (Base‘𝑑) = (Base‘𝐷))
6		isfunc.b	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝐷)
7	5, 6	eqtr4di 2794	. . . . . . 7 ⊢ ((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) → (Base‘𝑑) = 𝐵)
8		simpr 485	. . . . . . . . . . 11 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵)
9		simplr 767	. . . . . . . . . . . . 13 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → 𝑒 = 𝐸)
10	9	fveq2d 6846	. . . . . . . . . . . 12 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Base‘𝑒) = (Base‘𝐸))
11		isfunc.c	. . . . . . . . . . . 12 ⊢ 𝐶 = (Base‘𝐸)
12	10, 11	eqtr4di 2794	. . . . . . . . . . 11 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Base‘𝑒) = 𝐶)
13	8, 12	feq23d 6663	. . . . . . . . . 10 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑓:𝑏⟶(Base‘𝑒) ↔ 𝑓:𝐵⟶𝐶))
14	11	fvexi 6856	. . . . . . . . . . 11 ⊢ 𝐶 ∈ V
15	6	fvexi 6856	. . . . . . . . . . 11 ⊢ 𝐵 ∈ V
16	14, 15	elmap 8809	. . . . . . . . . 10 ⊢ (𝑓 ∈ (𝐶 ↑m 𝐵) ↔ 𝑓:𝐵⟶𝐶)
17	13, 16	bitr4di 288	. . . . . . . . 9 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑓:𝑏⟶(Base‘𝑒) ↔ 𝑓 ∈ (𝐶 ↑m 𝐵)))
18	8	sqxpeqd 5665	. . . . . . . . . . . 12 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑏 × 𝑏) = (𝐵 × 𝐵))
19	18	ixpeq1d 8847	. . . . . . . . . . 11 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) = X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)))
20	9	fveq2d 6846	. . . . . . . . . . . . . . 15 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Hom ‘𝑒) = (Hom ‘𝐸))
21		isfunc.j	. . . . . . . . . . . . . . 15 ⊢ 𝐽 = (Hom ‘𝐸)
22	20, 21	eqtr4di 2794	. . . . . . . . . . . . . 14 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Hom ‘𝑒) = 𝐽)
23	22	oveqd 7374	. . . . . . . . . . . . 13 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) = ((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))))
24		simpll 765	. . . . . . . . . . . . . . . 16 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → 𝑑 = 𝐷)
25	24	fveq2d 6846	. . . . . . . . . . . . . . 15 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Hom ‘𝑑) = (Hom ‘𝐷))
26		isfunc.h	. . . . . . . . . . . . . . 15 ⊢ 𝐻 = (Hom ‘𝐷)
27	25, 26	eqtr4di 2794	. . . . . . . . . . . . . 14 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Hom ‘𝑑) = 𝐻)
28	27	fveq1d 6844	. . . . . . . . . . . . 13 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((Hom ‘𝑑)‘𝑧) = (𝐻‘𝑧))
29	23, 28	oveq12d 7375	. . . . . . . . . . . 12 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) = (((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))
30	29	ixpeq2dv 8851	. . . . . . . . . . 11 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) = X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))
31	19, 30	eqtrd 2776	. . . . . . . . . 10 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) = X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))
32	31	eleq2d 2823	. . . . . . . . 9 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) ↔ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))))
33	24	fveq2d 6846	. . . . . . . . . . . . . . 15 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Id‘𝑑) = (Id‘𝐷))
34		isfunc.1	. . . . . . . . . . . . . . 15 ⊢ 1 = (Id‘𝐷)
35	33, 34	eqtr4di 2794	. . . . . . . . . . . . . 14 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Id‘𝑑) = 1 )
36	35	fveq1d 6844	. . . . . . . . . . . . 13 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((Id‘𝑑)‘𝑥) = ( 1 ‘𝑥))
37	36	fveq2d 6846	. . . . . . . . . . . 12 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((𝑥𝑔𝑥)‘( 1 ‘𝑥)))
38	9	fveq2d 6846	. . . . . . . . . . . . . 14 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Id‘𝑒) = (Id‘𝐸))
39		isfunc.i	. . . . . . . . . . . . . 14 ⊢ 𝐼 = (Id‘𝐸)
40	38, 39	eqtr4di 2794	. . . . . . . . . . . . 13 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Id‘𝑒) = 𝐼)
41	40	fveq1d 6844	. . . . . . . . . . . 12 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((Id‘𝑒)‘(𝑓‘𝑥)) = (𝐼‘(𝑓‘𝑥)))
42	37, 41	eqeq12d 2752	. . . . . . . . . . 11 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓‘𝑥)) ↔ ((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥))))
43	27	oveqd 7374	. . . . . . . . . . . . . 14 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑥(Hom ‘𝑑)𝑦) = (𝑥𝐻𝑦))
44	27	oveqd 7374	. . . . . . . . . . . . . . 15 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑦(Hom ‘𝑑)𝑧) = (𝑦𝐻𝑧))
45	24	fveq2d 6846	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (comp‘𝑑) = (comp‘𝐷))
46		isfunc.x	. . . . . . . . . . . . . . . . . . . 20 ⊢ · = (comp‘𝐷)
47	45, 46	eqtr4di 2794	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (comp‘𝑑) = · )
48	47	oveqd 7374	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧) = (⟨𝑥, 𝑦⟩ · 𝑧))
49	48	oveqd 7374	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚) = (𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚))
50	49	fveq2d 6846	. . . . . . . . . . . . . . . 16 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)))
51	9	fveq2d 6846	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (comp‘𝑒) = (comp‘𝐸))
52		isfunc.o	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑂 = (comp‘𝐸)
53	51, 52	eqtr4di 2794	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (comp‘𝑒) = 𝑂)
54	53	oveqd 7374	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧)) = (⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧)))
55	54	oveqd 7374	. . . . . . . . . . . . . . . 16 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))
56	50, 55	eqeq12d 2752	. . . . . . . . . . . . . . 15 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
57	44, 56	raleqbidv 3319	. . . . . . . . . . . . . 14 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
58	43, 57	raleqbidv 3319	. . . . . . . . . . . . 13 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
59	8, 58	raleqbidv 3319	. . . . . . . . . . . 12 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
60	8, 59	raleqbidv 3319	. . . . . . . . . . 11 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))
61	42, 60	anbi12d 631	. . . . . . . . . 10 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))
62	8, 61	raleqbidv 3319	. . . . . . . . 9 ⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))
63	17, 32, 62	3anbi123d 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 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))
65	63, 64	bitrdi 286	. . . . . . 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 3786	. . . . . 6 ⊢ ((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) → ([(Base‘𝑑) / 𝑏](𝑓:𝑏⟶(Base‘𝑒) ∧ 𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑m ((Hom ‘𝑑)‘𝑧)) ∧ ∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))))
67	66	opabbidv 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
72	71	rgenw 3068	. . . . . . . . 9 ⊢ ∀𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∈ V
73		ixpexg 8860	. . . . . . . . 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 7687	. . . . . . 7 ⊢ ({𝑓} × X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∈ V
76	69, 75	iunex 7901	. . . . . 6 ⊢ ∪ 𝑓 ∈ (𝐶 ↑m 𝐵)({𝑓} × X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∈ V
77		simpl 483	. . . . . . . . . 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 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 (𝐻‘𝑧)))))
82	79, 80, 81	3imtr4i 291	. . . . . . 7 ⊢ (𝑑 ∈ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))} → 𝑑 ∈ ∪ 𝑓 ∈ (𝐶 ↑m 𝐵)({𝑓} × X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))))
83	82	ssriv 3948	. . . . . 6 ⊢ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))} ⊆ ∪ 𝑓 ∈ (𝐶 ↑m 𝐵)({𝑓} × X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))
84	76, 83	ssexi 5279	. . . . 5 ⊢ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))} ∈ V
85	67, 68, 84	ovmpoa 7510	. . . 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 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)
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 483	. . . . . . . 8 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → 𝑓 = 𝐹)
94	93	eleq1d 2822	. . . . . . 7 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓 ∈ (𝐶 ↑m 𝐵) ↔ 𝐹 ∈ (𝐶 ↑m 𝐵)))
95		simpr 485	. . . . . . . 8 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺)
96	93	fveq1d 6844	. . . . . . . . . . 11 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓‘(1st ‘𝑧)) = (𝐹‘(1st ‘𝑧)))
97	93	fveq1d 6844	. . . . . . . . . . 11 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓‘(2nd ‘𝑧)) = (𝐹‘(2nd ‘𝑧)))
98	96, 97	oveq12d 7375	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) = ((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))))
99	98	oveq1d 7372	. . . . . . . . 9 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) = (((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))
100	99	ixpeq2dv 8851	. . . . . . . 8 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) = X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))
101	95, 100	eleq12d 2832	. . . . . . 7 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))))
102	95	oveqd 7374	. . . . . . . . . . 11 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑥𝑔𝑥) = (𝑥𝐺𝑥))
103	102	fveq1d 6844	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = ((𝑥𝐺𝑥)‘( 1 ‘𝑥)))
104	93	fveq1d 6844	. . . . . . . . . . 11 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓‘𝑥) = (𝐹‘𝑥))
105	104	fveq2d 6846	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝐼‘(𝑓‘𝑥)) = (𝐼‘(𝐹‘𝑥)))
106	103, 105	eqeq12d 2752	. . . . . . . . 9 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ↔ ((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥))))
107	95	oveqd 7374	. . . . . . . . . . . . 13 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑥𝑔𝑧) = (𝑥𝐺𝑧))
108	107	fveq1d 6844	. . . . . . . . . . . 12 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = ((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)))
109	93	fveq1d 6844	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓‘𝑦) = (𝐹‘𝑦))
110	104, 109	opeq12d 4838	. . . . . . . . . . . . . 14 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩ = ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩)
111	93	fveq1d 6844	. . . . . . . . . . . . . 14 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓‘𝑧) = (𝐹‘𝑧))
112	110, 111	oveq12d 7375	. . . . . . . . . . . . 13 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧)) = (⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧)))
113	95	oveqd 7374	. . . . . . . . . . . . . 14 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑦𝑔𝑧) = (𝑦𝐺𝑧))
114	113	fveq1d 6844	. . . . . . . . . . . . 13 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑦𝑔𝑧)‘𝑛) = ((𝑦𝐺𝑧)‘𝑛))
115	95	oveqd 7374	. . . . . . . . . . . . . 14 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑥𝑔𝑦) = (𝑥𝐺𝑦))
116	115	fveq1d 6844	. . . . . . . . . . . . 13 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑥𝑔𝑦)‘𝑚) = ((𝑥𝐺𝑦)‘𝑚))
117	112, 114, 116	oveq123d 7378	. . . . . . . . . . . 12 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))
118	108, 117	eqeq12d 2752	. . . . . . . . . . 11 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))
119	118	2ralbidv 3212	. . . . . . . . . 10 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))
120	119	2ralbidv 3212	. . . . . . . . 9 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))
121	106, 120	anbi12d 631	. . . . . . . 8 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))))
122	121	ralbidv 3174	. . . . . . 7 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))))
123	94, 101, 122	3anbi123d 1436	. . . . . 6 ⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ (𝐹 ∈ (𝐶 ↑m 𝐵) ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))))
124	64, 123	bitr3id 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 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))}
126	124, 125	brabga 5491	. . . 4 ⊢ ((𝐹 ∈ V ∧ 𝐺 ∈ V) → (𝐹{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))}𝐺 ↔ (𝐹 ∈ (𝐶 ↑m 𝐵) ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))))
127	88, 92, 126	pm5.21nii 379	. . 3 ⊢ (𝐹{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))}𝐺 ↔ (𝐹 ∈ (𝐶 ↑m 𝐵) ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))))
128	14, 15	elmap 8809	. . . 4 ⊢ (𝐹 ∈ (𝐶 ↑m 𝐵) ↔ 𝐹:𝐵⟶𝐶)
129	128	3anbi1i 1157	. . 3 ⊢ ((𝐹 ∈ (𝐶 ↑m 𝐵) ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))) ↔ (𝐹:𝐵⟶𝐶 ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))))
130	127, 129	bitri 274	. 2 ⊢ (𝐹{⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝐶 ↑m 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓‘𝑥), (𝑓‘𝑦)⟩𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))}𝐺 ↔ (𝐹:𝐵⟶𝐶 ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))))
131	87, 130	bitrdi 286	1 ⊢ (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ (𝐹:𝐵⟶𝐶 ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))))

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  1^st c1st 7919  2^nd 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