Theorem hofcl 16722

Description: Closure of the Hom functor. Note that the codomain is the category SetCat‘𝑈 for any universe 𝑈 which contains each Hom-set. This corresponds to the assertion that 𝐶 be locally small (with respect to 𝑈). (Contributed by Mario Carneiro, 15-Jan-2017.)

Hypotheses

Ref	Expression
hofcl.m	⊢ 𝑀 = (HomF‘𝐶)
hofcl.o	⊢ 𝑂 = (oppCat‘𝐶)
hofcl.d	⊢ 𝐷 = (SetCat‘𝑈)
hofcl.c	⊢ (𝜑 → 𝐶 ∈ Cat)
hofcl.u	⊢ (𝜑 → 𝑈 ∈ 𝑉)
hofcl.h	⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)

Assertion

Ref	Expression
hofcl	⊢ (𝜑 → 𝑀 ∈ ((𝑂 ×c 𝐶) Func 𝐷))

Proof of Theorem hofcl

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

Step	Hyp	Ref	Expression
1		hofcl.m	. . . 4 ⊢ 𝑀 = (HomF‘𝐶)
2		hofcl.c	. . . 4 ⊢ (𝜑 → 𝐶 ∈ Cat)
3		eqid 2610	. . . 4 ⊢ (Base‘𝐶) = (Base‘𝐶)
4		eqid 2610	. . . 4 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
5		eqid 2610	. . . 4 ⊢ (comp‘𝐶) = (comp‘𝐶)
6	1, 2, 3, 4, 5	hofval 16715	. . 3 ⊢ (𝜑 → 𝑀 = ⟨(Homf ‘𝐶), (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓))))⟩)
7		fvex 6113	. . . . . 6 ⊢ (Homf ‘𝐶) ∈ V
8		fvex 6113	. . . . . . . 8 ⊢ (Base‘𝐶) ∈ V
9	8, 8	xpex 6860	. . . . . . 7 ⊢ ((Base‘𝐶) × (Base‘𝐶)) ∈ V
10	9, 9	mpt2ex 7136	. . . . . 6 ⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓)))) ∈ V
11	7, 10	op2ndd 7070	. . . . 5 ⊢ (𝑀 = ⟨(Homf ‘𝐶), (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓))))⟩ → (2nd ‘𝑀) = (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓)))))
12	6, 11	syl 17	. . . 4 ⊢ (𝜑 → (2nd ‘𝑀) = (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓)))))
13	12	opeq2d 4347	. . 3 ⊢ (𝜑 → ⟨(Homf ‘𝐶), (2nd ‘𝑀)⟩ = ⟨(Homf ‘𝐶), (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓))))⟩)
14	6, 13	eqtr4d 2647	. 2 ⊢ (𝜑 → 𝑀 = ⟨(Homf ‘𝐶), (2nd ‘𝑀)⟩)
15		eqid 2610	. . . . 5 ⊢ (𝑂 ×c 𝐶) = (𝑂 ×c 𝐶)
16		hofcl.o	. . . . . 6 ⊢ 𝑂 = (oppCat‘𝐶)
17	16, 3	oppcbas 16201	. . . . 5 ⊢ (Base‘𝐶) = (Base‘𝑂)
18	15, 17, 3	xpcbas 16641	. . . 4 ⊢ ((Base‘𝐶) × (Base‘𝐶)) = (Base‘(𝑂 ×c 𝐶))
19		eqid 2610	. . . 4 ⊢ (Base‘𝐷) = (Base‘𝐷)
20		eqid 2610	. . . 4 ⊢ (Hom ‘(𝑂 ×c 𝐶)) = (Hom ‘(𝑂 ×c 𝐶))
21		eqid 2610	. . . 4 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
22		eqid 2610	. . . 4 ⊢ (Id‘(𝑂 ×c 𝐶)) = (Id‘(𝑂 ×c 𝐶))
23		eqid 2610	. . . 4 ⊢ (Id‘𝐷) = (Id‘𝐷)
24		eqid 2610	. . . 4 ⊢ (comp‘(𝑂 ×c 𝐶)) = (comp‘(𝑂 ×c 𝐶))
25		eqid 2610	. . . 4 ⊢ (comp‘𝐷) = (comp‘𝐷)
26	16	oppccat 16205	. . . . . 6 ⊢ (𝐶 ∈ Cat → 𝑂 ∈ Cat)
27	2, 26	syl 17	. . . . 5 ⊢ (𝜑 → 𝑂 ∈ Cat)
28	15, 27, 2	xpccat 16653	. . . 4 ⊢ (𝜑 → (𝑂 ×c 𝐶) ∈ Cat)
29		hofcl.u	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ 𝑉)
30		hofcl.d	. . . . . 6 ⊢ 𝐷 = (SetCat‘𝑈)
31	30	setccat 16558	. . . . 5 ⊢ (𝑈 ∈ 𝑉 → 𝐷 ∈ Cat)
32	29, 31	syl 17	. . . 4 ⊢ (𝜑 → 𝐷 ∈ Cat)
33		eqid 2610	. . . . . . . 8 ⊢ (Homf ‘𝐶) = (Homf ‘𝐶)
34	33, 3	homffn 16176	. . . . . . 7 ⊢ (Homf ‘𝐶) Fn ((Base‘𝐶) × (Base‘𝐶))
35	34	a1i 11	. . . . . 6 ⊢ (𝜑 → (Homf ‘𝐶) Fn ((Base‘𝐶) × (Base‘𝐶)))
36		hofcl.h	. . . . . 6 ⊢ (𝜑 → ran (Homf ‘𝐶) ⊆ 𝑈)
37		df-f 5808	. . . . . 6 ⊢ ((Homf ‘𝐶):((Base‘𝐶) × (Base‘𝐶))⟶𝑈 ↔ ((Homf ‘𝐶) Fn ((Base‘𝐶) × (Base‘𝐶)) ∧ ran (Homf ‘𝐶) ⊆ 𝑈))
38	35, 36, 37	sylanbrc 695	. . . . 5 ⊢ (𝜑 → (Homf ‘𝐶):((Base‘𝐶) × (Base‘𝐶))⟶𝑈)
39	30, 29	setcbas 16551	. . . . . 6 ⊢ (𝜑 → 𝑈 = (Base‘𝐷))
40	39	feq3d 5945	. . . . 5 ⊢ (𝜑 → ((Homf ‘𝐶):((Base‘𝐶) × (Base‘𝐶))⟶𝑈 ↔ (Homf ‘𝐶):((Base‘𝐶) × (Base‘𝐶))⟶(Base‘𝐷)))
41	38, 40	mpbid 221	. . . 4 ⊢ (𝜑 → (Homf ‘𝐶):((Base‘𝐶) × (Base‘𝐶))⟶(Base‘𝐷))
42		eqid 2610	. . . . . 6 ⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓)))) = (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓))))
43		ovex 6577	. . . . . . 7 ⊢ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∈ V
44		ovex 6577	. . . . . . 7 ⊢ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ∈ V
45	43, 44	mpt2ex 7136	. . . . . 6 ⊢ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓))) ∈ V
46	42, 45	fnmpt2i 7128	. . . . 5 ⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓)))) Fn (((Base‘𝐶) × (Base‘𝐶)) × ((Base‘𝐶) × (Base‘𝐶)))
47	12	fneq1d 5895	. . . . 5 ⊢ (𝜑 → ((2nd ‘𝑀) Fn (((Base‘𝐶) × (Base‘𝐶)) × ((Base‘𝐶) × (Base‘𝐶))) ↔ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓)))) Fn (((Base‘𝐶) × (Base‘𝐶)) × ((Base‘𝐶) × (Base‘𝐶)))))
48	46, 47	mpbiri 247	. . . 4 ⊢ (𝜑 → (2nd ‘𝑀) Fn (((Base‘𝐶) × (Base‘𝐶)) × ((Base‘𝐶) × (Base‘𝐶))))
49	2	ad3antrrr 762	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝐶 ∈ Cat)
50		simplrr 797	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))
51		xp1st 7089	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (1st ‘𝑦) ∈ (Base‘𝐶))
52	50, 51	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → (1st ‘𝑦) ∈ (Base‘𝐶))
53	52	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (1st ‘𝑦) ∈ (Base‘𝐶))
54		simplrl 796	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)))
55		xp1st 7089	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (1st ‘𝑥) ∈ (Base‘𝐶))
56	54, 55	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → (1st ‘𝑥) ∈ (Base‘𝐶))
57	56	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (1st ‘𝑥) ∈ (Base‘𝐶))
58		xp2nd 7090	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (2nd ‘𝑦) ∈ (Base‘𝐶))
59	50, 58	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → (2nd ‘𝑦) ∈ (Base‘𝐶))
60	59	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (2nd ‘𝑦) ∈ (Base‘𝐶))
61		simplrl 796	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)))
62		1st2nd2 7096	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
63	54, 62	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
64	63	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
65	64	oveq1d 6564	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑥(comp‘𝐶)(2nd ‘𝑦)) = (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦)))
66	65	oveqd 6566	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ) = (𝑔(⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))ℎ))
67		xp2nd 7090	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (2nd ‘𝑥) ∈ (Base‘𝐶))
68	54, 67	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → (2nd ‘𝑥) ∈ (Base‘𝐶))
69	68	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (2nd ‘𝑥) ∈ (Base‘𝐶))
70	63	fveq2d 6107	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Hom ‘𝐶)‘𝑥) = ((Hom ‘𝐶)‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩))
71		df-ov 6552	. . . . . . . . . . . . . . . . 17 ⊢ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)) = ((Hom ‘𝐶)‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
72	70, 71	syl6eqr 2662	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Hom ‘𝐶)‘𝑥) = ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)))
73	72	eleq2d 2673	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↔ ℎ ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))))
74	73	biimpa 500	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → ℎ ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)))
75		simplrr 797	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))
76	3, 4, 5, 49, 57, 69, 60, 74, 75	catcocl 16169	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑔(⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))ℎ) ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))
77	66, 76	eqeltrd 2688	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ) ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))
78	3, 4, 5, 49, 53, 57, 60, 61, 77	catcocl 16169	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓) ∈ ((1st ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑦)))
79		1st2nd2 7096	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
80	50, 79	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
81	80	fveq2d 6107	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Hom ‘𝐶)‘𝑦) = ((Hom ‘𝐶)‘⟨(1st ‘𝑦), (2nd ‘𝑦)⟩))
82		df-ov 6552	. . . . . . . . . . . . 13 ⊢ ((1st ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑦)) = ((Hom ‘𝐶)‘⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
83	81, 82	syl6eqr 2662	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Hom ‘𝐶)‘𝑦) = ((1st ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑦)))
84	83	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → ((Hom ‘𝐶)‘𝑦) = ((1st ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑦)))
85	78, 84	eleqtrrd 2691	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓) ∈ ((Hom ‘𝐶)‘𝑦))
86		eqid 2610	. . . . . . . . . 10 ⊢ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓)) = (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓))
87	85, 86	fmptd 6292	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓)):((Hom ‘𝐶)‘𝑥)⟶((Hom ‘𝐶)‘𝑦))
88	29	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → 𝑈 ∈ 𝑉)
89	33, 3, 4, 56, 68	homfval 16175	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((1st ‘𝑥)(Homf ‘𝐶)(2nd ‘𝑥)) = ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)))
90	63	fveq2d 6107	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Homf ‘𝐶)‘𝑥) = ((Homf ‘𝐶)‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩))
91		df-ov 6552	. . . . . . . . . . . . 13 ⊢ ((1st ‘𝑥)(Homf ‘𝐶)(2nd ‘𝑥)) = ((Homf ‘𝐶)‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
92	90, 91	syl6eqr 2662	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Homf ‘𝐶)‘𝑥) = ((1st ‘𝑥)(Homf ‘𝐶)(2nd ‘𝑥)))
93	89, 92, 72	3eqtr4d 2654	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Homf ‘𝐶)‘𝑥) = ((Hom ‘𝐶)‘𝑥))
94	38	ad2antrr 758	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → (Homf ‘𝐶):((Base‘𝐶) × (Base‘𝐶))⟶𝑈)
95	94, 54	ffvelrnd 6268	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Homf ‘𝐶)‘𝑥) ∈ 𝑈)
96	93, 95	eqeltrrd 2689	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Hom ‘𝐶)‘𝑥) ∈ 𝑈)
97	33, 3, 4, 52, 59	homfval 16175	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((1st ‘𝑦)(Homf ‘𝐶)(2nd ‘𝑦)) = ((1st ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑦)))
98	80	fveq2d 6107	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Homf ‘𝐶)‘𝑦) = ((Homf ‘𝐶)‘⟨(1st ‘𝑦), (2nd ‘𝑦)⟩))
99		df-ov 6552	. . . . . . . . . . . . 13 ⊢ ((1st ‘𝑦)(Homf ‘𝐶)(2nd ‘𝑦)) = ((Homf ‘𝐶)‘⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
100	98, 99	syl6eqr 2662	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Homf ‘𝐶)‘𝑦) = ((1st ‘𝑦)(Homf ‘𝐶)(2nd ‘𝑦)))
101	97, 100, 83	3eqtr4d 2654	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Homf ‘𝐶)‘𝑦) = ((Hom ‘𝐶)‘𝑦))
102	94, 50	ffvelrnd 6268	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Homf ‘𝐶)‘𝑦) ∈ 𝑈)
103	101, 102	eqeltrrd 2689	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Hom ‘𝐶)‘𝑦) ∈ 𝑈)
104	30, 88, 21, 96, 103	elsetchom 16554	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓)) ∈ (((Hom ‘𝐶)‘𝑥)(Hom ‘𝐷)((Hom ‘𝐶)‘𝑦)) ↔ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓)):((Hom ‘𝐶)‘𝑥)⟶((Hom ‘𝐶)‘𝑦)))
105	87, 104	mpbird 246	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓)) ∈ (((Hom ‘𝐶)‘𝑥)(Hom ‘𝐷)((Hom ‘𝐶)‘𝑦)))
106	93, 101	oveq12d 6567	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → (((Homf ‘𝐶)‘𝑥)(Hom ‘𝐷)((Homf ‘𝐶)‘𝑦)) = (((Hom ‘𝐶)‘𝑥)(Hom ‘𝐷)((Hom ‘𝐶)‘𝑦)))
107	105, 106	eleqtrrd 2691	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓)) ∈ (((Homf ‘𝐶)‘𝑥)(Hom ‘𝐷)((Homf ‘𝐶)‘𝑦)))
108	107	ralrimivva 2954	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → ∀𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥))∀𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))(ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓)) ∈ (((Homf ‘𝐶)‘𝑥)(Hom ‘𝐷)((Homf ‘𝐶)‘𝑦)))
109		eqid 2610	. . . . . . 7 ⊢ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓))) = (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓)))
110	109	fmpt2 7126	. . . . . 6 ⊢ (∀𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥))∀𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))(ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓)) ∈ (((Homf ‘𝐶)‘𝑥)(Hom ‘𝐷)((Homf ‘𝐶)‘𝑦)) ↔ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓))):(((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))⟶(((Homf ‘𝐶)‘𝑥)(Hom ‘𝐷)((Homf ‘𝐶)‘𝑦)))
111	108, 110	sylib 207	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓))):(((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))⟶(((Homf ‘𝐶)‘𝑥)(Hom ‘𝐷)((Homf ‘𝐶)‘𝑦)))
112	12	oveqd 6566	. . . . . . 7 ⊢ (𝜑 → (𝑥(2nd ‘𝑀)𝑦) = (𝑥(𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓))))𝑦))
113	42	ovmpt4g 6681	. . . . . . . 8 ⊢ ((𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓))) ∈ V) → (𝑥(𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓))))𝑦) = (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓))))
114	45, 113	mp3an3 1405	. . . . . . 7 ⊢ ((𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (𝑥(𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓))))𝑦) = (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓))))
115	112, 114	sylan9eq 2664	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (𝑥(2nd ‘𝑀)𝑦) = (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓))))
116		eqid 2610	. . . . . . . 8 ⊢ (Hom ‘𝑂) = (Hom ‘𝑂)
117		simprl 790	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)))
118		simprr 792	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))
119	15, 18, 116, 4, 20, 117, 118	xpchom 16643	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) = (((1st ‘𝑥)(Hom ‘𝑂)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))))
120	4, 16	oppchom 16198	. . . . . . . 8 ⊢ ((1st ‘𝑥)(Hom ‘𝑂)(1st ‘𝑦)) = ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥))
121	120	xpeq1i 5059	. . . . . . 7 ⊢ (((1st ‘𝑥)(Hom ‘𝑂)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))) = (((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))
122	119, 121	syl6eq 2660	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) = (((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))))
123	115, 122	feq12d 5946	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → ((𝑥(2nd ‘𝑀)𝑦):(𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦)⟶(((Homf ‘𝐶)‘𝑥)(Hom ‘𝐷)((Homf ‘𝐶)‘𝑦)) ↔ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(⟨(1st ‘𝑦), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑦))𝑓))):(((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))⟶(((Homf ‘𝐶)‘𝑥)(Hom ‘𝐷)((Homf ‘𝐶)‘𝑦))))
124	111, 123	mpbird 246	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (𝑥(2nd ‘𝑀)𝑦):(𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦)⟶(((Homf ‘𝐶)‘𝑥)(Hom ‘𝐷)((Homf ‘𝐶)‘𝑦)))
125		eqid 2610	. . . . . . . . . 10 ⊢ (Id‘𝐶) = (Id‘𝐶)
126	2	ad2antrr 758	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) → 𝐶 ∈ Cat)
127	55	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (1st ‘𝑥) ∈ (Base‘𝐶))
128	127	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) → (1st ‘𝑥) ∈ (Base‘𝐶))
129	67	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (2nd ‘𝑥) ∈ (Base‘𝐶))
130	129	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) → (2nd ‘𝑥) ∈ (Base‘𝐶))
131		simpr 476	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) → 𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)))
132	3, 4, 125, 126, 128, 5, 130, 131	catlid 16167	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) → (((Id‘𝐶)‘(2nd ‘𝑥))(⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑥))𝑓) = 𝑓)
133	132	oveq1d 6564	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) → ((((Id‘𝐶)‘(2nd ‘𝑥))(⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑥))𝑓)(⟨(1st ‘𝑥), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑥))((Id‘𝐶)‘(1st ‘𝑥))) = (𝑓(⟨(1st ‘𝑥), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑥))((Id‘𝐶)‘(1st ‘𝑥))))
134	3, 4, 125, 126, 128, 5, 130, 131	catrid 16168	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) → (𝑓(⟨(1st ‘𝑥), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑥))((Id‘𝐶)‘(1st ‘𝑥))) = 𝑓)
135	133, 134	eqtrd 2644	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) → ((((Id‘𝐶)‘(2nd ‘𝑥))(⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑥))𝑓)(⟨(1st ‘𝑥), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑥))((Id‘𝐶)‘(1st ‘𝑥))) = 𝑓)
136	135	mpteq2dva 4672	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)) ↦ ((((Id‘𝐶)‘(2nd ‘𝑥))(⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑥))𝑓)(⟨(1st ‘𝑥), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑥))((Id‘𝐶)‘(1st ‘𝑥)))) = (𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)) ↦ 𝑓))
137		df-ov 6552	. . . . . . 7 ⊢ (((Id‘𝐶)‘(1st ‘𝑥))(⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(2nd ‘𝑀)⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)((Id‘𝐶)‘(2nd ‘𝑥))) = ((⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(2nd ‘𝑀)⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)‘⟨((Id‘𝐶)‘(1st ‘𝑥)), ((Id‘𝐶)‘(2nd ‘𝑥))⟩)
138	2	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → 𝐶 ∈ Cat)
139	3, 4, 125, 138, 127	catidcl 16166	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘𝐶)‘(1st ‘𝑥)) ∈ ((1st ‘𝑥)(Hom ‘𝐶)(1st ‘𝑥)))
140	3, 4, 125, 138, 129	catidcl 16166	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘𝐶)‘(2nd ‘𝑥)) ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)))
141	1, 138, 3, 4, 127, 129, 127, 129, 5, 139, 140	hof2val 16719	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (((Id‘𝐶)‘(1st ‘𝑥))(⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(2nd ‘𝑀)⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)((Id‘𝐶)‘(2nd ‘𝑥))) = (𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)) ↦ ((((Id‘𝐶)‘(2nd ‘𝑥))(⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑥))𝑓)(⟨(1st ‘𝑥), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑥))((Id‘𝐶)‘(1st ‘𝑥)))))
142	137, 141	syl5eqr 2658	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(2nd ‘𝑀)⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)‘⟨((Id‘𝐶)‘(1st ‘𝑥)), ((Id‘𝐶)‘(2nd ‘𝑥))⟩) = (𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)) ↦ ((((Id‘𝐶)‘(2nd ‘𝑥))(⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑥))𝑓)(⟨(1st ‘𝑥), (1st ‘𝑥)⟩(comp‘𝐶)(2nd ‘𝑥))((Id‘𝐶)‘(1st ‘𝑥)))))
143	62	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
144	143	fveq2d 6107	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Homf ‘𝐶)‘𝑥) = ((Homf ‘𝐶)‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩))
145	144, 91	syl6eqr 2662	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Homf ‘𝐶)‘𝑥) = ((1st ‘𝑥)(Homf ‘𝐶)(2nd ‘𝑥)))
146	33, 3, 4, 127, 129	homfval 16175	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((1st ‘𝑥)(Homf ‘𝐶)(2nd ‘𝑥)) = ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)))
147	145, 146	eqtrd 2644	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Homf ‘𝐶)‘𝑥) = ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)))
148	147	reseq2d 5317	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ( I ↾ ((Homf ‘𝐶)‘𝑥)) = ( I ↾ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))))
149		mptresid 5375	. . . . . . 7 ⊢ (𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)) ↦ 𝑓) = ( I ↾ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)))
150	148, 149	syl6eqr 2662	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ( I ↾ ((Homf ‘𝐶)‘𝑥)) = (𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)) ↦ 𝑓))
151	136, 142, 150	3eqtr4d 2654	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(2nd ‘𝑀)⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)‘⟨((Id‘𝐶)‘(1st ‘𝑥)), ((Id‘𝐶)‘(2nd ‘𝑥))⟩) = ( I ↾ ((Homf ‘𝐶)‘𝑥)))
152	143, 143	oveq12d 6567	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (𝑥(2nd ‘𝑀)𝑥) = (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(2nd ‘𝑀)⟨(1st ‘𝑥), (2nd ‘𝑥)⟩))
153	143	fveq2d 6107	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘(𝑂 ×c 𝐶))‘𝑥) = ((Id‘(𝑂 ×c 𝐶))‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩))
154	27	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → 𝑂 ∈ Cat)
155		eqid 2610	. . . . . . . 8 ⊢ (Id‘𝑂) = (Id‘𝑂)
156	15, 154, 138, 17, 3, 155, 125, 22, 127, 129	xpcid 16652	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘(𝑂 ×c 𝐶))‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩) = ⟨((Id‘𝑂)‘(1st ‘𝑥)), ((Id‘𝐶)‘(2nd ‘𝑥))⟩)
157	16, 125	oppcid 16204	. . . . . . . . . 10 ⊢ (𝐶 ∈ Cat → (Id‘𝑂) = (Id‘𝐶))
158	138, 157	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (Id‘𝑂) = (Id‘𝐶))
159	158	fveq1d 6105	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘𝑂)‘(1st ‘𝑥)) = ((Id‘𝐶)‘(1st ‘𝑥)))
160	159	opeq1d 4346	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ⟨((Id‘𝑂)‘(1st ‘𝑥)), ((Id‘𝐶)‘(2nd ‘𝑥))⟩ = ⟨((Id‘𝐶)‘(1st ‘𝑥)), ((Id‘𝐶)‘(2nd ‘𝑥))⟩)
161	153, 156, 160	3eqtrd 2648	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘(𝑂 ×c 𝐶))‘𝑥) = ⟨((Id‘𝐶)‘(1st ‘𝑥)), ((Id‘𝐶)‘(2nd ‘𝑥))⟩)
162	152, 161	fveq12d 6109	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((𝑥(2nd ‘𝑀)𝑥)‘((Id‘(𝑂 ×c 𝐶))‘𝑥)) = ((⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(2nd ‘𝑀)⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)‘⟨((Id‘𝐶)‘(1st ‘𝑥)), ((Id‘𝐶)‘(2nd ‘𝑥))⟩))
163	29	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → 𝑈 ∈ 𝑉)
164	38	ffvelrnda 6267	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Homf ‘𝐶)‘𝑥) ∈ 𝑈)
165	30, 23, 163, 164	setcid 16559	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘𝐷)‘((Homf ‘𝐶)‘𝑥)) = ( I ↾ ((Homf ‘𝐶)‘𝑥)))
166	151, 162, 165	3eqtr4d 2654	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((𝑥(2nd ‘𝑀)𝑥)‘((Id‘(𝑂 ×c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((Homf ‘𝐶)‘𝑥)))
167	2	3ad2ant1 1075	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝐶 ∈ Cat)
168	29	3ad2ant1 1075	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑈 ∈ 𝑉)
169	36	3ad2ant1 1075	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ran (Homf ‘𝐶) ⊆ 𝑈)
170		simp21 1087	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)))
171	170, 55	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (1st ‘𝑥) ∈ (Base‘𝐶))
172	170, 67	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (2nd ‘𝑥) ∈ (Base‘𝐶))
173		simp22 1088	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))
174	173, 51	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (1st ‘𝑦) ∈ (Base‘𝐶))
175	173, 58	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (2nd ‘𝑦) ∈ (Base‘𝐶))
176		simp23 1089	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)))
177		xp1st 7089	. . . . . . 7 ⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (1st ‘𝑧) ∈ (Base‘𝐶))
178	176, 177	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (1st ‘𝑧) ∈ (Base‘𝐶))
179		xp2nd 7090	. . . . . . 7 ⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (2nd ‘𝑧) ∈ (Base‘𝐶))
180	176, 179	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (2nd ‘𝑧) ∈ (Base‘𝐶))
181		simp3l 1082	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦))
182	15, 18, 116, 4, 20, 170, 173	xpchom 16643	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) = (((1st ‘𝑥)(Hom ‘𝑂)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))))
183	181, 182	eleqtrd 2690	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑓 ∈ (((1st ‘𝑥)(Hom ‘𝑂)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))))
184		xp1st 7089	. . . . . . . 8 ⊢ (𝑓 ∈ (((1st ‘𝑥)(Hom ‘𝑂)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))) → (1st ‘𝑓) ∈ ((1st ‘𝑥)(Hom ‘𝑂)(1st ‘𝑦)))
185	183, 184	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (1st ‘𝑓) ∈ ((1st ‘𝑥)(Hom ‘𝑂)(1st ‘𝑦)))
186	185, 120	syl6eleq 2698	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (1st ‘𝑓) ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)))
187		xp2nd 7090	. . . . . . 7 ⊢ (𝑓 ∈ (((1st ‘𝑥)(Hom ‘𝑂)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))) → (2nd ‘𝑓) ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))
188	183, 187	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (2nd ‘𝑓) ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))
189		simp3r 1083	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))
190	15, 18, 116, 4, 20, 173, 176	xpchom 16643	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧) = (((1st ‘𝑦)(Hom ‘𝑂)(1st ‘𝑧)) × ((2nd ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧))))
191	189, 190	eleqtrd 2690	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑔 ∈ (((1st ‘𝑦)(Hom ‘𝑂)(1st ‘𝑧)) × ((2nd ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧))))
192		xp1st 7089	. . . . . . . 8 ⊢ (𝑔 ∈ (((1st ‘𝑦)(Hom ‘𝑂)(1st ‘𝑧)) × ((2nd ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧))) → (1st ‘𝑔) ∈ ((1st ‘𝑦)(Hom ‘𝑂)(1st ‘𝑧)))
193	191, 192	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (1st ‘𝑔) ∈ ((1st ‘𝑦)(Hom ‘𝑂)(1st ‘𝑧)))
194	4, 16	oppchom 16198	. . . . . . 7 ⊢ ((1st ‘𝑦)(Hom ‘𝑂)(1st ‘𝑧)) = ((1st ‘𝑧)(Hom ‘𝐶)(1st ‘𝑦))
195	193, 194	syl6eleq 2698	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (1st ‘𝑔) ∈ ((1st ‘𝑧)(Hom ‘𝐶)(1st ‘𝑦)))
196		xp2nd 7090	. . . . . . 7 ⊢ (𝑔 ∈ (((1st ‘𝑦)(Hom ‘𝑂)(1st ‘𝑧)) × ((2nd ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧))) → (2nd ‘𝑔) ∈ ((2nd ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧)))
197	191, 196	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (2nd ‘𝑔) ∈ ((2nd ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧)))
198	1, 16, 30, 167, 168, 169, 3, 4, 171, 172, 174, 175, 178, 180, 186, 188, 195, 197	hofcllem 16721	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (((1st ‘𝑓)(⟨(1st ‘𝑧), (1st ‘𝑦)⟩(comp‘𝐶)(1st ‘𝑥))(1st ‘𝑔))(⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(2nd ‘𝑀)⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)((2nd ‘𝑔)(⟨(2nd ‘𝑥), (2nd ‘𝑦)⟩(comp‘𝐶)(2nd ‘𝑧))(2nd ‘𝑓))) = (((1st ‘𝑔)(⟨(1st ‘𝑦), (2nd ‘𝑦)⟩(2nd ‘𝑀)⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)(2nd ‘𝑔))(⟨((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)), ((1st ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑦))⟩(comp‘𝐷)((1st ‘𝑧)(Hom ‘𝐶)(2nd ‘𝑧)))((1st ‘𝑓)(⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(2nd ‘𝑀)⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)(2nd ‘𝑓))))
199	170, 62	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
200		1st2nd2 7096	. . . . . . . . 9 ⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) → 𝑧 = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
201	176, 200	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑧 = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
202	199, 201	oveq12d 6567	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (𝑥(2nd ‘𝑀)𝑧) = (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(2nd ‘𝑀)⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
203	173, 79	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
204	199, 203	opeq12d 4348	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ⟨𝑥, 𝑦⟩ = ⟨⟨(1st ‘𝑥), (2nd ‘𝑥)⟩, ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩⟩)
205	204, 201	oveq12d 6567	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (⟨𝑥, 𝑦⟩(comp‘(𝑂 ×c 𝐶))𝑧) = (⟨⟨(1st ‘𝑥), (2nd ‘𝑥)⟩, ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩⟩(comp‘(𝑂 ×c 𝐶))⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
206		1st2nd2 7096	. . . . . . . . . 10 ⊢ (𝑔 ∈ (((1st ‘𝑦)(Hom ‘𝑂)(1st ‘𝑧)) × ((2nd ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧))) → 𝑔 = ⟨(1st ‘𝑔), (2nd ‘𝑔)⟩)
207	191, 206	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑔 = ⟨(1st ‘𝑔), (2nd ‘𝑔)⟩)
208		1st2nd2 7096	. . . . . . . . . 10 ⊢ (𝑓 ∈ (((1st ‘𝑥)(Hom ‘𝑂)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))) → 𝑓 = ⟨(1st ‘𝑓), (2nd ‘𝑓)⟩)
209	183, 208	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑓 = ⟨(1st ‘𝑓), (2nd ‘𝑓)⟩)
210	205, 207, 209	oveq123d 6570	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘(𝑂 ×c 𝐶))𝑧)𝑓) = (⟨(1st ‘𝑔), (2nd ‘𝑔)⟩(⟨⟨(1st ‘𝑥), (2nd ‘𝑥)⟩, ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩⟩(comp‘(𝑂 ×c 𝐶))⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)⟨(1st ‘𝑓), (2nd ‘𝑓)⟩))
211		eqid 2610	. . . . . . . . 9 ⊢ (comp‘𝑂) = (comp‘𝑂)
212	15, 17, 3, 116, 4, 171, 172, 174, 175, 211, 5, 24, 178, 180, 185, 188, 193, 197	xpcco2 16650	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (⟨(1st ‘𝑔), (2nd ‘𝑔)⟩(⟨⟨(1st ‘𝑥), (2nd ‘𝑥)⟩, ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩⟩(comp‘(𝑂 ×c 𝐶))⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)⟨(1st ‘𝑓), (2nd ‘𝑓)⟩) = ⟨((1st ‘𝑔)(⟨(1st ‘𝑥), (1st ‘𝑦)⟩(comp‘𝑂)(1st ‘𝑧))(1st ‘𝑓)), ((2nd ‘𝑔)(⟨(2nd ‘𝑥), (2nd ‘𝑦)⟩(comp‘𝐶)(2nd ‘𝑧))(2nd ‘𝑓))⟩)
213	3, 5, 16, 171, 174, 178	oppcco 16200	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((1st ‘𝑔)(⟨(1st ‘𝑥), (1st ‘𝑦)⟩(comp‘𝑂)(1st ‘𝑧))(1st ‘𝑓)) = ((1st ‘𝑓)(⟨(1st ‘𝑧), (1st ‘𝑦)⟩(comp‘𝐶)(1st ‘𝑥))(1st ‘𝑔)))
214	213	opeq1d 4346	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ⟨((1st ‘𝑔)(⟨(1st ‘𝑥), (1st ‘𝑦)⟩(comp‘𝑂)(1st ‘𝑧))(1st ‘𝑓)), ((2nd ‘𝑔)(⟨(2nd ‘𝑥), (2nd ‘𝑦)⟩(comp‘𝐶)(2nd ‘𝑧))(2nd ‘𝑓))⟩ = ⟨((1st ‘𝑓)(⟨(1st ‘𝑧), (1st ‘𝑦)⟩(comp‘𝐶)(1st ‘𝑥))(1st ‘𝑔)), ((2nd ‘𝑔)(⟨(2nd ‘𝑥), (2nd ‘𝑦)⟩(comp‘𝐶)(2nd ‘𝑧))(2nd ‘𝑓))⟩)
215	210, 212, 214	3eqtrd 2648	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘(𝑂 ×c 𝐶))𝑧)𝑓) = ⟨((1st ‘𝑓)(⟨(1st ‘𝑧), (1st ‘𝑦)⟩(comp‘𝐶)(1st ‘𝑥))(1st ‘𝑔)), ((2nd ‘𝑔)(⟨(2nd ‘𝑥), (2nd ‘𝑦)⟩(comp‘𝐶)(2nd ‘𝑧))(2nd ‘𝑓))⟩)
216	202, 215	fveq12d 6109	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((𝑥(2nd ‘𝑀)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘(𝑂 ×c 𝐶))𝑧)𝑓)) = ((⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(2nd ‘𝑀)⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)‘⟨((1st ‘𝑓)(⟨(1st ‘𝑧), (1st ‘𝑦)⟩(comp‘𝐶)(1st ‘𝑥))(1st ‘𝑔)), ((2nd ‘𝑔)(⟨(2nd ‘𝑥), (2nd ‘𝑦)⟩(comp‘𝐶)(2nd ‘𝑧))(2nd ‘𝑓))⟩))
217		df-ov 6552	. . . . . 6 ⊢ (((1st ‘𝑓)(⟨(1st ‘𝑧), (1st ‘𝑦)⟩(comp‘𝐶)(1st ‘𝑥))(1st ‘𝑔))(⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(2nd ‘𝑀)⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)((2nd ‘𝑔)(⟨(2nd ‘𝑥), (2nd ‘𝑦)⟩(comp‘𝐶)(2nd ‘𝑧))(2nd ‘𝑓))) = ((⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(2nd ‘𝑀)⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)‘⟨((1st ‘𝑓)(⟨(1st ‘𝑧), (1st ‘𝑦)⟩(comp‘𝐶)(1st ‘𝑥))(1st ‘𝑔)), ((2nd ‘𝑔)(⟨(2nd ‘𝑥), (2nd ‘𝑦)⟩(comp‘𝐶)(2nd ‘𝑧))(2nd ‘𝑓))⟩)
218	216, 217	syl6eqr 2662	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((𝑥(2nd ‘𝑀)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘(𝑂 ×c 𝐶))𝑧)𝑓)) = (((1st ‘𝑓)(⟨(1st ‘𝑧), (1st ‘𝑦)⟩(comp‘𝐶)(1st ‘𝑥))(1st ‘𝑔))(⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(2nd ‘𝑀)⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)((2nd ‘𝑔)(⟨(2nd ‘𝑥), (2nd ‘𝑦)⟩(comp‘𝐶)(2nd ‘𝑧))(2nd ‘𝑓))))
219	199	fveq2d 6107	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf ‘𝐶)‘𝑥) = ((Homf ‘𝐶)‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩))
220	219, 91	syl6eqr 2662	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf ‘𝐶)‘𝑥) = ((1st ‘𝑥)(Homf ‘𝐶)(2nd ‘𝑥)))
221	33, 3, 4, 171, 172	homfval 16175	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((1st ‘𝑥)(Homf ‘𝐶)(2nd ‘𝑥)) = ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)))
222	220, 221	eqtrd 2644	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf ‘𝐶)‘𝑥) = ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)))
223	203	fveq2d 6107	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf ‘𝐶)‘𝑦) = ((Homf ‘𝐶)‘⟨(1st ‘𝑦), (2nd ‘𝑦)⟩))
224	223, 99	syl6eqr 2662	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf ‘𝐶)‘𝑦) = ((1st ‘𝑦)(Homf ‘𝐶)(2nd ‘𝑦)))
225	33, 3, 4, 174, 175	homfval 16175	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((1st ‘𝑦)(Homf ‘𝐶)(2nd ‘𝑦)) = ((1st ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑦)))
226	224, 225	eqtrd 2644	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf ‘𝐶)‘𝑦) = ((1st ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑦)))
227	222, 226	opeq12d 4348	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ⟨((Homf ‘𝐶)‘𝑥), ((Homf ‘𝐶)‘𝑦)⟩ = ⟨((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)), ((1st ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑦))⟩)
228	201	fveq2d 6107	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf ‘𝐶)‘𝑧) = ((Homf ‘𝐶)‘⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
229		df-ov 6552	. . . . . . . . 9 ⊢ ((1st ‘𝑧)(Homf ‘𝐶)(2nd ‘𝑧)) = ((Homf ‘𝐶)‘⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
230	228, 229	syl6eqr 2662	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf ‘𝐶)‘𝑧) = ((1st ‘𝑧)(Homf ‘𝐶)(2nd ‘𝑧)))
231	33, 3, 4, 178, 180	homfval 16175	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((1st ‘𝑧)(Homf ‘𝐶)(2nd ‘𝑧)) = ((1st ‘𝑧)(Hom ‘𝐶)(2nd ‘𝑧)))
232	230, 231	eqtrd 2644	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf ‘𝐶)‘𝑧) = ((1st ‘𝑧)(Hom ‘𝐶)(2nd ‘𝑧)))
233	227, 232	oveq12d 6567	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (⟨((Homf ‘𝐶)‘𝑥), ((Homf ‘𝐶)‘𝑦)⟩(comp‘𝐷)((Homf ‘𝐶)‘𝑧)) = (⟨((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)), ((1st ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑦))⟩(comp‘𝐷)((1st ‘𝑧)(Hom ‘𝐶)(2nd ‘𝑧))))
234	203, 201	oveq12d 6567	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (𝑦(2nd ‘𝑀)𝑧) = (⟨(1st ‘𝑦), (2nd ‘𝑦)⟩(2nd ‘𝑀)⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
235	234, 207	fveq12d 6109	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((𝑦(2nd ‘𝑀)𝑧)‘𝑔) = ((⟨(1st ‘𝑦), (2nd ‘𝑦)⟩(2nd ‘𝑀)⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)‘⟨(1st ‘𝑔), (2nd ‘𝑔)⟩))
236		df-ov 6552	. . . . . . 7 ⊢ ((1st ‘𝑔)(⟨(1st ‘𝑦), (2nd ‘𝑦)⟩(2nd ‘𝑀)⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)(2nd ‘𝑔)) = ((⟨(1st ‘𝑦), (2nd ‘𝑦)⟩(2nd ‘𝑀)⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)‘⟨(1st ‘𝑔), (2nd ‘𝑔)⟩)
237	235, 236	syl6eqr 2662	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((𝑦(2nd ‘𝑀)𝑧)‘𝑔) = ((1st ‘𝑔)(⟨(1st ‘𝑦), (2nd ‘𝑦)⟩(2nd ‘𝑀)⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)(2nd ‘𝑔)))
238	199, 203	oveq12d 6567	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (𝑥(2nd ‘𝑀)𝑦) = (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(2nd ‘𝑀)⟨(1st ‘𝑦), (2nd ‘𝑦)⟩))
239	238, 209	fveq12d 6109	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((𝑥(2nd ‘𝑀)𝑦)‘𝑓) = ((⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(2nd ‘𝑀)⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)‘⟨(1st ‘𝑓), (2nd ‘𝑓)⟩))
240		df-ov 6552	. . . . . . 7 ⊢ ((1st ‘𝑓)(⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(2nd ‘𝑀)⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)(2nd ‘𝑓)) = ((⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(2nd ‘𝑀)⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)‘⟨(1st ‘𝑓), (2nd ‘𝑓)⟩)
241	239, 240	syl6eqr 2662	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((𝑥(2nd ‘𝑀)𝑦)‘𝑓) = ((1st ‘𝑓)(⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(2nd ‘𝑀)⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)(2nd ‘𝑓)))
242	233, 237, 241	oveq123d 6570	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (((𝑦(2nd ‘𝑀)𝑧)‘𝑔)(⟨((Homf ‘𝐶)‘𝑥), ((Homf ‘𝐶)‘𝑦)⟩(comp‘𝐷)((Homf ‘𝐶)‘𝑧))((𝑥(2nd ‘𝑀)𝑦)‘𝑓)) = (((1st ‘𝑔)(⟨(1st ‘𝑦), (2nd ‘𝑦)⟩(2nd ‘𝑀)⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)(2nd ‘𝑔))(⟨((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)), ((1st ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑦))⟩(comp‘𝐷)((1st ‘𝑧)(Hom ‘𝐶)(2nd ‘𝑧)))((1st ‘𝑓)(⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(2nd ‘𝑀)⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)(2nd ‘𝑓))))
243	198, 218, 242	3eqtr4d 2654	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((𝑥(2nd ‘𝑀)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘(𝑂 ×c 𝐶))𝑧)𝑓)) = (((𝑦(2nd ‘𝑀)𝑧)‘𝑔)(⟨((Homf ‘𝐶)‘𝑥), ((Homf ‘𝐶)‘𝑦)⟩(comp‘𝐷)((Homf ‘𝐶)‘𝑧))((𝑥(2nd ‘𝑀)𝑦)‘𝑓)))
244	18, 19, 20, 21, 22, 23, 24, 25, 28, 32, 41, 48, 124, 166, 243	isfuncd 16348	. . 3 ⊢ (𝜑 → (Homf ‘𝐶)((𝑂 ×c 𝐶) Func 𝐷)(2nd ‘𝑀))
245		df-br 4584	. . 3 ⊢ ((Homf ‘𝐶)((𝑂 ×c 𝐶) Func 𝐷)(2nd ‘𝑀) ↔ ⟨(Homf ‘𝐶), (2nd ‘𝑀)⟩ ∈ ((𝑂 ×c 𝐶) Func 𝐷))
246	244, 245	sylib 207	. 2 ⊢ (𝜑 → ⟨(Homf ‘𝐶), (2nd ‘𝑀)⟩ ∈ ((𝑂 ×c 𝐶) Func 𝐷))
247	14, 246	eqeltrd 2688	1 ⊢ (𝜑 → 𝑀 ∈ ((𝑂 ×c 𝐶) Func 𝐷))

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∀wral 2896  Vcvv 3173   ⊆ wss 3540  ⟨cop 4131   class class class wbr 4583   ↦ cmpt 4643   I cid 4948   × cxp 5036  ran crn 5039   ↾ cres 5040   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551  1^st c1st 7057  2^nd c2nd 7058  Basecbs 15695  Hom chom 15779  compcco 15780  Catccat 16148  Idccid 16149  Hom_f chomf 16150  oppCatcoppc 16194   Func cfunc 16337  SetCatcsetc 16548   ×_c cxpc 16631  Hom_Fchof 16711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-tpos 7239  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-fz 12198  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-hom 15793  df-cco 15794  df-cat 16152  df-cid 16153  df-homf 16154  df-oppc 16195  df-func 16341  df-setc 16549  df-xpc 16635  df-hof 16713

This theorem is referenced by:  oppchofcl  16723  oppcyon  16732  yonedalem1  16735  yonedalem21  16736  yonedalem22  16741