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

Theorem evlfcl 18279
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 2735 . . . . 5 (Base‘𝐶) = (Base‘𝐶)
5 eqid 2735 . . . . 5 (Hom ‘𝐶) = (Hom ‘𝐶)
6 eqid 2735 . . . . 5 (comp‘𝐷) = (comp‘𝐷)
7 eqid 2735 . . . . 5 (𝐶 Nat 𝐷) = (𝐶 Nat 𝐷)
81, 2, 3, 4, 5, 6, 7evlfval 18274 . . . 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 7464 . . . . . 6 (𝐶 Func 𝐷) ∈ V
10 fvex 6920 . . . . . 6 (Base‘𝐶) ∈ V
119, 10mpoex 8103 . . . . 5 (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st𝑓)‘𝑥)) ∈ V
129, 10xpex 7772 . . . . . 6 ((𝐶 Func 𝐷) × (Base‘𝐶)) ∈ V
1312, 12mpoex 8103 . . . . 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 5729 . . . 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 2847 . . 3 (𝜑𝐸 ∈ (V × V))
16 1st2nd2 8052 . . 3 (𝐸 ∈ (V × V) → 𝐸 = ⟨(1st𝐸), (2nd𝐸)⟩)
1715, 16syl 17 . 2 (𝜑𝐸 = ⟨(1st𝐸), (2nd𝐸)⟩)
18 eqid 2735 . . . . 5 (𝑄 ×c 𝐶) = (𝑄 ×c 𝐶)
19 evlfcl.q . . . . . 6 𝑄 = (𝐶 FuncCat 𝐷)
2019fucbas 18016 . . . . 5 (𝐶 Func 𝐷) = (Base‘𝑄)
2118, 20, 4xpcbas 18234 . . . 4 ((𝐶 Func 𝐷) × (Base‘𝐶)) = (Base‘(𝑄 ×c 𝐶))
22 eqid 2735 . . . 4 (Base‘𝐷) = (Base‘𝐷)
23 eqid 2735 . . . 4 (Hom ‘(𝑄 ×c 𝐶)) = (Hom ‘(𝑄 ×c 𝐶))
24 eqid 2735 . . . 4 (Hom ‘𝐷) = (Hom ‘𝐷)
25 eqid 2735 . . . 4 (Id‘(𝑄 ×c 𝐶)) = (Id‘(𝑄 ×c 𝐶))
26 eqid 2735 . . . 4 (Id‘𝐷) = (Id‘𝐷)
27 eqid 2735 . . . 4 (comp‘(𝑄 ×c 𝐶)) = (comp‘(𝑄 ×c 𝐶))
2819, 2, 3fuccat 18027 . . . . 5 (𝜑𝑄 ∈ Cat)
2918, 28, 2xpccat 18246 . . . 4 (𝜑 → (𝑄 ×c 𝐶) ∈ Cat)
30 relfunc 17913 . . . . . . . . . . 11 Rel (𝐶 Func 𝐷)
31 simpr 484 . . . . . . . . . . 11 ((𝜑𝑓 ∈ (𝐶 Func 𝐷)) → 𝑓 ∈ (𝐶 Func 𝐷))
32 1st2ndbr 8066 . . . . . . . . . . 11 ((Rel (𝐶 Func 𝐷) ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → (1st𝑓)(𝐶 Func 𝐷)(2nd𝑓))
3330, 31, 32sylancr 587 . . . . . . . . . 10 ((𝜑𝑓 ∈ (𝐶 Func 𝐷)) → (1st𝑓)(𝐶 Func 𝐷)(2nd𝑓))
344, 22, 33funcf1 17917 . . . . . . . . 9 ((𝜑𝑓 ∈ (𝐶 Func 𝐷)) → (1st𝑓):(Base‘𝐶)⟶(Base‘𝐷))
3534ffvelcdmda 7104 . . . . . . . 8 (((𝜑𝑓 ∈ (𝐶 Func 𝐷)) ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st𝑓)‘𝑥) ∈ (Base‘𝐷))
3635ralrimiva 3144 . . . . . . 7 ((𝜑𝑓 ∈ (𝐶 Func 𝐷)) → ∀𝑥 ∈ (Base‘𝐶)((1st𝑓)‘𝑥) ∈ (Base‘𝐷))
3736ralrimiva 3144 . . . . . 6 (𝜑 → ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑥 ∈ (Base‘𝐶)((1st𝑓)‘𝑥) ∈ (Base‘𝐷))
38 eqid 2735 . . . . . . 7 (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st𝑓)‘𝑥)) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st𝑓)‘𝑥))
3938fmpo 8092 . . . . . 6 (∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑥 ∈ (Base‘𝐶)((1st𝑓)‘𝑥) ∈ (Base‘𝐷) ↔ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st𝑓)‘𝑥)):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷))
4037, 39sylib 218 . . . . 5 (𝜑 → (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st𝑓)‘𝑥)):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷))
4111, 13op1std 8023 . . . . . . 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 6721 . . . . 5 (𝜑 → ((1st𝐸):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷) ↔ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st𝑓)‘𝑥)):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷)))
4440, 43mpbird 257 . . . 4 (𝜑 → (1st𝐸):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷))
45 eqid 2735 . . . . . 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 7464 . . . . . . . . 9 (𝑚(𝐶 Nat 𝐷)𝑛) ∈ V
47 ovex 7464 . . . . . . . . 9 ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ∈ V
4846, 47mpoex 8103 . . . . . . . 8 (𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ↦ ((𝑎‘(2nd𝑦))(⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩(comp‘𝐷)((1st𝑛)‘(2nd𝑦)))(((2nd𝑥)(2nd𝑚)(2nd𝑦))‘𝑔))) ∈ V
4948csbex 5317 . . . . . . 7 (1st𝑦) / 𝑛(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ↦ ((𝑎‘(2nd𝑦))(⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩(comp‘𝐷)((1st𝑛)‘(2nd𝑦)))(((2nd𝑥)(2nd𝑚)(2nd𝑦))‘𝑔))) ∈ V
5049csbex 5317 . . . . . 6 (1st𝑥) / 𝑚(1st𝑦) / 𝑛(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ↦ ((𝑎‘(2nd𝑦))(⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩(comp‘𝐷)((1st𝑛)‘(2nd𝑦)))(((2nd𝑥)(2nd𝑚)(2nd𝑦))‘𝑔))) ∈ V
5145, 50fnmpoi 8094 . . . . 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 8024 . . . . . . 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 6662 . . . . 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 258 . . . 4 (𝜑 → (2nd𝐸) Fn (((𝐶 Func 𝐷) × (Base‘𝐶)) × ((𝐶 Func 𝐷) × (Base‘𝐶))))
563ad2antrr 726 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝐷 ∈ Cat)
5756adantr 480 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝐷 ∈ Cat)
58 simplrl 777 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑓 ∈ (𝐶 Func 𝐷))
5930, 58, 32sylancr 587 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1st𝑓)(𝐶 Func 𝐷)(2nd𝑓))
604, 22, 59funcf1 17917 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1st𝑓):(Base‘𝐶)⟶(Base‘𝐷))
6160adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (1st𝑓):(Base‘𝐶)⟶(Base‘𝐷))
62 simplrr 778 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑢 ∈ (Base‘𝐶))
6362adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑢 ∈ (Base‘𝐶))
6461, 63ffvelcdmd 7105 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((1st𝑓)‘𝑢) ∈ (Base‘𝐷))
65 simplrr 778 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑣 ∈ (Base‘𝐶))
6661, 65ffvelcdmd 7105 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((1st𝑓)‘𝑣) ∈ (Base‘𝐷))
67 simprl 771 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑔 ∈ (𝐶 Func 𝐷))
68 1st2ndbr 8066 . . . . . . . . . . . . . . . . . . 19 ((Rel (𝐶 Func 𝐷) ∧ 𝑔 ∈ (𝐶 Func 𝐷)) → (1st𝑔)(𝐶 Func 𝐷)(2nd𝑔))
6930, 67, 68sylancr 587 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1st𝑔)(𝐶 Func 𝐷)(2nd𝑔))
704, 22, 69funcf1 17917 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1st𝑔):(Base‘𝐶)⟶(Base‘𝐷))
7170adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (1st𝑔):(Base‘𝐶)⟶(Base‘𝐷))
7271, 65ffvelcdmd 7105 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((1st𝑔)‘𝑣) ∈ (Base‘𝐷))
73 simprr 773 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑣 ∈ (Base‘𝐶))
744, 5, 24, 59, 62, 73funcf2 17919 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑢(2nd𝑓)𝑣):(𝑢(Hom ‘𝐶)𝑣)⟶(((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑓)‘𝑣)))
7574adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (𝑢(2nd𝑓)𝑣):(𝑢(Hom ‘𝐶)𝑣)⟶(((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑓)‘𝑣)))
76 simprr 773 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ∈ (𝑢(Hom ‘𝐶)𝑣))
7775, 76ffvelcdmd 7105 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((𝑢(2nd𝑓)𝑣)‘) ∈ (((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑓)‘𝑣)))
78 simprl 771 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔))
797, 78nat1st2nd 18006 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑎 ∈ (⟨(1st𝑓), (2nd𝑓)⟩(𝐶 Nat 𝐷)⟨(1st𝑔), (2nd𝑔)⟩))
807, 79, 4, 24, 65natcl 18008 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (𝑎𝑣) ∈ (((1st𝑓)‘𝑣)(Hom ‘𝐷)((1st𝑔)‘𝑣)))
8122, 24, 6, 57, 64, 66, 72, 77, 80catcocl 17730 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((𝑎𝑣)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑣)⟩(comp‘𝐷)((1st𝑔)‘𝑣))((𝑢(2nd𝑓)𝑣)‘)) ∈ (((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑔)‘𝑣)))
8281ralrimivva 3200 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → ∀𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔)∀ ∈ (𝑢(Hom ‘𝐶)𝑣)((𝑎𝑣)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑣)⟩(comp‘𝐷)((1st𝑔)‘𝑣))((𝑢(2nd𝑓)𝑣)‘)) ∈ (((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑔)‘𝑣)))
83 eqid 2735 . . . . . . . . . . . . . 14 (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎𝑣)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑣)⟩(comp‘𝐷)((1st𝑔)‘𝑣))((𝑢(2nd𝑓)𝑣)‘))) = (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎𝑣)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑣)⟩(comp‘𝐷)((1st𝑔)‘𝑣))((𝑢(2nd𝑓)𝑣)‘)))
8483fmpo 8092 . . . . . . . . . . . . 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 218 . . . . . . . . . . . 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 2735 . . . . . . . . . . . . . 14 (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩) = (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩)
881, 86, 56, 4, 5, 6, 7, 58, 67, 62, 73, 87evlf2 18275 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩) = (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎𝑣)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑣)⟩(comp‘𝐷)((1st𝑔)‘𝑣))((𝑢(2nd𝑓)𝑣)‘))))
8988feq1d 6721 . . . . . . . . . . . 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 257 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑔)‘𝑣)))
9119, 7fuchom 18017 . . . . . . . . . . . . 13 (𝐶 Nat 𝐷) = (Hom ‘𝑄)
9218, 20, 4, 91, 5, 58, 62, 67, 73, 23xpchom2 18242 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩) = ((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣)))
931, 86, 56, 4, 58, 62evlf1 18277 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑓(1st𝐸)𝑢) = ((1st𝑓)‘𝑢))
941, 86, 56, 4, 67, 73evlf1 18277 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑔(1st𝐸)𝑣) = ((1st𝑔)‘𝑣))
9593, 94oveq12d 7449 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → ((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)) = (((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑔)‘𝑣)))
9692, 95feq23d 6732 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)) ↔ (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑔)‘𝑣))))
9790, 96mpbird 257 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)))
9897ralrimivva 3200 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)))
9998ralrimivva 3200 . . . . . . . 8 (𝜑 → ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)))
100 oveq2 7439 . . . . . . . . . . . 12 (𝑦 = ⟨𝑔, 𝑣⟩ → (𝑥(2nd𝐸)𝑦) = (𝑥(2nd𝐸)⟨𝑔, 𝑣⟩))
101 oveq2 7439 . . . . . . . . . . . 12 (𝑦 = ⟨𝑔, 𝑣⟩ → (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) = (𝑥(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩))
102 fveq2 6907 . . . . . . . . . . . . . 14 (𝑦 = ⟨𝑔, 𝑣⟩ → ((1st𝐸)‘𝑦) = ((1st𝐸)‘⟨𝑔, 𝑣⟩))
103 df-ov 7434 . . . . . . . . . . . . . 14 (𝑔(1st𝐸)𝑣) = ((1st𝐸)‘⟨𝑔, 𝑣⟩)
104102, 103eqtr4di 2793 . . . . . . . . . . . . 13 (𝑦 = ⟨𝑔, 𝑣⟩ → ((1st𝐸)‘𝑦) = (𝑔(1st𝐸)𝑣))
105104oveq2d 7447 . . . . . . . . . . . 12 (𝑦 = ⟨𝑔, 𝑣⟩ → (((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)) = (((1st𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)))
106100, 101, 105feq123d 6726 . . . . . . . . . . 11 (𝑦 = ⟨𝑔, 𝑣⟩ → ((𝑥(2nd𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)) ↔ (𝑥(2nd𝐸)⟨𝑔, 𝑣⟩):(𝑥(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣))))
107106ralxp 5855 . . . . . . . . . 10 (∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2nd𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)) ↔ ∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(𝑥(2nd𝐸)⟨𝑔, 𝑣⟩):(𝑥(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)))
108 oveq1 7438 . . . . . . . . . . . 12 (𝑥 = ⟨𝑓, 𝑢⟩ → (𝑥(2nd𝐸)⟨𝑔, 𝑣⟩) = (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩))
109 oveq1 7438 . . . . . . . . . . . 12 (𝑥 = ⟨𝑓, 𝑢⟩ → (𝑥(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩) = (⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩))
110 fveq2 6907 . . . . . . . . . . . . . 14 (𝑥 = ⟨𝑓, 𝑢⟩ → ((1st𝐸)‘𝑥) = ((1st𝐸)‘⟨𝑓, 𝑢⟩))
111 df-ov 7434 . . . . . . . . . . . . . 14 (𝑓(1st𝐸)𝑢) = ((1st𝐸)‘⟨𝑓, 𝑢⟩)
112110, 111eqtr4di 2793 . . . . . . . . . . . . 13 (𝑥 = ⟨𝑓, 𝑢⟩ → ((1st𝐸)‘𝑥) = (𝑓(1st𝐸)𝑢))
113112oveq1d 7446 . . . . . . . . . . . 12 (𝑥 = ⟨𝑓, 𝑢⟩ → (((1st𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)) = ((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)))
114108, 109, 113feq123d 6726 . . . . . . . . . . 11 (𝑥 = ⟨𝑓, 𝑢⟩ → ((𝑥(2nd𝐸)⟨𝑔, 𝑣⟩):(𝑥(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)) ↔ (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣))))
1151142ralbidv 3219 . . . . . . . . . 10 (𝑥 = ⟨𝑓, 𝑢⟩ → (∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(𝑥(2nd𝐸)⟨𝑔, 𝑣⟩):(𝑥(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)) ↔ ∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣))))
116107, 115bitrid 283 . . . . . . . . 9 (𝑥 = ⟨𝑓, 𝑢⟩ → (∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2nd𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)) ↔ ∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣))))
117116ralxp 5855 . . . . . . . 8 (∀𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2nd𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)) ↔ ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)))
11899, 117sylibr 234 . . . . . . 7 (𝜑 → ∀𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2nd𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)))
119118r19.21bi 3249 . . . . . 6 ((𝜑𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) → ∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2nd𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)))
120119r19.21bi 3249 . . . . 5 (((𝜑𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) → (𝑥(2nd𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)))
121120anasss 466 . . . 4 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))) → (𝑥(2nd𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)))
12228adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝑄 ∈ Cat)
1232adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝐶 ∈ Cat)
124 eqid 2735 . . . . . . . . . . 11 (Id‘𝑄) = (Id‘𝑄)
125 eqid 2735 . . . . . . . . . . 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 18245 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩) = ⟨((Id‘𝑄)‘𝑓), ((Id‘𝐶)‘𝑢)⟩)
129128fveq2d 6911 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘⟨((Id‘𝑄)‘𝑓), ((Id‘𝐶)‘𝑢)⟩))
130 df-ov 7434 . . . . . . . . 9 (((Id‘𝑄)‘𝑓)(⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)((Id‘𝐶)‘𝑢)) = ((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘⟨((Id‘𝑄)‘𝑓), ((Id‘𝐶)‘𝑢)⟩)
131129, 130eqtr4di 2793 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)) = (((Id‘𝑄)‘𝑓)(⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)((Id‘𝐶)‘𝑢)))
1323adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝐷 ∈ Cat)
133 eqid 2735 . . . . . . . . 9 (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩) = (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)
13420, 91, 124, 122, 126catidcl 17727 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝑄)‘𝑓) ∈ (𝑓(𝐶 Nat 𝐷)𝑓))
1354, 5, 125, 123, 127catidcl 17727 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝐶)‘𝑢) ∈ (𝑢(Hom ‘𝐶)𝑢))
1361, 123, 132, 4, 5, 6, 7, 126, 126, 127, 127, 133, 134, 135evlf2val 18276 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝑄)‘𝑓)(⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)((Id‘𝐶)‘𝑢)) = ((((Id‘𝑄)‘𝑓)‘𝑢)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑢)⟩(comp‘𝐷)((1st𝑓)‘𝑢))((𝑢(2nd𝑓)𝑢)‘((Id‘𝐶)‘𝑢))))
13730, 126, 32sylancr 587 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (1st𝑓)(𝐶 Func 𝐷)(2nd𝑓))
1384, 22, 137funcf1 17917 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (1st𝑓):(Base‘𝐶)⟶(Base‘𝐷))
139138, 127ffvelcdmd 7105 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((1st𝑓)‘𝑢) ∈ (Base‘𝐷))
14022, 24, 26, 132, 139catidcl 17727 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝐷)‘((1st𝑓)‘𝑢)) ∈ (((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑓)‘𝑢)))
14122, 24, 26, 132, 139, 6, 139, 140catlid 17728 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝐷)‘((1st𝑓)‘𝑢))(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑢)⟩(comp‘𝐷)((1st𝑓)‘𝑢))((Id‘𝐷)‘((1st𝑓)‘𝑢))) = ((Id‘𝐷)‘((1st𝑓)‘𝑢)))
14219, 124, 26, 126fucid 18028 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝑄)‘𝑓) = ((Id‘𝐷) ∘ (1st𝑓)))
143142fveq1d 6909 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝑄)‘𝑓)‘𝑢) = (((Id‘𝐷) ∘ (1st𝑓))‘𝑢))
144 fvco3 7008 . . . . . . . . . . . 12 (((1st𝑓):(Base‘𝐶)⟶(Base‘𝐷) ∧ 𝑢 ∈ (Base‘𝐶)) → (((Id‘𝐷) ∘ (1st𝑓))‘𝑢) = ((Id‘𝐷)‘((1st𝑓)‘𝑢)))
145138, 127, 144syl2anc 584 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝐷) ∘ (1st𝑓))‘𝑢) = ((Id‘𝐷)‘((1st𝑓)‘𝑢)))
146143, 145eqtrd 2775 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝑄)‘𝑓)‘𝑢) = ((Id‘𝐷)‘((1st𝑓)‘𝑢)))
1474, 125, 26, 137, 127funcid 17921 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((𝑢(2nd𝑓)𝑢)‘((Id‘𝐶)‘𝑢)) = ((Id‘𝐷)‘((1st𝑓)‘𝑢)))
148146, 147oveq12d 7449 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((((Id‘𝑄)‘𝑓)‘𝑢)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑢)⟩(comp‘𝐷)((1st𝑓)‘𝑢))((𝑢(2nd𝑓)𝑢)‘((Id‘𝐶)‘𝑢))) = (((Id‘𝐷)‘((1st𝑓)‘𝑢))(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑢)⟩(comp‘𝐷)((1st𝑓)‘𝑢))((Id‘𝐷)‘((1st𝑓)‘𝑢))))
1491, 123, 132, 4, 126, 127evlf1 18277 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (𝑓(1st𝐸)𝑢) = ((1st𝑓)‘𝑢))
150149fveq2d 6911 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝐷)‘(𝑓(1st𝐸)𝑢)) = ((Id‘𝐷)‘((1st𝑓)‘𝑢)))
151141, 148, 1503eqtr4d 2785 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((((Id‘𝑄)‘𝑓)‘𝑢)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑢)⟩(comp‘𝐷)((1st𝑓)‘𝑢))((𝑢(2nd𝑓)𝑢)‘((Id‘𝐶)‘𝑢))) = ((Id‘𝐷)‘(𝑓(1st𝐸)𝑢)))
152131, 136, 1513eqtrd 2779 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1st𝐸)𝑢)))
153152ralrimivva 3200 . . . . . 6 (𝜑 → ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1st𝐸)𝑢)))
154 id 22 . . . . . . . . . 10 (𝑥 = ⟨𝑓, 𝑢⟩ → 𝑥 = ⟨𝑓, 𝑢⟩)
155154, 154oveq12d 7449 . . . . . . . . 9 (𝑥 = ⟨𝑓, 𝑢⟩ → (𝑥(2nd𝐸)𝑥) = (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩))
156 fveq2 6907 . . . . . . . . 9 (𝑥 = ⟨𝑓, 𝑢⟩ → ((Id‘(𝑄 ×c 𝐶))‘𝑥) = ((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩))
157155, 156fveq12d 6914 . . . . . . . 8 (𝑥 = ⟨𝑓, 𝑢⟩ → ((𝑥(2nd𝐸)𝑥)‘((Id‘(𝑄 ×c 𝐶))‘𝑥)) = ((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)))
158112fveq2d 6911 . . . . . . . 8 (𝑥 = ⟨𝑓, 𝑢⟩ → ((Id‘𝐷)‘((1st𝐸)‘𝑥)) = ((Id‘𝐷)‘(𝑓(1st𝐸)𝑢)))
159157, 158eqeq12d 2751 . . . . . . 7 (𝑥 = ⟨𝑓, 𝑢⟩ → (((𝑥(2nd𝐸)𝑥)‘((Id‘(𝑄 ×c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1st𝐸)‘𝑥)) ↔ ((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1st𝐸)𝑢))))
160159ralxp 5855 . . . . . 6 (∀𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))((𝑥(2nd𝐸)𝑥)‘((Id‘(𝑄 ×c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1st𝐸)‘𝑥)) ↔ ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1st𝐸)𝑢)))
161153, 160sylibr 234 . . . . 5 (𝜑 → ∀𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))((𝑥(2nd𝐸)𝑥)‘((Id‘(𝑄 ×c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1st𝐸)‘𝑥)))
162161r19.21bi 3249 . . . 4 ((𝜑𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) → ((𝑥(2nd𝐸)𝑥)‘((Id‘(𝑄 ×c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1st𝐸)‘𝑥)))
16323ad2ant1 1132 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝐶 ∈ Cat)
16433ad2ant1 1132 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝐷 ∈ Cat)
165 simp21 1205 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
166 1st2nd2 8052 . . . . . . . . 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 5725 . . . . . . 7 (⟨(1st𝑥), (2nd𝑥)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↔ ((1st𝑥) ∈ (𝐶 Func 𝐷) ∧ (2nd𝑥) ∈ (Base‘𝐶)))
170168, 169sylib 218 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st𝑥) ∈ (𝐶 Func 𝐷) ∧ (2nd𝑥) ∈ (Base‘𝐶)))
171 simp22 1206 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
172 1st2nd2 8052 . . . . . . . . 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 5725 . . . . . . 7 (⟨(1st𝑦), (2nd𝑦)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↔ ((1st𝑦) ∈ (𝐶 Func 𝐷) ∧ (2nd𝑦) ∈ (Base‘𝐶)))
176174, 175sylib 218 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st𝑦) ∈ (𝐶 Func 𝐷) ∧ (2nd𝑦) ∈ (Base‘𝐶)))
177 simp23 1207 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
178 1st2nd2 8052 . . . . . . . . 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 5725 . . . . . . 7 (⟨(1st𝑧), (2nd𝑧)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↔ ((1st𝑧) ∈ (𝐶 Func 𝐷) ∧ (2nd𝑧) ∈ (Base‘𝐶)))
182180, 181sylib 218 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st𝑧) ∈ (𝐶 Func 𝐷) ∧ (2nd𝑧) ∈ (Base‘𝐶)))
183 simp3l 1200 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦))
18418, 21, 91, 5, 23, 165, 171xpchom 18236 . . . . . . . . . 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 8052 . . . . . . . . 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 5725 . . . . . . 7 (⟨(1st𝑓), (2nd𝑓)⟩ ∈ (((1st𝑥)(𝐶 Nat 𝐷)(1st𝑦)) × ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦))) ↔ ((1st𝑓) ∈ ((1st𝑥)(𝐶 Nat 𝐷)(1st𝑦)) ∧ (2nd𝑓) ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦))))
190188, 189sylib 218 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st𝑓) ∈ ((1st𝑥)(𝐶 Nat 𝐷)(1st𝑦)) ∧ (2nd𝑓) ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦))))
191 simp3r 1201 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))
19218, 21, 91, 5, 23, 171, 177xpchom 18236 . . . . . . . . . 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 8052 . . . . . . . . 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 5725 . . . . . . 7 (⟨(1st𝑔), (2nd𝑔)⟩ ∈ (((1st𝑦)(𝐶 Nat 𝐷)(1st𝑧)) × ((2nd𝑦)(Hom ‘𝐶)(2nd𝑧))) ↔ ((1st𝑔) ∈ ((1st𝑦)(𝐶 Nat 𝐷)(1st𝑧)) ∧ (2nd𝑔) ∈ ((2nd𝑦)(Hom ‘𝐶)(2nd𝑧))))
198196, 197sylib 218 . . . . . 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 18278 . . . . 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 7449 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (𝑥(2nd𝐸)𝑧) = (⟨(1st𝑥), (2nd𝑥)⟩(2nd𝐸)⟨(1st𝑧), (2nd𝑧)⟩))
201167, 173opeq12d 4886 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ⟨𝑥, 𝑦⟩ = ⟨⟨(1st𝑥), (2nd𝑥)⟩, ⟨(1st𝑦), (2nd𝑦)⟩⟩)
202201, 179oveq12d 7449 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (⟨𝑥, 𝑦⟩(comp‘(𝑄 ×c 𝐶))𝑧) = (⟨⟨(1st𝑥), (2nd𝑥)⟩, ⟨(1st𝑦), (2nd𝑦)⟩⟩(comp‘(𝑄 ×c 𝐶))⟨(1st𝑧), (2nd𝑧)⟩))
203202, 195, 187oveq123d 7452 . . . . . 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 6914 . . . . 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 6911 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st𝐸)‘𝑥) = ((1st𝐸)‘⟨(1st𝑥), (2nd𝑥)⟩))
206173fveq2d 6911 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st𝐸)‘𝑦) = ((1st𝐸)‘⟨(1st𝑦), (2nd𝑦)⟩))
207205, 206opeq12d 4886 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ⟨((1st𝐸)‘𝑥), ((1st𝐸)‘𝑦)⟩ = ⟨((1st𝐸)‘⟨(1st𝑥), (2nd𝑥)⟩), ((1st𝐸)‘⟨(1st𝑦), (2nd𝑦)⟩)⟩)
208179fveq2d 6911 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st𝐸)‘𝑧) = ((1st𝐸)‘⟨(1st𝑧), (2nd𝑧)⟩))
209207, 208oveq12d 7449 . . . . . 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 7449 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (𝑦(2nd𝐸)𝑧) = (⟨(1st𝑦), (2nd𝑦)⟩(2nd𝐸)⟨(1st𝑧), (2nd𝑧)⟩))
211210, 195fveq12d 6914 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((𝑦(2nd𝐸)𝑧)‘𝑔) = ((⟨(1st𝑦), (2nd𝑦)⟩(2nd𝐸)⟨(1st𝑧), (2nd𝑧)⟩)‘⟨(1st𝑔), (2nd𝑔)⟩))
212167, 173oveq12d 7449 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (𝑥(2nd𝐸)𝑦) = (⟨(1st𝑥), (2nd𝑥)⟩(2nd𝐸)⟨(1st𝑦), (2nd𝑦)⟩))
213212, 187fveq12d 6914 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((𝑥(2nd𝐸)𝑦)‘𝑓) = ((⟨(1st𝑥), (2nd𝑥)⟩(2nd𝐸)⟨(1st𝑦), (2nd𝑦)⟩)‘⟨(1st𝑓), (2nd𝑓)⟩))
214209, 211, 213oveq123d 7452 . . . . 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 2785 . . . 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 17916 . . 3 (𝜑 → (1st𝐸)((𝑄 ×c 𝐶) Func 𝐷)(2nd𝐸))
217 df-br 5149 . . 3 ((1st𝐸)((𝑄 ×c 𝐶) Func 𝐷)(2nd𝐸) ↔ ⟨(1st𝐸), (2nd𝐸)⟩ ∈ ((𝑄 ×c 𝐶) Func 𝐷))
218216, 217sylib 218 . 2 (𝜑 → ⟨(1st𝐸), (2nd𝐸)⟩ ∈ ((𝑄 ×c 𝐶) Func 𝐷))
21917, 218eqeltrd 2839 1 (𝜑𝐸 ∈ ((𝑄 ×c 𝐶) Func 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1086   = wceq 1537  wcel 2106  wral 3059  Vcvv 3478  csb 3908  cop 4637   class class class wbr 5148   × cxp 5687  ccom 5693  Rel wrel 5694   Fn wfn 6558  wf 6559  cfv 6563  (class class class)co 7431  cmpo 7433  1st c1st 8011  2nd c2nd 8012  Basecbs 17245  Hom chom 17309  compcco 17310  Catccat 17709  Idccid 17710   Func cfunc 17905   Nat cnat 17996   FuncCat cfuc 17997   ×c cxpc 18224   evalF cevlf 18266
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-tp 4636  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8013  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-1o 8505  df-er 8744  df-map 8867  df-ixp 8937  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-nn 12265  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332  df-8 12333  df-9 12334  df-n0 12525  df-z 12612  df-dec 12732  df-uz 12877  df-fz 13545  df-struct 17181  df-slot 17216  df-ndx 17228  df-base 17246  df-hom 17322  df-cco 17323  df-cat 17713  df-cid 17714  df-func 17909  df-nat 17998  df-fuc 17999  df-xpc 18228  df-evlf 18270
This theorem is referenced by:  uncfcl  18292  uncf1  18293  uncf2  18294  yonedalem1  18329
  Copyright terms: Public domain W3C validator