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 17856

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 2738	. . . . 5 ⊢ (Base‘𝐶) = (Base‘𝐶)
5		eqid 2738	. . . . 5 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
6		eqid 2738	. . . . 5 ⊢ (comp‘𝐷) = (comp‘𝐷)
7		eqid 2738	. . . . 5 ⊢ (𝐶 Nat 𝐷) = (𝐶 Nat 𝐷)
8	1, 2, 3, 4, 5, 6, 7	evlfval 17851	. . . 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 7288	. . . . . 6 ⊢ (𝐶 Func 𝐷) ∈ V
10		fvex 6769	. . . . . 6 ⊢ (Base‘𝐶) ∈ V
11	9, 10	mpoex 7893	. . . . 5 ⊢ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1^st ‘𝑓)‘𝑥)) ∈ V
12	9, 10	xpex 7581	. . . . . 6 ⊢ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∈ V
13	12, 12	mpoex 7893	. . . . 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 5619	. . . 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 2847	. . 3 ⊢ (𝜑 → 𝐸 ∈ (V × V))
16		1st2nd2 7843	. . 3 ⊢ (𝐸 ∈ (V × V) → 𝐸 = ⟨(1^st ‘𝐸), (2^nd ‘𝐸)⟩)
17	15, 16	syl 17	. 2 ⊢ (𝜑 → 𝐸 = ⟨(1^st ‘𝐸), (2^nd ‘𝐸)⟩)
18		eqid 2738	. . . . 5 ⊢ (𝑄 ×_c 𝐶) = (𝑄 ×_c 𝐶)
19		evlfcl.q	. . . . . 6 ⊢ 𝑄 = (𝐶 FuncCat 𝐷)
20	19	fucbas 17593	. . . . 5 ⊢ (𝐶 Func 𝐷) = (Base‘𝑄)
21	18, 20, 4	xpcbas 17811	. . . 4 ⊢ ((𝐶 Func 𝐷) × (Base‘𝐶)) = (Base‘(𝑄 ×_c 𝐶))
22		eqid 2738	. . . 4 ⊢ (Base‘𝐷) = (Base‘𝐷)
23		eqid 2738	. . . 4 ⊢ (Hom ‘(𝑄 ×_c 𝐶)) = (Hom ‘(𝑄 ×_c 𝐶))
24		eqid 2738	. . . 4 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
25		eqid 2738	. . . 4 ⊢ (Id‘(𝑄 ×_c 𝐶)) = (Id‘(𝑄 ×_c 𝐶))
26		eqid 2738	. . . 4 ⊢ (Id‘𝐷) = (Id‘𝐷)
27		eqid 2738	. . . 4 ⊢ (comp‘(𝑄 ×_c 𝐶)) = (comp‘(𝑄 ×_c 𝐶))
28	19, 2, 3	fuccat 17604	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ Cat)
29	18, 28, 2	xpccat 17823	. . . 4 ⊢ (𝜑 → (𝑄 ×_c 𝐶) ∈ Cat)
30		relfunc 17493	. . . . . . . . . . 11 ⊢ Rel (𝐶 Func 𝐷)
31		simpr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → 𝑓 ∈ (𝐶 Func 𝐷))
32		1st2ndbr 7856	. . . . . . . . . . 11 ⊢ ((Rel (𝐶 Func 𝐷) ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → (1^st ‘𝑓)(𝐶 Func 𝐷)(2^nd ‘𝑓))
33	30, 31, 32	sylancr 586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → (1^st ‘𝑓)(𝐶 Func 𝐷)(2^nd ‘𝑓))
34	4, 22, 33	funcf1 17497	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → (1^st ‘𝑓):(Base‘𝐶)⟶(Base‘𝐷))
35	34	ffvelrnda 6943	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) ∧ 𝑥 ∈ (Base‘𝐶)) → ((1^st ‘𝑓)‘𝑥) ∈ (Base‘𝐷))
36	35	ralrimiva 3107	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → ∀𝑥 ∈ (Base‘𝐶)((1^st ‘𝑓)‘𝑥) ∈ (Base‘𝐷))
37	36	ralrimiva 3107	. . . . . 6 ⊢ (𝜑 → ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑥 ∈ (Base‘𝐶)((1^st ‘𝑓)‘𝑥) ∈ (Base‘𝐷))
38		eqid 2738	. . . . . . 7 ⊢ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1^st ‘𝑓)‘𝑥)) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1^st ‘𝑓)‘𝑥))
39	38	fmpo 7881	. . . . . 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 7814	. . . . . . 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 6569	. . . . 5 ⊢ (𝜑 → ((1^st ‘𝐸):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷) ↔ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1^st ‘𝑓)‘𝑥)):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷)))
44	40, 43	mpbird 256	. . . 4 ⊢ (𝜑 → (1^st ‘𝐸):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷))
45		eqid 2738	. . . . . 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 7288	. . . . . . . . 9 ⊢ (𝑚(𝐶 Nat 𝐷)𝑛) ∈ V
47		ovex 7288	. . . . . . . . 9 ⊢ ((2^nd ‘𝑥)(Hom ‘𝐶)(2^nd ‘𝑦)) ∈ V
48	46, 47	mpoex 7893	. . . . . . . 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 5230	. . . . . . 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 5230	. . . . . 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 7883	. . . . 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 7815	. . . . . . 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 6510	. . . . 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 257	. . . 4 ⊢ (𝜑 → (2^nd ‘𝐸) Fn (((𝐶 Func 𝐷) × (Base‘𝐶)) × ((𝐶 Func 𝐷) × (Base‘𝐶))))
56	3	ad2antrr 722	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝐷 ∈ Cat)
57	56	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝐷 ∈ Cat)
58		simplrl 773	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑓 ∈ (𝐶 Func 𝐷))
59	30, 58, 32	sylancr 586	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1^st ‘𝑓)(𝐶 Func 𝐷)(2^nd ‘𝑓))
60	4, 22, 59	funcf1 17497	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1^st ‘𝑓):(Base‘𝐶)⟶(Base‘𝐷))
61	60	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (1^st ‘𝑓):(Base‘𝐶)⟶(Base‘𝐷))
62		simplrr 774	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑢 ∈ (Base‘𝐶))
63	62	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑢 ∈ (Base‘𝐶))
64	61, 63	ffvelrnd 6944	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((1^st ‘𝑓)‘𝑢) ∈ (Base‘𝐷))
65		simplrr 774	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑣 ∈ (Base‘𝐶))
66	61, 65	ffvelrnd 6944	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((1^st ‘𝑓)‘𝑣) ∈ (Base‘𝐷))
67		simprl 767	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑔 ∈ (𝐶 Func 𝐷))
68		1st2ndbr 7856	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Rel (𝐶 Func 𝐷) ∧ 𝑔 ∈ (𝐶 Func 𝐷)) → (1^st ‘𝑔)(𝐶 Func 𝐷)(2^nd ‘𝑔))
69	30, 67, 68	sylancr 586	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1^st ‘𝑔)(𝐶 Func 𝐷)(2^nd ‘𝑔))
70	4, 22, 69	funcf1 17497	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1^st ‘𝑔):(Base‘𝐶)⟶(Base‘𝐷))
71	70	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (1^st ‘𝑔):(Base‘𝐶)⟶(Base‘𝐷))
72	71, 65	ffvelrnd 6944	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((1^st ‘𝑔)‘𝑣) ∈ (Base‘𝐷))
73		simprr 769	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑣 ∈ (Base‘𝐶))
74	4, 5, 24, 59, 62, 73	funcf2 17499	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑢(2^nd ‘𝑓)𝑣):(𝑢(Hom ‘𝐶)𝑣)⟶(((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑓)‘𝑣)))
75	74	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (𝑢(2^nd ‘𝑓)𝑣):(𝑢(Hom ‘𝐶)𝑣)⟶(((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑓)‘𝑣)))
76		simprr 769	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))
77	75, 76	ffvelrnd 6944	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((𝑢(2^nd ‘𝑓)𝑣)‘ℎ) ∈ (((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑓)‘𝑣)))
78		simprl 767	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔))
79	7, 78	nat1st2nd 17583	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑎 ∈ (⟨(1^st ‘𝑓), (2^nd ‘𝑓)⟩(𝐶 Nat 𝐷)⟨(1^st ‘𝑔), (2^nd ‘𝑔)⟩))
80	7, 79, 4, 24, 65	natcl 17585	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (𝑎‘𝑣) ∈ (((1^st ‘𝑓)‘𝑣)(Hom ‘𝐷)((1^st ‘𝑔)‘𝑣)))
81	22, 24, 6, 57, 64, 66, 72, 77, 80	catcocl 17311	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((𝑎‘𝑣)(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑣)⟩(comp‘𝐷)((1^st ‘𝑔)‘𝑣))((𝑢(2^nd ‘𝑓)𝑣)‘ℎ)) ∈ (((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑔)‘𝑣)))
82	81	ralrimivva 3114	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → ∀𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔)∀ℎ ∈ (𝑢(Hom ‘𝐶)𝑣)((𝑎‘𝑣)(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑣)⟩(comp‘𝐷)((1^st ‘𝑔)‘𝑣))((𝑢(2^nd ‘𝑓)𝑣)‘ℎ)) ∈ (((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑔)‘𝑣)))
83		eqid 2738	. . . . . . . . . . . . . 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 7881	. . . . . . . . . . . . 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 722	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝐶 ∈ Cat)
87		eqid 2738	. . . . . . . . . . . . . 14 ⊢ (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩) = (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩)
88	1, 86, 56, 4, 5, 6, 7, 58, 67, 62, 73, 87	evlf2 17852	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩) = (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ℎ ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎‘𝑣)(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑣)⟩(comp‘𝐷)((1^st ‘𝑔)‘𝑣))((𝑢(2^nd ‘𝑓)𝑣)‘ℎ))))
89	88	feq1d 6569	. . . . . . . . . . . 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 256	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑔)‘𝑣)))
91	19, 7	fuchom 17594	. . . . . . . . . . . . 13 ⊢ (𝐶 Nat 𝐷) = (Hom ‘𝑄)
92	18, 20, 4, 91, 5, 58, 62, 67, 73, 23	xpchom2 17819	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩) = ((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣)))
93	1, 86, 56, 4, 58, 62	evlf1 17854	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑓(1^st ‘𝐸)𝑢) = ((1^st ‘𝑓)‘𝑢))
94	1, 86, 56, 4, 67, 73	evlf1 17854	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑔(1^st ‘𝐸)𝑣) = ((1^st ‘𝑔)‘𝑣))
95	93, 94	oveq12d 7273	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → ((𝑓(1^st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)) = (((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑔)‘𝑣)))
96	92, 95	feq23d 6579	. . . . . . . . . . 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 256	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1^st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)))
98	97	ralrimivva 3114	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1^st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)))
99	98	ralrimivva 3114	. . . . . . . 8 ⊢ (𝜑 → ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1^st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)))
100		oveq2 7263	. . . . . . . . . . . 12 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → (𝑥(2^nd ‘𝐸)𝑦) = (𝑥(2^nd ‘𝐸)⟨𝑔, 𝑣⟩))
101		oveq2 7263	. . . . . . . . . . . 12 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) = (𝑥(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩))
102		fveq2 6756	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → ((1^st ‘𝐸)‘𝑦) = ((1^st ‘𝐸)‘⟨𝑔, 𝑣⟩))
103		df-ov 7258	. . . . . . . . . . . . . 14 ⊢ (𝑔(1^st ‘𝐸)𝑣) = ((1^st ‘𝐸)‘⟨𝑔, 𝑣⟩)
104	102, 103	eqtr4di 2797	. . . . . . . . . . . . 13 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → ((1^st ‘𝐸)‘𝑦) = (𝑔(1^st ‘𝐸)𝑣))
105	104	oveq2d 7271	. . . . . . . . . . . 12 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → (((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐸)‘𝑦)) = (((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)))
106	100, 101, 105	feq123d 6573	. . . . . . . . . . 11 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → ((𝑥(2^nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐸)‘𝑦)) ↔ (𝑥(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(𝑥(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣))))
107	106	ralxp 5739	. . . . . . . . . 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 7262	. . . . . . . . . . . 12 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (𝑥(2^nd ‘𝐸)⟨𝑔, 𝑣⟩) = (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩))
109		oveq1 7262	. . . . . . . . . . . 12 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (𝑥(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩) = (⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩))
110		fveq2 6756	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((1^st ‘𝐸)‘𝑥) = ((1^st ‘𝐸)‘⟨𝑓, 𝑢⟩))
111		df-ov 7258	. . . . . . . . . . . . . 14 ⊢ (𝑓(1^st ‘𝐸)𝑢) = ((1^st ‘𝐸)‘⟨𝑓, 𝑢⟩)
112	110, 111	eqtr4di 2797	. . . . . . . . . . . . 13 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((1^st ‘𝐸)‘𝑥) = (𝑓(1^st ‘𝐸)𝑢))
113	112	oveq1d 7270	. . . . . . . . . . . 12 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)) = ((𝑓(1^st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)))
114	108, 109, 113	feq123d 6573	. . . . . . . . . . 11 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((𝑥(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(𝑥(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)) ↔ (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1^st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣))))
115	114	2ralbidv 3122	. . . . . . . . . 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	syl5bb 282	. . . . . . . . 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 5739	. . . . . . . 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 3132	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) → ∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2^nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐸)‘𝑦)))
120	119	r19.21bi 3132	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) → (𝑥(2^nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐸)‘𝑦)))
121	120	anasss 466	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))) → (𝑥(2^nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐸)‘𝑦)))
122	28	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝑄 ∈ Cat)
123	2	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝐶 ∈ Cat)
124		eqid 2738	. . . . . . . . . . 11 ⊢ (Id‘𝑄) = (Id‘𝑄)
125		eqid 2738	. . . . . . . . . . 11 ⊢ (Id‘𝐶) = (Id‘𝐶)
126		simprl 767	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝑓 ∈ (𝐶 Func 𝐷))
127		simprr 769	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝑢 ∈ (Base‘𝐶))
128	18, 122, 123, 20, 4, 124, 125, 25, 126, 127	xpcid 17822	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩) = ⟨((Id‘𝑄)‘𝑓), ((Id‘𝐶)‘𝑢)⟩)
129	128	fveq2d 6760	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘⟨((Id‘𝑄)‘𝑓), ((Id‘𝐶)‘𝑢)⟩))
130		df-ov 7258	. . . . . . . . 9 ⊢ (((Id‘𝑄)‘𝑓)(⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)((Id‘𝐶)‘𝑢)) = ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘⟨((Id‘𝑄)‘𝑓), ((Id‘𝐶)‘𝑢)⟩)
131	129, 130	eqtr4di 2797	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩)) = (((Id‘𝑄)‘𝑓)(⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)((Id‘𝐶)‘𝑢)))
132	3	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝐷 ∈ Cat)
133		eqid 2738	. . . . . . . . 9 ⊢ (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩) = (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)
134	20, 91, 124, 122, 126	catidcl 17308	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝑄)‘𝑓) ∈ (𝑓(𝐶 Nat 𝐷)𝑓))
135	4, 5, 125, 123, 127	catidcl 17308	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝐶)‘𝑢) ∈ (𝑢(Hom ‘𝐶)𝑢))
136	1, 123, 132, 4, 5, 6, 7, 126, 126, 127, 127, 133, 134, 135	evlf2val 17853	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝑄)‘𝑓)(⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)((Id‘𝐶)‘𝑢)) = ((((Id‘𝑄)‘𝑓)‘𝑢)(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑢)⟩(comp‘𝐷)((1^st ‘𝑓)‘𝑢))((𝑢(2^nd ‘𝑓)𝑢)‘((Id‘𝐶)‘𝑢))))
137	30, 126, 32	sylancr 586	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (1^st ‘𝑓)(𝐶 Func 𝐷)(2^nd ‘𝑓))
138	4, 22, 137	funcf1 17497	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (1^st ‘𝑓):(Base‘𝐶)⟶(Base‘𝐷))
139	138, 127	ffvelrnd 6944	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((1^st ‘𝑓)‘𝑢) ∈ (Base‘𝐷))
140	22, 24, 26, 132, 139	catidcl 17308	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢)) ∈ (((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑓)‘𝑢)))
141	22, 24, 26, 132, 139, 6, 139, 140	catlid 17309	. . . . . . . . 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 17605	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝑄)‘𝑓) = ((Id‘𝐷) ∘ (1^st ‘𝑓)))
143	142	fveq1d 6758	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝑄)‘𝑓)‘𝑢) = (((Id‘𝐷) ∘ (1^st ‘𝑓))‘𝑢))
144		fvco3 6849	. . . . . . . . . . . 12 ⊢ (((1^st ‘𝑓):(Base‘𝐶)⟶(Base‘𝐷) ∧ 𝑢 ∈ (Base‘𝐶)) → (((Id‘𝐷) ∘ (1^st ‘𝑓))‘𝑢) = ((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢)))
145	138, 127, 144	syl2anc 583	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝐷) ∘ (1^st ‘𝑓))‘𝑢) = ((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢)))
146	143, 145	eqtrd 2778	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝑄)‘𝑓)‘𝑢) = ((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢)))
147	4, 125, 26, 137, 127	funcid 17501	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((𝑢(2^nd ‘𝑓)𝑢)‘((Id‘𝐶)‘𝑢)) = ((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢)))
148	146, 147	oveq12d 7273	. . . . . . . . 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 17854	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (𝑓(1^st ‘𝐸)𝑢) = ((1^st ‘𝑓)‘𝑢))
150	149	fveq2d 6760	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝐷)‘(𝑓(1^st ‘𝐸)𝑢)) = ((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢)))
151	141, 148, 150	3eqtr4d 2788	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((((Id‘𝑄)‘𝑓)‘𝑢)(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑢)⟩(comp‘𝐷)((1^st ‘𝑓)‘𝑢))((𝑢(2^nd ‘𝑓)𝑢)‘((Id‘𝐶)‘𝑢))) = ((Id‘𝐷)‘(𝑓(1^st ‘𝐸)𝑢)))
152	131, 136, 151	3eqtrd 2782	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1^st ‘𝐸)𝑢)))
153	152	ralrimivva 3114	. . . . . 6 ⊢ (𝜑 → ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1^st ‘𝐸)𝑢)))
154		id 22	. . . . . . . . . 10 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → 𝑥 = ⟨𝑓, 𝑢⟩)
155	154, 154	oveq12d 7273	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (𝑥(2^nd ‘𝐸)𝑥) = (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩))
156		fveq2 6756	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((Id‘(𝑄 ×_c 𝐶))‘𝑥) = ((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩))
157	155, 156	fveq12d 6763	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((𝑥(2^nd ‘𝐸)𝑥)‘((Id‘(𝑄 ×_c 𝐶))‘𝑥)) = ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩)))
158	112	fveq2d 6760	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((Id‘𝐷)‘((1^st ‘𝐸)‘𝑥)) = ((Id‘𝐷)‘(𝑓(1^st ‘𝐸)𝑢)))
159	157, 158	eqeq12d 2754	. . . . . . 7 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (((𝑥(2^nd ‘𝐸)𝑥)‘((Id‘(𝑄 ×_c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1^st ‘𝐸)‘𝑥)) ↔ ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1^st ‘𝐸)𝑢))))
160	159	ralxp 5739	. . . . . 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 3132	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) → ((𝑥(2^nd ‘𝐸)𝑥)‘((Id‘(𝑄 ×_c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1^st ‘𝐸)‘𝑥)))
163	2	3ad2ant1 1131	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝐶 ∈ Cat)
164	3	3ad2ant1 1131	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝐷 ∈ Cat)
165		simp21 1204	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
166		1st2nd2 7843	. . . . . . . . 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 2840	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
169		opelxp 5616	. . . . . . 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 1205	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
172		1st2nd2 7843	. . . . . . . . 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 2840	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
175		opelxp 5616	. . . . . . 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 1206	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
178		1st2nd2 7843	. . . . . . . . 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 2840	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
181		opelxp 5616	. . . . . . 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 1199	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦))
184	18, 21, 91, 5, 23, 165, 171	xpchom 17813	. . . . . . . . . 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 2841	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑓 ∈ (((1^st ‘𝑥)(𝐶 Nat 𝐷)(1^st ‘𝑦)) × ((2^nd ‘𝑥)(Hom ‘𝐶)(2^nd ‘𝑦))))
186		1st2nd2 7843	. . . . . . . . 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 2840	. . . . . . 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 5616	. . . . . . 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 1200	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))
192	18, 21, 91, 5, 23, 171, 177	xpchom 17813	. . . . . . . . . 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 2841	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑔 ∈ (((1^st ‘𝑦)(𝐶 Nat 𝐷)(1^st ‘𝑧)) × ((2^nd ‘𝑦)(Hom ‘𝐶)(2^nd ‘𝑧))))
194		1st2nd2 7843	. . . . . . . . 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 2840	. . . . . . 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 5616	. . . . . . 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 17855	. . . . 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 7273	. . . . . 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 4809	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ⟨𝑥, 𝑦⟩ = ⟨⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩, ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩⟩)
202	201, 179	oveq12d 7273	. . . . . . 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 7276	. . . . . 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 6763	. . . . 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 6760	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ((1^st ‘𝐸)‘𝑥) = ((1^st ‘𝐸)‘⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩))
206	173	fveq2d 6760	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ((1^st ‘𝐸)‘𝑦) = ((1^st ‘𝐸)‘⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩))
207	205, 206	opeq12d 4809	. . . . . . 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 6760	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ((1^st ‘𝐸)‘𝑧) = ((1^st ‘𝐸)‘⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩))
209	207, 208	oveq12d 7273	. . . . . 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 7273	. . . . . . 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 6763	. . . . . 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 7273	. . . . . . 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 6763	. . . . . 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 7276	. . . . 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 2788	. . . 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 17496	. . 3 ⊢ (𝜑 → (1^st ‘𝐸)((𝑄 ×_c 𝐶) Func 𝐷)(2^nd ‘𝐸))
217		df-br 5071	. . 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 2839	1 ⊢ (𝜑 → 𝐸 ∈ ((𝑄 ×_c 𝐶) Func 𝐷))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1085 = wceq 1539 ∈ wcel 2108 ∀wral 3063 Vcvv 3422 ⦋csb 3828 ⟨cop 4564 class class class wbr 5070 × cxp 5578 ∘ ccom 5584 Rel wrel 5585 Fn wfn 6413 ⟶wf 6414 ‘cfv 6418 (class class class)co 7255 ∈ cmpo 7257 1^st c1st 7802 2^nd c2nd 7803 Basecbs 16840 Hom chom 16899 compcco 16900 Catccat 17290 Idccid 17291 Func cfunc 17485 Nat cnat 17573 FuncCat cfuc 17574 ×_c cxpc 17801 eval_F cevlf 17843

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-er 8456 df-map 8575 df-ixp 8644 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-nn 11904 df-2 11966 df-3 11967 df-4 11968 df-5 11969 df-6 11970 df-7 11971 df-8 11972 df-9 11973 df-n0 12164 df-z 12250 df-dec 12367 df-uz 12512 df-fz 13169 df-struct 16776 df-slot 16811 df-ndx 16823 df-base 16841 df-hom 16912 df-cco 16913 df-cat 17294 df-cid 17295 df-func 17489 df-nat 17575 df-fuc 17576 df-xpc 17805 df-evlf 17847

This theorem is referenced by: uncfcl 17869 uncf1 17870 uncf2 17871 yonedalem1 17906

W3C validator