evlfcl - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > evlfcl		Structured version Visualization version GIF version

Theorem evlfcl 18175

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	⊢ 𝐸 = (𝐶 eval_F 𝐷)
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 ⊢ 𝐸 = (𝐶 eval_F 𝐷)
2		evlfcl.c	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ Cat)
3		evlfcl.d	. . . . 5 ⊢ (𝜑 → 𝐷 ∈ Cat)
4		eqid 2733	. . . . 5 ⊢ (Base‘𝐶) = (Base‘𝐶)
5		eqid 2733	. . . . 5 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
6		eqid 2733	. . . . 5 ⊢ (comp‘𝐷) = (comp‘𝐷)
7		eqid 2733	. . . . 5 ⊢ (𝐶 Nat 𝐷) = (𝐶 Nat 𝐷)
8	1, 2, 3, 4, 5, 6, 7	evlfval 18170	. . . 4 ⊢ (𝜑 → 𝐸 = ⟨(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1^st ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ ⦋(1^st ‘𝑥) / 𝑚⦌⦋(1^st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2^nd ‘𝑥)(Hom ‘𝐶)(2^nd ‘𝑦)) ↦ ((𝑎‘(2^nd ‘𝑦))(⟨((1^st ‘𝑚)‘(2^nd ‘𝑥)), ((1^st ‘𝑚)‘(2^nd ‘𝑦))⟩(comp‘𝐷)((1^st ‘𝑛)‘(2^nd ‘𝑦)))(((2^nd ‘𝑥)(2^nd ‘𝑚)(2^nd ‘𝑦))‘𝑔))))⟩)
9		ovex 7442	. . . . . 6 ⊢ (𝐶 Func 𝐷) ∈ V
10		fvex 6905	. . . . . 6 ⊢ (Base‘𝐶) ∈ V
11	9, 10	mpoex 8066	. . . . 5 ⊢ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1^st ‘𝑓)‘𝑥)) ∈ V
12	9, 10	xpex 7740	. . . . . 6 ⊢ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∈ V
13	12, 12	mpoex 8066	. . . . 5 ⊢ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ ⦋(1^st ‘𝑥) / 𝑚⦌⦋(1^st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2^nd ‘𝑥)(Hom ‘𝐶)(2^nd ‘𝑦)) ↦ ((𝑎‘(2^nd ‘𝑦))(⟨((1^st ‘𝑚)‘(2^nd ‘𝑥)), ((1^st ‘𝑚)‘(2^nd ‘𝑦))⟩(comp‘𝐷)((1^st ‘𝑛)‘(2^nd ‘𝑦)))(((2^nd ‘𝑥)(2^nd ‘𝑚)(2^nd ‘𝑦))‘𝑔)))) ∈ V
14	11, 13	opelvv 5717	. . . 4 ⊢ ⟨(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1^st ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ ⦋(1^st ‘𝑥) / 𝑚⦌⦋(1^st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2^nd ‘𝑥)(Hom ‘𝐶)(2^nd ‘𝑦)) ↦ ((𝑎‘(2^nd ‘𝑦))(⟨((1^st ‘𝑚)‘(2^nd ‘𝑥)), ((1^st ‘𝑚)‘(2^nd ‘𝑦))⟩(comp‘𝐷)((1^st ‘𝑛)‘(2^nd ‘𝑦)))(((2^nd ‘𝑥)(2^nd ‘𝑚)(2^nd ‘𝑦))‘𝑔))))⟩ ∈ (V × V)
15	8, 14	eqeltrdi 2842	. . 3 ⊢ (𝜑 → 𝐸 ∈ (V × V))
16		1st2nd2 8014	. . 3 ⊢ (𝐸 ∈ (V × V) → 𝐸 = ⟨(1^st ‘𝐸), (2^nd ‘𝐸)⟩)
17	15, 16	syl 17	. 2 ⊢ (𝜑 → 𝐸 = ⟨(1^st ‘𝐸), (2^nd ‘𝐸)⟩)
18		eqid 2733	. . . . 5 ⊢ (𝑄 ×_c 𝐶) = (𝑄 ×_c 𝐶)
19		evlfcl.q	. . . . . 6 ⊢ 𝑄 = (𝐶 FuncCat 𝐷)
20	19	fucbas 17912	. . . . 5 ⊢ (𝐶 Func 𝐷) = (Base‘𝑄)
21	18, 20, 4	xpcbas 18130	. . . 4 ⊢ ((𝐶 Func 𝐷) × (Base‘𝐶)) = (Base‘(𝑄 ×_c 𝐶))
22		eqid 2733	. . . 4 ⊢ (Base‘𝐷) = (Base‘𝐷)
23		eqid 2733	. . . 4 ⊢ (Hom ‘(𝑄 ×_c 𝐶)) = (Hom ‘(𝑄 ×_c 𝐶))
24		eqid 2733	. . . 4 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
25		eqid 2733	. . . 4 ⊢ (Id‘(𝑄 ×_c 𝐶)) = (Id‘(𝑄 ×_c 𝐶))
26		eqid 2733	. . . 4 ⊢ (Id‘𝐷) = (Id‘𝐷)
27		eqid 2733	. . . 4 ⊢ (comp‘(𝑄 ×_c 𝐶)) = (comp‘(𝑄 ×_c 𝐶))
28	19, 2, 3	fuccat 17923	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ Cat)
29	18, 28, 2	xpccat 18142	. . . 4 ⊢ (𝜑 → (𝑄 ×_c 𝐶) ∈ Cat)
30		relfunc 17812	. . . . . . . . . . 11 ⊢ Rel (𝐶 Func 𝐷)
31		simpr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → 𝑓 ∈ (𝐶 Func 𝐷))
32		1st2ndbr 8028	. . . . . . . . . . 11 ⊢ ((Rel (𝐶 Func 𝐷) ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → (1^st ‘𝑓)(𝐶 Func 𝐷)(2^nd ‘𝑓))
33	30, 31, 32	sylancr 588	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → (1^st ‘𝑓)(𝐶 Func 𝐷)(2^nd ‘𝑓))
34	4, 22, 33	funcf1 17816	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → (1^st ‘𝑓):(Base‘𝐶)⟶(Base‘𝐷))
35	34	ffvelcdmda 7087	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) ∧ 𝑥 ∈ (Base‘𝐶)) → ((1^st ‘𝑓)‘𝑥) ∈ (Base‘𝐷))
36	35	ralrimiva 3147	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → ∀𝑥 ∈ (Base‘𝐶)((1^st ‘𝑓)‘𝑥) ∈ (Base‘𝐷))
37	36	ralrimiva 3147	. . . . . 6 ⊢ (𝜑 → ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑥 ∈ (Base‘𝐶)((1^st ‘𝑓)‘𝑥) ∈ (Base‘𝐷))
38		eqid 2733	. . . . . . 7 ⊢ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1^st ‘𝑓)‘𝑥)) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1^st ‘𝑓)‘𝑥))
39	38	fmpo 8054	. . . . . 6 ⊢ (∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑥 ∈ (Base‘𝐶)((1^st ‘𝑓)‘𝑥) ∈ (Base‘𝐷) ↔ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1^st ‘𝑓)‘𝑥)):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷))
40	37, 39	sylib 217	. . . . 5 ⊢ (𝜑 → (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1^st ‘𝑓)‘𝑥)):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷))
41	11, 13	op1std 7985	. . . . . . 7 ⊢ (𝐸 = ⟨(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1^st ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ ⦋(1^st ‘𝑥) / 𝑚⦌⦋(1^st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2^nd ‘𝑥)(Hom ‘𝐶)(2^nd ‘𝑦)) ↦ ((𝑎‘(2^nd ‘𝑦))(⟨((1^st ‘𝑚)‘(2^nd ‘𝑥)), ((1^st ‘𝑚)‘(2^nd ‘𝑦))⟩(comp‘𝐷)((1^st ‘𝑛)‘(2^nd ‘𝑦)))(((2^nd ‘𝑥)(2^nd ‘𝑚)(2^nd ‘𝑦))‘𝑔))))⟩ → (1^st ‘𝐸) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1^st ‘𝑓)‘𝑥)))
42	8, 41	syl 17	. . . . . 6 ⊢ (𝜑 → (1^st ‘𝐸) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1^st ‘𝑓)‘𝑥)))
43	42	feq1d 6703	. . . . 5 ⊢ (𝜑 → ((1^st ‘𝐸):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷) ↔ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1^st ‘𝑓)‘𝑥)):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷)))
44	40, 43	mpbird 257	. . . 4 ⊢ (𝜑 → (1^st ‘𝐸):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷))
45		eqid 2733	. . . . . 6 ⊢ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ ⦋(1^st ‘𝑥) / 𝑚⦌⦋(1^st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2^nd ‘𝑥)(Hom ‘𝐶)(2^nd ‘𝑦)) ↦ ((𝑎‘(2^nd ‘𝑦))(⟨((1^st ‘𝑚)‘(2^nd ‘𝑥)), ((1^st ‘𝑚)‘(2^nd ‘𝑦))⟩(comp‘𝐷)((1^st ‘𝑛)‘(2^nd ‘𝑦)))(((2^nd ‘𝑥)(2^nd ‘𝑚)(2^nd ‘𝑦))‘𝑔)))) = (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ ⦋(1^st ‘𝑥) / 𝑚⦌⦋(1^st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2^nd ‘𝑥)(Hom ‘𝐶)(2^nd ‘𝑦)) ↦ ((𝑎‘(2^nd ‘𝑦))(⟨((1^st ‘𝑚)‘(2^nd ‘𝑥)), ((1^st ‘𝑚)‘(2^nd ‘𝑦))⟩(comp‘𝐷)((1^st ‘𝑛)‘(2^nd ‘𝑦)))(((2^nd ‘𝑥)(2^nd ‘𝑚)(2^nd ‘𝑦))‘𝑔))))
46		ovex 7442	. . . . . . . . 9 ⊢ (𝑚(𝐶 Nat 𝐷)𝑛) ∈ V
47		ovex 7442	. . . . . . . . 9 ⊢ ((2^nd ‘𝑥)(Hom ‘𝐶)(2^nd ‘𝑦)) ∈ V
48	46, 47	mpoex 8066	. . . . . . . 8 ⊢ (𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2^nd ‘𝑥)(Hom ‘𝐶)(2^nd ‘𝑦)) ↦ ((𝑎‘(2^nd ‘𝑦))(⟨((1^st ‘𝑚)‘(2^nd ‘𝑥)), ((1^st ‘𝑚)‘(2^nd ‘𝑦))⟩(comp‘𝐷)((1^st ‘𝑛)‘(2^nd ‘𝑦)))(((2^nd ‘𝑥)(2^nd ‘𝑚)(2^nd ‘𝑦))‘𝑔))) ∈ V
49	48	csbex 5312	. . . . . . 7 ⊢ ⦋(1^st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2^nd ‘𝑥)(Hom ‘𝐶)(2^nd ‘𝑦)) ↦ ((𝑎‘(2^nd ‘𝑦))(⟨((1^st ‘𝑚)‘(2^nd ‘𝑥)), ((1^st ‘𝑚)‘(2^nd ‘𝑦))⟩(comp‘𝐷)((1^st ‘𝑛)‘(2^nd ‘𝑦)))(((2^nd ‘𝑥)(2^nd ‘𝑚)(2^nd ‘𝑦))‘𝑔))) ∈ V
50	49	csbex 5312	. . . . . 6 ⊢ ⦋(1^st ‘𝑥) / 𝑚⦌⦋(1^st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2^nd ‘𝑥)(Hom ‘𝐶)(2^nd ‘𝑦)) ↦ ((𝑎‘(2^nd ‘𝑦))(⟨((1^st ‘𝑚)‘(2^nd ‘𝑥)), ((1^st ‘𝑚)‘(2^nd ‘𝑦))⟩(comp‘𝐷)((1^st ‘𝑛)‘(2^nd ‘𝑦)))(((2^nd ‘𝑥)(2^nd ‘𝑚)(2^nd ‘𝑦))‘𝑔))) ∈ V
51	45, 50	fnmpoi 8056	. . . . 5 ⊢ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ ⦋(1^st ‘𝑥) / 𝑚⦌⦋(1^st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2^nd ‘𝑥)(Hom ‘𝐶)(2^nd ‘𝑦)) ↦ ((𝑎‘(2^nd ‘𝑦))(⟨((1^st ‘𝑚)‘(2^nd ‘𝑥)), ((1^st ‘𝑚)‘(2^nd ‘𝑦))⟩(comp‘𝐷)((1^st ‘𝑛)‘(2^nd ‘𝑦)))(((2^nd ‘𝑥)(2^nd ‘𝑚)(2^nd ‘𝑦))‘𝑔)))) Fn (((𝐶 Func 𝐷) × (Base‘𝐶)) × ((𝐶 Func 𝐷) × (Base‘𝐶)))
52	11, 13	op2ndd 7986	. . . . . . 7 ⊢ (𝐸 = ⟨(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1^st ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ ⦋(1^st ‘𝑥) / 𝑚⦌⦋(1^st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2^nd ‘𝑥)(Hom ‘𝐶)(2^nd ‘𝑦)) ↦ ((𝑎‘(2^nd ‘𝑦))(⟨((1^st ‘𝑚)‘(2^nd ‘𝑥)), ((1^st ‘𝑚)‘(2^nd ‘𝑦))⟩(comp‘𝐷)((1^st ‘𝑛)‘(2^nd ‘𝑦)))(((2^nd ‘𝑥)(2^nd ‘𝑚)(2^nd ‘𝑦))‘𝑔))))⟩ → (2^nd ‘𝐸) = (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ ⦋(1^st ‘𝑥) / 𝑚⦌⦋(1^st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2^nd ‘𝑥)(Hom ‘𝐶)(2^nd ‘𝑦)) ↦ ((𝑎‘(2^nd ‘𝑦))(⟨((1^st ‘𝑚)‘(2^nd ‘𝑥)), ((1^st ‘𝑚)‘(2^nd ‘𝑦))⟩(comp‘𝐷)((1^st ‘𝑛)‘(2^nd ‘𝑦)))(((2^nd ‘𝑥)(2^nd ‘𝑚)(2^nd ‘𝑦))‘𝑔)))))
53	8, 52	syl 17	. . . . . 6 ⊢ (𝜑 → (2^nd ‘𝐸) = (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ ⦋(1^st ‘𝑥) / 𝑚⦌⦋(1^st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2^nd ‘𝑥)(Hom ‘𝐶)(2^nd ‘𝑦)) ↦ ((𝑎‘(2^nd ‘𝑦))(⟨((1^st ‘𝑚)‘(2^nd ‘𝑥)), ((1^st ‘𝑚)‘(2^nd ‘𝑦))⟩(comp‘𝐷)((1^st ‘𝑛)‘(2^nd ‘𝑦)))(((2^nd ‘𝑥)(2^nd ‘𝑚)(2^nd ‘𝑦))‘𝑔)))))
54	53	fneq1d 6643	. . . . 5 ⊢ (𝜑 → ((2^nd ‘𝐸) Fn (((𝐶 Func 𝐷) × (Base‘𝐶)) × ((𝐶 Func 𝐷) × (Base‘𝐶))) ↔ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ ⦋(1^st ‘𝑥) / 𝑚⦌⦋(1^st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2^nd ‘𝑥)(Hom ‘𝐶)(2^nd ‘𝑦)) ↦ ((𝑎‘(2^nd ‘𝑦))(⟨((1^st ‘𝑚)‘(2^nd ‘𝑥)), ((1^st ‘𝑚)‘(2^nd ‘𝑦))⟩(comp‘𝐷)((1^st ‘𝑛)‘(2^nd ‘𝑦)))(((2^nd ‘𝑥)(2^nd ‘𝑚)(2^nd ‘𝑦))‘𝑔)))) Fn (((𝐶 Func 𝐷) × (Base‘𝐶)) × ((𝐶 Func 𝐷) × (Base‘𝐶)))))
55	51, 54	mpbiri 258	. . . 4 ⊢ (𝜑 → (2^nd ‘𝐸) Fn (((𝐶 Func 𝐷) × (Base‘𝐶)) × ((𝐶 Func 𝐷) × (Base‘𝐶))))
56	3	ad2antrr 725	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝐷 ∈ Cat)
57	56	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝐷 ∈ Cat)
58		simplrl 776	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑓 ∈ (𝐶 Func 𝐷))
59	30, 58, 32	sylancr 588	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1^st ‘𝑓)(𝐶 Func 𝐷)(2^nd ‘𝑓))
60	4, 22, 59	funcf1 17816	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1^st ‘𝑓):(Base‘𝐶)⟶(Base‘𝐷))
61	60	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (1^st ‘𝑓):(Base‘𝐶)⟶(Base‘𝐷))
62		simplrr 777	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑢 ∈ (Base‘𝐶))
63	62	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑢 ∈ (Base‘𝐶))
64	61, 63	ffvelcdmd 7088	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((1^st ‘𝑓)‘𝑢) ∈ (Base‘𝐷))
65		simplrr 777	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑣 ∈ (Base‘𝐶))
66	61, 65	ffvelcdmd 7088	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((1^st ‘𝑓)‘𝑣) ∈ (Base‘𝐷))
67		simprl 770	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑔 ∈ (𝐶 Func 𝐷))
68		1st2ndbr 8028	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Rel (𝐶 Func 𝐷) ∧ 𝑔 ∈ (𝐶 Func 𝐷)) → (1^st ‘𝑔)(𝐶 Func 𝐷)(2^nd ‘𝑔))
69	30, 67, 68	sylancr 588	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1^st ‘𝑔)(𝐶 Func 𝐷)(2^nd ‘𝑔))
70	4, 22, 69	funcf1 17816	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1^st ‘𝑔):(Base‘𝐶)⟶(Base‘𝐷))
71	70	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (1^st ‘𝑔):(Base‘𝐶)⟶(Base‘𝐷))
72	71, 65	ffvelcdmd 7088	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((1^st ‘𝑔)‘𝑣) ∈ (Base‘𝐷))
73		simprr 772	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑣 ∈ (Base‘𝐶))
74	4, 5, 24, 59, 62, 73	funcf2 17818	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑢(2^nd ‘𝑓)𝑣):(𝑢(Hom ‘𝐶)𝑣)⟶(((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑓)‘𝑣)))
75	74	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (𝑢(2^nd ‘𝑓)𝑣):(𝑢(Hom ‘𝐶)𝑣)⟶(((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑓)‘𝑣)))
76		simprr 772	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))
77	75, 76	ffvelcdmd 7088	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((𝑢(2^nd ‘𝑓)𝑣)‘ℎ) ∈ (((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑓)‘𝑣)))
78		simprl 770	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔))
79	7, 78	nat1st2nd 17902	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑎 ∈ (⟨(1^st ‘𝑓), (2^nd ‘𝑓)⟩(𝐶 Nat 𝐷)⟨(1^st ‘𝑔), (2^nd ‘𝑔)⟩))
80	7, 79, 4, 24, 65	natcl 17904	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (𝑎‘𝑣) ∈ (((1^st ‘𝑓)‘𝑣)(Hom ‘𝐷)((1^st ‘𝑔)‘𝑣)))
81	22, 24, 6, 57, 64, 66, 72, 77, 80	catcocl 17629	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((𝑎‘𝑣)(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑣)⟩(comp‘𝐷)((1^st ‘𝑔)‘𝑣))((𝑢(2^nd ‘𝑓)𝑣)‘ℎ)) ∈ (((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑔)‘𝑣)))
82	81	ralrimivva 3201	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → ∀𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔)∀ℎ ∈ (𝑢(Hom ‘𝐶)𝑣)((𝑎‘𝑣)(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑣)⟩(comp‘𝐷)((1^st ‘𝑔)‘𝑣))((𝑢(2^nd ‘𝑓)𝑣)‘ℎ)) ∈ (((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑔)‘𝑣)))
83		eqid 2733	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ℎ ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎‘𝑣)(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑣)⟩(comp‘𝐷)((1^st ‘𝑔)‘𝑣))((𝑢(2^nd ‘𝑓)𝑣)‘ℎ))) = (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ℎ ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎‘𝑣)(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑣)⟩(comp‘𝐷)((1^st ‘𝑔)‘𝑣))((𝑢(2^nd ‘𝑓)𝑣)‘ℎ)))
84	83	fmpo 8054	. . . . . . . . . . . . 13 ⊢ (∀𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔)∀ℎ ∈ (𝑢(Hom ‘𝐶)𝑣)((𝑎‘𝑣)(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑣)⟩(comp‘𝐷)((1^st ‘𝑔)‘𝑣))((𝑢(2^nd ‘𝑓)𝑣)‘ℎ)) ∈ (((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑔)‘𝑣)) ↔ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ℎ ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎‘𝑣)(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑣)⟩(comp‘𝐷)((1^st ‘𝑔)‘𝑣))((𝑢(2^nd ‘𝑓)𝑣)‘ℎ))):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑔)‘𝑣)))
85	82, 84	sylib 217	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ℎ ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎‘𝑣)(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑣)⟩(comp‘𝐷)((1^st ‘𝑔)‘𝑣))((𝑢(2^nd ‘𝑓)𝑣)‘ℎ))):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑔)‘𝑣)))
86	2	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝐶 ∈ Cat)
87		eqid 2733	. . . . . . . . . . . . . 14 ⊢ (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩) = (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩)
88	1, 86, 56, 4, 5, 6, 7, 58, 67, 62, 73, 87	evlf2 18171	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩) = (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ℎ ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎‘𝑣)(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑣)⟩(comp‘𝐷)((1^st ‘𝑔)‘𝑣))((𝑢(2^nd ‘𝑓)𝑣)‘ℎ))))
89	88	feq1d 6703	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑔)‘𝑣)) ↔ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ℎ ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎‘𝑣)(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑣)⟩(comp‘𝐷)((1^st ‘𝑔)‘𝑣))((𝑢(2^nd ‘𝑓)𝑣)‘ℎ))):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑔)‘𝑣))))
90	85, 89	mpbird 257	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑔)‘𝑣)))
91	19, 7	fuchom 17913	. . . . . . . . . . . . 13 ⊢ (𝐶 Nat 𝐷) = (Hom ‘𝑄)
92	18, 20, 4, 91, 5, 58, 62, 67, 73, 23	xpchom2 18138	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩) = ((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣)))
93	1, 86, 56, 4, 58, 62	evlf1 18173	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑓(1^st ‘𝐸)𝑢) = ((1^st ‘𝑓)‘𝑢))
94	1, 86, 56, 4, 67, 73	evlf1 18173	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑔(1^st ‘𝐸)𝑣) = ((1^st ‘𝑔)‘𝑣))
95	93, 94	oveq12d 7427	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → ((𝑓(1^st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)) = (((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑔)‘𝑣)))
96	92, 95	feq23d 6713	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1^st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)) ↔ (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑔)‘𝑣))))
97	90, 96	mpbird 257	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1^st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)))
98	97	ralrimivva 3201	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1^st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)))
99	98	ralrimivva 3201	. . . . . . . 8 ⊢ (𝜑 → ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1^st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)))
100		oveq2 7417	. . . . . . . . . . . 12 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → (𝑥(2^nd ‘𝐸)𝑦) = (𝑥(2^nd ‘𝐸)⟨𝑔, 𝑣⟩))
101		oveq2 7417	. . . . . . . . . . . 12 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) = (𝑥(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩))
102		fveq2 6892	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → ((1^st ‘𝐸)‘𝑦) = ((1^st ‘𝐸)‘⟨𝑔, 𝑣⟩))
103		df-ov 7412	. . . . . . . . . . . . . 14 ⊢ (𝑔(1^st ‘𝐸)𝑣) = ((1^st ‘𝐸)‘⟨𝑔, 𝑣⟩)
104	102, 103	eqtr4di 2791	. . . . . . . . . . . . 13 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → ((1^st ‘𝐸)‘𝑦) = (𝑔(1^st ‘𝐸)𝑣))
105	104	oveq2d 7425	. . . . . . . . . . . 12 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → (((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐸)‘𝑦)) = (((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)))
106	100, 101, 105	feq123d 6707	. . . . . . . . . . 11 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → ((𝑥(2^nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐸)‘𝑦)) ↔ (𝑥(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(𝑥(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣))))
107	106	ralxp 5842	. . . . . . . . . 10 ⊢ (∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2^nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐸)‘𝑦)) ↔ ∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(𝑥(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(𝑥(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)))
108		oveq1 7416	. . . . . . . . . . . 12 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (𝑥(2^nd ‘𝐸)⟨𝑔, 𝑣⟩) = (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩))
109		oveq1 7416	. . . . . . . . . . . 12 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (𝑥(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩) = (⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩))
110		fveq2 6892	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((1^st ‘𝐸)‘𝑥) = ((1^st ‘𝐸)‘⟨𝑓, 𝑢⟩))
111		df-ov 7412	. . . . . . . . . . . . . 14 ⊢ (𝑓(1^st ‘𝐸)𝑢) = ((1^st ‘𝐸)‘⟨𝑓, 𝑢⟩)
112	110, 111	eqtr4di 2791	. . . . . . . . . . . . 13 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((1^st ‘𝐸)‘𝑥) = (𝑓(1^st ‘𝐸)𝑢))
113	112	oveq1d 7424	. . . . . . . . . . . 12 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)) = ((𝑓(1^st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)))
114	108, 109, 113	feq123d 6707	. . . . . . . . . . 11 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((𝑥(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(𝑥(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)) ↔ (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1^st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣))))
115	114	2ralbidv 3219	. . . . . . . . . 10 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(𝑥(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(𝑥(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)) ↔ ∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1^st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣))))
116	107, 115	bitrid 283	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2^nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐸)‘𝑦)) ↔ ∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1^st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣))))
117	116	ralxp 5842	. . . . . . . 8 ⊢ (∀𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2^nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐸)‘𝑦)) ↔ ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1^st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)))
118	99, 117	sylibr 233	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2^nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐸)‘𝑦)))
119	118	r19.21bi 3249	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) → ∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2^nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐸)‘𝑦)))
120	119	r19.21bi 3249	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) → (𝑥(2^nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐸)‘𝑦)))
121	120	anasss 468	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))) → (𝑥(2^nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐸)‘𝑦)))
122	28	adantr 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝑄 ∈ Cat)
123	2	adantr 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝐶 ∈ Cat)
124		eqid 2733	. . . . . . . . . . 11 ⊢ (Id‘𝑄) = (Id‘𝑄)
125		eqid 2733	. . . . . . . . . . 11 ⊢ (Id‘𝐶) = (Id‘𝐶)
126		simprl 770	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝑓 ∈ (𝐶 Func 𝐷))
127		simprr 772	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝑢 ∈ (Base‘𝐶))
128	18, 122, 123, 20, 4, 124, 125, 25, 126, 127	xpcid 18141	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩) = ⟨((Id‘𝑄)‘𝑓), ((Id‘𝐶)‘𝑢)⟩)
129	128	fveq2d 6896	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘⟨((Id‘𝑄)‘𝑓), ((Id‘𝐶)‘𝑢)⟩))
130		df-ov 7412	. . . . . . . . 9 ⊢ (((Id‘𝑄)‘𝑓)(⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)((Id‘𝐶)‘𝑢)) = ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘⟨((Id‘𝑄)‘𝑓), ((Id‘𝐶)‘𝑢)⟩)
131	129, 130	eqtr4di 2791	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩)) = (((Id‘𝑄)‘𝑓)(⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)((Id‘𝐶)‘𝑢)))
132	3	adantr 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝐷 ∈ Cat)
133		eqid 2733	. . . . . . . . 9 ⊢ (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩) = (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)
134	20, 91, 124, 122, 126	catidcl 17626	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝑄)‘𝑓) ∈ (𝑓(𝐶 Nat 𝐷)𝑓))
135	4, 5, 125, 123, 127	catidcl 17626	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝐶)‘𝑢) ∈ (𝑢(Hom ‘𝐶)𝑢))
136	1, 123, 132, 4, 5, 6, 7, 126, 126, 127, 127, 133, 134, 135	evlf2val 18172	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝑄)‘𝑓)(⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)((Id‘𝐶)‘𝑢)) = ((((Id‘𝑄)‘𝑓)‘𝑢)(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑢)⟩(comp‘𝐷)((1^st ‘𝑓)‘𝑢))((𝑢(2^nd ‘𝑓)𝑢)‘((Id‘𝐶)‘𝑢))))
137	30, 126, 32	sylancr 588	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (1^st ‘𝑓)(𝐶 Func 𝐷)(2^nd ‘𝑓))
138	4, 22, 137	funcf1 17816	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (1^st ‘𝑓):(Base‘𝐶)⟶(Base‘𝐷))
139	138, 127	ffvelcdmd 7088	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((1^st ‘𝑓)‘𝑢) ∈ (Base‘𝐷))
140	22, 24, 26, 132, 139	catidcl 17626	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢)) ∈ (((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑓)‘𝑢)))
141	22, 24, 26, 132, 139, 6, 139, 140	catlid 17627	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢))(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑢)⟩(comp‘𝐷)((1^st ‘𝑓)‘𝑢))((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢))) = ((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢)))
142	19, 124, 26, 126	fucid 17924	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝑄)‘𝑓) = ((Id‘𝐷) ∘ (1^st ‘𝑓)))
143	142	fveq1d 6894	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝑄)‘𝑓)‘𝑢) = (((Id‘𝐷) ∘ (1^st ‘𝑓))‘𝑢))
144		fvco3 6991	. . . . . . . . . . . 12 ⊢ (((1^st ‘𝑓):(Base‘𝐶)⟶(Base‘𝐷) ∧ 𝑢 ∈ (Base‘𝐶)) → (((Id‘𝐷) ∘ (1^st ‘𝑓))‘𝑢) = ((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢)))
145	138, 127, 144	syl2anc 585	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝐷) ∘ (1^st ‘𝑓))‘𝑢) = ((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢)))
146	143, 145	eqtrd 2773	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝑄)‘𝑓)‘𝑢) = ((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢)))
147	4, 125, 26, 137, 127	funcid 17820	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((𝑢(2^nd ‘𝑓)𝑢)‘((Id‘𝐶)‘𝑢)) = ((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢)))
148	146, 147	oveq12d 7427	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((((Id‘𝑄)‘𝑓)‘𝑢)(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑢)⟩(comp‘𝐷)((1^st ‘𝑓)‘𝑢))((𝑢(2^nd ‘𝑓)𝑢)‘((Id‘𝐶)‘𝑢))) = (((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢))(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑢)⟩(comp‘𝐷)((1^st ‘𝑓)‘𝑢))((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢))))
149	1, 123, 132, 4, 126, 127	evlf1 18173	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (𝑓(1^st ‘𝐸)𝑢) = ((1^st ‘𝑓)‘𝑢))
150	149	fveq2d 6896	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝐷)‘(𝑓(1^st ‘𝐸)𝑢)) = ((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢)))
151	141, 148, 150	3eqtr4d 2783	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((((Id‘𝑄)‘𝑓)‘𝑢)(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑢)⟩(comp‘𝐷)((1^st ‘𝑓)‘𝑢))((𝑢(2^nd ‘𝑓)𝑢)‘((Id‘𝐶)‘𝑢))) = ((Id‘𝐷)‘(𝑓(1^st ‘𝐸)𝑢)))
152	131, 136, 151	3eqtrd 2777	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1^st ‘𝐸)𝑢)))
153	152	ralrimivva 3201	. . . . . 6 ⊢ (𝜑 → ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1^st ‘𝐸)𝑢)))
154		id 22	. . . . . . . . . 10 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → 𝑥 = ⟨𝑓, 𝑢⟩)
155	154, 154	oveq12d 7427	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (𝑥(2^nd ‘𝐸)𝑥) = (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩))
156		fveq2 6892	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((Id‘(𝑄 ×_c 𝐶))‘𝑥) = ((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩))
157	155, 156	fveq12d 6899	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((𝑥(2^nd ‘𝐸)𝑥)‘((Id‘(𝑄 ×_c 𝐶))‘𝑥)) = ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩)))
158	112	fveq2d 6896	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((Id‘𝐷)‘((1^st ‘𝐸)‘𝑥)) = ((Id‘𝐷)‘(𝑓(1^st ‘𝐸)𝑢)))
159	157, 158	eqeq12d 2749	. . . . . . 7 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (((𝑥(2^nd ‘𝐸)𝑥)‘((Id‘(𝑄 ×_c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1^st ‘𝐸)‘𝑥)) ↔ ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1^st ‘𝐸)𝑢))))
160	159	ralxp 5842	. . . . . 6 ⊢ (∀𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))((𝑥(2^nd ‘𝐸)𝑥)‘((Id‘(𝑄 ×_c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1^st ‘𝐸)‘𝑥)) ↔ ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1^st ‘𝐸)𝑢)))
161	153, 160	sylibr 233	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))((𝑥(2^nd ‘𝐸)𝑥)‘((Id‘(𝑄 ×_c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1^st ‘𝐸)‘𝑥)))
162	161	r19.21bi 3249	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) → ((𝑥(2^nd ‘𝐸)𝑥)‘((Id‘(𝑄 ×_c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1^st ‘𝐸)‘𝑥)))
163	2	3ad2ant1 1134	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝐶 ∈ Cat)
164	3	3ad2ant1 1134	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝐷 ∈ Cat)
165		simp21 1207	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
166		1st2nd2 8014	. . . . . . . . 9 ⊢ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) → 𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩)
167	165, 166	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑥 = ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩)
168	167, 165	eqeltrrd 2835	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
169		opelxp 5713	. . . . . . 7 ⊢ (⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↔ ((1^st ‘𝑥) ∈ (𝐶 Func 𝐷) ∧ (2^nd ‘𝑥) ∈ (Base‘𝐶)))
170	168, 169	sylib 217	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ((1^st ‘𝑥) ∈ (𝐶 Func 𝐷) ∧ (2^nd ‘𝑥) ∈ (Base‘𝐶)))
171		simp22 1208	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
172		1st2nd2 8014	. . . . . . . . 9 ⊢ (𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) → 𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩)
173	171, 172	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩)
174	173, 171	eqeltrrd 2835	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
175		opelxp 5713	. . . . . . 7 ⊢ (⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↔ ((1^st ‘𝑦) ∈ (𝐶 Func 𝐷) ∧ (2^nd ‘𝑦) ∈ (Base‘𝐶)))
176	174, 175	sylib 217	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ((1^st ‘𝑦) ∈ (𝐶 Func 𝐷) ∧ (2^nd ‘𝑦) ∈ (Base‘𝐶)))
177		simp23 1209	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
178		1st2nd2 8014	. . . . . . . . 9 ⊢ (𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) → 𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)
179	177, 178	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)
180	179, 177	eqeltrrd 2835	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
181		opelxp 5713	. . . . . . 7 ⊢ (⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↔ ((1^st ‘𝑧) ∈ (𝐶 Func 𝐷) ∧ (2^nd ‘𝑧) ∈ (Base‘𝐶)))
182	180, 181	sylib 217	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ((1^st ‘𝑧) ∈ (𝐶 Func 𝐷) ∧ (2^nd ‘𝑧) ∈ (Base‘𝐶)))
183		simp3l 1202	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦))
184	18, 21, 91, 5, 23, 165, 171	xpchom 18132	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) = (((1^st ‘𝑥)(𝐶 Nat 𝐷)(1^st ‘𝑦)) × ((2^nd ‘𝑥)(Hom ‘𝐶)(2^nd ‘𝑦))))
185	183, 184	eleqtrd 2836	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑓 ∈ (((1^st ‘𝑥)(𝐶 Nat 𝐷)(1^st ‘𝑦)) × ((2^nd ‘𝑥)(Hom ‘𝐶)(2^nd ‘𝑦))))
186		1st2nd2 8014	. . . . . . . . 9 ⊢ (𝑓 ∈ (((1^st ‘𝑥)(𝐶 Nat 𝐷)(1^st ‘𝑦)) × ((2^nd ‘𝑥)(Hom ‘𝐶)(2^nd ‘𝑦))) → 𝑓 = ⟨(1^st ‘𝑓), (2^nd ‘𝑓)⟩)
187	185, 186	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑓 = ⟨(1^st ‘𝑓), (2^nd ‘𝑓)⟩)
188	187, 185	eqeltrrd 2835	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ⟨(1^st ‘𝑓), (2^nd ‘𝑓)⟩ ∈ (((1^st ‘𝑥)(𝐶 Nat 𝐷)(1^st ‘𝑦)) × ((2^nd ‘𝑥)(Hom ‘𝐶)(2^nd ‘𝑦))))
189		opelxp 5713	. . . . . . 7 ⊢ (⟨(1^st ‘𝑓), (2^nd ‘𝑓)⟩ ∈ (((1^st ‘𝑥)(𝐶 Nat 𝐷)(1^st ‘𝑦)) × ((2^nd ‘𝑥)(Hom ‘𝐶)(2^nd ‘𝑦))) ↔ ((1^st ‘𝑓) ∈ ((1^st ‘𝑥)(𝐶 Nat 𝐷)(1^st ‘𝑦)) ∧ (2^nd ‘𝑓) ∈ ((2^nd ‘𝑥)(Hom ‘𝐶)(2^nd ‘𝑦))))
190	188, 189	sylib 217	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ((1^st ‘𝑓) ∈ ((1^st ‘𝑥)(𝐶 Nat 𝐷)(1^st ‘𝑦)) ∧ (2^nd ‘𝑓) ∈ ((2^nd ‘𝑥)(Hom ‘𝐶)(2^nd ‘𝑦))))
191		simp3r 1203	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))
192	18, 21, 91, 5, 23, 171, 177	xpchom 18132	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧) = (((1^st ‘𝑦)(𝐶 Nat 𝐷)(1^st ‘𝑧)) × ((2^nd ‘𝑦)(Hom ‘𝐶)(2^nd ‘𝑧))))
193	191, 192	eleqtrd 2836	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑔 ∈ (((1^st ‘𝑦)(𝐶 Nat 𝐷)(1^st ‘𝑧)) × ((2^nd ‘𝑦)(Hom ‘𝐶)(2^nd ‘𝑧))))
194		1st2nd2 8014	. . . . . . . . 9 ⊢ (𝑔 ∈ (((1^st ‘𝑦)(𝐶 Nat 𝐷)(1^st ‘𝑧)) × ((2^nd ‘𝑦)(Hom ‘𝐶)(2^nd ‘𝑧))) → 𝑔 = ⟨(1^st ‘𝑔), (2^nd ‘𝑔)⟩)
195	193, 194	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑔 = ⟨(1^st ‘𝑔), (2^nd ‘𝑔)⟩)
196	195, 193	eqeltrrd 2835	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ⟨(1^st ‘𝑔), (2^nd ‘𝑔)⟩ ∈ (((1^st ‘𝑦)(𝐶 Nat 𝐷)(1^st ‘𝑧)) × ((2^nd ‘𝑦)(Hom ‘𝐶)(2^nd ‘𝑧))))
197		opelxp 5713	. . . . . . 7 ⊢ (⟨(1^st ‘𝑔), (2^nd ‘𝑔)⟩ ∈ (((1^st ‘𝑦)(𝐶 Nat 𝐷)(1^st ‘𝑧)) × ((2^nd ‘𝑦)(Hom ‘𝐶)(2^nd ‘𝑧))) ↔ ((1^st ‘𝑔) ∈ ((1^st ‘𝑦)(𝐶 Nat 𝐷)(1^st ‘𝑧)) ∧ (2^nd ‘𝑔) ∈ ((2^nd ‘𝑦)(Hom ‘𝐶)(2^nd ‘𝑧))))
198	196, 197	sylib 217	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ((1^st ‘𝑔) ∈ ((1^st ‘𝑦)(𝐶 Nat 𝐷)(1^st ‘𝑧)) ∧ (2^nd ‘𝑔) ∈ ((2^nd ‘𝑦)(Hom ‘𝐶)(2^nd ‘𝑧))))
199	1, 19, 163, 164, 7, 170, 176, 182, 190, 198	evlfcllem 18174	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ((⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩(2^nd ‘𝐸)⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)‘(⟨(1^st ‘𝑔), (2^nd ‘𝑔)⟩(⟨⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩, ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩⟩(comp‘(𝑄 ×_c 𝐶))⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)⟨(1^st ‘𝑓), (2^nd ‘𝑓)⟩)) = (((⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩(2^nd ‘𝐸)⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)‘⟨(1^st ‘𝑔), (2^nd ‘𝑔)⟩)(⟨((1^st ‘𝐸)‘⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩), ((1^st ‘𝐸)‘⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩)⟩(comp‘𝐷)((1^st ‘𝐸)‘⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩))((⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩(2^nd ‘𝐸)⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩)‘⟨(1^st ‘𝑓), (2^nd ‘𝑓)⟩)))
200	167, 179	oveq12d 7427	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → (𝑥(2^nd ‘𝐸)𝑧) = (⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩(2^nd ‘𝐸)⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩))
201	167, 173	opeq12d 4882	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ⟨𝑥, 𝑦⟩ = ⟨⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩, ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩⟩)
202	201, 179	oveq12d 7427	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → (⟨𝑥, 𝑦⟩(comp‘(𝑄 ×_c 𝐶))𝑧) = (⟨⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩, ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩⟩(comp‘(𝑄 ×_c 𝐶))⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩))
203	202, 195, 187	oveq123d 7430	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘(𝑄 ×_c 𝐶))𝑧)𝑓) = (⟨(1^st ‘𝑔), (2^nd ‘𝑔)⟩(⟨⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩, ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩⟩(comp‘(𝑄 ×_c 𝐶))⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)⟨(1^st ‘𝑓), (2^nd ‘𝑓)⟩))
204	200, 203	fveq12d 6899	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ((𝑥(2^nd ‘𝐸)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘(𝑄 ×_c 𝐶))𝑧)𝑓)) = ((⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩(2^nd ‘𝐸)⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)‘(⟨(1^st ‘𝑔), (2^nd ‘𝑔)⟩(⟨⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩, ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩⟩(comp‘(𝑄 ×_c 𝐶))⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)⟨(1^st ‘𝑓), (2^nd ‘𝑓)⟩)))
205	167	fveq2d 6896	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ((1^st ‘𝐸)‘𝑥) = ((1^st ‘𝐸)‘⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩))
206	173	fveq2d 6896	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ((1^st ‘𝐸)‘𝑦) = ((1^st ‘𝐸)‘⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩))
207	205, 206	opeq12d 4882	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ⟨((1^st ‘𝐸)‘𝑥), ((1^st ‘𝐸)‘𝑦)⟩ = ⟨((1^st ‘𝐸)‘⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩), ((1^st ‘𝐸)‘⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩)⟩)
208	179	fveq2d 6896	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ((1^st ‘𝐸)‘𝑧) = ((1^st ‘𝐸)‘⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩))
209	207, 208	oveq12d 7427	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → (⟨((1^st ‘𝐸)‘𝑥), ((1^st ‘𝐸)‘𝑦)⟩(comp‘𝐷)((1^st ‘𝐸)‘𝑧)) = (⟨((1^st ‘𝐸)‘⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩), ((1^st ‘𝐸)‘⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩)⟩(comp‘𝐷)((1^st ‘𝐸)‘⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)))
210	173, 179	oveq12d 7427	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → (𝑦(2^nd ‘𝐸)𝑧) = (⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩(2^nd ‘𝐸)⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩))
211	210, 195	fveq12d 6899	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ((𝑦(2^nd ‘𝐸)𝑧)‘𝑔) = ((⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩(2^nd ‘𝐸)⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)‘⟨(1^st ‘𝑔), (2^nd ‘𝑔)⟩))
212	167, 173	oveq12d 7427	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → (𝑥(2^nd ‘𝐸)𝑦) = (⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩(2^nd ‘𝐸)⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩))
213	212, 187	fveq12d 6899	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ((𝑥(2^nd ‘𝐸)𝑦)‘𝑓) = ((⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩(2^nd ‘𝐸)⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩)‘⟨(1^st ‘𝑓), (2^nd ‘𝑓)⟩))
214	209, 211, 213	oveq123d 7430	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → (((𝑦(2^nd ‘𝐸)𝑧)‘𝑔)(⟨((1^st ‘𝐸)‘𝑥), ((1^st ‘𝐸)‘𝑦)⟩(comp‘𝐷)((1^st ‘𝐸)‘𝑧))((𝑥(2^nd ‘𝐸)𝑦)‘𝑓)) = (((⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩(2^nd ‘𝐸)⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)‘⟨(1^st ‘𝑔), (2^nd ‘𝑔)⟩)(⟨((1^st ‘𝐸)‘⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩), ((1^st ‘𝐸)‘⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩)⟩(comp‘𝐷)((1^st ‘𝐸)‘⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩))((⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩(2^nd ‘𝐸)⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩)‘⟨(1^st ‘𝑓), (2^nd ‘𝑓)⟩)))
215	199, 204, 214	3eqtr4d 2783	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ((𝑥(2^nd ‘𝐸)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘(𝑄 ×_c 𝐶))𝑧)𝑓)) = (((𝑦(2^nd ‘𝐸)𝑧)‘𝑔)(⟨((1^st ‘𝐸)‘𝑥), ((1^st ‘𝐸)‘𝑦)⟩(comp‘𝐷)((1^st ‘𝐸)‘𝑧))((𝑥(2^nd ‘𝐸)𝑦)‘𝑓)))
216	21, 22, 23, 24, 25, 26, 27, 6, 29, 3, 44, 55, 121, 162, 215	isfuncd 17815	. . 3 ⊢ (𝜑 → (1^st ‘𝐸)((𝑄 ×_c 𝐶) Func 𝐷)(2^nd ‘𝐸))
217		df-br 5150	. . 3 ⊢ ((1^st ‘𝐸)((𝑄 ×_c 𝐶) Func 𝐷)(2^nd ‘𝐸) ↔ ⟨(1^st ‘𝐸), (2^nd ‘𝐸)⟩ ∈ ((𝑄 ×_c 𝐶) Func 𝐷))
218	216, 217	sylib 217	. 2 ⊢ (𝜑 → ⟨(1^st ‘𝐸), (2^nd ‘𝐸)⟩ ∈ ((𝑄 ×_c 𝐶) Func 𝐷))
219	17, 218	eqeltrd 2834	1 ⊢ (𝜑 → 𝐸 ∈ ((𝑄 ×_c 𝐶) Func 𝐷))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 397 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 ∀wral 3062 Vcvv 3475 ⦋csb 3894 ⟨cop 4635 class class class wbr 5149 × cxp 5675 ∘ ccom 5681 Rel wrel 5682 Fn wfn 6539 ⟶wf 6540 ‘cfv 6544 (class class class)co 7409 ∈ cmpo 7411 1^st c1st 7973 2^nd c2nd 7974 Basecbs 17144 Hom chom 17208 compcco 17209 Catccat 17608 Idccid 17609 Func cfunc 17804 Nat cnat 17892 FuncCat cfuc 17893 ×_c cxpc 18120 eval_F cevlf 18162

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-cnex 11166 ax-resscn 11167 ax-1cn 11168 ax-icn 11169 ax-addcl 11170 ax-addrcl 11171 ax-mulcl 11172 ax-mulrcl 11173 ax-mulcom 11174 ax-addass 11175 ax-mulass 11176 ax-distr 11177 ax-i2m1 11178 ax-1ne0 11179 ax-1rid 11180 ax-rnegex 11181 ax-rrecex 11182 ax-cnre 11183 ax-pre-lttri 11184 ax-pre-lttrn 11185 ax-pre-ltadd 11186 ax-pre-mulgt0 11187

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-tp 4634 df-op 4636 df-uni 4910 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-riota 7365 df-ov 7412 df-oprab 7413 df-mpo 7414 df-om 7856 df-1st 7975 df-2nd 7976 df-frecs 8266 df-wrecs 8297 df-recs 8371 df-rdg 8410 df-1o 8466 df-er 8703 df-map 8822 df-ixp 8892 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-pnf 11250 df-mnf 11251 df-xr 11252 df-ltxr 11253 df-le 11254 df-sub 11446 df-neg 11447 df-nn 12213 df-2 12275 df-3 12276 df-4 12277 df-5 12278 df-6 12279 df-7 12280 df-8 12281 df-9 12282 df-n0 12473 df-z 12559 df-dec 12678 df-uz 12823 df-fz 13485 df-struct 17080 df-slot 17115 df-ndx 17127 df-base 17145 df-hom 17221 df-cco 17222 df-cat 17612 df-cid 17613 df-func 17808 df-nat 17894 df-fuc 17895 df-xpc 18124 df-evlf 18166

This theorem is referenced by: uncfcl 18188 uncf1 18189 uncf2 18190 yonedalem1 18225

W3C validator