Theorem evlfcl 17471

Description: The evaluation functor is a bifunctor (a two-argument functor) with the first parameter taking values in the set of functors 𝐶⟶𝐷, and the second parameter in 𝐷. (Contributed by Mario Carneiro, 12-Jan-2017.)

Hypotheses

Ref	Expression
evlfcl.e	⊢ 𝐸 = (𝐶 evalF 𝐷)
evlfcl.q	⊢ 𝑄 = (𝐶 FuncCat 𝐷)
evlfcl.c	⊢ (𝜑 → 𝐶 ∈ Cat)
evlfcl.d	⊢ (𝜑 → 𝐷 ∈ Cat)

Assertion

Ref	Expression
evlfcl	⊢ (𝜑 → 𝐸 ∈ ((𝑄 ×c 𝐶) Func 𝐷))

Proof of Theorem evlfcl

Dummy variables 𝑓 𝑎 𝑔 ℎ 𝑚 𝑛 𝑢 𝑣 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		evlfcl.e	. . . . 5 ⊢ 𝐸 = (𝐶 evalF 𝐷)
2		evlfcl.c	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ Cat)
3		evlfcl.d	. . . . 5 ⊢ (𝜑 → 𝐷 ∈ Cat)
4		eqid 2821	. . . . 5 ⊢ (Base‘𝐶) = (Base‘𝐶)
5		eqid 2821	. . . . 5 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
6		eqid 2821	. . . . 5 ⊢ (comp‘𝐷) = (comp‘𝐷)
7		eqid 2821	. . . . 5 ⊢ (𝐶 Nat 𝐷) = (𝐶 Nat 𝐷)
8	1, 2, 3, 4, 5, 6, 7	evlfval 17466	. . . 4 ⊢ (𝜑 → 𝐸 = ⟨(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩(comp‘𝐷)((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))))⟩)
9		ovex 7188	. . . . . 6 ⊢ (𝐶 Func 𝐷) ∈ V
10		fvex 6682	. . . . . 6 ⊢ (Base‘𝐶) ∈ V
11	9, 10	mpoex 7776	. . . . 5 ⊢ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘𝑓)‘𝑥)) ∈ V
12	9, 10	xpex 7475	. . . . . 6 ⊢ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∈ V
13	12, 12	mpoex 7776	. . . . 5 ⊢ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩(comp‘𝐷)((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔)))) ∈ V
14	11, 13	opelvv 5593	. . . 4 ⊢ ⟨(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩(comp‘𝐷)((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))))⟩ ∈ (V × V)
15	8, 14	eqeltrdi 2921	. . 3 ⊢ (𝜑 → 𝐸 ∈ (V × V))
16		1st2nd2 7727	. . 3 ⊢ (𝐸 ∈ (V × V) → 𝐸 = ⟨(1st ‘𝐸), (2nd ‘𝐸)⟩)
17	15, 16	syl 17	. 2 ⊢ (𝜑 → 𝐸 = ⟨(1st ‘𝐸), (2nd ‘𝐸)⟩)
18		eqid 2821	. . . . 5 ⊢ (𝑄 ×c 𝐶) = (𝑄 ×c 𝐶)
19		evlfcl.q	. . . . . 6 ⊢ 𝑄 = (𝐶 FuncCat 𝐷)
20	19	fucbas 17229	. . . . 5 ⊢ (𝐶 Func 𝐷) = (Base‘𝑄)
21	18, 20, 4	xpcbas 17427	. . . 4 ⊢ ((𝐶 Func 𝐷) × (Base‘𝐶)) = (Base‘(𝑄 ×c 𝐶))
22		eqid 2821	. . . 4 ⊢ (Base‘𝐷) = (Base‘𝐷)
23		eqid 2821	. . . 4 ⊢ (Hom ‘(𝑄 ×c 𝐶)) = (Hom ‘(𝑄 ×c 𝐶))
24		eqid 2821	. . . 4 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
25		eqid 2821	. . . 4 ⊢ (Id‘(𝑄 ×c 𝐶)) = (Id‘(𝑄 ×c 𝐶))
26		eqid 2821	. . . 4 ⊢ (Id‘𝐷) = (Id‘𝐷)
27		eqid 2821	. . . 4 ⊢ (comp‘(𝑄 ×c 𝐶)) = (comp‘(𝑄 ×c 𝐶))
28	19, 2, 3	fuccat 17239	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ Cat)
29	18, 28, 2	xpccat 17439	. . . 4 ⊢ (𝜑 → (𝑄 ×c 𝐶) ∈ Cat)
30		relfunc 17131	. . . . . . . . . . 11 ⊢ Rel (𝐶 Func 𝐷)
31		simpr 487	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → 𝑓 ∈ (𝐶 Func 𝐷))
32		1st2ndbr 7740	. . . . . . . . . . 11 ⊢ ((Rel (𝐶 Func 𝐷) ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → (1st ‘𝑓)(𝐶 Func 𝐷)(2nd ‘𝑓))
33	30, 31, 32	sylancr 589	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → (1st ‘𝑓)(𝐶 Func 𝐷)(2nd ‘𝑓))
34	4, 22, 33	funcf1 17135	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → (1st ‘𝑓):(Base‘𝐶)⟶(Base‘𝐷))
35	34	ffvelrnda 6850	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘𝑓)‘𝑥) ∈ (Base‘𝐷))
36	35	ralrimiva 3182	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → ∀𝑥 ∈ (Base‘𝐶)((1st ‘𝑓)‘𝑥) ∈ (Base‘𝐷))
37	36	ralrimiva 3182	. . . . . 6 ⊢ (𝜑 → ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑥 ∈ (Base‘𝐶)((1st ‘𝑓)‘𝑥) ∈ (Base‘𝐷))
38		eqid 2821	. . . . . . 7 ⊢ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘𝑓)‘𝑥)) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘𝑓)‘𝑥))
39	38	fmpo 7765	. . . . . 6 ⊢ (∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑥 ∈ (Base‘𝐶)((1st ‘𝑓)‘𝑥) ∈ (Base‘𝐷) ↔ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘𝑓)‘𝑥)):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷))
40	37, 39	sylib 220	. . . . 5 ⊢ (𝜑 → (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘𝑓)‘𝑥)):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷))
41	11, 13	op1std 7698	. . . . . . 7 ⊢ (𝐸 = ⟨(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩(comp‘𝐷)((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))))⟩ → (1st ‘𝐸) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘𝑓)‘𝑥)))
42	8, 41	syl 17	. . . . . 6 ⊢ (𝜑 → (1st ‘𝐸) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘𝑓)‘𝑥)))
43	42	feq1d 6498	. . . . 5 ⊢ (𝜑 → ((1st ‘𝐸):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷) ↔ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘𝑓)‘𝑥)):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷)))
44	40, 43	mpbird 259	. . . 4 ⊢ (𝜑 → (1st ‘𝐸):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷))
45		eqid 2821	. . . . . 6 ⊢ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩(comp‘𝐷)((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔)))) = (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩(comp‘𝐷)((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))))
46		ovex 7188	. . . . . . . . 9 ⊢ (𝑚(𝐶 Nat 𝐷)𝑛) ∈ V
47		ovex 7188	. . . . . . . . 9 ⊢ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ∈ V
48	46, 47	mpoex 7776	. . . . . . . 8 ⊢ (𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩(comp‘𝐷)((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))) ∈ V
49	48	csbex 5214	. . . . . . 7 ⊢ ⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩(comp‘𝐷)((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))) ∈ V
50	49	csbex 5214	. . . . . 6 ⊢ ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩(comp‘𝐷)((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))) ∈ V
51	45, 50	fnmpoi 7767	. . . . 5 ⊢ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩(comp‘𝐷)((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔)))) Fn (((𝐶 Func 𝐷) × (Base‘𝐶)) × ((𝐶 Func 𝐷) × (Base‘𝐶)))
52	11, 13	op2ndd 7699	. . . . . . 7 ⊢ (𝐸 = ⟨(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩(comp‘𝐷)((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))))⟩ → (2nd ‘𝐸) = (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩(comp‘𝐷)((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔)))))
53	8, 52	syl 17	. . . . . 6 ⊢ (𝜑 → (2nd ‘𝐸) = (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩(comp‘𝐷)((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔)))))
54	53	fneq1d 6445	. . . . 5 ⊢ (𝜑 → ((2nd ‘𝐸) Fn (((𝐶 Func 𝐷) × (Base‘𝐶)) × ((𝐶 Func 𝐷) × (Base‘𝐶))) ↔ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ ⦋(1st ‘𝑥) / 𝑚⦌⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(⟨((1st ‘𝑚)‘(2nd ‘𝑥)), ((1st ‘𝑚)‘(2nd ‘𝑦))⟩(comp‘𝐷)((1st ‘𝑛)‘(2nd ‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔)))) Fn (((𝐶 Func 𝐷) × (Base‘𝐶)) × ((𝐶 Func 𝐷) × (Base‘𝐶)))))
55	51, 54	mpbiri 260	. . . 4 ⊢ (𝜑 → (2nd ‘𝐸) Fn (((𝐶 Func 𝐷) × (Base‘𝐶)) × ((𝐶 Func 𝐷) × (Base‘𝐶))))
56	3	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝐷 ∈ Cat)
57	56	adantr 483	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝐷 ∈ Cat)
58		simplrl 775	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑓 ∈ (𝐶 Func 𝐷))
59	30, 58, 32	sylancr 589	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1st ‘𝑓)(𝐶 Func 𝐷)(2nd ‘𝑓))
60	4, 22, 59	funcf1 17135	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1st ‘𝑓):(Base‘𝐶)⟶(Base‘𝐷))
61	60	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (1st ‘𝑓):(Base‘𝐶)⟶(Base‘𝐷))
62		simplrr 776	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑢 ∈ (Base‘𝐶))
63	62	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑢 ∈ (Base‘𝐶))
64	61, 63	ffvelrnd 6851	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((1st ‘𝑓)‘𝑢) ∈ (Base‘𝐷))
65		simplrr 776	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑣 ∈ (Base‘𝐶))
66	61, 65	ffvelrnd 6851	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((1st ‘𝑓)‘𝑣) ∈ (Base‘𝐷))
67		simprl 769	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑔 ∈ (𝐶 Func 𝐷))
68		1st2ndbr 7740	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Rel (𝐶 Func 𝐷) ∧ 𝑔 ∈ (𝐶 Func 𝐷)) → (1st ‘𝑔)(𝐶 Func 𝐷)(2nd ‘𝑔))
69	30, 67, 68	sylancr 589	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1st ‘𝑔)(𝐶 Func 𝐷)(2nd ‘𝑔))
70	4, 22, 69	funcf1 17135	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1st ‘𝑔):(Base‘𝐶)⟶(Base‘𝐷))
71	70	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (1st ‘𝑔):(Base‘𝐶)⟶(Base‘𝐷))
72	71, 65	ffvelrnd 6851	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((1st ‘𝑔)‘𝑣) ∈ (Base‘𝐷))
73		simprr 771	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑣 ∈ (Base‘𝐶))
74	4, 5, 24, 59, 62, 73	funcf2 17137	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑢(2nd ‘𝑓)𝑣):(𝑢(Hom ‘𝐶)𝑣)⟶(((1st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1st ‘𝑓)‘𝑣)))
75	74	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (𝑢(2nd ‘𝑓)𝑣):(𝑢(Hom ‘𝐶)𝑣)⟶(((1st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1st ‘𝑓)‘𝑣)))
76		simprr 771	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))
77	75, 76	ffvelrnd 6851	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((𝑢(2nd ‘𝑓)𝑣)‘ℎ) ∈ (((1st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1st ‘𝑓)‘𝑣)))
78		simprl 769	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔))
79	7, 78	nat1st2nd 17220	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑎 ∈ (⟨(1st ‘𝑓), (2nd ‘𝑓)⟩(𝐶 Nat 𝐷)⟨(1st ‘𝑔), (2nd ‘𝑔)⟩))
80	7, 79, 4, 24, 65	natcl 17222	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (𝑎‘𝑣) ∈ (((1st ‘𝑓)‘𝑣)(Hom ‘𝐷)((1st ‘𝑔)‘𝑣)))
81	22, 24, 6, 57, 64, 66, 72, 77, 80	catcocl 16955	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((𝑎‘𝑣)(⟨((1st ‘𝑓)‘𝑢), ((1st ‘𝑓)‘𝑣)⟩(comp‘𝐷)((1st ‘𝑔)‘𝑣))((𝑢(2nd ‘𝑓)𝑣)‘ℎ)) ∈ (((1st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1st ‘𝑔)‘𝑣)))
82	81	ralrimivva 3191	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → ∀𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔)∀ℎ ∈ (𝑢(Hom ‘𝐶)𝑣)((𝑎‘𝑣)(⟨((1st ‘𝑓)‘𝑢), ((1st ‘𝑓)‘𝑣)⟩(comp‘𝐷)((1st ‘𝑔)‘𝑣))((𝑢(2nd ‘𝑓)𝑣)‘ℎ)) ∈ (((1st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1st ‘𝑔)‘𝑣)))
83		eqid 2821	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ℎ ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎‘𝑣)(⟨((1st ‘𝑓)‘𝑢), ((1st ‘𝑓)‘𝑣)⟩(comp‘𝐷)((1st ‘𝑔)‘𝑣))((𝑢(2nd ‘𝑓)𝑣)‘ℎ))) = (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ℎ ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎‘𝑣)(⟨((1st ‘𝑓)‘𝑢), ((1st ‘𝑓)‘𝑣)⟩(comp‘𝐷)((1st ‘𝑔)‘𝑣))((𝑢(2nd ‘𝑓)𝑣)‘ℎ)))
84	83	fmpo 7765	. . . . . . . . . . . . 13 ⊢ (∀𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔)∀ℎ ∈ (𝑢(Hom ‘𝐶)𝑣)((𝑎‘𝑣)(⟨((1st ‘𝑓)‘𝑢), ((1st ‘𝑓)‘𝑣)⟩(comp‘𝐷)((1st ‘𝑔)‘𝑣))((𝑢(2nd ‘𝑓)𝑣)‘ℎ)) ∈ (((1st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1st ‘𝑔)‘𝑣)) ↔ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ℎ ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎‘𝑣)(⟨((1st ‘𝑓)‘𝑢), ((1st ‘𝑓)‘𝑣)⟩(comp‘𝐷)((1st ‘𝑔)‘𝑣))((𝑢(2nd ‘𝑓)𝑣)‘ℎ))):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1st ‘𝑔)‘𝑣)))
85	82, 84	sylib 220	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ℎ ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎‘𝑣)(⟨((1st ‘𝑓)‘𝑢), ((1st ‘𝑓)‘𝑣)⟩(comp‘𝐷)((1st ‘𝑔)‘𝑣))((𝑢(2nd ‘𝑓)𝑣)‘ℎ))):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1st ‘𝑔)‘𝑣)))
86	2	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝐶 ∈ Cat)
87		eqid 2821	. . . . . . . . . . . . . 14 ⊢ (⟨𝑓, 𝑢⟩(2nd ‘𝐸)⟨𝑔, 𝑣⟩) = (⟨𝑓, 𝑢⟩(2nd ‘𝐸)⟨𝑔, 𝑣⟩)
88	1, 86, 56, 4, 5, 6, 7, 58, 67, 62, 73, 87	evlf2 17467	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(2nd ‘𝐸)⟨𝑔, 𝑣⟩) = (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ℎ ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎‘𝑣)(⟨((1st ‘𝑓)‘𝑢), ((1st ‘𝑓)‘𝑣)⟩(comp‘𝐷)((1st ‘𝑔)‘𝑣))((𝑢(2nd ‘𝑓)𝑣)‘ℎ))))
89	88	feq1d 6498	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2nd ‘𝐸)⟨𝑔, 𝑣⟩):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1st ‘𝑔)‘𝑣)) ↔ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ℎ ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎‘𝑣)(⟨((1st ‘𝑓)‘𝑢), ((1st ‘𝑓)‘𝑣)⟩(comp‘𝐷)((1st ‘𝑔)‘𝑣))((𝑢(2nd ‘𝑓)𝑣)‘ℎ))):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1st ‘𝑔)‘𝑣))))
90	85, 89	mpbird 259	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(2nd ‘𝐸)⟨𝑔, 𝑣⟩):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1st ‘𝑔)‘𝑣)))
91	19, 7	fuchom 17230	. . . . . . . . . . . . 13 ⊢ (𝐶 Nat 𝐷) = (Hom ‘𝑄)
92	18, 20, 4, 91, 5, 58, 62, 67, 73, 23	xpchom2 17435	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩) = ((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣)))
93	1, 86, 56, 4, 58, 62	evlf1 17469	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑓(1st ‘𝐸)𝑢) = ((1st ‘𝑓)‘𝑢))
94	1, 86, 56, 4, 67, 73	evlf1 17469	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑔(1st ‘𝐸)𝑣) = ((1st ‘𝑔)‘𝑣))
95	93, 94	oveq12d 7173	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → ((𝑓(1st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st ‘𝐸)𝑣)) = (((1st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1st ‘𝑔)‘𝑣)))
96	92, 95	feq23d 6508	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2nd ‘𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st ‘𝐸)𝑣)) ↔ (⟨𝑓, 𝑢⟩(2nd ‘𝐸)⟨𝑔, 𝑣⟩):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1st ‘𝑔)‘𝑣))))
97	90, 96	mpbird 259	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(2nd ‘𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st ‘𝐸)𝑣)))
98	97	ralrimivva 3191	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2nd ‘𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st ‘𝐸)𝑣)))
99	98	ralrimivva 3191	. . . . . . . 8 ⊢ (𝜑 → ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2nd ‘𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st ‘𝐸)𝑣)))
100		oveq2 7163	. . . . . . . . . . . 12 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → (𝑥(2nd ‘𝐸)𝑦) = (𝑥(2nd ‘𝐸)⟨𝑔, 𝑣⟩))
101		oveq2 7163	. . . . . . . . . . . 12 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) = (𝑥(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩))
102		fveq2 6669	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → ((1st ‘𝐸)‘𝑦) = ((1st ‘𝐸)‘⟨𝑔, 𝑣⟩))
103		df-ov 7158	. . . . . . . . . . . . . 14 ⊢ (𝑔(1st ‘𝐸)𝑣) = ((1st ‘𝐸)‘⟨𝑔, 𝑣⟩)
104	102, 103	syl6eqr 2874	. . . . . . . . . . . . 13 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → ((1st ‘𝐸)‘𝑦) = (𝑔(1st ‘𝐸)𝑣))
105	104	oveq2d 7171	. . . . . . . . . . . 12 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → (((1st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1st ‘𝐸)‘𝑦)) = (((1st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st ‘𝐸)𝑣)))
106	100, 101, 105	feq123d 6502	. . . . . . . . . . 11 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → ((𝑥(2nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1st ‘𝐸)‘𝑦)) ↔ (𝑥(2nd ‘𝐸)⟨𝑔, 𝑣⟩):(𝑥(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶(((1st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st ‘𝐸)𝑣))))
107	106	ralxp 5711	. . . . . . . . . 10 ⊢ (∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1st ‘𝐸)‘𝑦)) ↔ ∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(𝑥(2nd ‘𝐸)⟨𝑔, 𝑣⟩):(𝑥(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶(((1st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st ‘𝐸)𝑣)))
108		oveq1 7162	. . . . . . . . . . . 12 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (𝑥(2nd ‘𝐸)⟨𝑔, 𝑣⟩) = (⟨𝑓, 𝑢⟩(2nd ‘𝐸)⟨𝑔, 𝑣⟩))
109		oveq1 7162	. . . . . . . . . . . 12 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (𝑥(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩) = (⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩))
110		fveq2 6669	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((1st ‘𝐸)‘𝑥) = ((1st ‘𝐸)‘⟨𝑓, 𝑢⟩))
111		df-ov 7158	. . . . . . . . . . . . . 14 ⊢ (𝑓(1st ‘𝐸)𝑢) = ((1st ‘𝐸)‘⟨𝑓, 𝑢⟩)
112	110, 111	syl6eqr 2874	. . . . . . . . . . . . 13 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((1st ‘𝐸)‘𝑥) = (𝑓(1st ‘𝐸)𝑢))
113	112	oveq1d 7170	. . . . . . . . . . . 12 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (((1st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st ‘𝐸)𝑣)) = ((𝑓(1st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st ‘𝐸)𝑣)))
114	108, 109, 113	feq123d 6502	. . . . . . . . . . 11 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((𝑥(2nd ‘𝐸)⟨𝑔, 𝑣⟩):(𝑥(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶(((1st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st ‘𝐸)𝑣)) ↔ (⟨𝑓, 𝑢⟩(2nd ‘𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st ‘𝐸)𝑣))))
115	114	2ralbidv 3199	. . . . . . . . . 10 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(𝑥(2nd ‘𝐸)⟨𝑔, 𝑣⟩):(𝑥(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶(((1st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st ‘𝐸)𝑣)) ↔ ∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2nd ‘𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st ‘𝐸)𝑣))))
116	107, 115	syl5bb 285	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1st ‘𝐸)‘𝑦)) ↔ ∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2nd ‘𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st ‘𝐸)𝑣))))
117	116	ralxp 5711	. . . . . . . 8 ⊢ (∀𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1st ‘𝐸)‘𝑦)) ↔ ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2nd ‘𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st ‘𝐸)𝑣)))
118	99, 117	sylibr 236	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1st ‘𝐸)‘𝑦)))
119	118	r19.21bi 3208	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) → ∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1st ‘𝐸)‘𝑦)))
120	119	r19.21bi 3208	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) → (𝑥(2nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1st ‘𝐸)‘𝑦)))
121	120	anasss 469	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))) → (𝑥(2nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1st ‘𝐸)‘𝑦)))
122	28	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝑄 ∈ Cat)
123	2	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝐶 ∈ Cat)
124		eqid 2821	. . . . . . . . . . 11 ⊢ (Id‘𝑄) = (Id‘𝑄)
125		eqid 2821	. . . . . . . . . . 11 ⊢ (Id‘𝐶) = (Id‘𝐶)
126		simprl 769	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝑓 ∈ (𝐶 Func 𝐷))
127		simprr 771	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝑢 ∈ (Base‘𝐶))
128	18, 122, 123, 20, 4, 124, 125, 25, 126, 127	xpcid 17438	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩) = ⟨((Id‘𝑄)‘𝑓), ((Id‘𝐶)‘𝑢)⟩)
129	128	fveq2d 6673	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((⟨𝑓, 𝑢⟩(2nd ‘𝐸)⟨𝑓, 𝑢⟩)‘⟨((Id‘𝑄)‘𝑓), ((Id‘𝐶)‘𝑢)⟩))
130		df-ov 7158	. . . . . . . . 9 ⊢ (((Id‘𝑄)‘𝑓)(⟨𝑓, 𝑢⟩(2nd ‘𝐸)⟨𝑓, 𝑢⟩)((Id‘𝐶)‘𝑢)) = ((⟨𝑓, 𝑢⟩(2nd ‘𝐸)⟨𝑓, 𝑢⟩)‘⟨((Id‘𝑄)‘𝑓), ((Id‘𝐶)‘𝑢)⟩)
131	129, 130	syl6eqr 2874	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)) = (((Id‘𝑄)‘𝑓)(⟨𝑓, 𝑢⟩(2nd ‘𝐸)⟨𝑓, 𝑢⟩)((Id‘𝐶)‘𝑢)))
132	3	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝐷 ∈ Cat)
133		eqid 2821	. . . . . . . . 9 ⊢ (⟨𝑓, 𝑢⟩(2nd ‘𝐸)⟨𝑓, 𝑢⟩) = (⟨𝑓, 𝑢⟩(2nd ‘𝐸)⟨𝑓, 𝑢⟩)
134	20, 91, 124, 122, 126	catidcl 16952	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝑄)‘𝑓) ∈ (𝑓(𝐶 Nat 𝐷)𝑓))
135	4, 5, 125, 123, 127	catidcl 16952	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝐶)‘𝑢) ∈ (𝑢(Hom ‘𝐶)𝑢))
136	1, 123, 132, 4, 5, 6, 7, 126, 126, 127, 127, 133, 134, 135	evlf2val 17468	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝑄)‘𝑓)(⟨𝑓, 𝑢⟩(2nd ‘𝐸)⟨𝑓, 𝑢⟩)((Id‘𝐶)‘𝑢)) = ((((Id‘𝑄)‘𝑓)‘𝑢)(⟨((1st ‘𝑓)‘𝑢), ((1st ‘𝑓)‘𝑢)⟩(comp‘𝐷)((1st ‘𝑓)‘𝑢))((𝑢(2nd ‘𝑓)𝑢)‘((Id‘𝐶)‘𝑢))))
137	30, 126, 32	sylancr 589	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (1st ‘𝑓)(𝐶 Func 𝐷)(2nd ‘𝑓))
138	4, 22, 137	funcf1 17135	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (1st ‘𝑓):(Base‘𝐶)⟶(Base‘𝐷))
139	138, 127	ffvelrnd 6851	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((1st ‘𝑓)‘𝑢) ∈ (Base‘𝐷))
140	22, 24, 26, 132, 139	catidcl 16952	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝐷)‘((1st ‘𝑓)‘𝑢)) ∈ (((1st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1st ‘𝑓)‘𝑢)))
141	22, 24, 26, 132, 139, 6, 139, 140	catlid 16953	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝐷)‘((1st ‘𝑓)‘𝑢))(⟨((1st ‘𝑓)‘𝑢), ((1st ‘𝑓)‘𝑢)⟩(comp‘𝐷)((1st ‘𝑓)‘𝑢))((Id‘𝐷)‘((1st ‘𝑓)‘𝑢))) = ((Id‘𝐷)‘((1st ‘𝑓)‘𝑢)))
142	19, 124, 26, 126	fucid 17240	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝑄)‘𝑓) = ((Id‘𝐷) ∘ (1st ‘𝑓)))
143	142	fveq1d 6671	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝑄)‘𝑓)‘𝑢) = (((Id‘𝐷) ∘ (1st ‘𝑓))‘𝑢))
144		fvco3 6759	. . . . . . . . . . . 12 ⊢ (((1st ‘𝑓):(Base‘𝐶)⟶(Base‘𝐷) ∧ 𝑢 ∈ (Base‘𝐶)) → (((Id‘𝐷) ∘ (1st ‘𝑓))‘𝑢) = ((Id‘𝐷)‘((1st ‘𝑓)‘𝑢)))
145	138, 127, 144	syl2anc 586	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝐷) ∘ (1st ‘𝑓))‘𝑢) = ((Id‘𝐷)‘((1st ‘𝑓)‘𝑢)))
146	143, 145	eqtrd 2856	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝑄)‘𝑓)‘𝑢) = ((Id‘𝐷)‘((1st ‘𝑓)‘𝑢)))
147	4, 125, 26, 137, 127	funcid 17139	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((𝑢(2nd ‘𝑓)𝑢)‘((Id‘𝐶)‘𝑢)) = ((Id‘𝐷)‘((1st ‘𝑓)‘𝑢)))
148	146, 147	oveq12d 7173	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((((Id‘𝑄)‘𝑓)‘𝑢)(⟨((1st ‘𝑓)‘𝑢), ((1st ‘𝑓)‘𝑢)⟩(comp‘𝐷)((1st ‘𝑓)‘𝑢))((𝑢(2nd ‘𝑓)𝑢)‘((Id‘𝐶)‘𝑢))) = (((Id‘𝐷)‘((1st ‘𝑓)‘𝑢))(⟨((1st ‘𝑓)‘𝑢), ((1st ‘𝑓)‘𝑢)⟩(comp‘𝐷)((1st ‘𝑓)‘𝑢))((Id‘𝐷)‘((1st ‘𝑓)‘𝑢))))
149	1, 123, 132, 4, 126, 127	evlf1 17469	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (𝑓(1st ‘𝐸)𝑢) = ((1st ‘𝑓)‘𝑢))
150	149	fveq2d 6673	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝐷)‘(𝑓(1st ‘𝐸)𝑢)) = ((Id‘𝐷)‘((1st ‘𝑓)‘𝑢)))
151	141, 148, 150	3eqtr4d 2866	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((((Id‘𝑄)‘𝑓)‘𝑢)(⟨((1st ‘𝑓)‘𝑢), ((1st ‘𝑓)‘𝑢)⟩(comp‘𝐷)((1st ‘𝑓)‘𝑢))((𝑢(2nd ‘𝑓)𝑢)‘((Id‘𝐶)‘𝑢))) = ((Id‘𝐷)‘(𝑓(1st ‘𝐸)𝑢)))
152	131, 136, 151	3eqtrd 2860	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1st ‘𝐸)𝑢)))
153	152	ralrimivva 3191	. . . . . 6 ⊢ (𝜑 → ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)((⟨𝑓, 𝑢⟩(2nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1st ‘𝐸)𝑢)))
154		id 22	. . . . . . . . . 10 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → 𝑥 = ⟨𝑓, 𝑢⟩)
155	154, 154	oveq12d 7173	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (𝑥(2nd ‘𝐸)𝑥) = (⟨𝑓, 𝑢⟩(2nd ‘𝐸)⟨𝑓, 𝑢⟩))
156		fveq2 6669	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((Id‘(𝑄 ×c 𝐶))‘𝑥) = ((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩))
157	155, 156	fveq12d 6676	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((𝑥(2nd ‘𝐸)𝑥)‘((Id‘(𝑄 ×c 𝐶))‘𝑥)) = ((⟨𝑓, 𝑢⟩(2nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)))
158	112	fveq2d 6673	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((Id‘𝐷)‘((1st ‘𝐸)‘𝑥)) = ((Id‘𝐷)‘(𝑓(1st ‘𝐸)𝑢)))
159	157, 158	eqeq12d 2837	. . . . . . 7 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (((𝑥(2nd ‘𝐸)𝑥)‘((Id‘(𝑄 ×c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1st ‘𝐸)‘𝑥)) ↔ ((⟨𝑓, 𝑢⟩(2nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1st ‘𝐸)𝑢))))
160	159	ralxp 5711	. . . . . 6 ⊢ (∀𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))((𝑥(2nd ‘𝐸)𝑥)‘((Id‘(𝑄 ×c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1st ‘𝐸)‘𝑥)) ↔ ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)((⟨𝑓, 𝑢⟩(2nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1st ‘𝐸)𝑢)))
161	153, 160	sylibr 236	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))((𝑥(2nd ‘𝐸)𝑥)‘((Id‘(𝑄 ×c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1st ‘𝐸)‘𝑥)))
162	161	r19.21bi 3208	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) → ((𝑥(2nd ‘𝐸)𝑥)‘((Id‘(𝑄 ×c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1st ‘𝐸)‘𝑥)))
163	2	3ad2ant1 1129	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝐶 ∈ Cat)
164	3	3ad2ant1 1129	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝐷 ∈ Cat)
165		simp21 1202	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
166		1st2nd2 7727	. . . . . . . . 9 ⊢ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
167	165, 166	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
168	167, 165	eqeltrrd 2914	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
169		opelxp 5590	. . . . . . 7 ⊢ (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↔ ((1st ‘𝑥) ∈ (𝐶 Func 𝐷) ∧ (2nd ‘𝑥) ∈ (Base‘𝐶)))
170	168, 169	sylib 220	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st ‘𝑥) ∈ (𝐶 Func 𝐷) ∧ (2nd ‘𝑥) ∈ (Base‘𝐶)))
171		simp22 1203	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
172		1st2nd2 7727	. . . . . . . . 9 ⊢ (𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
173	171, 172	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
174	173, 171	eqeltrrd 2914	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
175		opelxp 5590	. . . . . . 7 ⊢ (⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↔ ((1st ‘𝑦) ∈ (𝐶 Func 𝐷) ∧ (2nd ‘𝑦) ∈ (Base‘𝐶)))
176	174, 175	sylib 220	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st ‘𝑦) ∈ (𝐶 Func 𝐷) ∧ (2nd ‘𝑦) ∈ (Base‘𝐶)))
177		simp23 1204	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
178		1st2nd2 7727	. . . . . . . . 9 ⊢ (𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) → 𝑧 = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
179	177, 178	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑧 = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
180	179, 177	eqeltrrd 2914	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
181		opelxp 5590	. . . . . . 7 ⊢ (⟨(1st ‘𝑧), (2nd ‘𝑧)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↔ ((1st ‘𝑧) ∈ (𝐶 Func 𝐷) ∧ (2nd ‘𝑧) ∈ (Base‘𝐶)))
182	180, 181	sylib 220	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st ‘𝑧) ∈ (𝐶 Func 𝐷) ∧ (2nd ‘𝑧) ∈ (Base‘𝐶)))
183		simp3l 1197	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦))
184	18, 21, 91, 5, 23, 165, 171	xpchom 17429	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) = (((1st ‘𝑥)(𝐶 Nat 𝐷)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))))
185	183, 184	eleqtrd 2915	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑓 ∈ (((1st ‘𝑥)(𝐶 Nat 𝐷)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))))
186		1st2nd2 7727	. . . . . . . . 9 ⊢ (𝑓 ∈ (((1st ‘𝑥)(𝐶 Nat 𝐷)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))) → 𝑓 = ⟨(1st ‘𝑓), (2nd ‘𝑓)⟩)
187	185, 186	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑓 = ⟨(1st ‘𝑓), (2nd ‘𝑓)⟩)
188	187, 185	eqeltrrd 2914	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ⟨(1st ‘𝑓), (2nd ‘𝑓)⟩ ∈ (((1st ‘𝑥)(𝐶 Nat 𝐷)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))))
189		opelxp 5590	. . . . . . 7 ⊢ (⟨(1st ‘𝑓), (2nd ‘𝑓)⟩ ∈ (((1st ‘𝑥)(𝐶 Nat 𝐷)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))) ↔ ((1st ‘𝑓) ∈ ((1st ‘𝑥)(𝐶 Nat 𝐷)(1st ‘𝑦)) ∧ (2nd ‘𝑓) ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))))
190	188, 189	sylib 220	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st ‘𝑓) ∈ ((1st ‘𝑥)(𝐶 Nat 𝐷)(1st ‘𝑦)) ∧ (2nd ‘𝑓) ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))))
191		simp3r 1198	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))
192	18, 21, 91, 5, 23, 171, 177	xpchom 17429	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧) = (((1st ‘𝑦)(𝐶 Nat 𝐷)(1st ‘𝑧)) × ((2nd ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧))))
193	191, 192	eleqtrd 2915	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑔 ∈ (((1st ‘𝑦)(𝐶 Nat 𝐷)(1st ‘𝑧)) × ((2nd ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧))))
194		1st2nd2 7727	. . . . . . . . 9 ⊢ (𝑔 ∈ (((1st ‘𝑦)(𝐶 Nat 𝐷)(1st ‘𝑧)) × ((2nd ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧))) → 𝑔 = ⟨(1st ‘𝑔), (2nd ‘𝑔)⟩)
195	193, 194	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑔 = ⟨(1st ‘𝑔), (2nd ‘𝑔)⟩)
196	195, 193	eqeltrrd 2914	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ⟨(1st ‘𝑔), (2nd ‘𝑔)⟩ ∈ (((1st ‘𝑦)(𝐶 Nat 𝐷)(1st ‘𝑧)) × ((2nd ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧))))
197		opelxp 5590	. . . . . . 7 ⊢ (⟨(1st ‘𝑔), (2nd ‘𝑔)⟩ ∈ (((1st ‘𝑦)(𝐶 Nat 𝐷)(1st ‘𝑧)) × ((2nd ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧))) ↔ ((1st ‘𝑔) ∈ ((1st ‘𝑦)(𝐶 Nat 𝐷)(1st ‘𝑧)) ∧ (2nd ‘𝑔) ∈ ((2nd ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧))))
198	196, 197	sylib 220	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st ‘𝑔) ∈ ((1st ‘𝑦)(𝐶 Nat 𝐷)(1st ‘𝑧)) ∧ (2nd ‘𝑔) ∈ ((2nd ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧))))
199	1, 19, 163, 164, 7, 170, 176, 182, 190, 198	evlfcllem 17470	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(2nd ‘𝐸)⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)‘(⟨(1st ‘𝑔), (2nd ‘𝑔)⟩(⟨⟨(1st ‘𝑥), (2nd ‘𝑥)⟩, ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩⟩(comp‘(𝑄 ×c 𝐶))⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)⟨(1st ‘𝑓), (2nd ‘𝑓)⟩)) = (((⟨(1st ‘𝑦), (2nd ‘𝑦)⟩(2nd ‘𝐸)⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)‘⟨(1st ‘𝑔), (2nd ‘𝑔)⟩)(⟨((1st ‘𝐸)‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩), ((1st ‘𝐸)‘⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)⟩(comp‘𝐷)((1st ‘𝐸)‘⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))((⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(2nd ‘𝐸)⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)‘⟨(1st ‘𝑓), (2nd ‘𝑓)⟩)))
200	167, 179	oveq12d 7173	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (𝑥(2nd ‘𝐸)𝑧) = (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(2nd ‘𝐸)⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
201	167, 173	opeq12d 4810	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ⟨𝑥, 𝑦⟩ = ⟨⟨(1st ‘𝑥), (2nd ‘𝑥)⟩, ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩⟩)
202	201, 179	oveq12d 7173	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (⟨𝑥, 𝑦⟩(comp‘(𝑄 ×c 𝐶))𝑧) = (⟨⟨(1st ‘𝑥), (2nd ‘𝑥)⟩, ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩⟩(comp‘(𝑄 ×c 𝐶))⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
203	202, 195, 187	oveq123d 7176	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘(𝑄 ×c 𝐶))𝑧)𝑓) = (⟨(1st ‘𝑔), (2nd ‘𝑔)⟩(⟨⟨(1st ‘𝑥), (2nd ‘𝑥)⟩, ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩⟩(comp‘(𝑄 ×c 𝐶))⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)⟨(1st ‘𝑓), (2nd ‘𝑓)⟩))
204	200, 203	fveq12d 6676	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((𝑥(2nd ‘𝐸)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘(𝑄 ×c 𝐶))𝑧)𝑓)) = ((⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(2nd ‘𝐸)⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)‘(⟨(1st ‘𝑔), (2nd ‘𝑔)⟩(⟨⟨(1st ‘𝑥), (2nd ‘𝑥)⟩, ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩⟩(comp‘(𝑄 ×c 𝐶))⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)⟨(1st ‘𝑓), (2nd ‘𝑓)⟩)))
205	167	fveq2d 6673	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st ‘𝐸)‘𝑥) = ((1st ‘𝐸)‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩))
206	173	fveq2d 6673	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st ‘𝐸)‘𝑦) = ((1st ‘𝐸)‘⟨(1st ‘𝑦), (2nd ‘𝑦)⟩))
207	205, 206	opeq12d 4810	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ⟨((1st ‘𝐸)‘𝑥), ((1st ‘𝐸)‘𝑦)⟩ = ⟨((1st ‘𝐸)‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩), ((1st ‘𝐸)‘⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)⟩)
208	179	fveq2d 6673	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st ‘𝐸)‘𝑧) = ((1st ‘𝐸)‘⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
209	207, 208	oveq12d 7173	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (⟨((1st ‘𝐸)‘𝑥), ((1st ‘𝐸)‘𝑦)⟩(comp‘𝐷)((1st ‘𝐸)‘𝑧)) = (⟨((1st ‘𝐸)‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩), ((1st ‘𝐸)‘⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)⟩(comp‘𝐷)((1st ‘𝐸)‘⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)))
210	173, 179	oveq12d 7173	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (𝑦(2nd ‘𝐸)𝑧) = (⟨(1st ‘𝑦), (2nd ‘𝑦)⟩(2nd ‘𝐸)⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
211	210, 195	fveq12d 6676	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((𝑦(2nd ‘𝐸)𝑧)‘𝑔) = ((⟨(1st ‘𝑦), (2nd ‘𝑦)⟩(2nd ‘𝐸)⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)‘⟨(1st ‘𝑔), (2nd ‘𝑔)⟩))
212	167, 173	oveq12d 7173	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (𝑥(2nd ‘𝐸)𝑦) = (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(2nd ‘𝐸)⟨(1st ‘𝑦), (2nd ‘𝑦)⟩))
213	212, 187	fveq12d 6676	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((𝑥(2nd ‘𝐸)𝑦)‘𝑓) = ((⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(2nd ‘𝐸)⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)‘⟨(1st ‘𝑓), (2nd ‘𝑓)⟩))
214	209, 211, 213	oveq123d 7176	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (((𝑦(2nd ‘𝐸)𝑧)‘𝑔)(⟨((1st ‘𝐸)‘𝑥), ((1st ‘𝐸)‘𝑦)⟩(comp‘𝐷)((1st ‘𝐸)‘𝑧))((𝑥(2nd ‘𝐸)𝑦)‘𝑓)) = (((⟨(1st ‘𝑦), (2nd ‘𝑦)⟩(2nd ‘𝐸)⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)‘⟨(1st ‘𝑔), (2nd ‘𝑔)⟩)(⟨((1st ‘𝐸)‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩), ((1st ‘𝐸)‘⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)⟩(comp‘𝐷)((1st ‘𝐸)‘⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))((⟨(1st ‘𝑥), (2nd ‘𝑥)⟩(2nd ‘𝐸)⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)‘⟨(1st ‘𝑓), (2nd ‘𝑓)⟩)))
215	199, 204, 214	3eqtr4d 2866	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((𝑥(2nd ‘𝐸)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘(𝑄 ×c 𝐶))𝑧)𝑓)) = (((𝑦(2nd ‘𝐸)𝑧)‘𝑔)(⟨((1st ‘𝐸)‘𝑥), ((1st ‘𝐸)‘𝑦)⟩(comp‘𝐷)((1st ‘𝐸)‘𝑧))((𝑥(2nd ‘𝐸)𝑦)‘𝑓)))
216	21, 22, 23, 24, 25, 26, 27, 6, 29, 3, 44, 55, 121, 162, 215	isfuncd 17134	. . 3 ⊢ (𝜑 → (1st ‘𝐸)((𝑄 ×c 𝐶) Func 𝐷)(2nd ‘𝐸))
217		df-br 5066	. . 3 ⊢ ((1st ‘𝐸)((𝑄 ×c 𝐶) Func 𝐷)(2nd ‘𝐸) ↔ ⟨(1st ‘𝐸), (2nd ‘𝐸)⟩ ∈ ((𝑄 ×c 𝐶) Func 𝐷))
218	216, 217	sylib 220	. 2 ⊢ (𝜑 → ⟨(1st ‘𝐸), (2nd ‘𝐸)⟩ ∈ ((𝑄 ×c 𝐶) Func 𝐷))
219	17, 218	eqeltrd 2913	1 ⊢ (𝜑 → 𝐸 ∈ ((𝑄 ×c 𝐶) Func 𝐷))

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083   = wceq 1533   ∈ wcel 2110  ∀wral 3138  Vcvv 3494  ⦋csb 3882  ⟨cop 4572   class class class wbr 5065   × cxp 5552   ∘ ccom 5558  Rel wrel 5559   Fn wfn 6349  ⟶wf 6350  ‘cfv 6354  (class class class)co 7155   ∈ cmpo 7157  1^st c1st 7686  2^nd c2nd 7687  Basecbs 16482  Hom chom 16575  compcco 16576  Catccat 16934  Idccid 16935   Func cfunc 17123   Nat cnat 17210   FuncCat cfuc 17211   ×_c cxpc 17417   eval_F cevlf 17458

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-rep 5189  ax-sep 5202  ax-nul 5209  ax-pow 5265  ax-pr 5329  ax-un 7460  ax-cnex 10592  ax-resscn 10593  ax-1cn 10594  ax-icn 10595  ax-addcl 10596  ax-addrcl 10597  ax-mulcl 10598  ax-mulrcl 10599  ax-mulcom 10600  ax-addass 10601  ax-mulass 10602  ax-distr 10603  ax-i2m1 10604  ax-1ne0 10605  ax-1rid 10606  ax-rnegex 10607  ax-rrecex 10608  ax-cnre 10609  ax-pre-lttri 10610  ax-pre-lttrn 10611  ax-pre-ltadd 10612  ax-pre-mulgt0 10613

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-fal 1546  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4838  df-int 4876  df-iun 4920  df-br 5066  df-opab 5128  df-mpt 5146  df-tr 5172  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6147  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-riota 7113  df-ov 7158  df-oprab 7159  df-mpo 7160  df-om 7580  df-1st 7688  df-2nd 7689  df-wrecs 7946  df-recs 8007  df-rdg 8045  df-1o 8101  df-oadd 8105  df-er 8288  df-map 8407  df-ixp 8461  df-en 8509  df-dom 8510  df-sdom 8511  df-fin 8512  df-pnf 10676  df-mnf 10677  df-xr 10678  df-ltxr 10679  df-le 10680  df-sub 10871  df-neg 10872  df-nn 11638  df-2 11699  df-3 11700  df-4 11701  df-5 11702  df-6 11703  df-7 11704  df-8 11705  df-9 11706  df-n0 11897  df-z 11981  df-dec 12098  df-uz 12243  df-fz 12892  df-struct 16484  df-ndx 16485  df-slot 16486  df-base 16488  df-hom 16588  df-cco 16589  df-cat 16938  df-cid 16939  df-func 17127  df-nat 17212  df-fuc 17213  df-xpc 17421  df-evlf 17462

This theorem is referenced by:  uncfcl  17484  uncf1  17485  uncf2  17486  yonedalem1  17521