Theorem curf1cl 17594

Description: The partially evaluated curry functor is a functor. (Contributed by Mario Carneiro, 13-Jan-2017.)

Hypotheses

Ref	Expression
curfval.g	⊢ 𝐺 = (⟨𝐶, 𝐷⟩ curryF 𝐹)
curfval.a	⊢ 𝐴 = (Base‘𝐶)
curfval.c	⊢ (𝜑 → 𝐶 ∈ Cat)
curfval.d	⊢ (𝜑 → 𝐷 ∈ Cat)
curfval.f	⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
curfval.b	⊢ 𝐵 = (Base‘𝐷)
curf1.x	⊢ (𝜑 → 𝑋 ∈ 𝐴)
curf1.k	⊢ 𝐾 = ((1st ‘𝐺)‘𝑋)

Assertion

Ref	Expression
curf1cl	⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐸))

Proof of Theorem curf1cl

Dummy variables 𝑔 𝑦 𝑧 ℎ 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		curfval.g	. . . 4 ⊢ 𝐺 = (⟨𝐶, 𝐷⟩ curryF 𝐹)
2		curfval.a	. . . 4 ⊢ 𝐴 = (Base‘𝐶)
3		curfval.c	. . . 4 ⊢ (𝜑 → 𝐶 ∈ Cat)
4		curfval.d	. . . 4 ⊢ (𝜑 → 𝐷 ∈ Cat)
5		curfval.f	. . . 4 ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
6		curfval.b	. . . 4 ⊢ 𝐵 = (Base‘𝐷)
7		curf1.x	. . . 4 ⊢ (𝜑 → 𝑋 ∈ 𝐴)
8		curf1.k	. . . 4 ⊢ 𝐾 = ((1st ‘𝐺)‘𝑋)
9		eqid 2738	. . . 4 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
10		eqid 2738	. . . 4 ⊢ (Id‘𝐶) = (Id‘𝐶)
11	1, 2, 3, 4, 5, 6, 7, 8, 9, 10	curf1 17591	. . 3 ⊢ (𝜑 → 𝐾 = ⟨(𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))⟩)
12	6	fvexi 6688	. . . . . . 7 ⊢ 𝐵 ∈ V
13	12	mptex 6996	. . . . . 6 ⊢ (𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)) ∈ V
14	12, 12	mpoex 7803	. . . . . 6 ⊢ (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔))) ∈ V
15	13, 14	op1std 7724	. . . . 5 ⊢ (𝐾 = ⟨(𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))⟩ → (1st ‘𝐾) = (𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)))
16	11, 15	syl 17	. . . 4 ⊢ (𝜑 → (1st ‘𝐾) = (𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)))
17	13, 14	op2ndd 7725	. . . . 5 ⊢ (𝐾 = ⟨(𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))⟩ → (2nd ‘𝐾) = (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔))))
18	11, 17	syl 17	. . . 4 ⊢ (𝜑 → (2nd ‘𝐾) = (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔))))
19	16, 18	opeq12d 4769	. . 3 ⊢ (𝜑 → ⟨(1st ‘𝐾), (2nd ‘𝐾)⟩ = ⟨(𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))⟩)
20	11, 19	eqtr4d 2776	. 2 ⊢ (𝜑 → 𝐾 = ⟨(1st ‘𝐾), (2nd ‘𝐾)⟩)
21		eqid 2738	. . . 4 ⊢ (Base‘𝐸) = (Base‘𝐸)
22		eqid 2738	. . . 4 ⊢ (Hom ‘𝐸) = (Hom ‘𝐸)
23		eqid 2738	. . . 4 ⊢ (Id‘𝐷) = (Id‘𝐷)
24		eqid 2738	. . . 4 ⊢ (Id‘𝐸) = (Id‘𝐸)
25		eqid 2738	. . . 4 ⊢ (comp‘𝐷) = (comp‘𝐷)
26		eqid 2738	. . . 4 ⊢ (comp‘𝐸) = (comp‘𝐸)
27		funcrcl 17238	. . . . . 6 ⊢ (𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸) → ((𝐶 ×c 𝐷) ∈ Cat ∧ 𝐸 ∈ Cat))
28	5, 27	syl 17	. . . . 5 ⊢ (𝜑 → ((𝐶 ×c 𝐷) ∈ Cat ∧ 𝐸 ∈ Cat))
29	28	simprd 499	. . . 4 ⊢ (𝜑 → 𝐸 ∈ Cat)
30		eqid 2738	. . . . . . . . 9 ⊢ (𝐶 ×c 𝐷) = (𝐶 ×c 𝐷)
31	30, 2, 6	xpcbas 17544	. . . . . . . 8 ⊢ (𝐴 × 𝐵) = (Base‘(𝐶 ×c 𝐷))
32		relfunc 17237	. . . . . . . . 9 ⊢ Rel ((𝐶 ×c 𝐷) Func 𝐸)
33		1st2ndbr 7766	. . . . . . . . 9 ⊢ ((Rel ((𝐶 ×c 𝐷) Func 𝐸) ∧ 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹))
34	32, 5, 33	sylancr 590	. . . . . . . 8 ⊢ (𝜑 → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹))
35	31, 21, 34	funcf1 17241	. . . . . . 7 ⊢ (𝜑 → (1st ‘𝐹):(𝐴 × 𝐵)⟶(Base‘𝐸))
36	35	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1st ‘𝐹):(𝐴 × 𝐵)⟶(Base‘𝐸))
37	7	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑋 ∈ 𝐴)
38		simpr 488	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵)
39	36, 37, 38	fovrnd 7336	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑋(1st ‘𝐹)𝑦) ∈ (Base‘𝐸))
40	16, 39	fmpt3d 6890	. . . 4 ⊢ (𝜑 → (1st ‘𝐾):𝐵⟶(Base‘𝐸))
41		eqid 2738	. . . . . 6 ⊢ (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔))) = (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))
42		ovex 7203	. . . . . . 7 ⊢ (𝑦(Hom ‘𝐷)𝑧) ∈ V
43	42	mptex 6996	. . . . . 6 ⊢ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)) ∈ V
44	41, 43	fnmpoi 7793	. . . . 5 ⊢ (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔))) Fn (𝐵 × 𝐵)
45	18	fneq1d 6431	. . . . 5 ⊢ (𝜑 → ((2nd ‘𝐾) Fn (𝐵 × 𝐵) ↔ (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔))) Fn (𝐵 × 𝐵)))
46	44, 45	mpbiri 261	. . . 4 ⊢ (𝜑 → (2nd ‘𝐾) Fn (𝐵 × 𝐵))
47	18	oveqd 7187	. . . . . 6 ⊢ (𝜑 → (𝑦(2nd ‘𝐾)𝑧) = (𝑦(𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))𝑧))
48	41	ovmpt4g 7312	. . . . . . 7 ⊢ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)) ∈ V) → (𝑦(𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))𝑧) = (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))
49	43, 48	mp3an3 1451	. . . . . 6 ⊢ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝑦(𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))𝑧) = (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))
50	47, 49	sylan9eq 2793	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦(2nd ‘𝐾)𝑧) = (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))
51		eqid 2738	. . . . . . . 8 ⊢ (Hom ‘(𝐶 ×c 𝐷)) = (Hom ‘(𝐶 ×c 𝐷))
52	34	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹))
53	7	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑋 ∈ 𝐴)
54		simplrl 777	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑦 ∈ 𝐵)
55	53, 54	opelxpd 5563	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ⟨𝑋, 𝑦⟩ ∈ (𝐴 × 𝐵))
56		simplrr 778	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑧 ∈ 𝐵)
57	53, 56	opelxpd 5563	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ⟨𝑋, 𝑧⟩ ∈ (𝐴 × 𝐵))
58	31, 51, 22, 52, 55, 57	funcf2 17243	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩):(⟨𝑋, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑧⟩)⟶(((1st ‘𝐹)‘⟨𝑋, 𝑦⟩)(Hom ‘𝐸)((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)))
59		eqid 2738	. . . . . . . . 9 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
60	30, 31, 59, 9, 51, 55, 57	xpchom 17546	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (⟨𝑋, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑧⟩) = (((1st ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐶)(1st ‘⟨𝑋, 𝑧⟩)) × ((2nd ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐷)(2nd ‘⟨𝑋, 𝑧⟩))))
61	3	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝐶 ∈ Cat)
62	4	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝐷 ∈ Cat)
63	5	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
64	1, 2, 61, 62, 63, 6, 53, 8, 54	curf11 17592	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st ‘𝐾)‘𝑦) = (𝑋(1st ‘𝐹)𝑦))
65		df-ov 7173	. . . . . . . . . 10 ⊢ (𝑋(1st ‘𝐹)𝑦) = ((1st ‘𝐹)‘⟨𝑋, 𝑦⟩)
66	64, 65	eqtr2di 2790	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st ‘𝐹)‘⟨𝑋, 𝑦⟩) = ((1st ‘𝐾)‘𝑦))
67	1, 2, 61, 62, 63, 6, 53, 8, 56	curf11 17592	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st ‘𝐾)‘𝑧) = (𝑋(1st ‘𝐹)𝑧))
68		df-ov 7173	. . . . . . . . . 10 ⊢ (𝑋(1st ‘𝐹)𝑧) = ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)
69	67, 68	eqtr2di 2790	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩) = ((1st ‘𝐾)‘𝑧))
70	66, 69	oveq12d 7188	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (((1st ‘𝐹)‘⟨𝑋, 𝑦⟩)(Hom ‘𝐸)((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)) = (((1st ‘𝐾)‘𝑦)(Hom ‘𝐸)((1st ‘𝐾)‘𝑧)))
71	60, 70	feq23d 6499	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩):(⟨𝑋, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑧⟩)⟶(((1st ‘𝐹)‘⟨𝑋, 𝑦⟩)(Hom ‘𝐸)((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)) ↔ (⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩):(((1st ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐶)(1st ‘⟨𝑋, 𝑧⟩)) × ((2nd ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐷)(2nd ‘⟨𝑋, 𝑧⟩)))⟶(((1st ‘𝐾)‘𝑦)(Hom ‘𝐸)((1st ‘𝐾)‘𝑧))))
72	58, 71	mpbid 235	. . . . . 6 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩):(((1st ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐶)(1st ‘⟨𝑋, 𝑧⟩)) × ((2nd ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐷)(2nd ‘⟨𝑋, 𝑧⟩)))⟶(((1st ‘𝐾)‘𝑦)(Hom ‘𝐸)((1st ‘𝐾)‘𝑧)))
73	2, 59, 10, 61, 53	catidcl 17056	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((Id‘𝐶)‘𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋))
74		op1stg 7726	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (1st ‘⟨𝑋, 𝑦⟩) = 𝑋)
75	53, 54, 74	syl2anc 587	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (1st ‘⟨𝑋, 𝑦⟩) = 𝑋)
76		op1stg 7726	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → (1st ‘⟨𝑋, 𝑧⟩) = 𝑋)
77	53, 56, 76	syl2anc 587	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (1st ‘⟨𝑋, 𝑧⟩) = 𝑋)
78	75, 77	oveq12d 7188	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐶)(1st ‘⟨𝑋, 𝑧⟩)) = (𝑋(Hom ‘𝐶)𝑋))
79	73, 78	eleqtrrd 2836	. . . . . 6 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((Id‘𝐶)‘𝑋) ∈ ((1st ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐶)(1st ‘⟨𝑋, 𝑧⟩)))
80		simpr 488	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))
81		op2ndg 7727	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (2nd ‘⟨𝑋, 𝑦⟩) = 𝑦)
82	53, 54, 81	syl2anc 587	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (2nd ‘⟨𝑋, 𝑦⟩) = 𝑦)
83		op2ndg 7727	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → (2nd ‘⟨𝑋, 𝑧⟩) = 𝑧)
84	53, 56, 83	syl2anc 587	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (2nd ‘⟨𝑋, 𝑧⟩) = 𝑧)
85	82, 84	oveq12d 7188	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((2nd ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐷)(2nd ‘⟨𝑋, 𝑧⟩)) = (𝑦(Hom ‘𝐷)𝑧))
86	80, 85	eleqtrrd 2836	. . . . . 6 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑔 ∈ ((2nd ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐷)(2nd ‘⟨𝑋, 𝑧⟩)))
87	72, 79, 86	fovrnd 7336	. . . . 5 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔) ∈ (((1st ‘𝐾)‘𝑦)(Hom ‘𝐸)((1st ‘𝐾)‘𝑧)))
88	50, 87	fmpt3d 6890	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦(2nd ‘𝐾)𝑧):(𝑦(Hom ‘𝐷)𝑧)⟶(((1st ‘𝐾)‘𝑦)(Hom ‘𝐸)((1st ‘𝐾)‘𝑧)))
89	3	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ Cat)
90	4	adantr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ Cat)
91		eqid 2738	. . . . . . . . 9 ⊢ (Id‘(𝐶 ×c 𝐷)) = (Id‘(𝐶 ×c 𝐷))
92	30, 89, 90, 2, 6, 10, 23, 91, 37, 38	xpcid 17555	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((Id‘(𝐶 ×c 𝐷))‘⟨𝑋, 𝑦⟩) = ⟨((Id‘𝐶)‘𝑋), ((Id‘𝐷)‘𝑦)⟩)
93	92	fveq2d 6678	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)‘((Id‘(𝐶 ×c 𝐷))‘⟨𝑋, 𝑦⟩)) = ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)‘⟨((Id‘𝐶)‘𝑋), ((Id‘𝐷)‘𝑦)⟩))
94		df-ov 7173	. . . . . . 7 ⊢ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)((Id‘𝐷)‘𝑦)) = ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)‘⟨((Id‘𝐶)‘𝑋), ((Id‘𝐷)‘𝑦)⟩)
95	93, 94	eqtr4di 2791	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)‘((Id‘(𝐶 ×c 𝐷))‘⟨𝑋, 𝑦⟩)) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)((Id‘𝐷)‘𝑦)))
96	34	adantr 484	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹))
97		opelxpi 5562	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ⟨𝑋, 𝑦⟩ ∈ (𝐴 × 𝐵))
98	7, 97	sylan 583	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ⟨𝑋, 𝑦⟩ ∈ (𝐴 × 𝐵))
99	31, 91, 24, 96, 98	funcid 17245	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)‘((Id‘(𝐶 ×c 𝐷))‘⟨𝑋, 𝑦⟩)) = ((Id‘𝐸)‘((1st ‘𝐹)‘⟨𝑋, 𝑦⟩)))
100	95, 99	eqtr3d 2775	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)((Id‘𝐷)‘𝑦)) = ((Id‘𝐸)‘((1st ‘𝐹)‘⟨𝑋, 𝑦⟩)))
101	5	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
102	6, 9, 23, 90, 38	catidcl 17056	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((Id‘𝐷)‘𝑦) ∈ (𝑦(Hom ‘𝐷)𝑦))
103	1, 2, 89, 90, 101, 6, 37, 8, 38, 9, 10, 38, 102	curf12 17593	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((𝑦(2nd ‘𝐾)𝑦)‘((Id‘𝐷)‘𝑦)) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)((Id‘𝐷)‘𝑦)))
104	1, 2, 89, 90, 101, 6, 37, 8, 38	curf11 17592	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((1st ‘𝐾)‘𝑦) = (𝑋(1st ‘𝐹)𝑦))
105	104, 65	eqtrdi 2789	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((1st ‘𝐾)‘𝑦) = ((1st ‘𝐹)‘⟨𝑋, 𝑦⟩))
106	105	fveq2d 6678	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((Id‘𝐸)‘((1st ‘𝐾)‘𝑦)) = ((Id‘𝐸)‘((1st ‘𝐹)‘⟨𝑋, 𝑦⟩)))
107	100, 103, 106	3eqtr4d 2783	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((𝑦(2nd ‘𝐾)𝑦)‘((Id‘𝐷)‘𝑦)) = ((Id‘𝐸)‘((1st ‘𝐾)‘𝑦)))
108	7	3ad2ant1 1134	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑋 ∈ 𝐴)
109		simp21 1207	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑦 ∈ 𝐵)
110		simp22 1208	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑧 ∈ 𝐵)
111		eqid 2738	. . . . . . . . . 10 ⊢ (comp‘𝐶) = (comp‘𝐶)
112		eqid 2738	. . . . . . . . . 10 ⊢ (comp‘(𝐶 ×c 𝐷)) = (comp‘(𝐶 ×c 𝐷))
113		simp23 1209	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑤 ∈ 𝐵)
114	3	3ad2ant1 1134	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐶 ∈ Cat)
115	2, 59, 10, 114, 108	catidcl 17056	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((Id‘𝐶)‘𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋))
116		simp3l 1202	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))
117		simp3r 1203	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))
118	30, 2, 6, 59, 9, 108, 109, 108, 110, 111, 25, 112, 108, 113, 115, 116, 115, 117	xpcco2 17553	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨((Id‘𝐶)‘𝑋), ℎ⟩(⟨⟨𝑋, 𝑦⟩, ⟨𝑋, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑔⟩) = ⟨(((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑋)((Id‘𝐶)‘𝑋)), (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩)
119	2, 59, 10, 114, 108, 111, 108, 115	catlid 17057	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑋)((Id‘𝐶)‘𝑋)) = ((Id‘𝐶)‘𝑋))
120	119	opeq1d 4767	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨(((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑋)((Id‘𝐶)‘𝑋)), (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩ = ⟨((Id‘𝐶)‘𝑋), (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩)
121	118, 120	eqtrd 2773	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨((Id‘𝐶)‘𝑋), ℎ⟩(⟨⟨𝑋, 𝑦⟩, ⟨𝑋, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑔⟩) = ⟨((Id‘𝐶)‘𝑋), (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩)
122	121	fveq2d 6678	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘(⟨((Id‘𝐶)‘𝑋), ℎ⟩(⟨⟨𝑋, 𝑦⟩, ⟨𝑋, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑔⟩)) = ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩))
123		df-ov 7173	. . . . . . 7 ⊢ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)) = ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩)
124	122, 123	eqtr4di 2791	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘(⟨((Id‘𝐶)‘𝑋), ℎ⟩(⟨⟨𝑋, 𝑦⟩, ⟨𝑋, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑔⟩)) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)))
125	34	3ad2ant1 1134	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹))
126	108, 109	opelxpd 5563	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑋, 𝑦⟩ ∈ (𝐴 × 𝐵))
127	108, 110	opelxpd 5563	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑋, 𝑧⟩ ∈ (𝐴 × 𝐵))
128	108, 113	opelxpd 5563	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑋, 𝑤⟩ ∈ (𝐴 × 𝐵))
129	115, 116	opelxpd 5563	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), 𝑔⟩ ∈ ((𝑋(Hom ‘𝐶)𝑋) × (𝑦(Hom ‘𝐷)𝑧)))
130	30, 2, 6, 59, 9, 108, 109, 108, 110, 51	xpchom2 17552	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑋, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑧⟩) = ((𝑋(Hom ‘𝐶)𝑋) × (𝑦(Hom ‘𝐷)𝑧)))
131	129, 130	eleqtrrd 2836	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), 𝑔⟩ ∈ (⟨𝑋, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑧⟩))
132	115, 117	opelxpd 5563	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), ℎ⟩ ∈ ((𝑋(Hom ‘𝐶)𝑋) × (𝑧(Hom ‘𝐷)𝑤)))
133	30, 2, 6, 59, 9, 108, 110, 108, 113, 51	xpchom2 17552	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩) = ((𝑋(Hom ‘𝐶)𝑋) × (𝑧(Hom ‘𝐷)𝑤)))
134	132, 133	eleqtrrd 2836	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), ℎ⟩ ∈ (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩))
135	31, 51, 112, 26, 125, 126, 127, 128, 131, 134	funcco 17246	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘(⟨((Id‘𝐶)‘𝑋), ℎ⟩(⟨⟨𝑋, 𝑦⟩, ⟨𝑋, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑔⟩)) = (((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), ℎ⟩)(⟨((1st ‘𝐹)‘⟨𝑋, 𝑦⟩), ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)⟩(comp‘𝐸)((1st ‘𝐹)‘⟨𝑋, 𝑤⟩))((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑔⟩)))
136	124, 135	eqtr3d 2775	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)) = (((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), ℎ⟩)(⟨((1st ‘𝐹)‘⟨𝑋, 𝑦⟩), ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)⟩(comp‘𝐸)((1st ‘𝐹)‘⟨𝑋, 𝑤⟩))((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑔⟩)))
137	4	3ad2ant1 1134	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐷 ∈ Cat)
138	5	3ad2ant1 1134	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
139	6, 9, 25, 137, 109, 110, 113, 116, 117	catcocl 17059	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐷)𝑤))
140	1, 2, 114, 137, 138, 6, 108, 8, 109, 9, 10, 113, 139	curf12 17593	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑦(2nd ‘𝐾)𝑤)‘(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)))
141	1, 2, 114, 137, 138, 6, 108, 8, 109	curf11 17592	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘𝐾)‘𝑦) = (𝑋(1st ‘𝐹)𝑦))
142	141, 65	eqtrdi 2789	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘𝐾)‘𝑦) = ((1st ‘𝐹)‘⟨𝑋, 𝑦⟩))
143	1, 2, 114, 137, 138, 6, 108, 8, 110	curf11 17592	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘𝐾)‘𝑧) = (𝑋(1st ‘𝐹)𝑧))
144	143, 68	eqtrdi 2789	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘𝐾)‘𝑧) = ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩))
145	142, 144	opeq12d 4769	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((1st ‘𝐾)‘𝑦), ((1st ‘𝐾)‘𝑧)⟩ = ⟨((1st ‘𝐹)‘⟨𝑋, 𝑦⟩), ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)⟩)
146	1, 2, 114, 137, 138, 6, 108, 8, 113	curf11 17592	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘𝐾)‘𝑤) = (𝑋(1st ‘𝐹)𝑤))
147		df-ov 7173	. . . . . . . 8 ⊢ (𝑋(1st ‘𝐹)𝑤) = ((1st ‘𝐹)‘⟨𝑋, 𝑤⟩)
148	146, 147	eqtrdi 2789	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘𝐾)‘𝑤) = ((1st ‘𝐹)‘⟨𝑋, 𝑤⟩))
149	145, 148	oveq12d 7188	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨((1st ‘𝐾)‘𝑦), ((1st ‘𝐾)‘𝑧)⟩(comp‘𝐸)((1st ‘𝐾)‘𝑤)) = (⟨((1st ‘𝐹)‘⟨𝑋, 𝑦⟩), ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)⟩(comp‘𝐸)((1st ‘𝐹)‘⟨𝑋, 𝑤⟩)))
150	1, 2, 114, 137, 138, 6, 108, 8, 110, 9, 10, 113, 117	curf12 17593	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘𝐾)𝑤)‘ℎ) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)ℎ))
151		df-ov 7173	. . . . . . 7 ⊢ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)ℎ) = ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), ℎ⟩)
152	150, 151	eqtrdi 2789	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘𝐾)𝑤)‘ℎ) = ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), ℎ⟩))
153	1, 2, 114, 137, 138, 6, 108, 8, 109, 9, 10, 110, 116	curf12 17593	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑦(2nd ‘𝐾)𝑧)‘𝑔) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔))
154		df-ov 7173	. . . . . . 7 ⊢ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔) = ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑔⟩)
155	153, 154	eqtrdi 2789	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑦(2nd ‘𝐾)𝑧)‘𝑔) = ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑔⟩))
156	149, 152, 155	oveq123d 7191	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((𝑧(2nd ‘𝐾)𝑤)‘ℎ)(⟨((1st ‘𝐾)‘𝑦), ((1st ‘𝐾)‘𝑧)⟩(comp‘𝐸)((1st ‘𝐾)‘𝑤))((𝑦(2nd ‘𝐾)𝑧)‘𝑔)) = (((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), ℎ⟩)(⟨((1st ‘𝐹)‘⟨𝑋, 𝑦⟩), ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)⟩(comp‘𝐸)((1st ‘𝐹)‘⟨𝑋, 𝑤⟩))((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑔⟩)))
157	136, 140, 156	3eqtr4d 2783	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑦(2nd ‘𝐾)𝑤)‘(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)) = (((𝑧(2nd ‘𝐾)𝑤)‘ℎ)(⟨((1st ‘𝐾)‘𝑦), ((1st ‘𝐾)‘𝑧)⟩(comp‘𝐸)((1st ‘𝐾)‘𝑤))((𝑦(2nd ‘𝐾)𝑧)‘𝑔)))
158	6, 21, 9, 22, 23, 24, 25, 26, 4, 29, 40, 46, 88, 107, 157	isfuncd 17240	. . 3 ⊢ (𝜑 → (1st ‘𝐾)(𝐷 Func 𝐸)(2nd ‘𝐾))
159		df-br 5031	. . 3 ⊢ ((1st ‘𝐾)(𝐷 Func 𝐸)(2nd ‘𝐾) ↔ ⟨(1st ‘𝐾), (2nd ‘𝐾)⟩ ∈ (𝐷 Func 𝐸))
160	158, 159	sylib 221	. 2 ⊢ (𝜑 → ⟨(1st ‘𝐾), (2nd ‘𝐾)⟩ ∈ (𝐷 Func 𝐸))
161	20, 160	eqeltrd 2833	1 ⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐸))

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1088   = wceq 1542   ∈ wcel 2114  Vcvv 3398  ⟨cop 4522   class class class wbr 5030   ↦ cmpt 5110   × cxp 5523  Rel wrel 5530   Fn wfn 6334  ⟶wf 6335  ‘cfv 6339  (class class class)co 7170   ∈ cmpo 7172  1^st c1st 7712  2^nd c2nd 7713  Basecbs 16586  Hom chom 16679  compcco 16680  Catccat 17038  Idccid 17039   Func cfunc 17229   ×_c cxpc 17534   curry_F ccurf 17576

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7479  ax-cnex 10671  ax-resscn 10672  ax-1cn 10673  ax-icn 10674  ax-addcl 10675  ax-addrcl 10676  ax-mulcl 10677  ax-mulrcl 10678  ax-mulcom 10679  ax-addass 10680  ax-mulass 10681  ax-distr 10682  ax-i2m1 10683  ax-1ne0 10684  ax-1rid 10685  ax-rnegex 10686  ax-rrecex 10687  ax-cnre 10688  ax-pre-lttri 10689  ax-pre-lttrn 10690  ax-pre-ltadd 10691  ax-pre-mulgt0 10692

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3400  df-sbc 3681  df-csb 3791  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-pss 3862  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-tp 4521  df-op 4523  df-uni 4797  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5483  df-we 5485  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6129  df-ord 6175  df-on 6176  df-lim 6177  df-suc 6178  df-iota 6297  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-riota 7127  df-ov 7173  df-oprab 7174  df-mpo 7175  df-om 7600  df-1st 7714  df-2nd 7715  df-wrecs 7976  df-recs 8037  df-rdg 8075  df-1o 8131  df-er 8320  df-map 8439  df-ixp 8508  df-en 8556  df-dom 8557  df-sdom 8558  df-fin 8559  df-pnf 10755  df-mnf 10756  df-xr 10757  df-ltxr 10758  df-le 10759  df-sub 10950  df-neg 10951  df-nn 11717  df-2 11779  df-3 11780  df-4 11781  df-5 11782  df-6 11783  df-7 11784  df-8 11785  df-9 11786  df-n0 11977  df-z 12063  df-dec 12180  df-uz 12325  df-fz 12982  df-struct 16588  df-ndx 16589  df-slot 16590  df-base 16592  df-hom 16692  df-cco 16693  df-cat 17042  df-cid 17043  df-func 17233  df-xpc 17538  df-curf 17580

This theorem is referenced by:  curf2cl  17597  curfcl  17598