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

Theorem evlfcl 17730
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 2737 . . . . 5 (Base‘𝐶) = (Base‘𝐶)
5 eqid 2737 . . . . 5 (Hom ‘𝐶) = (Hom ‘𝐶)
6 eqid 2737 . . . . 5 (comp‘𝐷) = (comp‘𝐷)
7 eqid 2737 . . . . 5 (𝐶 Nat 𝐷) = (𝐶 Nat 𝐷)
81, 2, 3, 4, 5, 6, 7evlfval 17725 . . . 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 7246 . . . . . 6 (𝐶 Func 𝐷) ∈ V
10 fvex 6730 . . . . . 6 (Base‘𝐶) ∈ V
119, 10mpoex 7850 . . . . 5 (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st𝑓)‘𝑥)) ∈ V
129, 10xpex 7538 . . . . . 6 ((𝐶 Func 𝐷) × (Base‘𝐶)) ∈ V
1312, 12mpoex 7850 . . . . 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 5590 . . . 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, 14eqeltrdi 2846 . . 3 (𝜑𝐸 ∈ (V × V))
16 1st2nd2 7800 . . 3 (𝐸 ∈ (V × V) → 𝐸 = ⟨(1st𝐸), (2nd𝐸)⟩)
1715, 16syl 17 . 2 (𝜑𝐸 = ⟨(1st𝐸), (2nd𝐸)⟩)
18 eqid 2737 . . . . 5 (𝑄 ×c 𝐶) = (𝑄 ×c 𝐶)
19 evlfcl.q . . . . . 6 𝑄 = (𝐶 FuncCat 𝐷)
2019fucbas 17468 . . . . 5 (𝐶 Func 𝐷) = (Base‘𝑄)
2118, 20, 4xpcbas 17685 . . . 4 ((𝐶 Func 𝐷) × (Base‘𝐶)) = (Base‘(𝑄 ×c 𝐶))
22 eqid 2737 . . . 4 (Base‘𝐷) = (Base‘𝐷)
23 eqid 2737 . . . 4 (Hom ‘(𝑄 ×c 𝐶)) = (Hom ‘(𝑄 ×c 𝐶))
24 eqid 2737 . . . 4 (Hom ‘𝐷) = (Hom ‘𝐷)
25 eqid 2737 . . . 4 (Id‘(𝑄 ×c 𝐶)) = (Id‘(𝑄 ×c 𝐶))
26 eqid 2737 . . . 4 (Id‘𝐷) = (Id‘𝐷)
27 eqid 2737 . . . 4 (comp‘(𝑄 ×c 𝐶)) = (comp‘(𝑄 ×c 𝐶))
2819, 2, 3fuccat 17479 . . . . 5 (𝜑𝑄 ∈ Cat)
2918, 28, 2xpccat 17697 . . . 4 (𝜑 → (𝑄 ×c 𝐶) ∈ Cat)
30 relfunc 17368 . . . . . . . . . . 11 Rel (𝐶 Func 𝐷)
31 simpr 488 . . . . . . . . . . 11 ((𝜑𝑓 ∈ (𝐶 Func 𝐷)) → 𝑓 ∈ (𝐶 Func 𝐷))
32 1st2ndbr 7813 . . . . . . . . . . 11 ((Rel (𝐶 Func 𝐷) ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → (1st𝑓)(𝐶 Func 𝐷)(2nd𝑓))
3330, 31, 32sylancr 590 . . . . . . . . . 10 ((𝜑𝑓 ∈ (𝐶 Func 𝐷)) → (1st𝑓)(𝐶 Func 𝐷)(2nd𝑓))
344, 22, 33funcf1 17372 . . . . . . . . 9 ((𝜑𝑓 ∈ (𝐶 Func 𝐷)) → (1st𝑓):(Base‘𝐶)⟶(Base‘𝐷))
3534ffvelrnda 6904 . . . . . . . 8 (((𝜑𝑓 ∈ (𝐶 Func 𝐷)) ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st𝑓)‘𝑥) ∈ (Base‘𝐷))
3635ralrimiva 3105 . . . . . . 7 ((𝜑𝑓 ∈ (𝐶 Func 𝐷)) → ∀𝑥 ∈ (Base‘𝐶)((1st𝑓)‘𝑥) ∈ (Base‘𝐷))
3736ralrimiva 3105 . . . . . 6 (𝜑 → ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑥 ∈ (Base‘𝐶)((1st𝑓)‘𝑥) ∈ (Base‘𝐷))
38 eqid 2737 . . . . . . 7 (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st𝑓)‘𝑥)) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st𝑓)‘𝑥))
3938fmpo 7838 . . . . . 6 (∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑥 ∈ (Base‘𝐶)((1st𝑓)‘𝑥) ∈ (Base‘𝐷) ↔ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st𝑓)‘𝑥)):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷))
4037, 39sylib 221 . . . . 5 (𝜑 → (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st𝑓)‘𝑥)):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷))
4111, 13op1std 7771 . . . . . . 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 6530 . . . . 5 (𝜑 → ((1st𝐸):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷) ↔ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st𝑓)‘𝑥)):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷)))
4440, 43mpbird 260 . . . 4 (𝜑 → (1st𝐸):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷))
45 eqid 2737 . . . . . 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 7246 . . . . . . . . 9 (𝑚(𝐶 Nat 𝐷)𝑛) ∈ V
47 ovex 7246 . . . . . . . . 9 ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ∈ V
4846, 47mpoex 7850 . . . . . . . 8 (𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ↦ ((𝑎‘(2nd𝑦))(⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩(comp‘𝐷)((1st𝑛)‘(2nd𝑦)))(((2nd𝑥)(2nd𝑚)(2nd𝑦))‘𝑔))) ∈ V
4948csbex 5204 . . . . . . 7 (1st𝑦) / 𝑛(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ↦ ((𝑎‘(2nd𝑦))(⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩(comp‘𝐷)((1st𝑛)‘(2nd𝑦)))(((2nd𝑥)(2nd𝑚)(2nd𝑦))‘𝑔))) ∈ V
5049csbex 5204 . . . . . 6 (1st𝑥) / 𝑚(1st𝑦) / 𝑛(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ↦ ((𝑎‘(2nd𝑦))(⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩(comp‘𝐷)((1st𝑛)‘(2nd𝑦)))(((2nd𝑥)(2nd𝑚)(2nd𝑦))‘𝑔))) ∈ V
5145, 50fnmpoi 7840 . . . . 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 7772 . . . . . . 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 6472 . . . . 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 261 . . . 4 (𝜑 → (2nd𝐸) Fn (((𝐶 Func 𝐷) × (Base‘𝐶)) × ((𝐶 Func 𝐷) × (Base‘𝐶))))
563ad2antrr 726 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝐷 ∈ Cat)
5756adantr 484 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝐷 ∈ Cat)
58 simplrl 777 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑓 ∈ (𝐶 Func 𝐷))
5930, 58, 32sylancr 590 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1st𝑓)(𝐶 Func 𝐷)(2nd𝑓))
604, 22, 59funcf1 17372 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1st𝑓):(Base‘𝐶)⟶(Base‘𝐷))
6160adantr 484 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (1st𝑓):(Base‘𝐶)⟶(Base‘𝐷))
62 simplrr 778 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑢 ∈ (Base‘𝐶))
6362adantr 484 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑢 ∈ (Base‘𝐶))
6461, 63ffvelrnd 6905 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((1st𝑓)‘𝑢) ∈ (Base‘𝐷))
65 simplrr 778 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑣 ∈ (Base‘𝐶))
6661, 65ffvelrnd 6905 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((1st𝑓)‘𝑣) ∈ (Base‘𝐷))
67 simprl 771 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑔 ∈ (𝐶 Func 𝐷))
68 1st2ndbr 7813 . . . . . . . . . . . . . . . . . . 19 ((Rel (𝐶 Func 𝐷) ∧ 𝑔 ∈ (𝐶 Func 𝐷)) → (1st𝑔)(𝐶 Func 𝐷)(2nd𝑔))
6930, 67, 68sylancr 590 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1st𝑔)(𝐶 Func 𝐷)(2nd𝑔))
704, 22, 69funcf1 17372 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1st𝑔):(Base‘𝐶)⟶(Base‘𝐷))
7170adantr 484 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (1st𝑔):(Base‘𝐶)⟶(Base‘𝐷))
7271, 65ffvelrnd 6905 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((1st𝑔)‘𝑣) ∈ (Base‘𝐷))
73 simprr 773 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑣 ∈ (Base‘𝐶))
744, 5, 24, 59, 62, 73funcf2 17374 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑢(2nd𝑓)𝑣):(𝑢(Hom ‘𝐶)𝑣)⟶(((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑓)‘𝑣)))
7574adantr 484 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (𝑢(2nd𝑓)𝑣):(𝑢(Hom ‘𝐶)𝑣)⟶(((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑓)‘𝑣)))
76 simprr 773 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ∈ (𝑢(Hom ‘𝐶)𝑣))
7775, 76ffvelrnd 6905 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((𝑢(2nd𝑓)𝑣)‘) ∈ (((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑓)‘𝑣)))
78 simprl 771 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔))
797, 78nat1st2nd 17458 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑎 ∈ (⟨(1st𝑓), (2nd𝑓)⟩(𝐶 Nat 𝐷)⟨(1st𝑔), (2nd𝑔)⟩))
807, 79, 4, 24, 65natcl 17460 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (𝑎𝑣) ∈ (((1st𝑓)‘𝑣)(Hom ‘𝐷)((1st𝑔)‘𝑣)))
8122, 24, 6, 57, 64, 66, 72, 77, 80catcocl 17188 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((𝑎𝑣)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑣)⟩(comp‘𝐷)((1st𝑔)‘𝑣))((𝑢(2nd𝑓)𝑣)‘)) ∈ (((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑔)‘𝑣)))
8281ralrimivva 3112 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → ∀𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔)∀ ∈ (𝑢(Hom ‘𝐶)𝑣)((𝑎𝑣)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑣)⟩(comp‘𝐷)((1st𝑔)‘𝑣))((𝑢(2nd𝑓)𝑣)‘)) ∈ (((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑔)‘𝑣)))
83 eqid 2737 . . . . . . . . . . . . . 14 (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎𝑣)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑣)⟩(comp‘𝐷)((1st𝑔)‘𝑣))((𝑢(2nd𝑓)𝑣)‘))) = (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎𝑣)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑣)⟩(comp‘𝐷)((1st𝑔)‘𝑣))((𝑢(2nd𝑓)𝑣)‘)))
8483fmpo 7838 . . . . . . . . . . . . 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 221 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎𝑣)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑣)⟩(comp‘𝐷)((1st𝑔)‘𝑣))((𝑢(2nd𝑓)𝑣)‘))):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑔)‘𝑣)))
862ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝐶 ∈ Cat)
87 eqid 2737 . . . . . . . . . . . . . 14 (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩) = (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩)
881, 86, 56, 4, 5, 6, 7, 58, 67, 62, 73, 87evlf2 17726 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩) = (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎𝑣)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑣)⟩(comp‘𝐷)((1st𝑔)‘𝑣))((𝑢(2nd𝑓)𝑣)‘))))
8988feq1d 6530 . . . . . . . . . . . 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 260 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑔)‘𝑣)))
9119, 7fuchom 17469 . . . . . . . . . . . . 13 (𝐶 Nat 𝐷) = (Hom ‘𝑄)
9218, 20, 4, 91, 5, 58, 62, 67, 73, 23xpchom2 17693 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩) = ((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣)))
931, 86, 56, 4, 58, 62evlf1 17728 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑓(1st𝐸)𝑢) = ((1st𝑓)‘𝑢))
941, 86, 56, 4, 67, 73evlf1 17728 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑔(1st𝐸)𝑣) = ((1st𝑔)‘𝑣))
9593, 94oveq12d 7231 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → ((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)) = (((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑔)‘𝑣)))
9692, 95feq23d 6540 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)) ↔ (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑔)‘𝑣))))
9790, 96mpbird 260 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)))
9897ralrimivva 3112 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)))
9998ralrimivva 3112 . . . . . . . 8 (𝜑 → ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)))
100 oveq2 7221 . . . . . . . . . . . 12 (𝑦 = ⟨𝑔, 𝑣⟩ → (𝑥(2nd𝐸)𝑦) = (𝑥(2nd𝐸)⟨𝑔, 𝑣⟩))
101 oveq2 7221 . . . . . . . . . . . 12 (𝑦 = ⟨𝑔, 𝑣⟩ → (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) = (𝑥(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩))
102 fveq2 6717 . . . . . . . . . . . . . 14 (𝑦 = ⟨𝑔, 𝑣⟩ → ((1st𝐸)‘𝑦) = ((1st𝐸)‘⟨𝑔, 𝑣⟩))
103 df-ov 7216 . . . . . . . . . . . . . 14 (𝑔(1st𝐸)𝑣) = ((1st𝐸)‘⟨𝑔, 𝑣⟩)
104102, 103eqtr4di 2796 . . . . . . . . . . . . 13 (𝑦 = ⟨𝑔, 𝑣⟩ → ((1st𝐸)‘𝑦) = (𝑔(1st𝐸)𝑣))
105104oveq2d 7229 . . . . . . . . . . . 12 (𝑦 = ⟨𝑔, 𝑣⟩ → (((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)) = (((1st𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)))
106100, 101, 105feq123d 6534 . . . . . . . . . . 11 (𝑦 = ⟨𝑔, 𝑣⟩ → ((𝑥(2nd𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)) ↔ (𝑥(2nd𝐸)⟨𝑔, 𝑣⟩):(𝑥(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣))))
107106ralxp 5710 . . . . . . . . . 10 (∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2nd𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)) ↔ ∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(𝑥(2nd𝐸)⟨𝑔, 𝑣⟩):(𝑥(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)))
108 oveq1 7220 . . . . . . . . . . . 12 (𝑥 = ⟨𝑓, 𝑢⟩ → (𝑥(2nd𝐸)⟨𝑔, 𝑣⟩) = (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩))
109 oveq1 7220 . . . . . . . . . . . 12 (𝑥 = ⟨𝑓, 𝑢⟩ → (𝑥(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩) = (⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩))
110 fveq2 6717 . . . . . . . . . . . . . 14 (𝑥 = ⟨𝑓, 𝑢⟩ → ((1st𝐸)‘𝑥) = ((1st𝐸)‘⟨𝑓, 𝑢⟩))
111 df-ov 7216 . . . . . . . . . . . . . 14 (𝑓(1st𝐸)𝑢) = ((1st𝐸)‘⟨𝑓, 𝑢⟩)
112110, 111eqtr4di 2796 . . . . . . . . . . . . 13 (𝑥 = ⟨𝑓, 𝑢⟩ → ((1st𝐸)‘𝑥) = (𝑓(1st𝐸)𝑢))
113112oveq1d 7228 . . . . . . . . . . . 12 (𝑥 = ⟨𝑓, 𝑢⟩ → (((1st𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)) = ((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)))
114108, 109, 113feq123d 6534 . . . . . . . . . . 11 (𝑥 = ⟨𝑓, 𝑢⟩ → ((𝑥(2nd𝐸)⟨𝑔, 𝑣⟩):(𝑥(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)) ↔ (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣))))
1151142ralbidv 3120 . . . . . . . . . 10 (𝑥 = ⟨𝑓, 𝑢⟩ → (∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(𝑥(2nd𝐸)⟨𝑔, 𝑣⟩):(𝑥(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)) ↔ ∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣))))
116107, 115syl5bb 286 . . . . . . . . 9 (𝑥 = ⟨𝑓, 𝑢⟩ → (∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2nd𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)) ↔ ∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣))))
117116ralxp 5710 . . . . . . . 8 (∀𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2nd𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)) ↔ ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)))
11899, 117sylibr 237 . . . . . . 7 (𝜑 → ∀𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2nd𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)))
119118r19.21bi 3130 . . . . . 6 ((𝜑𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) → ∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2nd𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)))
120119r19.21bi 3130 . . . . 5 (((𝜑𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) → (𝑥(2nd𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)))
121120anasss 470 . . . 4 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))) → (𝑥(2nd𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)))
12228adantr 484 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝑄 ∈ Cat)
1232adantr 484 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝐶 ∈ Cat)
124 eqid 2737 . . . . . . . . . . 11 (Id‘𝑄) = (Id‘𝑄)
125 eqid 2737 . . . . . . . . . . 11 (Id‘𝐶) = (Id‘𝐶)
126 simprl 771 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝑓 ∈ (𝐶 Func 𝐷))
127 simprr 773 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝑢 ∈ (Base‘𝐶))
12818, 122, 123, 20, 4, 124, 125, 25, 126, 127xpcid 17696 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩) = ⟨((Id‘𝑄)‘𝑓), ((Id‘𝐶)‘𝑢)⟩)
129128fveq2d 6721 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘⟨((Id‘𝑄)‘𝑓), ((Id‘𝐶)‘𝑢)⟩))
130 df-ov 7216 . . . . . . . . 9 (((Id‘𝑄)‘𝑓)(⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)((Id‘𝐶)‘𝑢)) = ((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘⟨((Id‘𝑄)‘𝑓), ((Id‘𝐶)‘𝑢)⟩)
131129, 130eqtr4di 2796 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)) = (((Id‘𝑄)‘𝑓)(⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)((Id‘𝐶)‘𝑢)))
1323adantr 484 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝐷 ∈ Cat)
133 eqid 2737 . . . . . . . . 9 (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩) = (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)
13420, 91, 124, 122, 126catidcl 17185 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝑄)‘𝑓) ∈ (𝑓(𝐶 Nat 𝐷)𝑓))
1354, 5, 125, 123, 127catidcl 17185 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝐶)‘𝑢) ∈ (𝑢(Hom ‘𝐶)𝑢))
1361, 123, 132, 4, 5, 6, 7, 126, 126, 127, 127, 133, 134, 135evlf2val 17727 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝑄)‘𝑓)(⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)((Id‘𝐶)‘𝑢)) = ((((Id‘𝑄)‘𝑓)‘𝑢)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑢)⟩(comp‘𝐷)((1st𝑓)‘𝑢))((𝑢(2nd𝑓)𝑢)‘((Id‘𝐶)‘𝑢))))
13730, 126, 32sylancr 590 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (1st𝑓)(𝐶 Func 𝐷)(2nd𝑓))
1384, 22, 137funcf1 17372 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (1st𝑓):(Base‘𝐶)⟶(Base‘𝐷))
139138, 127ffvelrnd 6905 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((1st𝑓)‘𝑢) ∈ (Base‘𝐷))
14022, 24, 26, 132, 139catidcl 17185 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝐷)‘((1st𝑓)‘𝑢)) ∈ (((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑓)‘𝑢)))
14122, 24, 26, 132, 139, 6, 139, 140catlid 17186 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝐷)‘((1st𝑓)‘𝑢))(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑢)⟩(comp‘𝐷)((1st𝑓)‘𝑢))((Id‘𝐷)‘((1st𝑓)‘𝑢))) = ((Id‘𝐷)‘((1st𝑓)‘𝑢)))
14219, 124, 26, 126fucid 17480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝑄)‘𝑓) = ((Id‘𝐷) ∘ (1st𝑓)))
143142fveq1d 6719 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝑄)‘𝑓)‘𝑢) = (((Id‘𝐷) ∘ (1st𝑓))‘𝑢))
144 fvco3 6810 . . . . . . . . . . . 12 (((1st𝑓):(Base‘𝐶)⟶(Base‘𝐷) ∧ 𝑢 ∈ (Base‘𝐶)) → (((Id‘𝐷) ∘ (1st𝑓))‘𝑢) = ((Id‘𝐷)‘((1st𝑓)‘𝑢)))
145138, 127, 144syl2anc 587 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝐷) ∘ (1st𝑓))‘𝑢) = ((Id‘𝐷)‘((1st𝑓)‘𝑢)))
146143, 145eqtrd 2777 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝑄)‘𝑓)‘𝑢) = ((Id‘𝐷)‘((1st𝑓)‘𝑢)))
1474, 125, 26, 137, 127funcid 17376 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((𝑢(2nd𝑓)𝑢)‘((Id‘𝐶)‘𝑢)) = ((Id‘𝐷)‘((1st𝑓)‘𝑢)))
148146, 147oveq12d 7231 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((((Id‘𝑄)‘𝑓)‘𝑢)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑢)⟩(comp‘𝐷)((1st𝑓)‘𝑢))((𝑢(2nd𝑓)𝑢)‘((Id‘𝐶)‘𝑢))) = (((Id‘𝐷)‘((1st𝑓)‘𝑢))(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑢)⟩(comp‘𝐷)((1st𝑓)‘𝑢))((Id‘𝐷)‘((1st𝑓)‘𝑢))))
1491, 123, 132, 4, 126, 127evlf1 17728 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (𝑓(1st𝐸)𝑢) = ((1st𝑓)‘𝑢))
150149fveq2d 6721 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝐷)‘(𝑓(1st𝐸)𝑢)) = ((Id‘𝐷)‘((1st𝑓)‘𝑢)))
151141, 148, 1503eqtr4d 2787 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((((Id‘𝑄)‘𝑓)‘𝑢)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑢)⟩(comp‘𝐷)((1st𝑓)‘𝑢))((𝑢(2nd𝑓)𝑢)‘((Id‘𝐶)‘𝑢))) = ((Id‘𝐷)‘(𝑓(1st𝐸)𝑢)))
152131, 136, 1513eqtrd 2781 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1st𝐸)𝑢)))
153152ralrimivva 3112 . . . . . 6 (𝜑 → ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1st𝐸)𝑢)))
154 id 22 . . . . . . . . . 10 (𝑥 = ⟨𝑓, 𝑢⟩ → 𝑥 = ⟨𝑓, 𝑢⟩)
155154, 154oveq12d 7231 . . . . . . . . 9 (𝑥 = ⟨𝑓, 𝑢⟩ → (𝑥(2nd𝐸)𝑥) = (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩))
156 fveq2 6717 . . . . . . . . 9 (𝑥 = ⟨𝑓, 𝑢⟩ → ((Id‘(𝑄 ×c 𝐶))‘𝑥) = ((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩))
157155, 156fveq12d 6724 . . . . . . . 8 (𝑥 = ⟨𝑓, 𝑢⟩ → ((𝑥(2nd𝐸)𝑥)‘((Id‘(𝑄 ×c 𝐶))‘𝑥)) = ((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)))
158112fveq2d 6721 . . . . . . . 8 (𝑥 = ⟨𝑓, 𝑢⟩ → ((Id‘𝐷)‘((1st𝐸)‘𝑥)) = ((Id‘𝐷)‘(𝑓(1st𝐸)𝑢)))
159157, 158eqeq12d 2753 . . . . . . 7 (𝑥 = ⟨𝑓, 𝑢⟩ → (((𝑥(2nd𝐸)𝑥)‘((Id‘(𝑄 ×c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1st𝐸)‘𝑥)) ↔ ((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1st𝐸)𝑢))))
160159ralxp 5710 . . . . . 6 (∀𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))((𝑥(2nd𝐸)𝑥)‘((Id‘(𝑄 ×c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1st𝐸)‘𝑥)) ↔ ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1st𝐸)𝑢)))
161153, 160sylibr 237 . . . . 5 (𝜑 → ∀𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))((𝑥(2nd𝐸)𝑥)‘((Id‘(𝑄 ×c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1st𝐸)‘𝑥)))
162161r19.21bi 3130 . . . 4 ((𝜑𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) → ((𝑥(2nd𝐸)𝑥)‘((Id‘(𝑄 ×c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1st𝐸)‘𝑥)))
16323ad2ant1 1135 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝐶 ∈ Cat)
16433ad2ant1 1135 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝐷 ∈ Cat)
165 simp21 1208 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
166 1st2nd2 7800 . . . . . . . . 9 (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
167165, 166syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
168167, 165eqeltrrd 2839 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ⟨(1st𝑥), (2nd𝑥)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
169 opelxp 5587 . . . . . . 7 (⟨(1st𝑥), (2nd𝑥)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↔ ((1st𝑥) ∈ (𝐶 Func 𝐷) ∧ (2nd𝑥) ∈ (Base‘𝐶)))
170168, 169sylib 221 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st𝑥) ∈ (𝐶 Func 𝐷) ∧ (2nd𝑥) ∈ (Base‘𝐶)))
171 simp22 1209 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
172 1st2nd2 7800 . . . . . . . . 9 (𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
173171, 172syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
174173, 171eqeltrrd 2839 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ⟨(1st𝑦), (2nd𝑦)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
175 opelxp 5587 . . . . . . 7 (⟨(1st𝑦), (2nd𝑦)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↔ ((1st𝑦) ∈ (𝐶 Func 𝐷) ∧ (2nd𝑦) ∈ (Base‘𝐶)))
176174, 175sylib 221 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st𝑦) ∈ (𝐶 Func 𝐷) ∧ (2nd𝑦) ∈ (Base‘𝐶)))
177 simp23 1210 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
178 1st2nd2 7800 . . . . . . . . 9 (𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
179177, 178syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
180179, 177eqeltrrd 2839 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ⟨(1st𝑧), (2nd𝑧)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
181 opelxp 5587 . . . . . . 7 (⟨(1st𝑧), (2nd𝑧)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↔ ((1st𝑧) ∈ (𝐶 Func 𝐷) ∧ (2nd𝑧) ∈ (Base‘𝐶)))
182180, 181sylib 221 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st𝑧) ∈ (𝐶 Func 𝐷) ∧ (2nd𝑧) ∈ (Base‘𝐶)))
183 simp3l 1203 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦))
18418, 21, 91, 5, 23, 165, 171xpchom 17687 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) = (((1st𝑥)(𝐶 Nat 𝐷)(1st𝑦)) × ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦))))
185183, 184eleqtrd 2840 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑓 ∈ (((1st𝑥)(𝐶 Nat 𝐷)(1st𝑦)) × ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦))))
186 1st2nd2 7800 . . . . . . . . 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 2839 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ⟨(1st𝑓), (2nd𝑓)⟩ ∈ (((1st𝑥)(𝐶 Nat 𝐷)(1st𝑦)) × ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦))))
189 opelxp 5587 . . . . . . 7 (⟨(1st𝑓), (2nd𝑓)⟩ ∈ (((1st𝑥)(𝐶 Nat 𝐷)(1st𝑦)) × ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦))) ↔ ((1st𝑓) ∈ ((1st𝑥)(𝐶 Nat 𝐷)(1st𝑦)) ∧ (2nd𝑓) ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦))))
190188, 189sylib 221 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st𝑓) ∈ ((1st𝑥)(𝐶 Nat 𝐷)(1st𝑦)) ∧ (2nd𝑓) ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦))))
191 simp3r 1204 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))
19218, 21, 91, 5, 23, 171, 177xpchom 17687 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧) = (((1st𝑦)(𝐶 Nat 𝐷)(1st𝑧)) × ((2nd𝑦)(Hom ‘𝐶)(2nd𝑧))))
193191, 192eleqtrd 2840 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑔 ∈ (((1st𝑦)(𝐶 Nat 𝐷)(1st𝑧)) × ((2nd𝑦)(Hom ‘𝐶)(2nd𝑧))))
194 1st2nd2 7800 . . . . . . . . 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 2839 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ⟨(1st𝑔), (2nd𝑔)⟩ ∈ (((1st𝑦)(𝐶 Nat 𝐷)(1st𝑧)) × ((2nd𝑦)(Hom ‘𝐶)(2nd𝑧))))
197 opelxp 5587 . . . . . . 7 (⟨(1st𝑔), (2nd𝑔)⟩ ∈ (((1st𝑦)(𝐶 Nat 𝐷)(1st𝑧)) × ((2nd𝑦)(Hom ‘𝐶)(2nd𝑧))) ↔ ((1st𝑔) ∈ ((1st𝑦)(𝐶 Nat 𝐷)(1st𝑧)) ∧ (2nd𝑔) ∈ ((2nd𝑦)(Hom ‘𝐶)(2nd𝑧))))
198196, 197sylib 221 . . . . . 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 17729 . . . . 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 7231 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (𝑥(2nd𝐸)𝑧) = (⟨(1st𝑥), (2nd𝑥)⟩(2nd𝐸)⟨(1st𝑧), (2nd𝑧)⟩))
201167, 173opeq12d 4792 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ⟨𝑥, 𝑦⟩ = ⟨⟨(1st𝑥), (2nd𝑥)⟩, ⟨(1st𝑦), (2nd𝑦)⟩⟩)
202201, 179oveq12d 7231 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (⟨𝑥, 𝑦⟩(comp‘(𝑄 ×c 𝐶))𝑧) = (⟨⟨(1st𝑥), (2nd𝑥)⟩, ⟨(1st𝑦), (2nd𝑦)⟩⟩(comp‘(𝑄 ×c 𝐶))⟨(1st𝑧), (2nd𝑧)⟩))
203202, 195, 187oveq123d 7234 . . . . . 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 6724 . . . . 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 6721 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st𝐸)‘𝑥) = ((1st𝐸)‘⟨(1st𝑥), (2nd𝑥)⟩))
206173fveq2d 6721 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st𝐸)‘𝑦) = ((1st𝐸)‘⟨(1st𝑦), (2nd𝑦)⟩))
207205, 206opeq12d 4792 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ⟨((1st𝐸)‘𝑥), ((1st𝐸)‘𝑦)⟩ = ⟨((1st𝐸)‘⟨(1st𝑥), (2nd𝑥)⟩), ((1st𝐸)‘⟨(1st𝑦), (2nd𝑦)⟩)⟩)
208179fveq2d 6721 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st𝐸)‘𝑧) = ((1st𝐸)‘⟨(1st𝑧), (2nd𝑧)⟩))
209207, 208oveq12d 7231 . . . . . 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 7231 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (𝑦(2nd𝐸)𝑧) = (⟨(1st𝑦), (2nd𝑦)⟩(2nd𝐸)⟨(1st𝑧), (2nd𝑧)⟩))
211210, 195fveq12d 6724 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((𝑦(2nd𝐸)𝑧)‘𝑔) = ((⟨(1st𝑦), (2nd𝑦)⟩(2nd𝐸)⟨(1st𝑧), (2nd𝑧)⟩)‘⟨(1st𝑔), (2nd𝑔)⟩))
212167, 173oveq12d 7231 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (𝑥(2nd𝐸)𝑦) = (⟨(1st𝑥), (2nd𝑥)⟩(2nd𝐸)⟨(1st𝑦), (2nd𝑦)⟩))
213212, 187fveq12d 6724 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((𝑥(2nd𝐸)𝑦)‘𝑓) = ((⟨(1st𝑥), (2nd𝑥)⟩(2nd𝐸)⟨(1st𝑦), (2nd𝑦)⟩)‘⟨(1st𝑓), (2nd𝑓)⟩))
214209, 211, 213oveq123d 7234 . . . . 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 2787 . . . 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 17371 . . 3 (𝜑 → (1st𝐸)((𝑄 ×c 𝐶) Func 𝐷)(2nd𝐸))
217 df-br 5054 . . 3 ((1st𝐸)((𝑄 ×c 𝐶) Func 𝐷)(2nd𝐸) ↔ ⟨(1st𝐸), (2nd𝐸)⟩ ∈ ((𝑄 ×c 𝐶) Func 𝐷))
218216, 217sylib 221 . 2 (𝜑 → ⟨(1st𝐸), (2nd𝐸)⟩ ∈ ((𝑄 ×c 𝐶) Func 𝐷))
21917, 218eqeltrd 2838 1 (𝜑𝐸 ∈ ((𝑄 ×c 𝐶) Func 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1089   = wceq 1543  wcel 2110  wral 3061  Vcvv 3408  csb 3811  cop 4547   class class class wbr 5053   × cxp 5549  ccom 5555  Rel wrel 5556   Fn wfn 6375  wf 6376  cfv 6380  (class class class)co 7213  cmpo 7215  1st c1st 7759  2nd c2nd 7760  Basecbs 16760  Hom chom 16813  compcco 16814  Catccat 17167  Idccid 17168   Func cfunc 17360   Nat cnat 17448   FuncCat cfuc 17449   ×c cxpc 17675   evalF cevlf 17717
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5179  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-cnex 10785  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-om 7645  df-1st 7761  df-2nd 7762  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-1o 8202  df-er 8391  df-map 8510  df-ixp 8579  df-en 8627  df-dom 8628  df-sdom 8629  df-fin 8630  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065  df-nn 11831  df-2 11893  df-3 11894  df-4 11895  df-5 11896  df-6 11897  df-7 11898  df-8 11899  df-9 11900  df-n0 12091  df-z 12177  df-dec 12294  df-uz 12439  df-fz 13096  df-struct 16700  df-slot 16735  df-ndx 16745  df-base 16761  df-hom 16826  df-cco 16827  df-cat 17171  df-cid 17172  df-func 17364  df-nat 17450  df-fuc 17451  df-xpc 17679  df-evlf 17721
This theorem is referenced by:  uncfcl  17743  uncf1  17744  uncf2  17745  yonedalem1  17780
  Copyright terms: Public domain W3C validator