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

Theorem evlfcl 17063
 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 𝐸 = (𝐶 evalF 𝐷)
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.
StepHypRef Expression
1 evlfcl.e . . . . 5 𝐸 = (𝐶 evalF 𝐷)
2 evlfcl.c . . . . 5 (𝜑𝐶 ∈ Cat)
3 evlfcl.d . . . . 5 (𝜑𝐷 ∈ Cat)
4 eqid 2760 . . . . 5 (Base‘𝐶) = (Base‘𝐶)
5 eqid 2760 . . . . 5 (Hom ‘𝐶) = (Hom ‘𝐶)
6 eqid 2760 . . . . 5 (comp‘𝐷) = (comp‘𝐷)
7 eqid 2760 . . . . 5 (𝐶 Nat 𝐷) = (𝐶 Nat 𝐷)
81, 2, 3, 4, 5, 6, 7evlfval 17058 . . . 4 (𝜑𝐸 = ⟨(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ (1st𝑥) / 𝑚(1st𝑦) / 𝑛(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ↦ ((𝑎‘(2nd𝑦))(⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩(comp‘𝐷)((1st𝑛)‘(2nd𝑦)))(((2nd𝑥)(2nd𝑚)(2nd𝑦))‘𝑔))))⟩)
9 ovex 6841 . . . . . 6 (𝐶 Func 𝐷) ∈ V
10 fvex 6362 . . . . . 6 (Base‘𝐶) ∈ V
119, 10mpt2ex 7415 . . . . 5 (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st𝑓)‘𝑥)) ∈ V
129, 10xpex 7127 . . . . . 6 ((𝐶 Func 𝐷) × (Base‘𝐶)) ∈ V
1312, 12mpt2ex 7415 . . . . 5 (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ (1st𝑥) / 𝑚(1st𝑦) / 𝑛(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ↦ ((𝑎‘(2nd𝑦))(⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩(comp‘𝐷)((1st𝑛)‘(2nd𝑦)))(((2nd𝑥)(2nd𝑚)(2nd𝑦))‘𝑔)))) ∈ V
1411, 13opelvv 5323 . . . 4 ⟨(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ (1st𝑥) / 𝑚(1st𝑦) / 𝑛(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ↦ ((𝑎‘(2nd𝑦))(⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩(comp‘𝐷)((1st𝑛)‘(2nd𝑦)))(((2nd𝑥)(2nd𝑚)(2nd𝑦))‘𝑔))))⟩ ∈ (V × V)
158, 14syl6eqel 2847 . . 3 (𝜑𝐸 ∈ (V × V))
16 1st2nd2 7372 . . 3 (𝐸 ∈ (V × V) → 𝐸 = ⟨(1st𝐸), (2nd𝐸)⟩)
1715, 16syl 17 . 2 (𝜑𝐸 = ⟨(1st𝐸), (2nd𝐸)⟩)
18 eqid 2760 . . . . 5 (𝑄 ×c 𝐶) = (𝑄 ×c 𝐶)
19 evlfcl.q . . . . . 6 𝑄 = (𝐶 FuncCat 𝐷)
2019fucbas 16821 . . . . 5 (𝐶 Func 𝐷) = (Base‘𝑄)
2118, 20, 4xpcbas 17019 . . . 4 ((𝐶 Func 𝐷) × (Base‘𝐶)) = (Base‘(𝑄 ×c 𝐶))
22 eqid 2760 . . . 4 (Base‘𝐷) = (Base‘𝐷)
23 eqid 2760 . . . 4 (Hom ‘(𝑄 ×c 𝐶)) = (Hom ‘(𝑄 ×c 𝐶))
24 eqid 2760 . . . 4 (Hom ‘𝐷) = (Hom ‘𝐷)
25 eqid 2760 . . . 4 (Id‘(𝑄 ×c 𝐶)) = (Id‘(𝑄 ×c 𝐶))
26 eqid 2760 . . . 4 (Id‘𝐷) = (Id‘𝐷)
27 eqid 2760 . . . 4 (comp‘(𝑄 ×c 𝐶)) = (comp‘(𝑄 ×c 𝐶))
2819, 2, 3fuccat 16831 . . . . 5 (𝜑𝑄 ∈ Cat)
2918, 28, 2xpccat 17031 . . . 4 (𝜑 → (𝑄 ×c 𝐶) ∈ Cat)
30 relfunc 16723 . . . . . . . . . . 11 Rel (𝐶 Func 𝐷)
31 simpr 479 . . . . . . . . . . 11 ((𝜑𝑓 ∈ (𝐶 Func 𝐷)) → 𝑓 ∈ (𝐶 Func 𝐷))
32 1st2ndbr 7384 . . . . . . . . . . 11 ((Rel (𝐶 Func 𝐷) ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → (1st𝑓)(𝐶 Func 𝐷)(2nd𝑓))
3330, 31, 32sylancr 698 . . . . . . . . . 10 ((𝜑𝑓 ∈ (𝐶 Func 𝐷)) → (1st𝑓)(𝐶 Func 𝐷)(2nd𝑓))
344, 22, 33funcf1 16727 . . . . . . . . 9 ((𝜑𝑓 ∈ (𝐶 Func 𝐷)) → (1st𝑓):(Base‘𝐶)⟶(Base‘𝐷))
3534ffvelrnda 6522 . . . . . . . 8 (((𝜑𝑓 ∈ (𝐶 Func 𝐷)) ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st𝑓)‘𝑥) ∈ (Base‘𝐷))
3635ralrimiva 3104 . . . . . . 7 ((𝜑𝑓 ∈ (𝐶 Func 𝐷)) → ∀𝑥 ∈ (Base‘𝐶)((1st𝑓)‘𝑥) ∈ (Base‘𝐷))
3736ralrimiva 3104 . . . . . 6 (𝜑 → ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑥 ∈ (Base‘𝐶)((1st𝑓)‘𝑥) ∈ (Base‘𝐷))
38 eqid 2760 . . . . . . 7 (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st𝑓)‘𝑥)) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st𝑓)‘𝑥))
3938fmpt2 7405 . . . . . 6 (∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑥 ∈ (Base‘𝐶)((1st𝑓)‘𝑥) ∈ (Base‘𝐷) ↔ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st𝑓)‘𝑥)):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷))
4037, 39sylib 208 . . . . 5 (𝜑 → (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st𝑓)‘𝑥)):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷))
4111, 13op1std 7343 . . . . . . 7 (𝐸 = ⟨(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ (1st𝑥) / 𝑚(1st𝑦) / 𝑛(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ↦ ((𝑎‘(2nd𝑦))(⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩(comp‘𝐷)((1st𝑛)‘(2nd𝑦)))(((2nd𝑥)(2nd𝑚)(2nd𝑦))‘𝑔))))⟩ → (1st𝐸) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st𝑓)‘𝑥)))
428, 41syl 17 . . . . . 6 (𝜑 → (1st𝐸) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st𝑓)‘𝑥)))
4342feq1d 6191 . . . . 5 (𝜑 → ((1st𝐸):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷) ↔ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st𝑓)‘𝑥)):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷)))
4440, 43mpbird 247 . . . 4 (𝜑 → (1st𝐸):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷))
45 eqid 2760 . . . . . 6 (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ (1st𝑥) / 𝑚(1st𝑦) / 𝑛(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ↦ ((𝑎‘(2nd𝑦))(⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩(comp‘𝐷)((1st𝑛)‘(2nd𝑦)))(((2nd𝑥)(2nd𝑚)(2nd𝑦))‘𝑔)))) = (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ (1st𝑥) / 𝑚(1st𝑦) / 𝑛(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ↦ ((𝑎‘(2nd𝑦))(⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩(comp‘𝐷)((1st𝑛)‘(2nd𝑦)))(((2nd𝑥)(2nd𝑚)(2nd𝑦))‘𝑔))))
46 ovex 6841 . . . . . . . . 9 (𝑚(𝐶 Nat 𝐷)𝑛) ∈ V
47 ovex 6841 . . . . . . . . 9 ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ∈ V
4846, 47mpt2ex 7415 . . . . . . . 8 (𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ↦ ((𝑎‘(2nd𝑦))(⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩(comp‘𝐷)((1st𝑛)‘(2nd𝑦)))(((2nd𝑥)(2nd𝑚)(2nd𝑦))‘𝑔))) ∈ V
4948csbex 4945 . . . . . . 7 (1st𝑦) / 𝑛(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ↦ ((𝑎‘(2nd𝑦))(⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩(comp‘𝐷)((1st𝑛)‘(2nd𝑦)))(((2nd𝑥)(2nd𝑚)(2nd𝑦))‘𝑔))) ∈ V
5049csbex 4945 . . . . . 6 (1st𝑥) / 𝑚(1st𝑦) / 𝑛(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ↦ ((𝑎‘(2nd𝑦))(⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩(comp‘𝐷)((1st𝑛)‘(2nd𝑦)))(((2nd𝑥)(2nd𝑚)(2nd𝑦))‘𝑔))) ∈ V
5145, 50fnmpt2i 7407 . . . . 5 (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ (1st𝑥) / 𝑚(1st𝑦) / 𝑛(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ↦ ((𝑎‘(2nd𝑦))(⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩(comp‘𝐷)((1st𝑛)‘(2nd𝑦)))(((2nd𝑥)(2nd𝑚)(2nd𝑦))‘𝑔)))) Fn (((𝐶 Func 𝐷) × (Base‘𝐶)) × ((𝐶 Func 𝐷) × (Base‘𝐶)))
5211, 13op2ndd 7344 . . . . . . 7 (𝐸 = ⟨(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ (1st𝑥) / 𝑚(1st𝑦) / 𝑛(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ↦ ((𝑎‘(2nd𝑦))(⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩(comp‘𝐷)((1st𝑛)‘(2nd𝑦)))(((2nd𝑥)(2nd𝑚)(2nd𝑦))‘𝑔))))⟩ → (2nd𝐸) = (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ (1st𝑥) / 𝑚(1st𝑦) / 𝑛(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ↦ ((𝑎‘(2nd𝑦))(⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩(comp‘𝐷)((1st𝑛)‘(2nd𝑦)))(((2nd𝑥)(2nd𝑚)(2nd𝑦))‘𝑔)))))
538, 52syl 17 . . . . . 6 (𝜑 → (2nd𝐸) = (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ (1st𝑥) / 𝑚(1st𝑦) / 𝑛(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ↦ ((𝑎‘(2nd𝑦))(⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩(comp‘𝐷)((1st𝑛)‘(2nd𝑦)))(((2nd𝑥)(2nd𝑚)(2nd𝑦))‘𝑔)))))
5453fneq1d 6142 . . . . 5 (𝜑 → ((2nd𝐸) Fn (((𝐶 Func 𝐷) × (Base‘𝐶)) × ((𝐶 Func 𝐷) × (Base‘𝐶))) ↔ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ (1st𝑥) / 𝑚(1st𝑦) / 𝑛(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ↦ ((𝑎‘(2nd𝑦))(⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩(comp‘𝐷)((1st𝑛)‘(2nd𝑦)))(((2nd𝑥)(2nd𝑚)(2nd𝑦))‘𝑔)))) Fn (((𝐶 Func 𝐷) × (Base‘𝐶)) × ((𝐶 Func 𝐷) × (Base‘𝐶)))))
5551, 54mpbiri 248 . . . 4 (𝜑 → (2nd𝐸) Fn (((𝐶 Func 𝐷) × (Base‘𝐶)) × ((𝐶 Func 𝐷) × (Base‘𝐶))))
563ad2antrr 764 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝐷 ∈ Cat)
5756adantr 472 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝐷 ∈ Cat)
58 simplrl 819 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑓 ∈ (𝐶 Func 𝐷))
5930, 58, 32sylancr 698 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1st𝑓)(𝐶 Func 𝐷)(2nd𝑓))
604, 22, 59funcf1 16727 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1st𝑓):(Base‘𝐶)⟶(Base‘𝐷))
6160adantr 472 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (1st𝑓):(Base‘𝐶)⟶(Base‘𝐷))
62 simplrr 820 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑢 ∈ (Base‘𝐶))
6362adantr 472 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑢 ∈ (Base‘𝐶))
6461, 63ffvelrnd 6523 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((1st𝑓)‘𝑢) ∈ (Base‘𝐷))
65 simplrr 820 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑣 ∈ (Base‘𝐶))
6661, 65ffvelrnd 6523 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((1st𝑓)‘𝑣) ∈ (Base‘𝐷))
67 simprl 811 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑔 ∈ (𝐶 Func 𝐷))
68 1st2ndbr 7384 . . . . . . . . . . . . . . . . . . 19 ((Rel (𝐶 Func 𝐷) ∧ 𝑔 ∈ (𝐶 Func 𝐷)) → (1st𝑔)(𝐶 Func 𝐷)(2nd𝑔))
6930, 67, 68sylancr 698 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1st𝑔)(𝐶 Func 𝐷)(2nd𝑔))
704, 22, 69funcf1 16727 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1st𝑔):(Base‘𝐶)⟶(Base‘𝐷))
7170adantr 472 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (1st𝑔):(Base‘𝐶)⟶(Base‘𝐷))
7271, 65ffvelrnd 6523 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((1st𝑔)‘𝑣) ∈ (Base‘𝐷))
73 simprr 813 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑣 ∈ (Base‘𝐶))
744, 5, 24, 59, 62, 73funcf2 16729 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑢(2nd𝑓)𝑣):(𝑢(Hom ‘𝐶)𝑣)⟶(((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑓)‘𝑣)))
7574adantr 472 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (𝑢(2nd𝑓)𝑣):(𝑢(Hom ‘𝐶)𝑣)⟶(((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑓)‘𝑣)))
76 simprr 813 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ∈ (𝑢(Hom ‘𝐶)𝑣))
7775, 76ffvelrnd 6523 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((𝑢(2nd𝑓)𝑣)‘) ∈ (((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑓)‘𝑣)))
78 simprl 811 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔))
797, 78nat1st2nd 16812 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑎 ∈ (⟨(1st𝑓), (2nd𝑓)⟩(𝐶 Nat 𝐷)⟨(1st𝑔), (2nd𝑔)⟩))
807, 79, 4, 24, 65natcl 16814 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (𝑎𝑣) ∈ (((1st𝑓)‘𝑣)(Hom ‘𝐷)((1st𝑔)‘𝑣)))
8122, 24, 6, 57, 64, 66, 72, 77, 80catcocl 16547 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((𝑎𝑣)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑣)⟩(comp‘𝐷)((1st𝑔)‘𝑣))((𝑢(2nd𝑓)𝑣)‘)) ∈ (((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑔)‘𝑣)))
8281ralrimivva 3109 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → ∀𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔)∀ ∈ (𝑢(Hom ‘𝐶)𝑣)((𝑎𝑣)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑣)⟩(comp‘𝐷)((1st𝑔)‘𝑣))((𝑢(2nd𝑓)𝑣)‘)) ∈ (((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑔)‘𝑣)))
83 eqid 2760 . . . . . . . . . . . . . 14 (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎𝑣)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑣)⟩(comp‘𝐷)((1st𝑔)‘𝑣))((𝑢(2nd𝑓)𝑣)‘))) = (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎𝑣)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑣)⟩(comp‘𝐷)((1st𝑔)‘𝑣))((𝑢(2nd𝑓)𝑣)‘)))
8483fmpt2 7405 . . . . . . . . . . . . 13 (∀𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔)∀ ∈ (𝑢(Hom ‘𝐶)𝑣)((𝑎𝑣)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑣)⟩(comp‘𝐷)((1st𝑔)‘𝑣))((𝑢(2nd𝑓)𝑣)‘)) ∈ (((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑔)‘𝑣)) ↔ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎𝑣)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑣)⟩(comp‘𝐷)((1st𝑔)‘𝑣))((𝑢(2nd𝑓)𝑣)‘))):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑔)‘𝑣)))
8582, 84sylib 208 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎𝑣)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑣)⟩(comp‘𝐷)((1st𝑔)‘𝑣))((𝑢(2nd𝑓)𝑣)‘))):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑔)‘𝑣)))
862ad2antrr 764 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝐶 ∈ Cat)
87 eqid 2760 . . . . . . . . . . . . . 14 (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩) = (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩)
881, 86, 56, 4, 5, 6, 7, 58, 67, 62, 73, 87evlf2 17059 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩) = (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎𝑣)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑣)⟩(comp‘𝐷)((1st𝑔)‘𝑣))((𝑢(2nd𝑓)𝑣)‘))))
8988feq1d 6191 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑔)‘𝑣)) ↔ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎𝑣)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑣)⟩(comp‘𝐷)((1st𝑔)‘𝑣))((𝑢(2nd𝑓)𝑣)‘))):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑔)‘𝑣))))
9085, 89mpbird 247 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑔)‘𝑣)))
9119, 7fuchom 16822 . . . . . . . . . . . . 13 (𝐶 Nat 𝐷) = (Hom ‘𝑄)
9218, 20, 4, 91, 5, 58, 62, 67, 73, 23xpchom2 17027 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩) = ((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣)))
931, 86, 56, 4, 58, 62evlf1 17061 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑓(1st𝐸)𝑢) = ((1st𝑓)‘𝑢))
941, 86, 56, 4, 67, 73evlf1 17061 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑔(1st𝐸)𝑣) = ((1st𝑔)‘𝑣))
9593, 94oveq12d 6831 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → ((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)) = (((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑔)‘𝑣)))
9692, 95feq23d 6201 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)) ↔ (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑔)‘𝑣))))
9790, 96mpbird 247 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)))
9897ralrimivva 3109 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)))
9998ralrimivva 3109 . . . . . . . 8 (𝜑 → ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)))
100 oveq2 6821 . . . . . . . . . . . 12 (𝑦 = ⟨𝑔, 𝑣⟩ → (𝑥(2nd𝐸)𝑦) = (𝑥(2nd𝐸)⟨𝑔, 𝑣⟩))
101 oveq2 6821 . . . . . . . . . . . 12 (𝑦 = ⟨𝑔, 𝑣⟩ → (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) = (𝑥(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩))
102 fveq2 6352 . . . . . . . . . . . . . 14 (𝑦 = ⟨𝑔, 𝑣⟩ → ((1st𝐸)‘𝑦) = ((1st𝐸)‘⟨𝑔, 𝑣⟩))
103 df-ov 6816 . . . . . . . . . . . . . 14 (𝑔(1st𝐸)𝑣) = ((1st𝐸)‘⟨𝑔, 𝑣⟩)
104102, 103syl6eqr 2812 . . . . . . . . . . . . 13 (𝑦 = ⟨𝑔, 𝑣⟩ → ((1st𝐸)‘𝑦) = (𝑔(1st𝐸)𝑣))
105104oveq2d 6829 . . . . . . . . . . . 12 (𝑦 = ⟨𝑔, 𝑣⟩ → (((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)) = (((1st𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)))
106100, 101, 105feq123d 6195 . . . . . . . . . . 11 (𝑦 = ⟨𝑔, 𝑣⟩ → ((𝑥(2nd𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)) ↔ (𝑥(2nd𝐸)⟨𝑔, 𝑣⟩):(𝑥(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣))))
107106ralxp 5419 . . . . . . . . . 10 (∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2nd𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)) ↔ ∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(𝑥(2nd𝐸)⟨𝑔, 𝑣⟩):(𝑥(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)))
108 oveq1 6820 . . . . . . . . . . . 12 (𝑥 = ⟨𝑓, 𝑢⟩ → (𝑥(2nd𝐸)⟨𝑔, 𝑣⟩) = (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩))
109 oveq1 6820 . . . . . . . . . . . 12 (𝑥 = ⟨𝑓, 𝑢⟩ → (𝑥(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩) = (⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩))
110 fveq2 6352 . . . . . . . . . . . . . 14 (𝑥 = ⟨𝑓, 𝑢⟩ → ((1st𝐸)‘𝑥) = ((1st𝐸)‘⟨𝑓, 𝑢⟩))
111 df-ov 6816 . . . . . . . . . . . . . 14 (𝑓(1st𝐸)𝑢) = ((1st𝐸)‘⟨𝑓, 𝑢⟩)
112110, 111syl6eqr 2812 . . . . . . . . . . . . 13 (𝑥 = ⟨𝑓, 𝑢⟩ → ((1st𝐸)‘𝑥) = (𝑓(1st𝐸)𝑢))
113112oveq1d 6828 . . . . . . . . . . . 12 (𝑥 = ⟨𝑓, 𝑢⟩ → (((1st𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)) = ((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)))
114108, 109, 113feq123d 6195 . . . . . . . . . . 11 (𝑥 = ⟨𝑓, 𝑢⟩ → ((𝑥(2nd𝐸)⟨𝑔, 𝑣⟩):(𝑥(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)) ↔ (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣))))
1151142ralbidv 3127 . . . . . . . . . 10 (𝑥 = ⟨𝑓, 𝑢⟩ → (∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(𝑥(2nd𝐸)⟨𝑔, 𝑣⟩):(𝑥(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)) ↔ ∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣))))
116107, 115syl5bb 272 . . . . . . . . 9 (𝑥 = ⟨𝑓, 𝑢⟩ → (∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2nd𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)) ↔ ∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣))))
117116ralxp 5419 . . . . . . . 8 (∀𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2nd𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)) ↔ ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)))
11899, 117sylibr 224 . . . . . . 7 (𝜑 → ∀𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2nd𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)))
119118r19.21bi 3070 . . . . . 6 ((𝜑𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) → ∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2nd𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)))
120119r19.21bi 3070 . . . . 5 (((𝜑𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) → (𝑥(2nd𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)))
121120anasss 682 . . . 4 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))) → (𝑥(2nd𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)))
12228adantr 472 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝑄 ∈ Cat)
1232adantr 472 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝐶 ∈ Cat)
124 eqid 2760 . . . . . . . . . . 11 (Id‘𝑄) = (Id‘𝑄)
125 eqid 2760 . . . . . . . . . . 11 (Id‘𝐶) = (Id‘𝐶)
126 simprl 811 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝑓 ∈ (𝐶 Func 𝐷))
127 simprr 813 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝑢 ∈ (Base‘𝐶))
12818, 122, 123, 20, 4, 124, 125, 25, 126, 127xpcid 17030 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩) = ⟨((Id‘𝑄)‘𝑓), ((Id‘𝐶)‘𝑢)⟩)
129128fveq2d 6356 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘⟨((Id‘𝑄)‘𝑓), ((Id‘𝐶)‘𝑢)⟩))
130 df-ov 6816 . . . . . . . . 9 (((Id‘𝑄)‘𝑓)(⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)((Id‘𝐶)‘𝑢)) = ((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘⟨((Id‘𝑄)‘𝑓), ((Id‘𝐶)‘𝑢)⟩)
131129, 130syl6eqr 2812 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)) = (((Id‘𝑄)‘𝑓)(⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)((Id‘𝐶)‘𝑢)))
1323adantr 472 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝐷 ∈ Cat)
133 eqid 2760 . . . . . . . . 9 (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩) = (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)
13420, 91, 124, 122, 126catidcl 16544 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝑄)‘𝑓) ∈ (𝑓(𝐶 Nat 𝐷)𝑓))
1354, 5, 125, 123, 127catidcl 16544 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝐶)‘𝑢) ∈ (𝑢(Hom ‘𝐶)𝑢))
1361, 123, 132, 4, 5, 6, 7, 126, 126, 127, 127, 133, 134, 135evlf2val 17060 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝑄)‘𝑓)(⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)((Id‘𝐶)‘𝑢)) = ((((Id‘𝑄)‘𝑓)‘𝑢)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑢)⟩(comp‘𝐷)((1st𝑓)‘𝑢))((𝑢(2nd𝑓)𝑢)‘((Id‘𝐶)‘𝑢))))
13730, 126, 32sylancr 698 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (1st𝑓)(𝐶 Func 𝐷)(2nd𝑓))
1384, 22, 137funcf1 16727 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (1st𝑓):(Base‘𝐶)⟶(Base‘𝐷))
139138, 127ffvelrnd 6523 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((1st𝑓)‘𝑢) ∈ (Base‘𝐷))
14022, 24, 26, 132, 139catidcl 16544 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝐷)‘((1st𝑓)‘𝑢)) ∈ (((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑓)‘𝑢)))
14122, 24, 26, 132, 139, 6, 139, 140catlid 16545 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝐷)‘((1st𝑓)‘𝑢))(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑢)⟩(comp‘𝐷)((1st𝑓)‘𝑢))((Id‘𝐷)‘((1st𝑓)‘𝑢))) = ((Id‘𝐷)‘((1st𝑓)‘𝑢)))
14219, 124, 26, 126fucid 16832 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝑄)‘𝑓) = ((Id‘𝐷) ∘ (1st𝑓)))
143142fveq1d 6354 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝑄)‘𝑓)‘𝑢) = (((Id‘𝐷) ∘ (1st𝑓))‘𝑢))
144 fvco3 6437 . . . . . . . . . . . 12 (((1st𝑓):(Base‘𝐶)⟶(Base‘𝐷) ∧ 𝑢 ∈ (Base‘𝐶)) → (((Id‘𝐷) ∘ (1st𝑓))‘𝑢) = ((Id‘𝐷)‘((1st𝑓)‘𝑢)))
145138, 127, 144syl2anc 696 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝐷) ∘ (1st𝑓))‘𝑢) = ((Id‘𝐷)‘((1st𝑓)‘𝑢)))
146143, 145eqtrd 2794 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝑄)‘𝑓)‘𝑢) = ((Id‘𝐷)‘((1st𝑓)‘𝑢)))
1474, 125, 26, 137, 127funcid 16731 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((𝑢(2nd𝑓)𝑢)‘((Id‘𝐶)‘𝑢)) = ((Id‘𝐷)‘((1st𝑓)‘𝑢)))
148146, 147oveq12d 6831 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((((Id‘𝑄)‘𝑓)‘𝑢)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑢)⟩(comp‘𝐷)((1st𝑓)‘𝑢))((𝑢(2nd𝑓)𝑢)‘((Id‘𝐶)‘𝑢))) = (((Id‘𝐷)‘((1st𝑓)‘𝑢))(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑢)⟩(comp‘𝐷)((1st𝑓)‘𝑢))((Id‘𝐷)‘((1st𝑓)‘𝑢))))
1491, 123, 132, 4, 126, 127evlf1 17061 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (𝑓(1st𝐸)𝑢) = ((1st𝑓)‘𝑢))
150149fveq2d 6356 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝐷)‘(𝑓(1st𝐸)𝑢)) = ((Id‘𝐷)‘((1st𝑓)‘𝑢)))
151141, 148, 1503eqtr4d 2804 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((((Id‘𝑄)‘𝑓)‘𝑢)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑢)⟩(comp‘𝐷)((1st𝑓)‘𝑢))((𝑢(2nd𝑓)𝑢)‘((Id‘𝐶)‘𝑢))) = ((Id‘𝐷)‘(𝑓(1st𝐸)𝑢)))
152131, 136, 1513eqtrd 2798 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1st𝐸)𝑢)))
153152ralrimivva 3109 . . . . . 6 (𝜑 → ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1st𝐸)𝑢)))
154 id 22 . . . . . . . . . 10 (𝑥 = ⟨𝑓, 𝑢⟩ → 𝑥 = ⟨𝑓, 𝑢⟩)
155154, 154oveq12d 6831 . . . . . . . . 9 (𝑥 = ⟨𝑓, 𝑢⟩ → (𝑥(2nd𝐸)𝑥) = (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩))
156 fveq2 6352 . . . . . . . . 9 (𝑥 = ⟨𝑓, 𝑢⟩ → ((Id‘(𝑄 ×c 𝐶))‘𝑥) = ((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩))
157155, 156fveq12d 6358 . . . . . . . 8 (𝑥 = ⟨𝑓, 𝑢⟩ → ((𝑥(2nd𝐸)𝑥)‘((Id‘(𝑄 ×c 𝐶))‘𝑥)) = ((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)))
158112fveq2d 6356 . . . . . . . 8 (𝑥 = ⟨𝑓, 𝑢⟩ → ((Id‘𝐷)‘((1st𝐸)‘𝑥)) = ((Id‘𝐷)‘(𝑓(1st𝐸)𝑢)))
159157, 158eqeq12d 2775 . . . . . . 7 (𝑥 = ⟨𝑓, 𝑢⟩ → (((𝑥(2nd𝐸)𝑥)‘((Id‘(𝑄 ×c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1st𝐸)‘𝑥)) ↔ ((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1st𝐸)𝑢))))
160159ralxp 5419 . . . . . 6 (∀𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))((𝑥(2nd𝐸)𝑥)‘((Id‘(𝑄 ×c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1st𝐸)‘𝑥)) ↔ ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1st𝐸)𝑢)))
161153, 160sylibr 224 . . . . 5 (𝜑 → ∀𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))((𝑥(2nd𝐸)𝑥)‘((Id‘(𝑄 ×c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1st𝐸)‘𝑥)))
162161r19.21bi 3070 . . . 4 ((𝜑𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) → ((𝑥(2nd𝐸)𝑥)‘((Id‘(𝑄 ×c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1st𝐸)‘𝑥)))
16323ad2ant1 1128 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝐶 ∈ Cat)
16433ad2ant1 1128 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝐷 ∈ Cat)
165 simp21 1249 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
166 1st2nd2 7372 . . . . . . . . 9 (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
167165, 166syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
168167, 165eqeltrrd 2840 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ⟨(1st𝑥), (2nd𝑥)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
169 opelxp 5303 . . . . . . 7 (⟨(1st𝑥), (2nd𝑥)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↔ ((1st𝑥) ∈ (𝐶 Func 𝐷) ∧ (2nd𝑥) ∈ (Base‘𝐶)))
170168, 169sylib 208 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st𝑥) ∈ (𝐶 Func 𝐷) ∧ (2nd𝑥) ∈ (Base‘𝐶)))
171 simp22 1250 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
172 1st2nd2 7372 . . . . . . . . 9 (𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
173171, 172syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
174173, 171eqeltrrd 2840 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ⟨(1st𝑦), (2nd𝑦)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
175 opelxp 5303 . . . . . . 7 (⟨(1st𝑦), (2nd𝑦)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↔ ((1st𝑦) ∈ (𝐶 Func 𝐷) ∧ (2nd𝑦) ∈ (Base‘𝐶)))
176174, 175sylib 208 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st𝑦) ∈ (𝐶 Func 𝐷) ∧ (2nd𝑦) ∈ (Base‘𝐶)))
177 simp23 1251 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
178 1st2nd2 7372 . . . . . . . . 9 (𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
179177, 178syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
180179, 177eqeltrrd 2840 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ⟨(1st𝑧), (2nd𝑧)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
181 opelxp 5303 . . . . . . 7 (⟨(1st𝑧), (2nd𝑧)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↔ ((1st𝑧) ∈ (𝐶 Func 𝐷) ∧ (2nd𝑧) ∈ (Base‘𝐶)))
182180, 181sylib 208 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st𝑧) ∈ (𝐶 Func 𝐷) ∧ (2nd𝑧) ∈ (Base‘𝐶)))
183 simp3l 1244 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦))
18418, 21, 91, 5, 23, 165, 171xpchom 17021 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) = (((1st𝑥)(𝐶 Nat 𝐷)(1st𝑦)) × ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦))))
185183, 184eleqtrd 2841 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑓 ∈ (((1st𝑥)(𝐶 Nat 𝐷)(1st𝑦)) × ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦))))
186 1st2nd2 7372 . . . . . . . . 9 (𝑓 ∈ (((1st𝑥)(𝐶 Nat 𝐷)(1st𝑦)) × ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦))) → 𝑓 = ⟨(1st𝑓), (2nd𝑓)⟩)
187185, 186syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑓 = ⟨(1st𝑓), (2nd𝑓)⟩)
188187, 185eqeltrrd 2840 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ⟨(1st𝑓), (2nd𝑓)⟩ ∈ (((1st𝑥)(𝐶 Nat 𝐷)(1st𝑦)) × ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦))))
189 opelxp 5303 . . . . . . 7 (⟨(1st𝑓), (2nd𝑓)⟩ ∈ (((1st𝑥)(𝐶 Nat 𝐷)(1st𝑦)) × ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦))) ↔ ((1st𝑓) ∈ ((1st𝑥)(𝐶 Nat 𝐷)(1st𝑦)) ∧ (2nd𝑓) ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦))))
190188, 189sylib 208 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st𝑓) ∈ ((1st𝑥)(𝐶 Nat 𝐷)(1st𝑦)) ∧ (2nd𝑓) ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦))))
191 simp3r 1245 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))
19218, 21, 91, 5, 23, 171, 177xpchom 17021 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧) = (((1st𝑦)(𝐶 Nat 𝐷)(1st𝑧)) × ((2nd𝑦)(Hom ‘𝐶)(2nd𝑧))))
193191, 192eleqtrd 2841 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑔 ∈ (((1st𝑦)(𝐶 Nat 𝐷)(1st𝑧)) × ((2nd𝑦)(Hom ‘𝐶)(2nd𝑧))))
194 1st2nd2 7372 . . . . . . . . 9 (𝑔 ∈ (((1st𝑦)(𝐶 Nat 𝐷)(1st𝑧)) × ((2nd𝑦)(Hom ‘𝐶)(2nd𝑧))) → 𝑔 = ⟨(1st𝑔), (2nd𝑔)⟩)
195193, 194syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑔 = ⟨(1st𝑔), (2nd𝑔)⟩)
196195, 193eqeltrrd 2840 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ⟨(1st𝑔), (2nd𝑔)⟩ ∈ (((1st𝑦)(𝐶 Nat 𝐷)(1st𝑧)) × ((2nd𝑦)(Hom ‘𝐶)(2nd𝑧))))
197 opelxp 5303 . . . . . . 7 (⟨(1st𝑔), (2nd𝑔)⟩ ∈ (((1st𝑦)(𝐶 Nat 𝐷)(1st𝑧)) × ((2nd𝑦)(Hom ‘𝐶)(2nd𝑧))) ↔ ((1st𝑔) ∈ ((1st𝑦)(𝐶 Nat 𝐷)(1st𝑧)) ∧ (2nd𝑔) ∈ ((2nd𝑦)(Hom ‘𝐶)(2nd𝑧))))
198196, 197sylib 208 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st𝑔) ∈ ((1st𝑦)(𝐶 Nat 𝐷)(1st𝑧)) ∧ (2nd𝑔) ∈ ((2nd𝑦)(Hom ‘𝐶)(2nd𝑧))))
1991, 19, 163, 164, 7, 170, 176, 182, 190, 198evlfcllem 17062 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((⟨(1st𝑥), (2nd𝑥)⟩(2nd𝐸)⟨(1st𝑧), (2nd𝑧)⟩)‘(⟨(1st𝑔), (2nd𝑔)⟩(⟨⟨(1st𝑥), (2nd𝑥)⟩, ⟨(1st𝑦), (2nd𝑦)⟩⟩(comp‘(𝑄 ×c 𝐶))⟨(1st𝑧), (2nd𝑧)⟩)⟨(1st𝑓), (2nd𝑓)⟩)) = (((⟨(1st𝑦), (2nd𝑦)⟩(2nd𝐸)⟨(1st𝑧), (2nd𝑧)⟩)‘⟨(1st𝑔), (2nd𝑔)⟩)(⟨((1st𝐸)‘⟨(1st𝑥), (2nd𝑥)⟩), ((1st𝐸)‘⟨(1st𝑦), (2nd𝑦)⟩)⟩(comp‘𝐷)((1st𝐸)‘⟨(1st𝑧), (2nd𝑧)⟩))((⟨(1st𝑥), (2nd𝑥)⟩(2nd𝐸)⟨(1st𝑦), (2nd𝑦)⟩)‘⟨(1st𝑓), (2nd𝑓)⟩)))
200167, 179oveq12d 6831 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (𝑥(2nd𝐸)𝑧) = (⟨(1st𝑥), (2nd𝑥)⟩(2nd𝐸)⟨(1st𝑧), (2nd𝑧)⟩))
201167, 173opeq12d 4561 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ⟨𝑥, 𝑦⟩ = ⟨⟨(1st𝑥), (2nd𝑥)⟩, ⟨(1st𝑦), (2nd𝑦)⟩⟩)
202201, 179oveq12d 6831 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (⟨𝑥, 𝑦⟩(comp‘(𝑄 ×c 𝐶))𝑧) = (⟨⟨(1st𝑥), (2nd𝑥)⟩, ⟨(1st𝑦), (2nd𝑦)⟩⟩(comp‘(𝑄 ×c 𝐶))⟨(1st𝑧), (2nd𝑧)⟩))
203202, 195, 187oveq123d 6834 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘(𝑄 ×c 𝐶))𝑧)𝑓) = (⟨(1st𝑔), (2nd𝑔)⟩(⟨⟨(1st𝑥), (2nd𝑥)⟩, ⟨(1st𝑦), (2nd𝑦)⟩⟩(comp‘(𝑄 ×c 𝐶))⟨(1st𝑧), (2nd𝑧)⟩)⟨(1st𝑓), (2nd𝑓)⟩))
204200, 203fveq12d 6358 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((𝑥(2nd𝐸)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘(𝑄 ×c 𝐶))𝑧)𝑓)) = ((⟨(1st𝑥), (2nd𝑥)⟩(2nd𝐸)⟨(1st𝑧), (2nd𝑧)⟩)‘(⟨(1st𝑔), (2nd𝑔)⟩(⟨⟨(1st𝑥), (2nd𝑥)⟩, ⟨(1st𝑦), (2nd𝑦)⟩⟩(comp‘(𝑄 ×c 𝐶))⟨(1st𝑧), (2nd𝑧)⟩)⟨(1st𝑓), (2nd𝑓)⟩)))
205167fveq2d 6356 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st𝐸)‘𝑥) = ((1st𝐸)‘⟨(1st𝑥), (2nd𝑥)⟩))
206173fveq2d 6356 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st𝐸)‘𝑦) = ((1st𝐸)‘⟨(1st𝑦), (2nd𝑦)⟩))
207205, 206opeq12d 4561 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ⟨((1st𝐸)‘𝑥), ((1st𝐸)‘𝑦)⟩ = ⟨((1st𝐸)‘⟨(1st𝑥), (2nd𝑥)⟩), ((1st𝐸)‘⟨(1st𝑦), (2nd𝑦)⟩)⟩)
208179fveq2d 6356 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st𝐸)‘𝑧) = ((1st𝐸)‘⟨(1st𝑧), (2nd𝑧)⟩))
209207, 208oveq12d 6831 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (⟨((1st𝐸)‘𝑥), ((1st𝐸)‘𝑦)⟩(comp‘𝐷)((1st𝐸)‘𝑧)) = (⟨((1st𝐸)‘⟨(1st𝑥), (2nd𝑥)⟩), ((1st𝐸)‘⟨(1st𝑦), (2nd𝑦)⟩)⟩(comp‘𝐷)((1st𝐸)‘⟨(1st𝑧), (2nd𝑧)⟩)))
210173, 179oveq12d 6831 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (𝑦(2nd𝐸)𝑧) = (⟨(1st𝑦), (2nd𝑦)⟩(2nd𝐸)⟨(1st𝑧), (2nd𝑧)⟩))
211210, 195fveq12d 6358 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((𝑦(2nd𝐸)𝑧)‘𝑔) = ((⟨(1st𝑦), (2nd𝑦)⟩(2nd𝐸)⟨(1st𝑧), (2nd𝑧)⟩)‘⟨(1st𝑔), (2nd𝑔)⟩))
212167, 173oveq12d 6831 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (𝑥(2nd𝐸)𝑦) = (⟨(1st𝑥), (2nd𝑥)⟩(2nd𝐸)⟨(1st𝑦), (2nd𝑦)⟩))
213212, 187fveq12d 6358 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((𝑥(2nd𝐸)𝑦)‘𝑓) = ((⟨(1st𝑥), (2nd𝑥)⟩(2nd𝐸)⟨(1st𝑦), (2nd𝑦)⟩)‘⟨(1st𝑓), (2nd𝑓)⟩))
214209, 211, 213oveq123d 6834 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (((𝑦(2nd𝐸)𝑧)‘𝑔)(⟨((1st𝐸)‘𝑥), ((1st𝐸)‘𝑦)⟩(comp‘𝐷)((1st𝐸)‘𝑧))((𝑥(2nd𝐸)𝑦)‘𝑓)) = (((⟨(1st𝑦), (2nd𝑦)⟩(2nd𝐸)⟨(1st𝑧), (2nd𝑧)⟩)‘⟨(1st𝑔), (2nd𝑔)⟩)(⟨((1st𝐸)‘⟨(1st𝑥), (2nd𝑥)⟩), ((1st𝐸)‘⟨(1st𝑦), (2nd𝑦)⟩)⟩(comp‘𝐷)((1st𝐸)‘⟨(1st𝑧), (2nd𝑧)⟩))((⟨(1st𝑥), (2nd𝑥)⟩(2nd𝐸)⟨(1st𝑦), (2nd𝑦)⟩)‘⟨(1st𝑓), (2nd𝑓)⟩)))
215199, 204, 2143eqtr4d 2804 . . . 4 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((𝑥(2nd𝐸)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘(𝑄 ×c 𝐶))𝑧)𝑓)) = (((𝑦(2nd𝐸)𝑧)‘𝑔)(⟨((1st𝐸)‘𝑥), ((1st𝐸)‘𝑦)⟩(comp‘𝐷)((1st𝐸)‘𝑧))((𝑥(2nd𝐸)𝑦)‘𝑓)))
21621, 22, 23, 24, 25, 26, 27, 6, 29, 3, 44, 55, 121, 162, 215isfuncd 16726 . . 3 (𝜑 → (1st𝐸)((𝑄 ×c 𝐶) Func 𝐷)(2nd𝐸))
217 df-br 4805 . . 3 ((1st𝐸)((𝑄 ×c 𝐶) Func 𝐷)(2nd𝐸) ↔ ⟨(1st𝐸), (2nd𝐸)⟩ ∈ ((𝑄 ×c 𝐶) Func 𝐷))
218216, 217sylib 208 . 2 (𝜑 → ⟨(1st𝐸), (2nd𝐸)⟩ ∈ ((𝑄 ×c 𝐶) Func 𝐷))
21917, 218eqeltrd 2839 1 (𝜑𝐸 ∈ ((𝑄 ×c 𝐶) Func 𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072   = wceq 1632   ∈ wcel 2139  ∀wral 3050  Vcvv 3340  ⦋csb 3674  ⟨cop 4327   class class class wbr 4804   × cxp 5264   ∘ ccom 5270  Rel wrel 5271   Fn wfn 6044  ⟶wf 6045  ‘cfv 6049  (class class class)co 6813   ↦ cmpt2 6815  1st c1st 7331  2nd c2nd 7332  Basecbs 16059  Hom chom 16154  compcco 16155  Catccat 16526  Idccid 16527   Func cfunc 16715   Nat cnat 16802   FuncCat cfuc 16803   ×c cxpc 17009   evalF cevlf 17050 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-fal 1638  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-1st 7333  df-2nd 7334  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-oadd 7733  df-er 7911  df-map 8025  df-ixp 8075  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-nn 11213  df-2 11271  df-3 11272  df-4 11273  df-5 11274  df-6 11275  df-7 11276  df-8 11277  df-9 11278  df-n0 11485  df-z 11570  df-dec 11686  df-uz 11880  df-fz 12520  df-struct 16061  df-ndx 16062  df-slot 16063  df-base 16065  df-hom 16168  df-cco 16169  df-cat 16530  df-cid 16531  df-func 16719  df-nat 16804  df-fuc 16805  df-xpc 17013  df-evlf 17054 This theorem is referenced by:  uncfcl  17076  uncf1  17077  uncf2  17078  yonedalem1  17113
 Copyright terms: Public domain W3C validator