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 18171

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 2732	. . . . 5 ⊢ (Base‘𝐶) = (Base‘𝐶)
5		eqid 2732	. . . . 5 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
6		eqid 2732	. . . . 5 ⊢ (comp‘𝐷) = (comp‘𝐷)
7		eqid 2732	. . . . 5 ⊢ (𝐶 Nat 𝐷) = (𝐶 Nat 𝐷)
8	1, 2, 3, 4, 5, 6, 7	evlfval 18166	. . . 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 7438	. . . . . 6 ⊢ (𝐶 Func 𝐷) ∈ V
10		fvex 6901	. . . . . 6 ⊢ (Base‘𝐶) ∈ V
11	9, 10	mpoex 8062	. . . . 5 ⊢ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1^st ‘𝑓)‘𝑥)) ∈ V
12	9, 10	xpex 7736	. . . . . 6 ⊢ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∈ V
13	12, 12	mpoex 8062	. . . . 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 5714	. . . 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 2841	. . 3 ⊢ (𝜑 → 𝐸 ∈ (V × V))
16		1st2nd2 8010	. . 3 ⊢ (𝐸 ∈ (V × V) → 𝐸 = ⟨(1^st ‘𝐸), (2^nd ‘𝐸)⟩)
17	15, 16	syl 17	. 2 ⊢ (𝜑 → 𝐸 = ⟨(1^st ‘𝐸), (2^nd ‘𝐸)⟩)
18		eqid 2732	. . . . 5 ⊢ (𝑄 ×_c 𝐶) = (𝑄 ×_c 𝐶)
19		evlfcl.q	. . . . . 6 ⊢ 𝑄 = (𝐶 FuncCat 𝐷)
20	19	fucbas 17908	. . . . 5 ⊢ (𝐶 Func 𝐷) = (Base‘𝑄)
21	18, 20, 4	xpcbas 18126	. . . 4 ⊢ ((𝐶 Func 𝐷) × (Base‘𝐶)) = (Base‘(𝑄 ×_c 𝐶))
22		eqid 2732	. . . 4 ⊢ (Base‘𝐷) = (Base‘𝐷)
23		eqid 2732	. . . 4 ⊢ (Hom ‘(𝑄 ×_c 𝐶)) = (Hom ‘(𝑄 ×_c 𝐶))
24		eqid 2732	. . . 4 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
25		eqid 2732	. . . 4 ⊢ (Id‘(𝑄 ×_c 𝐶)) = (Id‘(𝑄 ×_c 𝐶))
26		eqid 2732	. . . 4 ⊢ (Id‘𝐷) = (Id‘𝐷)
27		eqid 2732	. . . 4 ⊢ (comp‘(𝑄 ×_c 𝐶)) = (comp‘(𝑄 ×_c 𝐶))
28	19, 2, 3	fuccat 17919	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ Cat)
29	18, 28, 2	xpccat 18138	. . . 4 ⊢ (𝜑 → (𝑄 ×_c 𝐶) ∈ Cat)
30		relfunc 17808	. . . . . . . . . . 11 ⊢ Rel (𝐶 Func 𝐷)
31		simpr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → 𝑓 ∈ (𝐶 Func 𝐷))
32		1st2ndbr 8024	. . . . . . . . . . 11 ⊢ ((Rel (𝐶 Func 𝐷) ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → (1^st ‘𝑓)(𝐶 Func 𝐷)(2^nd ‘𝑓))
33	30, 31, 32	sylancr 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → (1^st ‘𝑓)(𝐶 Func 𝐷)(2^nd ‘𝑓))
34	4, 22, 33	funcf1 17812	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → (1^st ‘𝑓):(Base‘𝐶)⟶(Base‘𝐷))
35	34	ffvelcdmda 7083	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) ∧ 𝑥 ∈ (Base‘𝐶)) → ((1^st ‘𝑓)‘𝑥) ∈ (Base‘𝐷))
36	35	ralrimiva 3146	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → ∀𝑥 ∈ (Base‘𝐶)((1^st ‘𝑓)‘𝑥) ∈ (Base‘𝐷))
37	36	ralrimiva 3146	. . . . . 6 ⊢ (𝜑 → ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑥 ∈ (Base‘𝐶)((1^st ‘𝑓)‘𝑥) ∈ (Base‘𝐷))
38		eqid 2732	. . . . . . 7 ⊢ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1^st ‘𝑓)‘𝑥)) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1^st ‘𝑓)‘𝑥))
39	38	fmpo 8050	. . . . . 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 7981	. . . . . . 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 6699	. . . . 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 2732	. . . . . 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 7438	. . . . . . . . 9 ⊢ (𝑚(𝐶 Nat 𝐷)𝑛) ∈ V
47		ovex 7438	. . . . . . . . 9 ⊢ ((2^nd ‘𝑥)(Hom ‘𝐶)(2^nd ‘𝑦)) ∈ V
48	46, 47	mpoex 8062	. . . . . . . 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 5310	. . . . . . 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 5310	. . . . . 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 8052	. . . . 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 7982	. . . . . . 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 6639	. . . . 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 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝐷 ∈ Cat)
57	56	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝐷 ∈ Cat)
58		simplrl 775	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑓 ∈ (𝐶 Func 𝐷))
59	30, 58, 32	sylancr 587	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1^st ‘𝑓)(𝐶 Func 𝐷)(2^nd ‘𝑓))
60	4, 22, 59	funcf1 17812	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1^st ‘𝑓):(Base‘𝐶)⟶(Base‘𝐷))
61	60	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (1^st ‘𝑓):(Base‘𝐶)⟶(Base‘𝐷))
62		simplrr 776	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑢 ∈ (Base‘𝐶))
63	62	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑢 ∈ (Base‘𝐶))
64	61, 63	ffvelcdmd 7084	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((1^st ‘𝑓)‘𝑢) ∈ (Base‘𝐷))
65		simplrr 776	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑣 ∈ (Base‘𝐶))
66	61, 65	ffvelcdmd 7084	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((1^st ‘𝑓)‘𝑣) ∈ (Base‘𝐷))
67		simprl 769	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑔 ∈ (𝐶 Func 𝐷))
68		1st2ndbr 8024	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Rel (𝐶 Func 𝐷) ∧ 𝑔 ∈ (𝐶 Func 𝐷)) → (1^st ‘𝑔)(𝐶 Func 𝐷)(2^nd ‘𝑔))
69	30, 67, 68	sylancr 587	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1^st ‘𝑔)(𝐶 Func 𝐷)(2^nd ‘𝑔))
70	4, 22, 69	funcf1 17812	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1^st ‘𝑔):(Base‘𝐶)⟶(Base‘𝐷))
71	70	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (1^st ‘𝑔):(Base‘𝐶)⟶(Base‘𝐷))
72	71, 65	ffvelcdmd 7084	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((1^st ‘𝑔)‘𝑣) ∈ (Base‘𝐷))
73		simprr 771	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑣 ∈ (Base‘𝐶))
74	4, 5, 24, 59, 62, 73	funcf2 17814	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑢(2^nd ‘𝑓)𝑣):(𝑢(Hom ‘𝐶)𝑣)⟶(((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑓)‘𝑣)))
75	74	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (𝑢(2^nd ‘𝑓)𝑣):(𝑢(Hom ‘𝐶)𝑣)⟶(((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑓)‘𝑣)))
76		simprr 771	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))
77	75, 76	ffvelcdmd 7084	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((𝑢(2^nd ‘𝑓)𝑣)‘ℎ) ∈ (((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑓)‘𝑣)))
78		simprl 769	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔))
79	7, 78	nat1st2nd 17898	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑎 ∈ (⟨(1^st ‘𝑓), (2^nd ‘𝑓)⟩(𝐶 Nat 𝐷)⟨(1^st ‘𝑔), (2^nd ‘𝑔)⟩))
80	7, 79, 4, 24, 65	natcl 17900	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (𝑎‘𝑣) ∈ (((1^st ‘𝑓)‘𝑣)(Hom ‘𝐷)((1^st ‘𝑔)‘𝑣)))
81	22, 24, 6, 57, 64, 66, 72, 77, 80	catcocl 17625	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((𝑎‘𝑣)(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑣)⟩(comp‘𝐷)((1^st ‘𝑔)‘𝑣))((𝑢(2^nd ‘𝑓)𝑣)‘ℎ)) ∈ (((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑔)‘𝑣)))
82	81	ralrimivva 3200	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → ∀𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔)∀ℎ ∈ (𝑢(Hom ‘𝐶)𝑣)((𝑎‘𝑣)(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑣)⟩(comp‘𝐷)((1^st ‘𝑔)‘𝑣))((𝑢(2^nd ‘𝑓)𝑣)‘ℎ)) ∈ (((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑔)‘𝑣)))
83		eqid 2732	. . . . . . . . . . . . . 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 8050	. . . . . . . . . . . . 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 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝐶 ∈ Cat)
87		eqid 2732	. . . . . . . . . . . . . 14 ⊢ (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩) = (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩)
88	1, 86, 56, 4, 5, 6, 7, 58, 67, 62, 73, 87	evlf2 18167	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩) = (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ℎ ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎‘𝑣)(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑣)⟩(comp‘𝐷)((1^st ‘𝑔)‘𝑣))((𝑢(2^nd ‘𝑓)𝑣)‘ℎ))))
89	88	feq1d 6699	. . . . . . . . . . . 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 17909	. . . . . . . . . . . . 13 ⊢ (𝐶 Nat 𝐷) = (Hom ‘𝑄)
92	18, 20, 4, 91, 5, 58, 62, 67, 73, 23	xpchom2 18134	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩) = ((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣)))
93	1, 86, 56, 4, 58, 62	evlf1 18169	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑓(1^st ‘𝐸)𝑢) = ((1^st ‘𝑓)‘𝑢))
94	1, 86, 56, 4, 67, 73	evlf1 18169	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑔(1^st ‘𝐸)𝑣) = ((1^st ‘𝑔)‘𝑣))
95	93, 94	oveq12d 7423	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → ((𝑓(1^st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)) = (((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑔)‘𝑣)))
96	92, 95	feq23d 6709	. . . . . . . . . . 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 3200	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1^st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)))
99	98	ralrimivva 3200	. . . . . . . 8 ⊢ (𝜑 → ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1^st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)))
100		oveq2 7413	. . . . . . . . . . . 12 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → (𝑥(2^nd ‘𝐸)𝑦) = (𝑥(2^nd ‘𝐸)⟨𝑔, 𝑣⟩))
101		oveq2 7413	. . . . . . . . . . . 12 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) = (𝑥(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩))
102		fveq2 6888	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → ((1^st ‘𝐸)‘𝑦) = ((1^st ‘𝐸)‘⟨𝑔, 𝑣⟩))
103		df-ov 7408	. . . . . . . . . . . . . 14 ⊢ (𝑔(1^st ‘𝐸)𝑣) = ((1^st ‘𝐸)‘⟨𝑔, 𝑣⟩)
104	102, 103	eqtr4di 2790	. . . . . . . . . . . . 13 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → ((1^st ‘𝐸)‘𝑦) = (𝑔(1^st ‘𝐸)𝑣))
105	104	oveq2d 7421	. . . . . . . . . . . 12 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → (((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐸)‘𝑦)) = (((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)))
106	100, 101, 105	feq123d 6703	. . . . . . . . . . 11 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → ((𝑥(2^nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐸)‘𝑦)) ↔ (𝑥(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(𝑥(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣))))
107	106	ralxp 5839	. . . . . . . . . 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 7412	. . . . . . . . . . . 12 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (𝑥(2^nd ‘𝐸)⟨𝑔, 𝑣⟩) = (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩))
109		oveq1 7412	. . . . . . . . . . . 12 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (𝑥(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩) = (⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩))
110		fveq2 6888	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((1^st ‘𝐸)‘𝑥) = ((1^st ‘𝐸)‘⟨𝑓, 𝑢⟩))
111		df-ov 7408	. . . . . . . . . . . . . 14 ⊢ (𝑓(1^st ‘𝐸)𝑢) = ((1^st ‘𝐸)‘⟨𝑓, 𝑢⟩)
112	110, 111	eqtr4di 2790	. . . . . . . . . . . . 13 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((1^st ‘𝐸)‘𝑥) = (𝑓(1^st ‘𝐸)𝑢))
113	112	oveq1d 7420	. . . . . . . . . . . 12 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)) = ((𝑓(1^st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)))
114	108, 109, 113	feq123d 6703	. . . . . . . . . . 11 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((𝑥(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(𝑥(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)) ↔ (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1^st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣))))
115	114	2ralbidv 3218	. . . . . . . . . 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 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 5839	. . . . . . . 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 3248	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) → ∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2^nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐸)‘𝑦)))
120	119	r19.21bi 3248	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) → (𝑥(2^nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐸)‘𝑦)))
121	120	anasss 467	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))) → (𝑥(2^nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐸)‘𝑦)))
122	28	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝑄 ∈ Cat)
123	2	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝐶 ∈ Cat)
124		eqid 2732	. . . . . . . . . . 11 ⊢ (Id‘𝑄) = (Id‘𝑄)
125		eqid 2732	. . . . . . . . . . 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 18137	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩) = ⟨((Id‘𝑄)‘𝑓), ((Id‘𝐶)‘𝑢)⟩)
129	128	fveq2d 6892	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘⟨((Id‘𝑄)‘𝑓), ((Id‘𝐶)‘𝑢)⟩))
130		df-ov 7408	. . . . . . . . 9 ⊢ (((Id‘𝑄)‘𝑓)(⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)((Id‘𝐶)‘𝑢)) = ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘⟨((Id‘𝑄)‘𝑓), ((Id‘𝐶)‘𝑢)⟩)
131	129, 130	eqtr4di 2790	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩)) = (((Id‘𝑄)‘𝑓)(⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)((Id‘𝐶)‘𝑢)))
132	3	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝐷 ∈ Cat)
133		eqid 2732	. . . . . . . . 9 ⊢ (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩) = (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)
134	20, 91, 124, 122, 126	catidcl 17622	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝑄)‘𝑓) ∈ (𝑓(𝐶 Nat 𝐷)𝑓))
135	4, 5, 125, 123, 127	catidcl 17622	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝐶)‘𝑢) ∈ (𝑢(Hom ‘𝐶)𝑢))
136	1, 123, 132, 4, 5, 6, 7, 126, 126, 127, 127, 133, 134, 135	evlf2val 18168	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝑄)‘𝑓)(⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)((Id‘𝐶)‘𝑢)) = ((((Id‘𝑄)‘𝑓)‘𝑢)(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑢)⟩(comp‘𝐷)((1^st ‘𝑓)‘𝑢))((𝑢(2^nd ‘𝑓)𝑢)‘((Id‘𝐶)‘𝑢))))
137	30, 126, 32	sylancr 587	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (1^st ‘𝑓)(𝐶 Func 𝐷)(2^nd ‘𝑓))
138	4, 22, 137	funcf1 17812	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (1^st ‘𝑓):(Base‘𝐶)⟶(Base‘𝐷))
139	138, 127	ffvelcdmd 7084	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((1^st ‘𝑓)‘𝑢) ∈ (Base‘𝐷))
140	22, 24, 26, 132, 139	catidcl 17622	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢)) ∈ (((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑓)‘𝑢)))
141	22, 24, 26, 132, 139, 6, 139, 140	catlid 17623	. . . . . . . . 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 17920	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝑄)‘𝑓) = ((Id‘𝐷) ∘ (1^st ‘𝑓)))
143	142	fveq1d 6890	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝑄)‘𝑓)‘𝑢) = (((Id‘𝐷) ∘ (1^st ‘𝑓))‘𝑢))
144		fvco3 6987	. . . . . . . . . . . 12 ⊢ (((1^st ‘𝑓):(Base‘𝐶)⟶(Base‘𝐷) ∧ 𝑢 ∈ (Base‘𝐶)) → (((Id‘𝐷) ∘ (1^st ‘𝑓))‘𝑢) = ((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢)))
145	138, 127, 144	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝐷) ∘ (1^st ‘𝑓))‘𝑢) = ((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢)))
146	143, 145	eqtrd 2772	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝑄)‘𝑓)‘𝑢) = ((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢)))
147	4, 125, 26, 137, 127	funcid 17816	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((𝑢(2^nd ‘𝑓)𝑢)‘((Id‘𝐶)‘𝑢)) = ((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢)))
148	146, 147	oveq12d 7423	. . . . . . . . 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 18169	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (𝑓(1^st ‘𝐸)𝑢) = ((1^st ‘𝑓)‘𝑢))
150	149	fveq2d 6892	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝐷)‘(𝑓(1^st ‘𝐸)𝑢)) = ((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢)))
151	141, 148, 150	3eqtr4d 2782	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((((Id‘𝑄)‘𝑓)‘𝑢)(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑢)⟩(comp‘𝐷)((1^st ‘𝑓)‘𝑢))((𝑢(2^nd ‘𝑓)𝑢)‘((Id‘𝐶)‘𝑢))) = ((Id‘𝐷)‘(𝑓(1^st ‘𝐸)𝑢)))
152	131, 136, 151	3eqtrd 2776	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1^st ‘𝐸)𝑢)))
153	152	ralrimivva 3200	. . . . . 6 ⊢ (𝜑 → ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1^st ‘𝐸)𝑢)))
154		id 22	. . . . . . . . . 10 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → 𝑥 = ⟨𝑓, 𝑢⟩)
155	154, 154	oveq12d 7423	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (𝑥(2^nd ‘𝐸)𝑥) = (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩))
156		fveq2 6888	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((Id‘(𝑄 ×_c 𝐶))‘𝑥) = ((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩))
157	155, 156	fveq12d 6895	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((𝑥(2^nd ‘𝐸)𝑥)‘((Id‘(𝑄 ×_c 𝐶))‘𝑥)) = ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩)))
158	112	fveq2d 6892	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((Id‘𝐷)‘((1^st ‘𝐸)‘𝑥)) = ((Id‘𝐷)‘(𝑓(1^st ‘𝐸)𝑢)))
159	157, 158	eqeq12d 2748	. . . . . . 7 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (((𝑥(2^nd ‘𝐸)𝑥)‘((Id‘(𝑄 ×_c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1^st ‘𝐸)‘𝑥)) ↔ ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1^st ‘𝐸)𝑢))))
160	159	ralxp 5839	. . . . . 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 3248	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) → ((𝑥(2^nd ‘𝐸)𝑥)‘((Id‘(𝑄 ×_c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1^st ‘𝐸)‘𝑥)))
163	2	3ad2ant1 1133	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝐶 ∈ Cat)
164	3	3ad2ant1 1133	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝐷 ∈ Cat)
165		simp21 1206	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
166		1st2nd2 8010	. . . . . . . . 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 2834	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
169		opelxp 5711	. . . . . . 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 1207	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
172		1st2nd2 8010	. . . . . . . . 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 2834	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
175		opelxp 5711	. . . . . . 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 1208	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
178		1st2nd2 8010	. . . . . . . . 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 2834	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
181		opelxp 5711	. . . . . . 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 1201	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦))
184	18, 21, 91, 5, 23, 165, 171	xpchom 18128	. . . . . . . . . 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 2835	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑓 ∈ (((1^st ‘𝑥)(𝐶 Nat 𝐷)(1^st ‘𝑦)) × ((2^nd ‘𝑥)(Hom ‘𝐶)(2^nd ‘𝑦))))
186		1st2nd2 8010	. . . . . . . . 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 2834	. . . . . . 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 5711	. . . . . . 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 1202	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))
192	18, 21, 91, 5, 23, 171, 177	xpchom 18128	. . . . . . . . . 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 2835	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑔 ∈ (((1^st ‘𝑦)(𝐶 Nat 𝐷)(1^st ‘𝑧)) × ((2^nd ‘𝑦)(Hom ‘𝐶)(2^nd ‘𝑧))))
194		1st2nd2 8010	. . . . . . . . 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 2834	. . . . . . 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 5711	. . . . . . 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 18170	. . . . 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 7423	. . . . . 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 4880	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ⟨𝑥, 𝑦⟩ = ⟨⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩, ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩⟩)
202	201, 179	oveq12d 7423	. . . . . . 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 7426	. . . . . 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 6895	. . . . 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 6892	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ((1^st ‘𝐸)‘𝑥) = ((1^st ‘𝐸)‘⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩))
206	173	fveq2d 6892	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ((1^st ‘𝐸)‘𝑦) = ((1^st ‘𝐸)‘⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩))
207	205, 206	opeq12d 4880	. . . . . . 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 6892	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ((1^st ‘𝐸)‘𝑧) = ((1^st ‘𝐸)‘⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩))
209	207, 208	oveq12d 7423	. . . . . 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 7423	. . . . . . 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 6895	. . . . . 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 7423	. . . . . . 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 6895	. . . . . 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 7426	. . . . 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 2782	. . . 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 17811	. . 3 ⊢ (𝜑 → (1^st ‘𝐸)((𝑄 ×_c 𝐶) Func 𝐷)(2^nd ‘𝐸))
217		df-br 5148	. . 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 2833	1 ⊢ (𝜑 → 𝐸 ∈ ((𝑄 ×_c 𝐶) Func 𝐷))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ∀wral 3061 Vcvv 3474 ⦋csb 3892 ⟨cop 4633 class class class wbr 5147 × cxp 5673 ∘ ccom 5679 Rel wrel 5680 Fn wfn 6535 ⟶wf 6536 ‘cfv 6540 (class class class)co 7405 ∈ cmpo 7407 1^st c1st 7969 2^nd c2nd 7970 Basecbs 17140 Hom chom 17204 compcco 17205 Catccat 17604 Idccid 17605 Func cfunc 17800 Nat cnat 17888 FuncCat cfuc 17889 ×_c cxpc 18116 eval_F cevlf 18158

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-tp 4632 df-op 4634 df-uni 4908 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6297 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7361 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7852 df-1st 7971 df-2nd 7972 df-frecs 8262 df-wrecs 8293 df-recs 8367 df-rdg 8406 df-1o 8462 df-er 8699 df-map 8818 df-ixp 8888 df-en 8936 df-dom 8937 df-sdom 8938 df-fin 8939 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11442 df-neg 11443 df-nn 12209 df-2 12271 df-3 12272 df-4 12273 df-5 12274 df-6 12275 df-7 12276 df-8 12277 df-9 12278 df-n0 12469 df-z 12555 df-dec 12674 df-uz 12819 df-fz 13481 df-struct 17076 df-slot 17111 df-ndx 17123 df-base 17141 df-hom 17217 df-cco 17218 df-cat 17608 df-cid 17609 df-func 17804 df-nat 17890 df-fuc 17891 df-xpc 18120 df-evlf 18162

This theorem is referenced by: uncfcl 18184 uncf1 18185 uncf2 18186 yonedalem1 18221

W3C validator