Theorem curf1cl 18117

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 2736	. . . 4 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
10		eqid 2736	. . . 4 ⊢ (Id‘𝐶) = (Id‘𝐶)
11	1, 2, 3, 4, 5, 6, 7, 8, 9, 10	curf1 18114	. . 3 ⊢ (𝜑 → 𝐾 = ⟨(𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))⟩)
12	6	fvexi 6856	. . . . . . 7 ⊢ 𝐵 ∈ V
13	12	mptex 7173	. . . . . 6 ⊢ (𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)) ∈ V
14	12, 12	mpoex 8012	. . . . . 6 ⊢ (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔))) ∈ V
15	13, 14	op1std 7931	. . . . 5 ⊢ (𝐾 = ⟨(𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))⟩ → (1st ‘𝐾) = (𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)))
16	11, 15	syl 17	. . . 4 ⊢ (𝜑 → (1st ‘𝐾) = (𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)))
17	13, 14	op2ndd 7932	. . . . 5 ⊢ (𝐾 = ⟨(𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))⟩ → (2nd ‘𝐾) = (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔))))
18	11, 17	syl 17	. . . 4 ⊢ (𝜑 → (2nd ‘𝐾) = (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔))))
19	16, 18	opeq12d 4838	. . 3 ⊢ (𝜑 → ⟨(1st ‘𝐾), (2nd ‘𝐾)⟩ = ⟨(𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))⟩)
20	11, 19	eqtr4d 2779	. 2 ⊢ (𝜑 → 𝐾 = ⟨(1st ‘𝐾), (2nd ‘𝐾)⟩)
21		eqid 2736	. . . 4 ⊢ (Base‘𝐸) = (Base‘𝐸)
22		eqid 2736	. . . 4 ⊢ (Hom ‘𝐸) = (Hom ‘𝐸)
23		eqid 2736	. . . 4 ⊢ (Id‘𝐷) = (Id‘𝐷)
24		eqid 2736	. . . 4 ⊢ (Id‘𝐸) = (Id‘𝐸)
25		eqid 2736	. . . 4 ⊢ (comp‘𝐷) = (comp‘𝐷)
26		eqid 2736	. . . 4 ⊢ (comp‘𝐸) = (comp‘𝐸)
27		funcrcl 17749	. . . . . 6 ⊢ (𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸) → ((𝐶 ×c 𝐷) ∈ Cat ∧ 𝐸 ∈ Cat))
28	5, 27	syl 17	. . . . 5 ⊢ (𝜑 → ((𝐶 ×c 𝐷) ∈ Cat ∧ 𝐸 ∈ Cat))
29	28	simprd 496	. . . 4 ⊢ (𝜑 → 𝐸 ∈ Cat)
30		eqid 2736	. . . . . . . . 9 ⊢ (𝐶 ×c 𝐷) = (𝐶 ×c 𝐷)
31	30, 2, 6	xpcbas 18066	. . . . . . . 8 ⊢ (𝐴 × 𝐵) = (Base‘(𝐶 ×c 𝐷))
32		relfunc 17748	. . . . . . . . 9 ⊢ Rel ((𝐶 ×c 𝐷) Func 𝐸)
33		1st2ndbr 7974	. . . . . . . . 9 ⊢ ((Rel ((𝐶 ×c 𝐷) Func 𝐸) ∧ 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹))
34	32, 5, 33	sylancr 587	. . . . . . . 8 ⊢ (𝜑 → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹))
35	31, 21, 34	funcf1 17752	. . . . . . 7 ⊢ (𝜑 → (1st ‘𝐹):(𝐴 × 𝐵)⟶(Base‘𝐸))
36	35	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1st ‘𝐹):(𝐴 × 𝐵)⟶(Base‘𝐸))
37	7	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑋 ∈ 𝐴)
38		simpr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵)
39	36, 37, 38	fovcdmd 7526	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑋(1st ‘𝐹)𝑦) ∈ (Base‘𝐸))
40	16, 39	fmpt3d 7064	. . . 4 ⊢ (𝜑 → (1st ‘𝐾):𝐵⟶(Base‘𝐸))
41		eqid 2736	. . . . . 6 ⊢ (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔))) = (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))
42		ovex 7390	. . . . . . 7 ⊢ (𝑦(Hom ‘𝐷)𝑧) ∈ V
43	42	mptex 7173	. . . . . 6 ⊢ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)) ∈ V
44	41, 43	fnmpoi 8002	. . . . 5 ⊢ (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔))) Fn (𝐵 × 𝐵)
45	18	fneq1d 6595	. . . . 5 ⊢ (𝜑 → ((2nd ‘𝐾) Fn (𝐵 × 𝐵) ↔ (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔))) Fn (𝐵 × 𝐵)))
46	44, 45	mpbiri 257	. . . 4 ⊢ (𝜑 → (2nd ‘𝐾) Fn (𝐵 × 𝐵))
47	18	oveqd 7374	. . . . . 6 ⊢ (𝜑 → (𝑦(2nd ‘𝐾)𝑧) = (𝑦(𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))𝑧))
48	41	ovmpt4g 7502	. . . . . . 7 ⊢ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)) ∈ V) → (𝑦(𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))𝑧) = (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))
49	43, 48	mp3an3 1450	. . . . . 6 ⊢ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝑦(𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))𝑧) = (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))
50	47, 49	sylan9eq 2796	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦(2nd ‘𝐾)𝑧) = (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))
51		eqid 2736	. . . . . . . 8 ⊢ (Hom ‘(𝐶 ×c 𝐷)) = (Hom ‘(𝐶 ×c 𝐷))
52	34	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹))
53	7	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑋 ∈ 𝐴)
54		simplrl 775	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑦 ∈ 𝐵)
55	53, 54	opelxpd 5671	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ⟨𝑋, 𝑦⟩ ∈ (𝐴 × 𝐵))
56		simplrr 776	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑧 ∈ 𝐵)
57	53, 56	opelxpd 5671	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ⟨𝑋, 𝑧⟩ ∈ (𝐴 × 𝐵))
58	31, 51, 22, 52, 55, 57	funcf2 17754	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩):(⟨𝑋, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑧⟩)⟶(((1st ‘𝐹)‘⟨𝑋, 𝑦⟩)(Hom ‘𝐸)((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)))
59		eqid 2736	. . . . . . . . 9 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
60	30, 31, 59, 9, 51, 55, 57	xpchom 18068	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (⟨𝑋, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑧⟩) = (((1st ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐶)(1st ‘⟨𝑋, 𝑧⟩)) × ((2nd ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐷)(2nd ‘⟨𝑋, 𝑧⟩))))
61	3	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝐶 ∈ Cat)
62	4	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝐷 ∈ Cat)
63	5	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
64	1, 2, 61, 62, 63, 6, 53, 8, 54	curf11 18115	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st ‘𝐾)‘𝑦) = (𝑋(1st ‘𝐹)𝑦))
65		df-ov 7360	. . . . . . . . . 10 ⊢ (𝑋(1st ‘𝐹)𝑦) = ((1st ‘𝐹)‘⟨𝑋, 𝑦⟩)
66	64, 65	eqtr2di 2793	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st ‘𝐹)‘⟨𝑋, 𝑦⟩) = ((1st ‘𝐾)‘𝑦))
67	1, 2, 61, 62, 63, 6, 53, 8, 56	curf11 18115	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st ‘𝐾)‘𝑧) = (𝑋(1st ‘𝐹)𝑧))
68		df-ov 7360	. . . . . . . . . 10 ⊢ (𝑋(1st ‘𝐹)𝑧) = ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)
69	67, 68	eqtr2di 2793	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩) = ((1st ‘𝐾)‘𝑧))
70	66, 69	oveq12d 7375	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (((1st ‘𝐹)‘⟨𝑋, 𝑦⟩)(Hom ‘𝐸)((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)) = (((1st ‘𝐾)‘𝑦)(Hom ‘𝐸)((1st ‘𝐾)‘𝑧)))
71	60, 70	feq23d 6663	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩):(⟨𝑋, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑧⟩)⟶(((1st ‘𝐹)‘⟨𝑋, 𝑦⟩)(Hom ‘𝐸)((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)) ↔ (⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩):(((1st ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐶)(1st ‘⟨𝑋, 𝑧⟩)) × ((2nd ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐷)(2nd ‘⟨𝑋, 𝑧⟩)))⟶(((1st ‘𝐾)‘𝑦)(Hom ‘𝐸)((1st ‘𝐾)‘𝑧))))
72	58, 71	mpbid 231	. . . . . 6 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩):(((1st ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐶)(1st ‘⟨𝑋, 𝑧⟩)) × ((2nd ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐷)(2nd ‘⟨𝑋, 𝑧⟩)))⟶(((1st ‘𝐾)‘𝑦)(Hom ‘𝐸)((1st ‘𝐾)‘𝑧)))
73	2, 59, 10, 61, 53	catidcl 17562	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((Id‘𝐶)‘𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋))
74		op1stg 7933	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (1st ‘⟨𝑋, 𝑦⟩) = 𝑋)
75	53, 54, 74	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (1st ‘⟨𝑋, 𝑦⟩) = 𝑋)
76		op1stg 7933	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → (1st ‘⟨𝑋, 𝑧⟩) = 𝑋)
77	53, 56, 76	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (1st ‘⟨𝑋, 𝑧⟩) = 𝑋)
78	75, 77	oveq12d 7375	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐶)(1st ‘⟨𝑋, 𝑧⟩)) = (𝑋(Hom ‘𝐶)𝑋))
79	73, 78	eleqtrrd 2841	. . . . . 6 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((Id‘𝐶)‘𝑋) ∈ ((1st ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐶)(1st ‘⟨𝑋, 𝑧⟩)))
80		simpr 485	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))
81		op2ndg 7934	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (2nd ‘⟨𝑋, 𝑦⟩) = 𝑦)
82	53, 54, 81	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (2nd ‘⟨𝑋, 𝑦⟩) = 𝑦)
83		op2ndg 7934	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → (2nd ‘⟨𝑋, 𝑧⟩) = 𝑧)
84	53, 56, 83	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (2nd ‘⟨𝑋, 𝑧⟩) = 𝑧)
85	82, 84	oveq12d 7375	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((2nd ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐷)(2nd ‘⟨𝑋, 𝑧⟩)) = (𝑦(Hom ‘𝐷)𝑧))
86	80, 85	eleqtrrd 2841	. . . . . 6 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑔 ∈ ((2nd ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐷)(2nd ‘⟨𝑋, 𝑧⟩)))
87	72, 79, 86	fovcdmd 7526	. . . . 5 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔) ∈ (((1st ‘𝐾)‘𝑦)(Hom ‘𝐸)((1st ‘𝐾)‘𝑧)))
88	50, 87	fmpt3d 7064	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦(2nd ‘𝐾)𝑧):(𝑦(Hom ‘𝐷)𝑧)⟶(((1st ‘𝐾)‘𝑦)(Hom ‘𝐸)((1st ‘𝐾)‘𝑧)))
89	3	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ Cat)
90	4	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ Cat)
91		eqid 2736	. . . . . . . . 9 ⊢ (Id‘(𝐶 ×c 𝐷)) = (Id‘(𝐶 ×c 𝐷))
92	30, 89, 90, 2, 6, 10, 23, 91, 37, 38	xpcid 18077	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((Id‘(𝐶 ×c 𝐷))‘⟨𝑋, 𝑦⟩) = ⟨((Id‘𝐶)‘𝑋), ((Id‘𝐷)‘𝑦)⟩)
93	92	fveq2d 6846	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)‘((Id‘(𝐶 ×c 𝐷))‘⟨𝑋, 𝑦⟩)) = ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)‘⟨((Id‘𝐶)‘𝑋), ((Id‘𝐷)‘𝑦)⟩))
94		df-ov 7360	. . . . . . 7 ⊢ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)((Id‘𝐷)‘𝑦)) = ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)‘⟨((Id‘𝐶)‘𝑋), ((Id‘𝐷)‘𝑦)⟩)
95	93, 94	eqtr4di 2794	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)‘((Id‘(𝐶 ×c 𝐷))‘⟨𝑋, 𝑦⟩)) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)((Id‘𝐷)‘𝑦)))
96	34	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹))
97		opelxpi 5670	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ⟨𝑋, 𝑦⟩ ∈ (𝐴 × 𝐵))
98	7, 97	sylan 580	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ⟨𝑋, 𝑦⟩ ∈ (𝐴 × 𝐵))
99	31, 91, 24, 96, 98	funcid 17756	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)‘((Id‘(𝐶 ×c 𝐷))‘⟨𝑋, 𝑦⟩)) = ((Id‘𝐸)‘((1st ‘𝐹)‘⟨𝑋, 𝑦⟩)))
100	95, 99	eqtr3d 2778	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)((Id‘𝐷)‘𝑦)) = ((Id‘𝐸)‘((1st ‘𝐹)‘⟨𝑋, 𝑦⟩)))
101	5	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
102	6, 9, 23, 90, 38	catidcl 17562	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((Id‘𝐷)‘𝑦) ∈ (𝑦(Hom ‘𝐷)𝑦))
103	1, 2, 89, 90, 101, 6, 37, 8, 38, 9, 10, 38, 102	curf12 18116	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((𝑦(2nd ‘𝐾)𝑦)‘((Id‘𝐷)‘𝑦)) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)((Id‘𝐷)‘𝑦)))
104	1, 2, 89, 90, 101, 6, 37, 8, 38	curf11 18115	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((1st ‘𝐾)‘𝑦) = (𝑋(1st ‘𝐹)𝑦))
105	104, 65	eqtrdi 2792	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((1st ‘𝐾)‘𝑦) = ((1st ‘𝐹)‘⟨𝑋, 𝑦⟩))
106	105	fveq2d 6846	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((Id‘𝐸)‘((1st ‘𝐾)‘𝑦)) = ((Id‘𝐸)‘((1st ‘𝐹)‘⟨𝑋, 𝑦⟩)))
107	100, 103, 106	3eqtr4d 2786	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((𝑦(2nd ‘𝐾)𝑦)‘((Id‘𝐷)‘𝑦)) = ((Id‘𝐸)‘((1st ‘𝐾)‘𝑦)))
108	7	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑋 ∈ 𝐴)
109		simp21 1206	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑦 ∈ 𝐵)
110		simp22 1207	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑧 ∈ 𝐵)
111		eqid 2736	. . . . . . . . . 10 ⊢ (comp‘𝐶) = (comp‘𝐶)
112		eqid 2736	. . . . . . . . . 10 ⊢ (comp‘(𝐶 ×c 𝐷)) = (comp‘(𝐶 ×c 𝐷))
113		simp23 1208	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑤 ∈ 𝐵)
114	3	3ad2ant1 1133	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐶 ∈ Cat)
115	2, 59, 10, 114, 108	catidcl 17562	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((Id‘𝐶)‘𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋))
116		simp3l 1201	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))
117		simp3r 1202	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))
118	30, 2, 6, 59, 9, 108, 109, 108, 110, 111, 25, 112, 108, 113, 115, 116, 115, 117	xpcco2 18075	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨((Id‘𝐶)‘𝑋), ℎ⟩(⟨⟨𝑋, 𝑦⟩, ⟨𝑋, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑔⟩) = ⟨(((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑋)((Id‘𝐶)‘𝑋)), (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩)
119	2, 59, 10, 114, 108, 111, 108, 115	catlid 17563	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑋)((Id‘𝐶)‘𝑋)) = ((Id‘𝐶)‘𝑋))
120	119	opeq1d 4836	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨(((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑋)((Id‘𝐶)‘𝑋)), (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩ = ⟨((Id‘𝐶)‘𝑋), (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩)
121	118, 120	eqtrd 2776	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨((Id‘𝐶)‘𝑋), ℎ⟩(⟨⟨𝑋, 𝑦⟩, ⟨𝑋, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑔⟩) = ⟨((Id‘𝐶)‘𝑋), (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩)
122	121	fveq2d 6846	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘(⟨((Id‘𝐶)‘𝑋), ℎ⟩(⟨⟨𝑋, 𝑦⟩, ⟨𝑋, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑔⟩)) = ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩))
123		df-ov 7360	. . . . . . 7 ⊢ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)) = ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩)
124	122, 123	eqtr4di 2794	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘(⟨((Id‘𝐶)‘𝑋), ℎ⟩(⟨⟨𝑋, 𝑦⟩, ⟨𝑋, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑔⟩)) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)))
125	34	3ad2ant1 1133	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹))
126	108, 109	opelxpd 5671	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑋, 𝑦⟩ ∈ (𝐴 × 𝐵))
127	108, 110	opelxpd 5671	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑋, 𝑧⟩ ∈ (𝐴 × 𝐵))
128	108, 113	opelxpd 5671	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑋, 𝑤⟩ ∈ (𝐴 × 𝐵))
129	115, 116	opelxpd 5671	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), 𝑔⟩ ∈ ((𝑋(Hom ‘𝐶)𝑋) × (𝑦(Hom ‘𝐷)𝑧)))
130	30, 2, 6, 59, 9, 108, 109, 108, 110, 51	xpchom2 18074	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑋, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑧⟩) = ((𝑋(Hom ‘𝐶)𝑋) × (𝑦(Hom ‘𝐷)𝑧)))
131	129, 130	eleqtrrd 2841	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), 𝑔⟩ ∈ (⟨𝑋, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑧⟩))
132	115, 117	opelxpd 5671	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), ℎ⟩ ∈ ((𝑋(Hom ‘𝐶)𝑋) × (𝑧(Hom ‘𝐷)𝑤)))
133	30, 2, 6, 59, 9, 108, 110, 108, 113, 51	xpchom2 18074	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩) = ((𝑋(Hom ‘𝐶)𝑋) × (𝑧(Hom ‘𝐷)𝑤)))
134	132, 133	eleqtrrd 2841	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), ℎ⟩ ∈ (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩))
135	31, 51, 112, 26, 125, 126, 127, 128, 131, 134	funcco 17757	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘(⟨((Id‘𝐶)‘𝑋), ℎ⟩(⟨⟨𝑋, 𝑦⟩, ⟨𝑋, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑔⟩)) = (((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), ℎ⟩)(⟨((1st ‘𝐹)‘⟨𝑋, 𝑦⟩), ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)⟩(comp‘𝐸)((1st ‘𝐹)‘⟨𝑋, 𝑤⟩))((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑔⟩)))
136	124, 135	eqtr3d 2778	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)) = (((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), ℎ⟩)(⟨((1st ‘𝐹)‘⟨𝑋, 𝑦⟩), ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)⟩(comp‘𝐸)((1st ‘𝐹)‘⟨𝑋, 𝑤⟩))((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑔⟩)))
137	4	3ad2ant1 1133	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐷 ∈ Cat)
138	5	3ad2ant1 1133	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
139	6, 9, 25, 137, 109, 110, 113, 116, 117	catcocl 17565	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐷)𝑤))
140	1, 2, 114, 137, 138, 6, 108, 8, 109, 9, 10, 113, 139	curf12 18116	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑦(2nd ‘𝐾)𝑤)‘(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)))
141	1, 2, 114, 137, 138, 6, 108, 8, 109	curf11 18115	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘𝐾)‘𝑦) = (𝑋(1st ‘𝐹)𝑦))
142	141, 65	eqtrdi 2792	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘𝐾)‘𝑦) = ((1st ‘𝐹)‘⟨𝑋, 𝑦⟩))
143	1, 2, 114, 137, 138, 6, 108, 8, 110	curf11 18115	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘𝐾)‘𝑧) = (𝑋(1st ‘𝐹)𝑧))
144	143, 68	eqtrdi 2792	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘𝐾)‘𝑧) = ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩))
145	142, 144	opeq12d 4838	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((1st ‘𝐾)‘𝑦), ((1st ‘𝐾)‘𝑧)⟩ = ⟨((1st ‘𝐹)‘⟨𝑋, 𝑦⟩), ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)⟩)
146	1, 2, 114, 137, 138, 6, 108, 8, 113	curf11 18115	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘𝐾)‘𝑤) = (𝑋(1st ‘𝐹)𝑤))
147		df-ov 7360	. . . . . . . 8 ⊢ (𝑋(1st ‘𝐹)𝑤) = ((1st ‘𝐹)‘⟨𝑋, 𝑤⟩)
148	146, 147	eqtrdi 2792	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘𝐾)‘𝑤) = ((1st ‘𝐹)‘⟨𝑋, 𝑤⟩))
149	145, 148	oveq12d 7375	. . . . . 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 18116	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘𝐾)𝑤)‘ℎ) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)ℎ))
151		df-ov 7360	. . . . . . 7 ⊢ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)ℎ) = ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), ℎ⟩)
152	150, 151	eqtrdi 2792	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘𝐾)𝑤)‘ℎ) = ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), ℎ⟩))
153	1, 2, 114, 137, 138, 6, 108, 8, 109, 9, 10, 110, 116	curf12 18116	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑦(2nd ‘𝐾)𝑧)‘𝑔) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔))
154		df-ov 7360	. . . . . . 7 ⊢ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔) = ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑔⟩)
155	153, 154	eqtrdi 2792	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑦(2nd ‘𝐾)𝑧)‘𝑔) = ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑔⟩))
156	149, 152, 155	oveq123d 7378	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((𝑧(2nd ‘𝐾)𝑤)‘ℎ)(⟨((1st ‘𝐾)‘𝑦), ((1st ‘𝐾)‘𝑧)⟩(comp‘𝐸)((1st ‘𝐾)‘𝑤))((𝑦(2nd ‘𝐾)𝑧)‘𝑔)) = (((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), ℎ⟩)(⟨((1st ‘𝐹)‘⟨𝑋, 𝑦⟩), ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)⟩(comp‘𝐸)((1st ‘𝐹)‘⟨𝑋, 𝑤⟩))((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑔⟩)))
157	136, 140, 156	3eqtr4d 2786	. . . 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 17751	. . 3 ⊢ (𝜑 → (1st ‘𝐾)(𝐷 Func 𝐸)(2nd ‘𝐾))
159		df-br 5106	. . 3 ⊢ ((1st ‘𝐾)(𝐷 Func 𝐸)(2nd ‘𝐾) ↔ ⟨(1st ‘𝐾), (2nd ‘𝐾)⟩ ∈ (𝐷 Func 𝐸))
160	158, 159	sylib 217	. 2 ⊢ (𝜑 → ⟨(1st ‘𝐾), (2nd ‘𝐾)⟩ ∈ (𝐷 Func 𝐸))
161	20, 160	eqeltrd 2838	1 ⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐸))

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  Vcvv 3445  ⟨cop 4592   class class class wbr 5105   ↦ cmpt 5188   × cxp 5631  Rel wrel 5638   Fn wfn 6491  ⟶wf 6492  ‘cfv 6496  (class class class)co 7357   ∈ cmpo 7359  1^st c1st 7919  2^nd c2nd 7920  Basecbs 17083  Hom chom 17144  compcco 17145  Catccat 17544  Idccid 17545   Func cfunc 17740   ×_c cxpc 18056   curry_F ccurf 18099

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  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  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-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  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-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-map 8767  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-fz 13425  df-struct 17019  df-slot 17054  df-ndx 17066  df-base 17084  df-hom 17157  df-cco 17158  df-cat 17548  df-cid 17549  df-func 17744  df-xpc 18060  df-curf 18103

This theorem is referenced by:  curf2cl  18120  curfcl  18121