Theorem curf1cl 18194

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 18191	. . 3 ⊢ (𝜑 → 𝐾 = ⟨(𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))⟩)
12	6	fvexi 6854	. . . . . . 7 ⊢ 𝐵 ∈ V
13	12	mptex 7178	. . . . . 6 ⊢ (𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)) ∈ V
14	12, 12	mpoex 8032	. . . . . 6 ⊢ (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔))) ∈ V
15	13, 14	op1std 7952	. . . . 5 ⊢ (𝐾 = ⟨(𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))⟩ → (1st ‘𝐾) = (𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)))
16	11, 15	syl 17	. . . 4 ⊢ (𝜑 → (1st ‘𝐾) = (𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)))
17	13, 14	op2ndd 7953	. . . . 5 ⊢ (𝐾 = ⟨(𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))⟩ → (2nd ‘𝐾) = (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔))))
18	11, 17	syl 17	. . . 4 ⊢ (𝜑 → (2nd ‘𝐾) = (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔))))
19	16, 18	opeq12d 4824	. . 3 ⊢ (𝜑 → ⟨(1st ‘𝐾), (2nd ‘𝐾)⟩ = ⟨(𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))⟩)
20	11, 19	eqtr4d 2774	. 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 17830	. . . . . 6 ⊢ (𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸) → ((𝐶 ×c 𝐷) ∈ Cat ∧ 𝐸 ∈ Cat))
28	5, 27	syl 17	. . . . 5 ⊢ (𝜑 → ((𝐶 ×c 𝐷) ∈ Cat ∧ 𝐸 ∈ Cat))
29	28	simprd 495	. . . 4 ⊢ (𝜑 → 𝐸 ∈ Cat)
30		eqid 2736	. . . . . . . . 9 ⊢ (𝐶 ×c 𝐷) = (𝐶 ×c 𝐷)
31	30, 2, 6	xpcbas 18144	. . . . . . . 8 ⊢ (𝐴 × 𝐵) = (Base‘(𝐶 ×c 𝐷))
32		relfunc 17829	. . . . . . . . 9 ⊢ Rel ((𝐶 ×c 𝐷) Func 𝐸)
33		1st2ndbr 7995	. . . . . . . . 9 ⊢ ((Rel ((𝐶 ×c 𝐷) Func 𝐸) ∧ 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹))
34	32, 5, 33	sylancr 588	. . . . . . . 8 ⊢ (𝜑 → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹))
35	31, 21, 34	funcf1 17833	. . . . . . 7 ⊢ (𝜑 → (1st ‘𝐹):(𝐴 × 𝐵)⟶(Base‘𝐸))
36	35	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1st ‘𝐹):(𝐴 × 𝐵)⟶(Base‘𝐸))
37	7	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑋 ∈ 𝐴)
38		simpr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵)
39	36, 37, 38	fovcdmd 7539	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑋(1st ‘𝐹)𝑦) ∈ (Base‘𝐸))
40	16, 39	fmpt3d 7068	. . . 4 ⊢ (𝜑 → (1st ‘𝐾):𝐵⟶(Base‘𝐸))
41		eqid 2736	. . . . . 6 ⊢ (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔))) = (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))
42		ovex 7400	. . . . . . 7 ⊢ (𝑦(Hom ‘𝐷)𝑧) ∈ V
43	42	mptex 7178	. . . . . 6 ⊢ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)) ∈ V
44	41, 43	fnmpoi 8023	. . . . 5 ⊢ (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔))) Fn (𝐵 × 𝐵)
45	18	fneq1d 6591	. . . . 5 ⊢ (𝜑 → ((2nd ‘𝐾) Fn (𝐵 × 𝐵) ↔ (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔))) Fn (𝐵 × 𝐵)))
46	44, 45	mpbiri 258	. . . 4 ⊢ (𝜑 → (2nd ‘𝐾) Fn (𝐵 × 𝐵))
47	18	oveqd 7384	. . . . . 6 ⊢ (𝜑 → (𝑦(2nd ‘𝐾)𝑧) = (𝑦(𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))𝑧))
48	41	ovmpt4g 7514	. . . . . . 7 ⊢ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)) ∈ V) → (𝑦(𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))𝑧) = (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))
49	43, 48	mp3an3 1453	. . . . . 6 ⊢ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝑦(𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))𝑧) = (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))
50	47, 49	sylan9eq 2791	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦(2nd ‘𝐾)𝑧) = (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔)))
51		eqid 2736	. . . . . . . 8 ⊢ (Hom ‘(𝐶 ×c 𝐷)) = (Hom ‘(𝐶 ×c 𝐷))
52	34	ad2antrr 727	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹))
53	7	ad2antrr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑋 ∈ 𝐴)
54		simplrl 777	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑦 ∈ 𝐵)
55	53, 54	opelxpd 5670	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ⟨𝑋, 𝑦⟩ ∈ (𝐴 × 𝐵))
56		simplrr 778	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑧 ∈ 𝐵)
57	53, 56	opelxpd 5670	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ⟨𝑋, 𝑧⟩ ∈ (𝐴 × 𝐵))
58	31, 51, 22, 52, 55, 57	funcf2 17835	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩):(⟨𝑋, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑧⟩)⟶(((1st ‘𝐹)‘⟨𝑋, 𝑦⟩)(Hom ‘𝐸)((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)))
59		eqid 2736	. . . . . . . . 9 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
60	30, 31, 59, 9, 51, 55, 57	xpchom 18146	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (⟨𝑋, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑧⟩) = (((1st ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐶)(1st ‘⟨𝑋, 𝑧⟩)) × ((2nd ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐷)(2nd ‘⟨𝑋, 𝑧⟩))))
61	3	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝐶 ∈ Cat)
62	4	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝐷 ∈ Cat)
63	5	ad2antrr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
64	1, 2, 61, 62, 63, 6, 53, 8, 54	curf11 18192	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st ‘𝐾)‘𝑦) = (𝑋(1st ‘𝐹)𝑦))
65		df-ov 7370	. . . . . . . . . 10 ⊢ (𝑋(1st ‘𝐹)𝑦) = ((1st ‘𝐹)‘⟨𝑋, 𝑦⟩)
66	64, 65	eqtr2di 2788	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st ‘𝐹)‘⟨𝑋, 𝑦⟩) = ((1st ‘𝐾)‘𝑦))
67	1, 2, 61, 62, 63, 6, 53, 8, 56	curf11 18192	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st ‘𝐾)‘𝑧) = (𝑋(1st ‘𝐹)𝑧))
68		df-ov 7370	. . . . . . . . . 10 ⊢ (𝑋(1st ‘𝐹)𝑧) = ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)
69	67, 68	eqtr2di 2788	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩) = ((1st ‘𝐾)‘𝑧))
70	66, 69	oveq12d 7385	. . . . . . . 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 232	. . . . . 6 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩):(((1st ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐶)(1st ‘⟨𝑋, 𝑧⟩)) × ((2nd ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐷)(2nd ‘⟨𝑋, 𝑧⟩)))⟶(((1st ‘𝐾)‘𝑦)(Hom ‘𝐸)((1st ‘𝐾)‘𝑧)))
73	2, 59, 10, 61, 53	catidcl 17648	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((Id‘𝐶)‘𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋))
74		op1stg 7954	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (1st ‘⟨𝑋, 𝑦⟩) = 𝑋)
75	53, 54, 74	syl2anc 585	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (1st ‘⟨𝑋, 𝑦⟩) = 𝑋)
76		op1stg 7954	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → (1st ‘⟨𝑋, 𝑧⟩) = 𝑋)
77	53, 56, 76	syl2anc 585	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (1st ‘⟨𝑋, 𝑧⟩) = 𝑋)
78	75, 77	oveq12d 7385	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐶)(1st ‘⟨𝑋, 𝑧⟩)) = (𝑋(Hom ‘𝐶)𝑋))
79	73, 78	eleqtrrd 2839	. . . . . 6 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((Id‘𝐶)‘𝑋) ∈ ((1st ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐶)(1st ‘⟨𝑋, 𝑧⟩)))
80		simpr 484	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))
81		op2ndg 7955	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (2nd ‘⟨𝑋, 𝑦⟩) = 𝑦)
82	53, 54, 81	syl2anc 585	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (2nd ‘⟨𝑋, 𝑦⟩) = 𝑦)
83		op2ndg 7955	. . . . . . . . 9 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → (2nd ‘⟨𝑋, 𝑧⟩) = 𝑧)
84	53, 56, 83	syl2anc 585	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (2nd ‘⟨𝑋, 𝑧⟩) = 𝑧)
85	82, 84	oveq12d 7385	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((2nd ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐷)(2nd ‘⟨𝑋, 𝑧⟩)) = (𝑦(Hom ‘𝐷)𝑧))
86	80, 85	eleqtrrd 2839	. . . . . 6 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑔 ∈ ((2nd ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐷)(2nd ‘⟨𝑋, 𝑧⟩)))
87	72, 79, 86	fovcdmd 7539	. . . . 5 ⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔) ∈ (((1st ‘𝐾)‘𝑦)(Hom ‘𝐸)((1st ‘𝐾)‘𝑧)))
88	50, 87	fmpt3d 7068	. . . 4 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦(2nd ‘𝐾)𝑧):(𝑦(Hom ‘𝐷)𝑧)⟶(((1st ‘𝐾)‘𝑦)(Hom ‘𝐸)((1st ‘𝐾)‘𝑧)))
89	3	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ Cat)
90	4	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ Cat)
91		eqid 2736	. . . . . . . . 9 ⊢ (Id‘(𝐶 ×c 𝐷)) = (Id‘(𝐶 ×c 𝐷))
92	30, 89, 90, 2, 6, 10, 23, 91, 37, 38	xpcid 18155	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((Id‘(𝐶 ×c 𝐷))‘⟨𝑋, 𝑦⟩) = ⟨((Id‘𝐶)‘𝑋), ((Id‘𝐷)‘𝑦)⟩)
93	92	fveq2d 6844	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)‘((Id‘(𝐶 ×c 𝐷))‘⟨𝑋, 𝑦⟩)) = ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)‘⟨((Id‘𝐶)‘𝑋), ((Id‘𝐷)‘𝑦)⟩))
94		df-ov 7370	. . . . . . 7 ⊢ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)((Id‘𝐷)‘𝑦)) = ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)‘⟨((Id‘𝐶)‘𝑋), ((Id‘𝐷)‘𝑦)⟩)
95	93, 94	eqtr4di 2789	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)‘((Id‘(𝐶 ×c 𝐷))‘⟨𝑋, 𝑦⟩)) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)((Id‘𝐷)‘𝑦)))
96	34	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹))
97		opelxpi 5668	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ⟨𝑋, 𝑦⟩ ∈ (𝐴 × 𝐵))
98	7, 97	sylan 581	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ⟨𝑋, 𝑦⟩ ∈ (𝐴 × 𝐵))
99	31, 91, 24, 96, 98	funcid 17837	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)‘((Id‘(𝐶 ×c 𝐷))‘⟨𝑋, 𝑦⟩)) = ((Id‘𝐸)‘((1st ‘𝐹)‘⟨𝑋, 𝑦⟩)))
100	95, 99	eqtr3d 2773	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)((Id‘𝐷)‘𝑦)) = ((Id‘𝐸)‘((1st ‘𝐹)‘⟨𝑋, 𝑦⟩)))
101	5	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
102	6, 9, 23, 90, 38	catidcl 17648	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((Id‘𝐷)‘𝑦) ∈ (𝑦(Hom ‘𝐷)𝑦))
103	1, 2, 89, 90, 101, 6, 37, 8, 38, 9, 10, 38, 102	curf12 18193	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((𝑦(2nd ‘𝐾)𝑦)‘((Id‘𝐷)‘𝑦)) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑦⟩)((Id‘𝐷)‘𝑦)))
104	1, 2, 89, 90, 101, 6, 37, 8, 38	curf11 18192	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((1st ‘𝐾)‘𝑦) = (𝑋(1st ‘𝐹)𝑦))
105	104, 65	eqtrdi 2787	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((1st ‘𝐾)‘𝑦) = ((1st ‘𝐹)‘⟨𝑋, 𝑦⟩))
106	105	fveq2d 6844	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((Id‘𝐸)‘((1st ‘𝐾)‘𝑦)) = ((Id‘𝐸)‘((1st ‘𝐹)‘⟨𝑋, 𝑦⟩)))
107	100, 103, 106	3eqtr4d 2781	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((𝑦(2nd ‘𝐾)𝑦)‘((Id‘𝐷)‘𝑦)) = ((Id‘𝐸)‘((1st ‘𝐾)‘𝑦)))
108	7	3ad2ant1 1134	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑋 ∈ 𝐴)
109		simp21 1208	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑦 ∈ 𝐵)
110		simp22 1209	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑧 ∈ 𝐵)
111		eqid 2736	. . . . . . . . . 10 ⊢ (comp‘𝐶) = (comp‘𝐶)
112		eqid 2736	. . . . . . . . . 10 ⊢ (comp‘(𝐶 ×c 𝐷)) = (comp‘(𝐶 ×c 𝐷))
113		simp23 1210	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑤 ∈ 𝐵)
114	3	3ad2ant1 1134	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐶 ∈ Cat)
115	2, 59, 10, 114, 108	catidcl 17648	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((Id‘𝐶)‘𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋))
116		simp3l 1203	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))
117		simp3r 1204	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))
118	30, 2, 6, 59, 9, 108, 109, 108, 110, 111, 25, 112, 108, 113, 115, 116, 115, 117	xpcco2 18153	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨((Id‘𝐶)‘𝑋), ℎ⟩(⟨⟨𝑋, 𝑦⟩, ⟨𝑋, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑔⟩) = ⟨(((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑋)((Id‘𝐶)‘𝑋)), (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩)
119	2, 59, 10, 114, 108, 111, 108, 115	catlid 17649	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑋)((Id‘𝐶)‘𝑋)) = ((Id‘𝐶)‘𝑋))
120	119	opeq1d 4822	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨(((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑋)((Id‘𝐶)‘𝑋)), (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩ = ⟨((Id‘𝐶)‘𝑋), (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩)
121	118, 120	eqtrd 2771	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨((Id‘𝐶)‘𝑋), ℎ⟩(⟨⟨𝑋, 𝑦⟩, ⟨𝑋, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑔⟩) = ⟨((Id‘𝐶)‘𝑋), (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩)
122	121	fveq2d 6844	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘(⟨((Id‘𝐶)‘𝑋), ℎ⟩(⟨⟨𝑋, 𝑦⟩, ⟨𝑋, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑔⟩)) = ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩))
123		df-ov 7370	. . . . . . 7 ⊢ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)) = ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩)
124	122, 123	eqtr4di 2789	. . . . . 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 5670	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑋, 𝑦⟩ ∈ (𝐴 × 𝐵))
127	108, 110	opelxpd 5670	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑋, 𝑧⟩ ∈ (𝐴 × 𝐵))
128	108, 113	opelxpd 5670	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑋, 𝑤⟩ ∈ (𝐴 × 𝐵))
129	115, 116	opelxpd 5670	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), 𝑔⟩ ∈ ((𝑋(Hom ‘𝐶)𝑋) × (𝑦(Hom ‘𝐷)𝑧)))
130	30, 2, 6, 59, 9, 108, 109, 108, 110, 51	xpchom2 18152	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑋, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑧⟩) = ((𝑋(Hom ‘𝐶)𝑋) × (𝑦(Hom ‘𝐷)𝑧)))
131	129, 130	eleqtrrd 2839	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), 𝑔⟩ ∈ (⟨𝑋, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑧⟩))
132	115, 117	opelxpd 5670	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), ℎ⟩ ∈ ((𝑋(Hom ‘𝐶)𝑋) × (𝑧(Hom ‘𝐷)𝑤)))
133	30, 2, 6, 59, 9, 108, 110, 108, 113, 51	xpchom2 18152	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩) = ((𝑋(Hom ‘𝐶)𝑋) × (𝑧(Hom ‘𝐷)𝑤)))
134	132, 133	eleqtrrd 2839	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), ℎ⟩ ∈ (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩))
135	31, 51, 112, 26, 125, 126, 127, 128, 131, 134	funcco 17838	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘(⟨((Id‘𝐶)‘𝑋), ℎ⟩(⟨⟨𝑋, 𝑦⟩, ⟨𝑋, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑔⟩)) = (((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), ℎ⟩)(⟨((1st ‘𝐹)‘⟨𝑋, 𝑦⟩), ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)⟩(comp‘𝐸)((1st ‘𝐹)‘⟨𝑋, 𝑤⟩))((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑔⟩)))
136	124, 135	eqtr3d 2773	. . . . 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 17651	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐷)𝑤))
140	1, 2, 114, 137, 138, 6, 108, 8, 109, 9, 10, 113, 139	curf12 18193	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑦(2nd ‘𝐾)𝑤)‘(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)(ℎ(⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)))
141	1, 2, 114, 137, 138, 6, 108, 8, 109	curf11 18192	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘𝐾)‘𝑦) = (𝑋(1st ‘𝐹)𝑦))
142	141, 65	eqtrdi 2787	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘𝐾)‘𝑦) = ((1st ‘𝐹)‘⟨𝑋, 𝑦⟩))
143	1, 2, 114, 137, 138, 6, 108, 8, 110	curf11 18192	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘𝐾)‘𝑧) = (𝑋(1st ‘𝐹)𝑧))
144	143, 68	eqtrdi 2787	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘𝐾)‘𝑧) = ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩))
145	142, 144	opeq12d 4824	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((1st ‘𝐾)‘𝑦), ((1st ‘𝐾)‘𝑧)⟩ = ⟨((1st ‘𝐹)‘⟨𝑋, 𝑦⟩), ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)⟩)
146	1, 2, 114, 137, 138, 6, 108, 8, 113	curf11 18192	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘𝐾)‘𝑤) = (𝑋(1st ‘𝐹)𝑤))
147		df-ov 7370	. . . . . . . 8 ⊢ (𝑋(1st ‘𝐹)𝑤) = ((1st ‘𝐹)‘⟨𝑋, 𝑤⟩)
148	146, 147	eqtrdi 2787	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘𝐾)‘𝑤) = ((1st ‘𝐹)‘⟨𝑋, 𝑤⟩))
149	145, 148	oveq12d 7385	. . . . . 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 18193	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘𝐾)𝑤)‘ℎ) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)ℎ))
151		df-ov 7370	. . . . . . 7 ⊢ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)ℎ) = ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), ℎ⟩)
152	150, 151	eqtrdi 2787	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘𝐾)𝑤)‘ℎ) = ((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), ℎ⟩))
153	1, 2, 114, 137, 138, 6, 108, 8, 109, 9, 10, 110, 116	curf12 18193	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑦(2nd ‘𝐾)𝑧)‘𝑔) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔))
154		df-ov 7370	. . . . . . 7 ⊢ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)𝑔) = ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑔⟩)
155	153, 154	eqtrdi 2787	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑦(2nd ‘𝐾)𝑧)‘𝑔) = ((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑔⟩))
156	149, 152, 155	oveq123d 7388	. . . . 5 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((𝑧(2nd ‘𝐾)𝑤)‘ℎ)(⟨((1st ‘𝐾)‘𝑦), ((1st ‘𝐾)‘𝑧)⟩(comp‘𝐸)((1st ‘𝐾)‘𝑤))((𝑦(2nd ‘𝐾)𝑧)‘𝑔)) = (((⟨𝑋, 𝑧⟩(2nd ‘𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), ℎ⟩)(⟨((1st ‘𝐹)‘⟨𝑋, 𝑦⟩), ((1st ‘𝐹)‘⟨𝑋, 𝑧⟩)⟩(comp‘𝐸)((1st ‘𝐹)‘⟨𝑋, 𝑤⟩))((⟨𝑋, 𝑦⟩(2nd ‘𝐹)⟨𝑋, 𝑧⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑔⟩)))
157	136, 140, 156	3eqtr4d 2781	. . . 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 17832	. . 3 ⊢ (𝜑 → (1st ‘𝐾)(𝐷 Func 𝐸)(2nd ‘𝐾))
159		df-br 5086	. . 3 ⊢ ((1st ‘𝐾)(𝐷 Func 𝐸)(2nd ‘𝐾) ↔ ⟨(1st ‘𝐾), (2nd ‘𝐾)⟩ ∈ (𝐷 Func 𝐸))
160	158, 159	sylib 218	. 2 ⊢ (𝜑 → ⟨(1st ‘𝐾), (2nd ‘𝐾)⟩ ∈ (𝐷 Func 𝐸))
161	20, 160	eqeltrd 2836	1 ⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐸))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  Vcvv 3429  ⟨cop 4573   class class class wbr 5085   ↦ cmpt 5166   × cxp 5629  Rel wrel 5636   Fn wfn 6493  ⟶wf 6494  ‘cfv 6498  (class class class)co 7367   ∈ cmpo 7369  1^st c1st 7940  2^nd c2nd 7941  Basecbs 17179  Hom chom 17231  compcco 17232  Catccat 17630  Idccid 17631   Func cfunc 17821   ×_c cxpc 18134   curry_F ccurf 18176

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-rmo 3342  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-om 7818  df-1st 7942  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-1o 8405  df-er 8643  df-map 8775  df-ixp 8846  df-en 8894  df-dom 8895  df-sdom 8896  df-fin 8897  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380  df-nn 12175  df-2 12244  df-3 12245  df-4 12246  df-5 12247  df-6 12248  df-7 12249  df-8 12250  df-9 12251  df-n0 12438  df-z 12525  df-dec 12645  df-uz 12789  df-fz 13462  df-struct 17117  df-slot 17152  df-ndx 17164  df-base 17180  df-hom 17244  df-cco 17245  df-cat 17634  df-cid 17635  df-func 17825  df-xpc 18138  df-curf 18180

This theorem is referenced by:  curf2cl  18197  curfcl  18198  tposcurf1cl  49771  postcofcl  49840