Theorem curf1cl 18129

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 2731	. . . 4 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
10		eqid 2731	. . . 4 ⊢ (Id‘𝐶) = (Id‘𝐶)
11	1, 2, 3, 4, 5, 6, 7, 8, 9, 10	curf1 18126	. . 3 ⊢ (𝜑 → 𝐾 = ⟨(𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))⟩)
12	6	fvexi 6831	. . . . . . 7 ⊢ 𝐵 ∈ V
13	12	mptex 7152	. . . . . 6 ⊢ (𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)) ∈ V
14	12, 12	mpoex 8006	. . . . . 6 ⊢ (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔))) ∈ V
15	13, 14	op1std 7926	. . . . 5 ⊢ (𝐾 = ⟨(𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))⟩ → (1st ‘𝐾) = (𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)))
16	11, 15	syl 17	. . . 4 ⊢ (𝜑 → (1st ‘𝐾) = (𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)))
17	13, 14	op2ndd 7927	. . . . 5 ⊢ (𝐾 = ⟨(𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))⟩ → (2nd ‘𝐾) = (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔))))
18	11, 17	syl 17	. . . 4 ⊢ (𝜑 → (2nd ‘𝐾) = (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔))))
19	16, 18	opeq12d 4828	. . 3 ⊢ (𝜑 → ⟨(1st ‘𝐾), (2nd ‘𝐾)⟩ = ⟨(𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))⟩)
20	11, 19	eqtr4d 2769	. 2 ⊢ (𝜑 → 𝐾 = ⟨(1st ‘𝐾), (2nd ‘𝐾)⟩)
21		eqid 2731	. . . 4 ⊢ (Base‘𝐸) = (Base‘𝐸)
22		eqid 2731	. . . 4 ⊢ (Hom ‘𝐸) = (Hom ‘𝐸)
23		eqid 2731	. . . 4 ⊢ (Id‘𝐷) = (Id‘𝐷)
24		eqid 2731	. . . 4 ⊢ (Id‘𝐸) = (Id‘𝐸)
25		eqid 2731	. . . 4 ⊢ (comp‘𝐷) = (comp‘𝐷)
26		eqid 2731	. . . 4 ⊢ (comp‘𝐸) = (comp‘𝐸)
27		funcrcl 17765	. . . . . 6 ⊢ (𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸) → ((𝐶 ×c 𝐷) ∈ Cat ∧ 𝐸 ∈ Cat))
28	5, 27	syl 17	. . . . 5 ⊢ (𝜑 → ((𝐶 ×c 𝐷) ∈ Cat ∧ 𝐸 ∈ Cat))
29	28	simprd 495	. . . 4 ⊢ (𝜑 → 𝐸 ∈ Cat)
30		eqid 2731	. . . . . . . . 9 ⊢ (𝐶 ×c 𝐷) = (𝐶 ×c 𝐷)
31	30, 2, 6	xpcbas 18079	. . . . . . . 8 ⊢ (𝐴 × 𝐵) = (Base‘(𝐶 ×c 𝐷))
32		relfunc 17764	. . . . . . . . 9 ⊢ Rel ((𝐶 ×c 𝐷) Func 𝐸)
33		1st2ndbr 7969	. . . . . . . . 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 17768	. . . . . . 7 ⊢ (𝜑 → (1st ‘𝐹):(𝐴 × 𝐵)⟶(Base‘𝐸))
36	35	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1st ‘𝐹):(𝐴 × 𝐵)⟶(Base‘𝐸))
37	7	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑋 ∈ 𝐴)
38		simpr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵)
39	36, 37, 38	fovcdmd 7513	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑋(1st ‘𝐹)𝑦) ∈ (Base‘𝐸))
40	16, 39	fmpt3d 7044	. . . 4 ⊢ (𝜑 → (1st ‘𝐾):𝐵⟶(Base‘𝐸))
41		eqid 2731	. . . . . 6 ⊢ (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔))) = (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))
42		ovex 7374	. . . . . . 7 ⊢ (𝑦(Hom ‘𝐷)𝑧) ∈ V
43	42	mptex 7152	. . . . . 6 ⊢ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)) ∈ V
44	41, 43	fnmpoi 7997	. . . . 5 ⊢ (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔))) Fn (𝐵 × 𝐵)
45	18	fneq1d 6569	. . . . 5 ⊢ (𝜑 → ((2nd ‘𝐾) Fn (𝐵 × 𝐵) ↔ (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔))) Fn (𝐵 × 𝐵)))
46	44, 45	mpbiri 258	. . . 4 ⊢ (𝜑 → (2nd ‘𝐾) Fn (𝐵 × 𝐵))
47	18	oveqd 7358	. . . . . 6 ⊢ (𝜑 → (𝑦(2nd ‘𝐾)𝑧) = (𝑦(𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))𝑧))
48	41	ovmpt4g 7488	. . . . . . 7 ⊢ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)) ∈ V) → (𝑦(𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))𝑧) = (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))
49	43, 48	mp3an3 1452	. . . . . 6 ⊢ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝑦(𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))𝑧) = (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))
50	47, 49	sylan9eq 2786	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦(2nd ‘𝐾)𝑧) = (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))
51		eqid 2731	. . . . . . . 8 ⊢ (Hom ‘(𝐶 ×c 𝐷)) = (Hom ‘(𝐶 ×c 𝐷))
52	34	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹))
53	7	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑋 ∈ 𝐴)
54		simplrl 776	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑦 ∈ 𝐵)
55	53, 54	opelxpd 5650	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ⟨𝑋, 𝑦⟩ ∈ (𝐴 × 𝐵))
56		simplrr 777	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑧 ∈ 𝐵)
57	53, 56	opelxpd 5650	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ⟨𝑋, 𝑧⟩ ∈ (𝐴 × 𝐵))
58	31, 51, 22, 52, 55, 57	funcf2 17770	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩):(⟨𝑋, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑧⟩)⟶(((1st ‘𝐹)‘⟨𝑋, 𝑦⟩)(Hom ‘𝐸)((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)))
59		eqid 2731	. . . . . . . . 9 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
60	30, 31, 59, 9, 51, 55, 57	xpchom 18081	. . . . . . . 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 18127	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st ‘𝐾)‘𝑦) = (𝑋(1st ‘𝐹)𝑦))
65		df-ov 7344	. . . . . . . . . 10 ⊢ (𝑋(1st ‘𝐹)𝑦) = ((1st ‘𝐹)‘⟨𝑋, 𝑦⟩)
66	64, 65	eqtr2di 2783	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st ‘𝐹)‘⟨𝑋, 𝑦⟩) = ((1st ‘𝐾)‘𝑦))
67	1, 2, 61, 62, 63, 6, 53, 8, 56	curf11 18127	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st ‘𝐾)‘𝑧) = (𝑋(1st ‘𝐹)𝑧))
68		df-ov 7344	. . . . . . . . . 10 ⊢ (𝑋(1st ‘𝐹)𝑧) = ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)
69	67, 68	eqtr2di 2783	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩) = ((1st ‘𝐾)‘𝑧))
70	66, 69	oveq12d 7359	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (((1st ‘𝐹)‘⟨𝑋, 𝑦⟩)(Hom ‘𝐸)((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)) = (((1st ‘𝐾)‘𝑦)(Hom ‘𝐸)((1st ‘𝐾)‘𝑧)))
71	60, 70	feq23d 6641	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩):(⟨𝑋, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑧⟩)⟶(((1st ‘𝐹)‘⟨𝑋, 𝑦⟩)(Hom ‘𝐸)((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)) ↔ (⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩):(((1st ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐶)(1st ‘⟨𝑋, 𝑧⟩)) × ((2nd ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐷)(2nd ‘⟨𝑋, 𝑧⟩)))⟶(((1st ‘𝐾)‘𝑦)(Hom ‘𝐸)((1st ‘𝐾)‘𝑧))))
72	58, 71	mpbid 232	. . . . . 6 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩):(((1st ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐶)(1st ‘⟨𝑋, 𝑧⟩)) × ((2nd ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐷)(2nd ‘⟨𝑋, 𝑧⟩)))⟶(((1st ‘𝐾)‘𝑦)(Hom ‘𝐸)((1st ‘𝐾)‘𝑧)))
73	2, 59, 10, 61, 53	catidcl 17583	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((Id‘𝐶)‘𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋))
74		op1stg 7928	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (1st ‘⟨𝑋, 𝑦⟩) = 𝑋)
75	53, 54, 74	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (1st ‘⟨𝑋, 𝑦⟩) = 𝑋)
76		op1stg 7928	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → (1st ‘⟨𝑋, 𝑧⟩) = 𝑋)
77	53, 56, 76	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (1st ‘⟨𝑋, 𝑧⟩) = 𝑋)
78	75, 77	oveq12d 7359	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐶)(1st ‘⟨𝑋, 𝑧⟩)) = (𝑋(Hom ‘𝐶)𝑋))
79	73, 78	eleqtrrd 2834	. . . . . 6 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((Id‘𝐶)‘𝑋) ∈ ((1st ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐶)(1st ‘⟨𝑋, 𝑧⟩)))
80		simpr 484	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))
81		op2ndg 7929	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (2nd ‘⟨𝑋, 𝑦⟩) = 𝑦)
82	53, 54, 81	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (2nd ‘⟨𝑋, 𝑦⟩) = 𝑦)
83		op2ndg 7929	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → (2nd ‘⟨𝑋, 𝑧⟩) = 𝑧)
84	53, 56, 83	syl2anc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (2nd ‘⟨𝑋, 𝑧⟩) = 𝑧)
85	82, 84	oveq12d 7359	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((2nd ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐷)(2nd ‘⟨𝑋, 𝑧⟩)) = (𝑦(Hom ‘𝐷)𝑧))
86	80, 85	eleqtrrd 2834	. . . . . 6 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑔 ∈ ((2nd ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐷)(2nd ‘⟨𝑋, 𝑧⟩)))
87	72, 79, 86	fovcdmd 7513	. . . . 5 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔) ∈ (((1st ‘𝐾)‘𝑦)(Hom ‘𝐸)((1st ‘𝐾)‘𝑧)))
88	50, 87	fmpt3d 7044	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦(2nd ‘𝐾)𝑧):(𝑦(Hom ‘𝐷)𝑧)⟶(((1st ‘𝐾)‘𝑦)(Hom ‘𝐸)((1st ‘𝐾)‘𝑧)))
89	3	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ Cat)
90	4	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ Cat)
91		eqid 2731	. . . . . . . . 9 ⊢ (Id‘(𝐶 ×c 𝐷)) = (Id‘(𝐶 ×c 𝐷))
92	30, 89, 90, 2, 6, 10, 23, 91, 37, 38	xpcid 18090	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((Id‘(𝐶 ×c 𝐷))‘⟨𝑋, 𝑦⟩) = ⟨((Id‘𝐶)‘𝑋), ((Id‘𝐷)‘𝑦)⟩)
93	92	fveq2d 6821	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)‘((Id‘(𝐶 ×c 𝐷))‘⟨𝑋, 𝑦⟩)) = ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)‘⟨((Id‘𝐶)‘𝑋), ((Id‘𝐷)‘𝑦)⟩))
94		df-ov 7344	. . . . . . 7 ⊢ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)((Id‘𝐷)‘𝑦)) = ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)‘⟨((Id‘𝐶)‘𝑋), ((Id‘𝐷)‘𝑦)⟩)
95	93, 94	eqtr4di 2784	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)‘((Id‘(𝐶 ×c 𝐷))‘⟨𝑋, 𝑦⟩)) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)((Id‘𝐷)‘𝑦)))
96	34	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹))
97		opelxpi 5648	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ⟨𝑋, 𝑦⟩ ∈ (𝐴 × 𝐵))
98	7, 97	sylan 580	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ⟨𝑋, 𝑦⟩ ∈ (𝐴 × 𝐵))
99	31, 91, 24, 96, 98	funcid 17772	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)‘((Id‘(𝐶 ×c 𝐷))‘⟨𝑋, 𝑦⟩)) = ((Id‘𝐸)‘((1st ‘𝐹)‘⟨𝑋, 𝑦⟩)))
100	95, 99	eqtr3d 2768	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)((Id‘𝐷)‘𝑦)) = ((Id‘𝐸)‘((1st ‘𝐹)‘⟨𝑋, 𝑦⟩)))
101	5	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
102	6, 9, 23, 90, 38	catidcl 17583	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((Id‘𝐷)‘𝑦) ∈ (𝑦(Hom ‘𝐷)𝑦))
103	1, 2, 89, 90, 101, 6, 37, 8, 38, 9, 10, 38, 102	curf12 18128	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((𝑦(2nd ‘𝐾)𝑦)‘((Id‘𝐷)‘𝑦)) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)((Id‘𝐷)‘𝑦)))
104	1, 2, 89, 90, 101, 6, 37, 8, 38	curf11 18127	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((1st ‘𝐾)‘𝑦) = (𝑋(1st ‘𝐹)𝑦))
105	104, 65	eqtrdi 2782	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((1st ‘𝐾)‘𝑦) = ((1st ‘𝐹)‘⟨𝑋, 𝑦⟩))
106	105	fveq2d 6821	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((Id‘𝐸)‘((1st ‘𝐾)‘𝑦)) = ((Id‘𝐸)‘((1st ‘𝐹)‘⟨𝑋, 𝑦⟩)))
107	100, 103, 106	3eqtr4d 2776	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((𝑦(2nd ‘𝐾)𝑦)‘((Id‘𝐷)‘𝑦)) = ((Id‘𝐸)‘((1st ‘𝐾)‘𝑦)))
108	7	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑋 ∈ 𝐴)
109		simp21 1207	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑦 ∈ 𝐵)
110		simp22 1208	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑧 ∈ 𝐵)
111		eqid 2731	. . . . . . . . . 10 ⊢ (comp‘𝐶) = (comp‘𝐶)
112		eqid 2731	. . . . . . . . . 10 ⊢ (comp‘(𝐶 ×c 𝐷)) = (comp‘(𝐶 ×c 𝐷))
113		simp23 1209	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑤 ∈ 𝐵)
114	3	3ad2ant1 1133	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐶 ∈ Cat)
115	2, 59, 10, 114, 108	catidcl 17583	. . . . . . . . . 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 18088	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨((Id‘𝐶)‘𝑋), ℎ⟩(⟨⟨𝑋, 𝑦⟩, ⟨𝑋, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑔⟩) = ⟨(((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑋)((Id‘𝐶)‘𝑋)), (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩)
119	2, 59, 10, 114, 108, 111, 108, 115	catlid 17584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑋)((Id‘𝐶)‘𝑋)) = ((Id‘𝐶)‘𝑋))
120	119	opeq1d 4826	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨(((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑋)((Id‘𝐶)‘𝑋)), (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩ = ⟨((Id‘𝐶)‘𝑋), (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩)
121	118, 120	eqtrd 2766	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨((Id‘𝐶)‘𝑋), ℎ⟩(⟨⟨𝑋, 𝑦⟩, ⟨𝑋, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑔⟩) = ⟨((Id‘𝐶)‘𝑋), (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩)
122	121	fveq2d 6821	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘(⟨((Id‘𝐶)‘𝑋), ℎ⟩(⟨⟨𝑋, 𝑦⟩, ⟨𝑋, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑔⟩)) = ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩))
123		df-ov 7344	. . . . . . 7 ⊢ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)) = ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩)
124	122, 123	eqtr4di 2784	. . . . . 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 5650	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑋, 𝑦⟩ ∈ (𝐴 × 𝐵))
127	108, 110	opelxpd 5650	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑋, 𝑧⟩ ∈ (𝐴 × 𝐵))
128	108, 113	opelxpd 5650	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑋, 𝑤⟩ ∈ (𝐴 × 𝐵))
129	115, 116	opelxpd 5650	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), 𝑔⟩ ∈ ((𝑋(Hom ‘𝐶)𝑋) × (𝑦(Hom ‘𝐷)𝑧)))
130	30, 2, 6, 59, 9, 108, 109, 108, 110, 51	xpchom2 18087	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑋, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑧⟩) = ((𝑋(Hom ‘𝐶)𝑋) × (𝑦(Hom ‘𝐷)𝑧)))
131	129, 130	eleqtrrd 2834	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), 𝑔⟩ ∈ (⟨𝑋, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑧⟩))
132	115, 117	opelxpd 5650	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), ℎ⟩ ∈ ((𝑋(Hom ‘𝐶)𝑋) × (𝑧(Hom ‘𝐷)𝑤)))
133	30, 2, 6, 59, 9, 108, 110, 108, 113, 51	xpchom2 18087	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩) = ((𝑋(Hom ‘𝐶)𝑋) × (𝑧(Hom ‘𝐷)𝑤)))
134	132, 133	eleqtrrd 2834	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), ℎ⟩ ∈ (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩))
135	31, 51, 112, 26, 125, 126, 127, 128, 131, 134	funcco 17773	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘(⟨((Id‘𝐶)‘𝑋), ℎ⟩(⟨⟨𝑋, 𝑦⟩, ⟨𝑋, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑔⟩)) = (((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), ℎ⟩)(⟨((1st ‘𝐹)‘⟨𝑋, 𝑦⟩), ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)⟩(comp‘𝐸)((1st ‘𝐹)‘⟨𝑋, 𝑤⟩))((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑔⟩)))
136	124, 135	eqtr3d 2768	. . . . 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 17586	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐷)𝑤))
140	1, 2, 114, 137, 138, 6, 108, 8, 109, 9, 10, 113, 139	curf12 18128	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑦(2nd ‘𝐾)𝑤)‘(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)))
141	1, 2, 114, 137, 138, 6, 108, 8, 109	curf11 18127	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘𝐾)‘𝑦) = (𝑋(1st ‘𝐹)𝑦))
142	141, 65	eqtrdi 2782	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘𝐾)‘𝑦) = ((1st ‘𝐹)‘⟨𝑋, 𝑦⟩))
143	1, 2, 114, 137, 138, 6, 108, 8, 110	curf11 18127	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘𝐾)‘𝑧) = (𝑋(1st ‘𝐹)𝑧))
144	143, 68	eqtrdi 2782	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘𝐾)‘𝑧) = ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩))
145	142, 144	opeq12d 4828	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((1st ‘𝐾)‘𝑦), ((1st ‘𝐾)‘𝑧)⟩ = ⟨((1st ‘𝐹)‘⟨𝑋, 𝑦⟩), ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)⟩)
146	1, 2, 114, 137, 138, 6, 108, 8, 113	curf11 18127	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘𝐾)‘𝑤) = (𝑋(1st ‘𝐹)𝑤))
147		df-ov 7344	. . . . . . . 8 ⊢ (𝑋(1st ‘𝐹)𝑤) = ((1st ‘𝐹)‘⟨𝑋, 𝑤⟩)
148	146, 147	eqtrdi 2782	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘𝐾)‘𝑤) = ((1st ‘𝐹)‘⟨𝑋, 𝑤⟩))
149	145, 148	oveq12d 7359	. . . . . 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 18128	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘𝐾)𝑤)‘ℎ) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)ℎ))
151		df-ov 7344	. . . . . . 7 ⊢ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)ℎ) = ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), ℎ⟩)
152	150, 151	eqtrdi 2782	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘𝐾)𝑤)‘ℎ) = ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), ℎ⟩))
153	1, 2, 114, 137, 138, 6, 108, 8, 109, 9, 10, 110, 116	curf12 18128	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑦(2nd ‘𝐾)𝑧)‘𝑔) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔))
154		df-ov 7344	. . . . . . 7 ⊢ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔) = ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑔⟩)
155	153, 154	eqtrdi 2782	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑦(2nd ‘𝐾)𝑧)‘𝑔) = ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑔⟩))
156	149, 152, 155	oveq123d 7362	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((𝑧(2nd ‘𝐾)𝑤)‘ℎ)(⟨((1st ‘𝐾)‘𝑦), ((1st ‘𝐾)‘𝑧)⟩(comp‘𝐸)((1st ‘𝐾)‘𝑤))((𝑦(2nd ‘𝐾)𝑧)‘𝑔)) = (((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), ℎ⟩)(⟨((1st ‘𝐹)‘⟨𝑋, 𝑦⟩), ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)⟩(comp‘𝐸)((1st ‘𝐹)‘⟨𝑋, 𝑤⟩))((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑔⟩)))
157	136, 140, 156	3eqtr4d 2776	. . . 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 17767	. . 3 ⊢ (𝜑 → (1st ‘𝐾)(𝐷 Func 𝐸)(2nd ‘𝐾))
159		df-br 5087	. . 3 ⊢ ((1st ‘𝐾)(𝐷 Func 𝐸)(2nd ‘𝐾) ↔ ⟨(1st ‘𝐾), (2nd ‘𝐾)⟩ ∈ (𝐷 Func 𝐸))
160	158, 159	sylib 218	. 2 ⊢ (𝜑 → ⟨(1st ‘𝐾), (2nd ‘𝐾)⟩ ∈ (𝐷 Func 𝐸))
161	20, 160	eqeltrd 2831	1 ⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐸))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2111  Vcvv 3436  ⟨cop 4577   class class class wbr 5086   ↦ cmpt 5167   × cxp 5609  Rel wrel 5616   Fn wfn 6471  ⟶wf 6472  ‘cfv 6476  (class class class)co 7341   ∈ cmpo 7343  1^st c1st 7914  2^nd c2nd 7915  Basecbs 17115  Hom chom 17167  compcco 17168  Catccat 17565  Idccid 17566   Func cfunc 17756   ×_c cxpc 18069   curry_F ccurf 18111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5212  ax-sep 5229  ax-nul 5239  ax-pow 5298  ax-pr 5365  ax-un 7663  ax-cnex 11057  ax-resscn 11058  ax-1cn 11059  ax-icn 11060  ax-addcl 11061  ax-addrcl 11062  ax-mulcl 11063  ax-mulrcl 11064  ax-mulcom 11065  ax-addass 11066  ax-mulass 11067  ax-distr 11068  ax-i2m1 11069  ax-1ne0 11070  ax-1rid 11071  ax-rnegex 11072  ax-rrecex 11073  ax-cnre 11074  ax-pre-lttri 11075  ax-pre-lttrn 11076  ax-pre-ltadd 11077  ax-pre-mulgt0 11078

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rmo 3346  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-tp 4576  df-op 4578  df-uni 4855  df-iun 4938  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5506  df-eprel 5511  df-po 5519  df-so 5520  df-fr 5564  df-we 5566  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-pred 6243  df-ord 6304  df-on 6305  df-lim 6306  df-suc 6307  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-riota 7298  df-ov 7344  df-oprab 7345  df-mpo 7346  df-om 7792  df-1st 7916  df-2nd 7917  df-frecs 8206  df-wrecs 8237  df-recs 8286  df-rdg 8324  df-1o 8380  df-er 8617  df-map 8747  df-ixp 8817  df-en 8865  df-dom 8866  df-sdom 8867  df-fin 8868  df-pnf 11143  df-mnf 11144  df-xr 11145  df-ltxr 11146  df-le 11147  df-sub 11341  df-neg 11342  df-nn 12121  df-2 12183  df-3 12184  df-4 12185  df-5 12186  df-6 12187  df-7 12188  df-8 12189  df-9 12190  df-n0 12377  df-z 12464  df-dec 12584  df-uz 12728  df-fz 13403  df-struct 17053  df-slot 17088  df-ndx 17100  df-base 17116  df-hom 17180  df-cco 17181  df-cat 17569  df-cid 17570  df-func 17760  df-xpc 18073  df-curf 18115

This theorem is referenced by:  curf2cl  18132  curfcl  18133  tposcurf1cl  49328  postcofcl  49397