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 16685

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 2610	. . . . 5 ⊢ (Base‘𝐶) = (Base‘𝐶)
5		eqid 2610	. . . . 5 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
6		eqid 2610	. . . . 5 ⊢ (comp‘𝐷) = (comp‘𝐷)
7		eqid 2610	. . . . 5 ⊢ (𝐶 Nat 𝐷) = (𝐶 Nat 𝐷)
8	1, 2, 3, 4, 5, 6, 7	evlfval 16680	. . . 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 6577	. . . . . 6 ⊢ (𝐶 Func 𝐷) ∈ V
10		fvex 6113	. . . . . 6 ⊢ (Base‘𝐶) ∈ V
11	9, 10	mpt2ex 7136	. . . . 5 ⊢ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1^st ‘𝑓)‘𝑥)) ∈ V
12	9, 10	xpex 6860	. . . . . 6 ⊢ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∈ V
13	12, 12	mpt2ex 7136	. . . . 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 5088	. . . 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	syl6eqel 2696	. . 3 ⊢ (𝜑 → 𝐸 ∈ (V × V))
16		1st2nd2 7096	. . 3 ⊢ (𝐸 ∈ (V × V) → 𝐸 = ⟨(1^st ‘𝐸), (2^nd ‘𝐸)⟩)
17	15, 16	syl 17	. 2 ⊢ (𝜑 → 𝐸 = ⟨(1^st ‘𝐸), (2^nd ‘𝐸)⟩)
18		eqid 2610	. . . . 5 ⊢ (𝑄 ×_c 𝐶) = (𝑄 ×_c 𝐶)
19		evlfcl.q	. . . . . 6 ⊢ 𝑄 = (𝐶 FuncCat 𝐷)
20	19	fucbas 16443	. . . . 5 ⊢ (𝐶 Func 𝐷) = (Base‘𝑄)
21	18, 20, 4	xpcbas 16641	. . . 4 ⊢ ((𝐶 Func 𝐷) × (Base‘𝐶)) = (Base‘(𝑄 ×_c 𝐶))
22		eqid 2610	. . . 4 ⊢ (Base‘𝐷) = (Base‘𝐷)
23		eqid 2610	. . . 4 ⊢ (Hom ‘(𝑄 ×_c 𝐶)) = (Hom ‘(𝑄 ×_c 𝐶))
24		eqid 2610	. . . 4 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
25		eqid 2610	. . . 4 ⊢ (Id‘(𝑄 ×_c 𝐶)) = (Id‘(𝑄 ×_c 𝐶))
26		eqid 2610	. . . 4 ⊢ (Id‘𝐷) = (Id‘𝐷)
27		eqid 2610	. . . 4 ⊢ (comp‘(𝑄 ×_c 𝐶)) = (comp‘(𝑄 ×_c 𝐶))
28	19, 2, 3	fuccat 16453	. . . . 5 ⊢ (𝜑 → 𝑄 ∈ Cat)
29	18, 28, 2	xpccat 16653	. . . 4 ⊢ (𝜑 → (𝑄 ×_c 𝐶) ∈ Cat)
30		relfunc 16345	. . . . . . . . . . 11 ⊢ Rel (𝐶 Func 𝐷)
31		simpr 476	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → 𝑓 ∈ (𝐶 Func 𝐷))
32		1st2ndbr 7108	. . . . . . . . . . 11 ⊢ ((Rel (𝐶 Func 𝐷) ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → (1^st ‘𝑓)(𝐶 Func 𝐷)(2^nd ‘𝑓))
33	30, 31, 32	sylancr 694	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → (1^st ‘𝑓)(𝐶 Func 𝐷)(2^nd ‘𝑓))
34	4, 22, 33	funcf1 16349	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → (1^st ‘𝑓):(Base‘𝐶)⟶(Base‘𝐷))
35	34	ffvelrnda 6267	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) ∧ 𝑥 ∈ (Base‘𝐶)) → ((1^st ‘𝑓)‘𝑥) ∈ (Base‘𝐷))
36	35	ralrimiva 2949	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → ∀𝑥 ∈ (Base‘𝐶)((1^st ‘𝑓)‘𝑥) ∈ (Base‘𝐷))
37	36	ralrimiva 2949	. . . . . 6 ⊢ (𝜑 → ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑥 ∈ (Base‘𝐶)((1^st ‘𝑓)‘𝑥) ∈ (Base‘𝐷))
38		eqid 2610	. . . . . . 7 ⊢ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1^st ‘𝑓)‘𝑥)) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1^st ‘𝑓)‘𝑥))
39	38	fmpt2 7126	. . . . . 6 ⊢ (∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑥 ∈ (Base‘𝐶)((1^st ‘𝑓)‘𝑥) ∈ (Base‘𝐷) ↔ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1^st ‘𝑓)‘𝑥)):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷))
40	37, 39	sylib 207	. . . . 5 ⊢ (𝜑 → (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1^st ‘𝑓)‘𝑥)):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷))
41	11, 13	op1std 7069	. . . . . . 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 5943	. . . . 5 ⊢ (𝜑 → ((1^st ‘𝐸):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷) ↔ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1^st ‘𝑓)‘𝑥)):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷)))
44	40, 43	mpbird 246	. . . 4 ⊢ (𝜑 → (1^st ‘𝐸):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷))
45		eqid 2610	. . . . . 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 6577	. . . . . . . . 9 ⊢ (𝑚(𝐶 Nat 𝐷)𝑛) ∈ V
47		ovex 6577	. . . . . . . . 9 ⊢ ((2^nd ‘𝑥)(Hom ‘𝐶)(2^nd ‘𝑦)) ∈ V
48	46, 47	mpt2ex 7136	. . . . . . . 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 4721	. . . . . . 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 4721	. . . . . 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	fnmpt2i 7128	. . . . 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 7070	. . . . . . 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 5895	. . . . 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 247	. . . 4 ⊢ (𝜑 → (2^nd ‘𝐸) Fn (((𝐶 Func 𝐷) × (Base‘𝐶)) × ((𝐶 Func 𝐷) × (Base‘𝐶))))
56	3	ad2antrr 758	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝐷 ∈ Cat)
57	56	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝐷 ∈ Cat)
58		simplrl 796	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑓 ∈ (𝐶 Func 𝐷))
59	30, 58, 32	sylancr 694	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1^st ‘𝑓)(𝐶 Func 𝐷)(2^nd ‘𝑓))
60	4, 22, 59	funcf1 16349	. . . . . . . . . . . . . . . . 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 797	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑢 ∈ (Base‘𝐶))
63	62	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑢 ∈ (Base‘𝐶))
64	61, 63	ffvelrnd 6268	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((1^st ‘𝑓)‘𝑢) ∈ (Base‘𝐷))
65		simplrr 797	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑣 ∈ (Base‘𝐶))
66	61, 65	ffvelrnd 6268	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((1^st ‘𝑓)‘𝑣) ∈ (Base‘𝐷))
67		simprl 790	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑔 ∈ (𝐶 Func 𝐷))
68		1st2ndbr 7108	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Rel (𝐶 Func 𝐷) ∧ 𝑔 ∈ (𝐶 Func 𝐷)) → (1^st ‘𝑔)(𝐶 Func 𝐷)(2^nd ‘𝑔))
69	30, 67, 68	sylancr 694	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1^st ‘𝑔)(𝐶 Func 𝐷)(2^nd ‘𝑔))
70	4, 22, 69	funcf1 16349	. . . . . . . . . . . . . . . . 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 6268	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((1^st ‘𝑔)‘𝑣) ∈ (Base‘𝐷))
73		simprr 792	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑣 ∈ (Base‘𝐶))
74	4, 5, 24, 59, 62, 73	funcf2 16351	. . . . . . . . . . . . . . . . 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 792	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))
77	75, 76	ffvelrnd 6268	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((𝑢(2^nd ‘𝑓)𝑣)‘ℎ) ∈ (((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑓)‘𝑣)))
78		simprl 790	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔))
79	7, 78	nat1st2nd 16434	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑎 ∈ (⟨(1^st ‘𝑓), (2^nd ‘𝑓)⟩(𝐶 Nat 𝐷)⟨(1^st ‘𝑔), (2^nd ‘𝑔)⟩))
80	7, 79, 4, 24, 65	natcl 16436	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (𝑎‘𝑣) ∈ (((1^st ‘𝑓)‘𝑣)(Hom ‘𝐷)((1^st ‘𝑔)‘𝑣)))
81	22, 24, 6, 57, 64, 66, 72, 77, 80	catcocl 16169	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((𝑎‘𝑣)(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑣)⟩(comp‘𝐷)((1^st ‘𝑔)‘𝑣))((𝑢(2^nd ‘𝑓)𝑣)‘ℎ)) ∈ (((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑔)‘𝑣)))
82	81	ralrimivva 2954	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → ∀𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔)∀ℎ ∈ (𝑢(Hom ‘𝐶)𝑣)((𝑎‘𝑣)(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑣)⟩(comp‘𝐷)((1^st ‘𝑔)‘𝑣))((𝑢(2^nd ‘𝑓)𝑣)‘ℎ)) ∈ (((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑔)‘𝑣)))
83		eqid 2610	. . . . . . . . . . . . . 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	fmpt2 7126	. . . . . . . . . . . . 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 207	. . . . . . . . . . . 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 758	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝐶 ∈ Cat)
87		eqid 2610	. . . . . . . . . . . . . 14 ⊢ (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩) = (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩)
88	1, 86, 56, 4, 5, 6, 7, 58, 67, 62, 73, 87	evlf2 16681	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩) = (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ℎ ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎‘𝑣)(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑣)⟩(comp‘𝐷)((1^st ‘𝑔)‘𝑣))((𝑢(2^nd ‘𝑓)𝑣)‘ℎ))))
89	88	feq1d 5943	. . . . . . . . . . . 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 246	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑔)‘𝑣)))
91	19, 7	fuchom 16444	. . . . . . . . . . . . 13 ⊢ (𝐶 Nat 𝐷) = (Hom ‘𝑄)
92	18, 20, 4, 91, 5, 58, 62, 67, 73, 23	xpchom2 16649	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩) = ((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣)))
93	1, 86, 56, 4, 58, 62	evlf1 16683	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑓(1^st ‘𝐸)𝑢) = ((1^st ‘𝑓)‘𝑢))
94	1, 86, 56, 4, 67, 73	evlf1 16683	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑔(1^st ‘𝐸)𝑣) = ((1^st ‘𝑔)‘𝑣))
95	93, 94	oveq12d 6567	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → ((𝑓(1^st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)) = (((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑔)‘𝑣)))
96	92, 95	feq23d 5953	. . . . . . . . . . 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 246	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1^st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)))
98	97	ralrimivva 2954	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1^st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)))
99	98	ralrimivva 2954	. . . . . . . 8 ⊢ (𝜑 → ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1^st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)))
100		oveq2 6557	. . . . . . . . . . . 12 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → (𝑥(2^nd ‘𝐸)𝑦) = (𝑥(2^nd ‘𝐸)⟨𝑔, 𝑣⟩))
101		oveq2 6557	. . . . . . . . . . . 12 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) = (𝑥(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩))
102		fveq2 6103	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → ((1^st ‘𝐸)‘𝑦) = ((1^st ‘𝐸)‘⟨𝑔, 𝑣⟩))
103		df-ov 6552	. . . . . . . . . . . . . 14 ⊢ (𝑔(1^st ‘𝐸)𝑣) = ((1^st ‘𝐸)‘⟨𝑔, 𝑣⟩)
104	102, 103	syl6eqr 2662	. . . . . . . . . . . . 13 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → ((1^st ‘𝐸)‘𝑦) = (𝑔(1^st ‘𝐸)𝑣))
105	104	oveq2d 6565	. . . . . . . . . . . 12 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → (((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐸)‘𝑦)) = (((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)))
106	100, 101, 105	feq123d 5947	. . . . . . . . . . 11 ⊢ (𝑦 = ⟨𝑔, 𝑣⟩ → ((𝑥(2^nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐸)‘𝑦)) ↔ (𝑥(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(𝑥(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣))))
107	106	ralxp 5185	. . . . . . . . . 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 6556	. . . . . . . . . . . 12 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (𝑥(2^nd ‘𝐸)⟨𝑔, 𝑣⟩) = (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩))
109		oveq1 6556	. . . . . . . . . . . 12 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (𝑥(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩) = (⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩))
110		fveq2 6103	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((1^st ‘𝐸)‘𝑥) = ((1^st ‘𝐸)‘⟨𝑓, 𝑢⟩))
111		df-ov 6552	. . . . . . . . . . . . . 14 ⊢ (𝑓(1^st ‘𝐸)𝑢) = ((1^st ‘𝐸)‘⟨𝑓, 𝑢⟩)
112	110, 111	syl6eqr 2662	. . . . . . . . . . . . 13 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((1^st ‘𝐸)‘𝑥) = (𝑓(1^st ‘𝐸)𝑢))
113	112	oveq1d 6564	. . . . . . . . . . . 12 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)) = ((𝑓(1^st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)))
114	108, 109, 113	feq123d 5947	. . . . . . . . . . 11 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((𝑥(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(𝑥(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣)) ↔ (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×_c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1^st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1^st ‘𝐸)𝑣))))
115	114	2ralbidv 2972	. . . . . . . . . 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 271	. . . . . . . . 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 5185	. . . . . . . 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 223	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2^nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐸)‘𝑦)))
119	118	r19.21bi 2916	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) → ∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2^nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐸)‘𝑦)))
120	119	r19.21bi 2916	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) → (𝑥(2^nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦)⟶(((1^st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1^st ‘𝐸)‘𝑦)))
121	120	anasss 677	. . . 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 2610	. . . . . . . . . . 11 ⊢ (Id‘𝑄) = (Id‘𝑄)
125		eqid 2610	. . . . . . . . . . 11 ⊢ (Id‘𝐶) = (Id‘𝐶)
126		simprl 790	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝑓 ∈ (𝐶 Func 𝐷))
127		simprr 792	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝑢 ∈ (Base‘𝐶))
128	18, 122, 123, 20, 4, 124, 125, 25, 126, 127	xpcid 16652	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩) = ⟨((Id‘𝑄)‘𝑓), ((Id‘𝐶)‘𝑢)⟩)
129	128	fveq2d 6107	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘⟨((Id‘𝑄)‘𝑓), ((Id‘𝐶)‘𝑢)⟩))
130		df-ov 6552	. . . . . . . . 9 ⊢ (((Id‘𝑄)‘𝑓)(⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)((Id‘𝐶)‘𝑢)) = ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘⟨((Id‘𝑄)‘𝑓), ((Id‘𝐶)‘𝑢)⟩)
131	129, 130	syl6eqr 2662	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩)) = (((Id‘𝑄)‘𝑓)(⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)((Id‘𝐶)‘𝑢)))
132	3	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝐷 ∈ Cat)
133		eqid 2610	. . . . . . . . 9 ⊢ (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩) = (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)
134	20, 91, 124, 122, 126	catidcl 16166	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝑄)‘𝑓) ∈ (𝑓(𝐶 Nat 𝐷)𝑓))
135	4, 5, 125, 123, 127	catidcl 16166	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝐶)‘𝑢) ∈ (𝑢(Hom ‘𝐶)𝑢))
136	1, 123, 132, 4, 5, 6, 7, 126, 126, 127, 127, 133, 134, 135	evlf2val 16682	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝑄)‘𝑓)(⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)((Id‘𝐶)‘𝑢)) = ((((Id‘𝑄)‘𝑓)‘𝑢)(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑢)⟩(comp‘𝐷)((1^st ‘𝑓)‘𝑢))((𝑢(2^nd ‘𝑓)𝑢)‘((Id‘𝐶)‘𝑢))))
137	30, 126, 32	sylancr 694	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (1^st ‘𝑓)(𝐶 Func 𝐷)(2^nd ‘𝑓))
138	4, 22, 137	funcf1 16349	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (1^st ‘𝑓):(Base‘𝐶)⟶(Base‘𝐷))
139	138, 127	ffvelrnd 6268	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((1^st ‘𝑓)‘𝑢) ∈ (Base‘𝐷))
140	22, 24, 26, 132, 139	catidcl 16166	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢)) ∈ (((1^st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1^st ‘𝑓)‘𝑢)))
141	22, 24, 26, 132, 139, 6, 139, 140	catlid 16167	. . . . . . . . 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 16454	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝑄)‘𝑓) = ((Id‘𝐷) ∘ (1^st ‘𝑓)))
143	142	fveq1d 6105	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝑄)‘𝑓)‘𝑢) = (((Id‘𝐷) ∘ (1^st ‘𝑓))‘𝑢))
144		fvco3 6185	. . . . . . . . . . . 12 ⊢ (((1^st ‘𝑓):(Base‘𝐶)⟶(Base‘𝐷) ∧ 𝑢 ∈ (Base‘𝐶)) → (((Id‘𝐷) ∘ (1^st ‘𝑓))‘𝑢) = ((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢)))
145	138, 127, 144	syl2anc 691	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝐷) ∘ (1^st ‘𝑓))‘𝑢) = ((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢)))
146	143, 145	eqtrd 2644	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝑄)‘𝑓)‘𝑢) = ((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢)))
147	4, 125, 26, 137, 127	funcid 16353	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((𝑢(2^nd ‘𝑓)𝑢)‘((Id‘𝐶)‘𝑢)) = ((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢)))
148	146, 147	oveq12d 6567	. . . . . . . . 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 16683	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (𝑓(1^st ‘𝐸)𝑢) = ((1^st ‘𝑓)‘𝑢))
150	149	fveq2d 6107	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝐷)‘(𝑓(1^st ‘𝐸)𝑢)) = ((Id‘𝐷)‘((1^st ‘𝑓)‘𝑢)))
151	141, 148, 150	3eqtr4d 2654	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((((Id‘𝑄)‘𝑓)‘𝑢)(⟨((1^st ‘𝑓)‘𝑢), ((1^st ‘𝑓)‘𝑢)⟩(comp‘𝐷)((1^st ‘𝑓)‘𝑢))((𝑢(2^nd ‘𝑓)𝑢)‘((Id‘𝐶)‘𝑢))) = ((Id‘𝐷)‘(𝑓(1^st ‘𝐸)𝑢)))
152	131, 136, 151	3eqtrd 2648	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1^st ‘𝐸)𝑢)))
153	152	ralrimivva 2954	. . . . . 6 ⊢ (𝜑 → ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1^st ‘𝐸)𝑢)))
154		id 22	. . . . . . . . . 10 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → 𝑥 = ⟨𝑓, 𝑢⟩)
155	154, 154	oveq12d 6567	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (𝑥(2^nd ‘𝐸)𝑥) = (⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩))
156		fveq2 6103	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((Id‘(𝑄 ×_c 𝐶))‘𝑥) = ((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩))
157	155, 156	fveq12d 6109	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((𝑥(2^nd ‘𝐸)𝑥)‘((Id‘(𝑄 ×_c 𝐶))‘𝑥)) = ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩)))
158	112	fveq2d 6107	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → ((Id‘𝐷)‘((1^st ‘𝐸)‘𝑥)) = ((Id‘𝐷)‘(𝑓(1^st ‘𝐸)𝑢)))
159	157, 158	eqeq12d 2625	. . . . . . 7 ⊢ (𝑥 = ⟨𝑓, 𝑢⟩ → (((𝑥(2^nd ‘𝐸)𝑥)‘((Id‘(𝑄 ×_c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1^st ‘𝐸)‘𝑥)) ↔ ((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1^st ‘𝐸)𝑢))))
160	159	ralxp 5185	. . . . . 6 ⊢ (∀𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))((𝑥(2^nd ‘𝐸)𝑥)‘((Id‘(𝑄 ×_c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1^st ‘𝐸)‘𝑥)) ↔ ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)((⟨𝑓, 𝑢⟩(2^nd ‘𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×_c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1^st ‘𝐸)𝑢)))
161	153, 160	sylibr 223	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))((𝑥(2^nd ‘𝐸)𝑥)‘((Id‘(𝑄 ×_c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1^st ‘𝐸)‘𝑥)))
162	161	r19.21bi 2916	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) → ((𝑥(2^nd ‘𝐸)𝑥)‘((Id‘(𝑄 ×_c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1^st ‘𝐸)‘𝑥)))
163	2	3ad2ant1 1075	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝐶 ∈ Cat)
164	3	3ad2ant1 1075	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝐷 ∈ Cat)
165		simp21 1087	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
166		1st2nd2 7096	. . . . . . . . 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 2689	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
169		opelxp 5070	. . . . . . 7 ⊢ (⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↔ ((1^st ‘𝑥) ∈ (𝐶 Func 𝐷) ∧ (2^nd ‘𝑥) ∈ (Base‘𝐶)))
170	168, 169	sylib 207	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ((1^st ‘𝑥) ∈ (𝐶 Func 𝐷) ∧ (2^nd ‘𝑥) ∈ (Base‘𝐶)))
171		simp22 1088	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
172		1st2nd2 7096	. . . . . . . . 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 2689	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
175		opelxp 5070	. . . . . . 7 ⊢ (⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↔ ((1^st ‘𝑦) ∈ (𝐶 Func 𝐷) ∧ (2^nd ‘𝑦) ∈ (Base‘𝐶)))
176	174, 175	sylib 207	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ((1^st ‘𝑦) ∈ (𝐶 Func 𝐷) ∧ (2^nd ‘𝑦) ∈ (Base‘𝐶)))
177		simp23 1089	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
178		1st2nd2 7096	. . . . . . . . 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 2689	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
181		opelxp 5070	. . . . . . 7 ⊢ (⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↔ ((1^st ‘𝑧) ∈ (𝐶 Func 𝐷) ∧ (2^nd ‘𝑧) ∈ (Base‘𝐶)))
182	180, 181	sylib 207	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ((1^st ‘𝑧) ∈ (𝐶 Func 𝐷) ∧ (2^nd ‘𝑧) ∈ (Base‘𝐶)))
183		simp3l 1082	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦))
184	18, 21, 91, 5, 23, 165, 171	xpchom 16643	. . . . . . . . . 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 2690	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑓 ∈ (((1^st ‘𝑥)(𝐶 Nat 𝐷)(1^st ‘𝑦)) × ((2^nd ‘𝑥)(Hom ‘𝐶)(2^nd ‘𝑦))))
186		1st2nd2 7096	. . . . . . . . 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 2689	. . . . . . 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 5070	. . . . . . 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 207	. . . . . 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 1083	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))
192	18, 21, 91, 5, 23, 171, 177	xpchom 16643	. . . . . . . . . 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 2690	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → 𝑔 ∈ (((1^st ‘𝑦)(𝐶 Nat 𝐷)(1^st ‘𝑧)) × ((2^nd ‘𝑦)(Hom ‘𝐶)(2^nd ‘𝑧))))
194		1st2nd2 7096	. . . . . . . . 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 2689	. . . . . . 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 5070	. . . . . . 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 207	. . . . . 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 16684	. . . . 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 6567	. . . . . 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 4348	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ⟨𝑥, 𝑦⟩ = ⟨⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩, ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩⟩)
202	201, 179	oveq12d 6567	. . . . . . 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 6570	. . . . . 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 6109	. . . . 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 6107	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ((1^st ‘𝐸)‘𝑥) = ((1^st ‘𝐸)‘⟨(1^st ‘𝑥), (2^nd ‘𝑥)⟩))
206	173	fveq2d 6107	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ((1^st ‘𝐸)‘𝑦) = ((1^st ‘𝐸)‘⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩))
207	205, 206	opeq12d 4348	. . . . . . 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 6107	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×_c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×_c 𝐶))𝑧))) → ((1^st ‘𝐸)‘𝑧) = ((1^st ‘𝐸)‘⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩))
209	207, 208	oveq12d 6567	. . . . . 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 6567	. . . . . . 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 6109	. . . . . 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 6567	. . . . . . 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 6109	. . . . . 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 6570	. . . . 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 2654	. . . 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 16348	. . 3 ⊢ (𝜑 → (1^st ‘𝐸)((𝑄 ×_c 𝐶) Func 𝐷)(2^nd ‘𝐸))
217		df-br 4584	. . 3 ⊢ ((1^st ‘𝐸)((𝑄 ×_c 𝐶) Func 𝐷)(2^nd ‘𝐸) ↔ ⟨(1^st ‘𝐸), (2^nd ‘𝐸)⟩ ∈ ((𝑄 ×_c 𝐶) Func 𝐷))
218	216, 217	sylib 207	. 2 ⊢ (𝜑 → ⟨(1^st ‘𝐸), (2^nd ‘𝐸)⟩ ∈ ((𝑄 ×_c 𝐶) Func 𝐷))
219	17, 218	eqeltrd 2688	1 ⊢ (𝜑 → 𝐸 ∈ ((𝑄 ×_c 𝐶) Func 𝐷))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ∀wral 2896 Vcvv 3173 ⦋csb 3499 ⟨cop 4131 class class class wbr 4583 × cxp 5036 ∘ ccom 5042 Rel wrel 5043 Fn wfn 5799 ⟶wf 5800 ‘cfv 5804 (class class class)co 6549 ↦ cmpt2 6551 1^st c1st 7057 2^nd c2nd 7058 Basecbs 15695 Hom chom 15779 compcco 15780 Catccat 16148 Idccid 16149 Func cfunc 16337 Nat cnat 16424 FuncCat cfuc 16425 ×_c cxpc 16631 eval_F cevlf 16672

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-fal 1481 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-oadd 7451 df-er 7629 df-map 7746 df-ixp 7795 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-nn 10898 df-2 10956 df-3 10957 df-4 10958 df-5 10959 df-6 10960 df-7 10961 df-8 10962 df-9 10963 df-n0 11170 df-z 11255 df-dec 11370 df-uz 11564 df-fz 12198 df-struct 15697 df-ndx 15698 df-slot 15699 df-base 15700 df-hom 15793 df-cco 15794 df-cat 16152 df-cid 16153 df-func 16341 df-nat 16426 df-fuc 16427 df-xpc 16635 df-evlf 16676

This theorem is referenced by: uncfcl 16698 uncf1 16699 uncf2 16700 yonedalem1 16735

W3C validator