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 18179

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 2739	. . . . 5 ⊢ (Base‘𝐶) = (Base‘𝐶)
5		eqid 2739	. . . . 5 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
6		eqid 2739	. . . . 5 ⊢ (comp‘𝐷) = (comp‘𝐷)
7		eqid 2739	. . . . 5 ⊢ (𝐶 Nat 𝐷) = (𝐶 Nat 𝐷)
8	1, 2, 3, 4, 5, 6, 7	evlfval 18174	. . . 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 7389	. . . . . 6 ⊢ (𝐶 Func 𝐷) ∈ V
10		fvex 6840	. . . . . 6 ⊢ (Base‘𝐶) ∈ V
11	9, 10	mpoex 8021	. . . . 5 ⊢ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1^st ‘𝑓)‘𝑥)) ∈ V
12	9, 10	xpex 7696	. . . . . 6 ⊢ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∈ V
13	12, 12	mpoex 8021	. . . . 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 5658	. . . 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 7970	. . 3 ⊢ (𝐸 ∈ (V × V) → 𝐸 = ⟨(1^st ‘𝐸), (2^nd ‘𝐸)⟩)
17	15, 16	syl 17	. 2 ⊢ (𝜑 → 𝐸 = ⟨(1^st ‘𝐸), (2^nd ‘𝐸)⟩)
18		eqid 2739	. . . . 5 ⊢ (𝑄 ×_c 𝐶) = (𝑄 ×_c 𝐶)
19		evlfcl.q	. . . . . 6 ⊢ 𝑄 = (𝐶 FuncCat 𝐷)
20	19	fucbas 17921	. . . . 5 ⊢ (𝐶 Func 𝐷) = (Base‘𝑄)
21	18, 20, 4	xpcbas 18135	. . . 4 ⊢ ((𝐶 Func 𝐷) × (Base‘𝐶)) = (Base‘(𝑄 ×_c 𝐶))
22		eqid 2739	. . . 4 ⊢ (Base‘𝐷) = (Base‘𝐷)
23		eqid 2739	. . . 4 ⊢ (Hom ‘(𝑄 ×_c 𝐶)) = (Hom ‘(𝑄 ×_c 𝐶))
24		eqid 2739	. . . 4 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
25		eqid 2739	. . . 4 ⊢ (Id‘(𝑄 ×_c 𝐶)) = (Id‘(𝑄 ×_c 𝐶))
26		eqid 2739	. . . 4 ⊢ (Id‘𝐷) = (Id‘𝐷)
27		eqid 2739	. . . 4 ⊢ (comp‘(𝑄 ×_c 𝐶)) = (comp‘(𝑄 ×_c 𝐶))
28	19, 2, 3	fuccat 17931	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ Cat)
29	18, 28, 2	xpccat 18147	. . . 4 ⊢ (𝜑 → (𝑄 ×_c 𝐶) ∈ Cat)
30		relfunc 17820	. . . . . . . . . . 11 ⊢ Rel (𝐶 Func 𝐷)
31		simpr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → 𝑓 ∈ (𝐶 Func 𝐷))
32		1st2ndbr 7984	. . . . . . . . . . 11 ⊢ ((Rel (𝐶 Func 𝐷) ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → (1^st ‘𝑓)(𝐶 Func 𝐷)(2^nd ‘𝑓))
33	30, 31, 32	sylancr 593	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → (1^st ‘𝑓)(𝐶 Func 𝐷)(2^nd ‘𝑓))
34	4, 22, 33	funcf1 17824	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → (1^st ‘𝑓):(Base‘𝐶)⟶(Base‘𝐷))
35	34	ffvelcdmda 7025	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) ∧ 𝑥 ∈ (Base‘𝐶)) → ((1^st ‘𝑓)‘𝑥) ∈ (Base‘𝐷))
36	35	ralrimiva 3131	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → ∀𝑥 ∈ (Base‘𝐶)((1^st ‘𝑓)‘𝑥) ∈ (Base‘𝐷))
37	36	ralrimiva 3131	. . . . . 6 ⊢ (𝜑 → ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑥 ∈ (Base‘𝐶)((1^st ‘𝑓)‘𝑥) ∈ (Base‘𝐷))
38		eqid 2739	. . . . . . 7 ⊢ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1^st ‘𝑓)‘𝑥)) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1^st ‘𝑓)‘𝑥))
39	38	fmpo 8010	. . . . . 6 ⊢ (∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑥 ∈ (Base‘𝐶)((1^st ‘𝑓)‘𝑥) ∈ (Base‘𝐷) ↔ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1^st ‘𝑓)‘𝑥)):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷))
40	37, 39	sylib 219	. . . . 5 ⊢ (𝜑 → (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1^st ‘𝑓)‘𝑥)):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷))
41	11, 13	op1std 7941	. . . . . . 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 6637	. . . . 5 ⊢ (𝜑 → ((1^st ‘𝐸):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷) ↔ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1^st ‘𝑓)‘𝑥)):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷)))
44	40, 43	mpbird 258	. . . 4 ⊢ (𝜑 → (1^st ‘𝐸):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷))
45		eqid 2739	. . . . . 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 7389	. . . . . . . . 9 ⊢ (𝑚(𝐶 Nat 𝐷)𝑛) ∈ V
47		ovex 7389	. . . . . . . . 9 ⊢ ((2^nd ‘𝑥)(Hom ‘𝐶)(2^nd ‘𝑦)) ∈ V
48	46, 47	mpoex 8021	. . . . . . . 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 5233	. . . . . . 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 5233	. . . . . 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 8012	. . . . 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 7942	. . . . . . 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 6578	. . . . 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 259	. . . 4 ⊢ (𝜑 → (2^nd ‘𝐸) Fn (((𝐶 Func 𝐷) × (Base‘𝐶)) × ((𝐶 Func 𝐷) × (Base‘𝐶))))
56	3	ad2antrr 732	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝐷 ∈ Cat)
57	56	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝐷 ∈ Cat)
58		simplrl 782	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑓 ∈ (𝐶 Func 𝐷))
59	30, 58, 32	sylancr 593	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1^st ‘𝑓)(𝐶 Func 𝐷)(2^nd ‘𝑓))
60	4, 22, 59	funcf1 17824	. . . . . . . . . . . . . . . . 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 783	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑢 ∈ (Base‘𝐶))
63	62	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑢 ∈ (Base‘𝐶))
64	61, 63	ffvelcdmd 7026	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((1^st ‘𝑓)‘𝑢) ∈ (Base‘𝐷))
65		simplrr 783	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑣 ∈ (Base‘𝐶))
66	61, 65	ffvelcdmd 7026	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((1^st ‘𝑓)‘𝑣) ∈ (Base‘𝐷))
67		simprl 776	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑔 ∈ (𝐶 Func 𝐷))
68		1st2ndbr 7984	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Rel (𝐶 Func 𝐷) ∧ 𝑔 ∈ (𝐶 Func 𝐷)) → (1^st ‘𝑔)(𝐶 Func 𝐷)(2^nd ‘𝑔))
69	30, 67, 68	sylancr 593	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1^st ‘𝑔)(𝐶 Func 𝐷)(2^nd ‘𝑔))
70	4, 22, 69	funcf1 17824	. . . . . . . . . . . . . . . . 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 7026	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((1^st ‘𝑔)‘𝑣) ∈ (Base‘𝐷))
73		simprr 778	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑣 ∈ (Base‘𝐶))
74	4, 5, 24, 59, 62, 73	funcf2 17826	. . . . . . . . . . . . . . . . 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 778	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))
77	75, 76	ffvelcdmd 7026	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((𝑢(2^nd ‘𝑓)𝑣)‘ℎ) ∈ (((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑓)‘𝑣)))
78		simprl 776	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔))
79	7, 78	nat1st2nd 17912	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑎 ∈ (⟨(1^st ‘𝑓), (2^nd ‘𝑓)⟩(𝐶 Nat 𝐷)⟨(1^st ‘𝑔), (2^nd ‘𝑔)⟩))
80	7, 79, 4, 24, 65	natcl 17914	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (𝑎‘𝑣) ∈ (((1^st ‘𝑓)‘𝑣)(Hom ‘𝐷)((1^st ‘𝑔)‘𝑣)))
81	22, 24, 6, 57, 64, 66, 72, 77, 80	catcocl 17642	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((𝑎‘𝑣)(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑣)⟩(comp‘𝐷)((1^st ‘𝑔)‘𝑣))((𝑢(2^nd ‘𝑓)𝑣)‘ℎ)) ∈ (((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑔)‘𝑣)))
82	81	ralrimivva 3182	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → ∀𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔)∀ℎ ∈ (𝑢(Hom ‘𝐶)𝑣)((𝑎‘𝑣)(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑣)⟩(comp‘𝐷)((1^st ‘𝑔)‘𝑣))((𝑢(2^nd ‘𝑓)𝑣)‘ℎ)) ∈ (((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑔)‘𝑣)))
83		eqid 2739	. . . . . . . . . . . . . 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 8010	. . . . . . . . . . . . 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 219	. . . . . . . . . . . 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 732	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝐶 ∈ Cat)
87		eqid 2739	. . . . . . . . . . . . . 14 ⊢ (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩) = (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩)
88	1, 86, 56, 4, 5, 6, 7, 58, 67, 62, 73, 87	evlf2 18175	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩) = (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ℎ ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎‘𝑣)(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑣)⟩(comp‘𝐷)((1^st ‘𝑔)‘𝑣))((𝑢(2^nd ‘𝑓)𝑣)‘ℎ))))
89	88	feq1d 6637	. . . . . . . . . . . 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 258	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑔)‘𝑣)))
91	19, 7	fuchom 17922	. . . . . . . . . . . . 13 ⊢ (𝐶 Nat 𝐷) = (Hom ‘𝑄)
92	18, 20, 4, 91, 5, 58, 62, 67, 73, 23	xpchom2 18143	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩) = ((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣)))
93	1, 86, 56, 4, 58, 62	evlf1 18177	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑓(1^st ‘𝐸)𝑢) = ((1^st ‘𝑓)‘𝑢))
94	1, 86, 56, 4, 67, 73	evlf1 18177	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑔(1^st ‘𝐸)𝑣) = ((1^st ‘𝑔)‘𝑣))
95	93, 94	oveq12d 7374	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → ((𝑓(1^st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)) = (((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑔)‘𝑣)))
96	92, 95	feq23d 6650	. . . . . . . . . . 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 258	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1^st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)))
98	97	ralrimivva 3182	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1^st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)))
99	98	ralrimivva 3182	. . . . . . . 8 ⊢ (𝜑 → ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1^st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)))
100		oveq2 7364	. . . . . . . . . . . 12 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → (𝑥(2^nd ‘𝐸)𝑦) = (𝑥(2^nd ‘𝐸)⟨𝑔, 𝑣⟩))
101		oveq2 7364	. . . . . . . . . . . 12 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) = (𝑥(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩))
102		fveq2 6827	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → ((1^st ‘𝐸)‘𝑦) = ((1^st ‘𝐸)‘⟨𝑔, 𝑣⟩))
103		df-ov 7359	. . . . . . . . . . . . . 14 ⊢ (𝑔(1^st ‘𝐸)𝑣) = ((1^st ‘𝐸)‘⟨𝑔, 𝑣⟩)
104	102, 103	eqtr4di 2792	. . . . . . . . . . . . 13 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → ((1^st ‘𝐸)‘𝑦) = (𝑔(1^st ‘𝐸)𝑣))
105	104	oveq2d 7372	. . . . . . . . . . . 12 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → (((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐸)‘𝑦)) = (((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)))
106	100, 101, 105	feq123d 6644	. . . . . . . . . . 11 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → ((𝑥(2^nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐸)‘𝑦)) ↔ (𝑥(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(𝑥(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣))))
107	106	ralxp 5783	. . . . . . . . . 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 7363	. . . . . . . . . . . 12 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (𝑥(2^nd ‘𝐸)⟨𝑔, 𝑣⟩) = (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩))
109		oveq1 7363	. . . . . . . . . . . 12 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (𝑥(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩) = (⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩))
110		fveq2 6827	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((1^st ‘𝐸)‘𝑥) = ((1^st ‘𝐸)‘⟨𝑓, 𝑢⟩))
111		df-ov 7359	. . . . . . . . . . . . . 14 ⊢ (𝑓(1^st ‘𝐸)𝑢) = ((1^st ‘𝐸)‘⟨𝑓, 𝑢⟩)
112	110, 111	eqtr4di 2792	. . . . . . . . . . . . 13 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((1^st ‘𝐸)‘𝑥) = (𝑓(1^st ‘𝐸)𝑢))
113	112	oveq1d 7371	. . . . . . . . . . . 12 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)) = ((𝑓(1^st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)))
114	108, 109, 113	feq123d 6644	. . . . . . . . . . 11 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((𝑥(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(𝑥(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)) ↔ (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1^st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣))))
115	114	2ralbidv 3203	. . . . . . . . . 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 284	. . . . . . . . 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 5783	. . . . . . . 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 235	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2^nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐸)‘𝑦)))
119	118	r19.21bi 3231	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) → ∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2^nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐸)‘𝑦)))
120	119	r19.21bi 3231	. . . . 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 2739	. . . . . . . . . . 11 ⊢ (Id‘𝑄) = (Id‘𝑄)
125		eqid 2739	. . . . . . . . . . 11 ⊢ (Id‘𝐶) = (Id‘𝐶)
126		simprl 776	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝑓 ∈ (𝐶 Func 𝐷))
127		simprr 778	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝑢 ∈ (Base‘𝐶))
128	18, 122, 123, 20, 4, 124, 125, 25, 126, 127	xpcid 18146	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩) = ⟨((Id‘𝑄)‘𝑓), ((Id‘𝐶)‘𝑢)⟩)
129	128	fveq2d 6831	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘⟨((Id‘𝑄)‘𝑓), ((Id‘𝐶)‘𝑢)⟩))
130		df-ov 7359	. . . . . . . . 9 ⊢ (((Id‘𝑄)‘𝑓)(⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)((Id‘𝐶)‘𝑢)) = ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘⟨((Id‘𝑄)‘𝑓), ((Id‘𝐶)‘𝑢)⟩)
131	129, 130	eqtr4di 2792	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩)) = (((Id‘𝑄)‘𝑓)(⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)((Id‘𝐶)‘𝑢)))
132	3	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝐷 ∈ Cat)
133		eqid 2739	. . . . . . . . 9 ⊢ (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩) = (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)
134	20, 91, 124, 122, 126	catidcl 17639	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝑄)‘𝑓) ∈ (𝑓(𝐶 Nat 𝐷)𝑓))
135	4, 5, 125, 123, 127	catidcl 17639	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝐶)‘𝑢) ∈ (𝑢(Hom ‘𝐶)𝑢))
136	1, 123, 132, 4, 5, 6, 7, 126, 126, 127, 127, 133, 134, 135	evlf2val 18176	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝑄)‘𝑓)(⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)((Id‘𝐶)‘𝑢)) = ((((Id‘𝑄)‘𝑓)‘𝑢)(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑢)⟩(comp‘𝐷)((1^st ‘𝑓)‘𝑢))((𝑢(2^nd ‘𝑓)𝑢)‘((Id‘𝐶)‘𝑢))))
137	30, 126, 32	sylancr 593	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (1^st ‘𝑓)(𝐶 Func 𝐷)(2^nd ‘𝑓))
138	4, 22, 137	funcf1 17824	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (1^st ‘𝑓):(Base‘𝐶)⟶(Base‘𝐷))
139	138, 127	ffvelcdmd 7026	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((1^st ‘𝑓)‘𝑢) ∈ (Base‘𝐷))
140	22, 24, 26, 132, 139	catidcl 17639	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢)) ∈ (((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑓)‘𝑢)))
141	22, 24, 26, 132, 139, 6, 139, 140	catlid 17640	. . . . . . . . 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 17932	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝑄)‘𝑓) = ((Id‘𝐷) ∘ (1^st ‘𝑓)))
143	142	fveq1d 6829	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝑄)‘𝑓)‘𝑢) = (((Id‘𝐷) ∘ (1^st ‘𝑓))‘𝑢))
144		fvco3 6927	. . . . . . . . . . . 12 ⊢ (((1^st ‘𝑓):(Base‘𝐶)⟶(Base‘𝐷) ∧ 𝑢 ∈ (Base‘𝐶)) → (((Id‘𝐷) ∘ (1^st ‘𝑓))‘𝑢) = ((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢)))
145	138, 127, 144	syl2anc 590	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝐷) ∘ (1^st ‘𝑓))‘𝑢) = ((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢)))
146	143, 145	eqtrd 2774	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝑄)‘𝑓)‘𝑢) = ((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢)))
147	4, 125, 26, 137, 127	funcid 17828	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((𝑢(2^nd ‘𝑓)𝑢)‘((Id‘𝐶)‘𝑢)) = ((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢)))
148	146, 147	oveq12d 7374	. . . . . . . . 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 18177	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (𝑓(1^st ‘𝐸)𝑢) = ((1^st ‘𝑓)‘𝑢))
150	149	fveq2d 6831	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝐷)‘(𝑓(1^st ‘𝐸)𝑢)) = ((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢)))
151	141, 148, 150	3eqtr4d 2784	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((((Id‘𝑄)‘𝑓)‘𝑢)(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑢)⟩(comp‘𝐷)((1^st ‘𝑓)‘𝑢))((𝑢(2^nd ‘𝑓)𝑢)‘((Id‘𝐶)‘𝑢))) = ((Id‘𝐷)‘(𝑓(1^st ‘𝐸)𝑢)))
152	131, 136, 151	3eqtrd 2778	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1^st ‘𝐸)𝑢)))
153	152	ralrimivva 3182	. . . . . 6 ⊢ (𝜑 → ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1^st ‘𝐸)𝑢)))
154		id 22	. . . . . . . . . 10 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → 𝑥 = ⟨𝑓, 𝑢⟩)
155	154, 154	oveq12d 7374	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (𝑥(2^nd ‘𝐸)𝑥) = (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩))
156		fveq2 6827	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((Id‘(𝑄 ×_c 𝐶))‘𝑥) = ((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩))
157	155, 156	fveq12d 6834	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((𝑥(2^nd ‘𝐸)𝑥)‘((Id‘(𝑄 ×_c 𝐶))‘𝑥)) = ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩)))
158	112	fveq2d 6831	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((Id‘𝐷)‘((1^st ‘𝐸)‘𝑥)) = ((Id‘𝐷)‘(𝑓(1^st ‘𝐸)𝑢)))
159	157, 158	eqeq12d 2755	. . . . . . 7 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (((𝑥(2^nd ‘𝐸)𝑥)‘((Id‘(𝑄 ×_c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1^st ‘𝐸)‘𝑥)) ↔ ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1^st ‘𝐸)𝑢))))
160	159	ralxp 5783	. . . . . 6 ⊢ (∀𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))((𝑥(2^nd ‘𝐸)𝑥)‘((Id‘(𝑄 ×_c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1^st ‘𝐸)‘𝑥)) ↔ ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1^st ‘𝐸)𝑢)))
161	153, 160	sylibr 235	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))((𝑥(2^nd ‘𝐸)𝑥)‘((Id‘(𝑄 ×_c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1^st ‘𝐸)‘𝑥)))
162	161	r19.21bi 3231	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) → ((𝑥(2^nd ‘𝐸)𝑥)‘((Id‘(𝑄 ×_c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1^st ‘𝐸)‘𝑥)))
163	2	3ad2ant1 1139	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝐶 ∈ Cat)
164	3	3ad2ant1 1139	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝐷 ∈ Cat)
165		simp21 1213	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
166		1st2nd2 7970	. . . . . . . . 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 5654	. . . . . . 7 ⊢ (⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↔ ((1^st ‘𝑥) ∈ (𝐶 Func 𝐷) ∧ (2^nd ‘𝑥) ∈ (Base‘𝐶)))
170	168, 169	sylib 219	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ((1^st ‘𝑥) ∈ (𝐶 Func 𝐷) ∧ (2^nd ‘𝑥) ∈ (Base‘𝐶)))
171		simp22 1214	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
172		1st2nd2 7970	. . . . . . . . 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 5654	. . . . . . 7 ⊢ (⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↔ ((1^st ‘𝑦) ∈ (𝐶 Func 𝐷) ∧ (2^nd ‘𝑦) ∈ (Base‘𝐶)))
176	174, 175	sylib 219	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ((1^st ‘𝑦) ∈ (𝐶 Func 𝐷) ∧ (2^nd ‘𝑦) ∈ (Base‘𝐶)))
177		simp23 1215	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
178		1st2nd2 7970	. . . . . . . . 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 5654	. . . . . . 7 ⊢ (⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↔ ((1^st ‘𝑧) ∈ (𝐶 Func 𝐷) ∧ (2^nd ‘𝑧) ∈ (Base‘𝐶)))
182	180, 181	sylib 219	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ((1^st ‘𝑧) ∈ (𝐶 Func 𝐷) ∧ (2^nd ‘𝑧) ∈ (Base‘𝐶)))
183		simp3l 1208	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦))
184	18, 21, 91, 5, 23, 165, 171	xpchom 18137	. . . . . . . . . 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 7970	. . . . . . . . 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 5654	. . . . . . 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 219	. . . . . 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 1209	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))
192	18, 21, 91, 5, 23, 171, 177	xpchom 18137	. . . . . . . . . 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 7970	. . . . . . . . 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 5654	. . . . . . 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 219	. . . . . 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 18178	. . . . 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 7374	. . . . . 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 4812	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ⟨𝑥, 𝑦⟩ = ⟨⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩, ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩⟩)
202	201, 179	oveq12d 7374	. . . . . . 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 7377	. . . . . 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 6834	. . . . 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 6831	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ((1^st ‘𝐸)‘𝑥) = ((1^st ‘𝐸)‘⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩))
206	173	fveq2d 6831	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ((1^st ‘𝐸)‘𝑦) = ((1^st ‘𝐸)‘⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩))
207	205, 206	opeq12d 4812	. . . . . . 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 6831	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ((1^st ‘𝐸)‘𝑧) = ((1^st ‘𝐸)‘⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩))
209	207, 208	oveq12d 7374	. . . . . 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 7374	. . . . . . 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 6834	. . . . . 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 7374	. . . . . . 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 6834	. . . . . 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 7377	. . . . 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 2784	. . . 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 17823	. . 3 ⊢ (𝜑 → (1^st ‘𝐸)((𝑄 ×_c 𝐶) Func 𝐷)(2^nd ‘𝐸))
217		df-br 5073	. . 3 ⊢ ((1^st ‘𝐸)((𝑄 ×_c 𝐶) Func 𝐷)(2^nd ‘𝐸) ↔ ⟨(1^st ‘𝐸), (2^nd ‘𝐸)⟩ ∈ ((𝑄 ×_c 𝐶) Func 𝐷))
218	216, 217	sylib 219	. 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 396 ∧ w3a 1092 = wceq 1547 ∈ wcel 2119 ∀wral 3053 Vcvv 3431 ⦋csb 3831 ⟨cop 4561 class class class wbr 5072 × cxp 5616 ∘ ccom 5622 Rel wrel 5623 Fn wfn 6480 ⟶wf 6481 ‘cfv 6485 (class class class)co 7356 ∈ cmpo 7358 1^st c1st 7929 2^nd c2nd 7930 Basecbs 17170 Hom chom 17222 compcco 17223 Catccat 17621 Idccid 17622 Func cfunc 17812 Nat cnat 17902 FuncCat cfuc 17903 ×_c cxpc 18125 eval_F cevlf 18166

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-rep 5199 ax-sep 5218 ax-nul 5228 ax-pow 5294 ax-pr 5362 ax-un 7678 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-nel 3039 df-ral 3054 df-rex 3064 df-rmo 3344 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3903 df-nul 4262 df-if 4455 df-pw 4531 df-sn 4556 df-pr 4558 df-tp 4560 df-op 4562 df-uni 4839 df-iun 4923 df-br 5073 df-opab 5135 df-mpt 5154 df-tr 5180 df-id 5513 df-eprel 5518 df-po 5526 df-so 5527 df-fr 5571 df-we 5573 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-res 5630 df-ima 5631 df-pred 6252 df-ord 6313 df-on 6314 df-lim 6315 df-suc 6316 df-iota 6441 df-fun 6487 df-fn 6488 df-f 6489 df-f1 6490 df-fo 6491 df-f1o 6492 df-fv 6493 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-om 7807 df-1st 7931 df-2nd 7932 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-er 8633 df-map 8765 df-ixp 8836 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-nn 12166 df-2 12235 df-3 12236 df-4 12237 df-5 12238 df-6 12239 df-7 12240 df-8 12241 df-9 12242 df-n0 12429 df-z 12516 df-dec 12636 df-uz 12780 df-fz 13453 df-struct 17108 df-slot 17143 df-ndx 17155 df-base 17171 df-hom 17235 df-cco 17236 df-cat 17625 df-cid 17626 df-func 17816 df-nat 17904 df-fuc 17905 df-xpc 18129 df-evlf 18170

This theorem is referenced by: uncfcl 18192 uncf1 18193 uncf2 18194 yonedalem1 18229

W3C validator