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

Theorem evlfcl 16685
 Description: The evaluation functor is a bifunctor (a two-argument functor) with the first parameter taking values in the set of functors 𝐶⟶𝐷, and the second parameter in 𝐷. (Contributed by Mario Carneiro, 12-Jan-2017.)
Hypotheses
Ref Expression
evlfcl.e 𝐸 = (𝐶 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 2610 . . . . 5 (Base‘𝐶) = (Base‘𝐶)
5 eqid 2610 . . . . 5 (Hom ‘𝐶) = (Hom ‘𝐶)
6 eqid 2610 . . . . 5 (comp‘𝐷) = (comp‘𝐷)
7 eqid 2610 . . . . 5 (𝐶 Nat 𝐷) = (𝐶 Nat 𝐷)
81, 2, 3, 4, 5, 6, 7evlfval 16680 . . . 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 6577 . . . . . 6 (𝐶 Func 𝐷) ∈ V
10 fvex 6113 . . . . . 6 (Base‘𝐶) ∈ V
119, 10mpt2ex 7136 . . . . 5 (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st𝑓)‘𝑥)) ∈ V
129, 10xpex 6860 . . . . . 6 ((𝐶 Func 𝐷) × (Base‘𝐶)) ∈ V
1312, 12mpt2ex 7136 . . . . 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 5088 . . . 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 2696 . . 3 (𝜑𝐸 ∈ (V × V))
16 1st2nd2 7096 . . 3 (𝐸 ∈ (V × V) → 𝐸 = ⟨(1st𝐸), (2nd𝐸)⟩)
1715, 16syl 17 . 2 (𝜑𝐸 = ⟨(1st𝐸), (2nd𝐸)⟩)
18 eqid 2610 . . . . 5 (𝑄 ×c 𝐶) = (𝑄 ×c 𝐶)
19 evlfcl.q . . . . . 6 𝑄 = (𝐶 FuncCat 𝐷)
2019fucbas 16443 . . . . 5 (𝐶 Func 𝐷) = (Base‘𝑄)
2118, 20, 4xpcbas 16641 . . . 4 ((𝐶 Func 𝐷) × (Base‘𝐶)) = (Base‘(𝑄 ×c 𝐶))
22 eqid 2610 . . . 4 (Base‘𝐷) = (Base‘𝐷)
23 eqid 2610 . . . 4 (Hom ‘(𝑄 ×c 𝐶)) = (Hom ‘(𝑄 ×c 𝐶))
24 eqid 2610 . . . 4 (Hom ‘𝐷) = (Hom ‘𝐷)
25 eqid 2610 . . . 4 (Id‘(𝑄 ×c 𝐶)) = (Id‘(𝑄 ×c 𝐶))
26 eqid 2610 . . . 4 (Id‘𝐷) = (Id‘𝐷)
27 eqid 2610 . . . 4 (comp‘(𝑄 ×c 𝐶)) = (comp‘(𝑄 ×c 𝐶))
2819, 2, 3fuccat 16453 . . . . 5 (𝜑𝑄 ∈ Cat)
2918, 28, 2xpccat 16653 . . . 4 (𝜑 → (𝑄 ×c 𝐶) ∈ Cat)
30 relfunc 16345 . . . . . . . . . . 11 Rel (𝐶 Func 𝐷)
31 simpr 476 . . . . . . . . . . 11 ((𝜑𝑓 ∈ (𝐶 Func 𝐷)) → 𝑓 ∈ (𝐶 Func 𝐷))
32 1st2ndbr 7108 . . . . . . . . . . 11 ((Rel (𝐶 Func 𝐷) ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → (1st𝑓)(𝐶 Func 𝐷)(2nd𝑓))
3330, 31, 32sylancr 694 . . . . . . . . . 10 ((𝜑𝑓 ∈ (𝐶 Func 𝐷)) → (1st𝑓)(𝐶 Func 𝐷)(2nd𝑓))
344, 22, 33funcf1 16349 . . . . . . . . 9 ((𝜑𝑓 ∈ (𝐶 Func 𝐷)) → (1st𝑓):(Base‘𝐶)⟶(Base‘𝐷))
3534ffvelrnda 6267 . . . . . . . 8 (((𝜑𝑓 ∈ (𝐶 Func 𝐷)) ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st𝑓)‘𝑥) ∈ (Base‘𝐷))
3635ralrimiva 2949 . . . . . . 7 ((𝜑𝑓 ∈ (𝐶 Func 𝐷)) → ∀𝑥 ∈ (Base‘𝐶)((1st𝑓)‘𝑥) ∈ (Base‘𝐷))
3736ralrimiva 2949 . . . . . 6 (𝜑 → ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑥 ∈ (Base‘𝐶)((1st𝑓)‘𝑥) ∈ (Base‘𝐷))
38 eqid 2610 . . . . . . 7 (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st𝑓)‘𝑥)) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st𝑓)‘𝑥))
3938fmpt2 7126 . . . . . 6 (∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑥 ∈ (Base‘𝐶)((1st𝑓)‘𝑥) ∈ (Base‘𝐷) ↔ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st𝑓)‘𝑥)):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷))
4037, 39sylib 207 . . . . 5 (𝜑 → (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st𝑓)‘𝑥)):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷))
4111, 13op1std 7069 . . . . . . 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 5943 . . . . 5 (𝜑 → ((1st𝐸):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷) ↔ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st𝑓)‘𝑥)):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷)))
4440, 43mpbird 246 . . . 4 (𝜑 → (1st𝐸):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷))
45 eqid 2610 . . . . . 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 6577 . . . . . . . . 9 (𝑚(𝐶 Nat 𝐷)𝑛) ∈ V
47 ovex 6577 . . . . . . . . 9 ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ∈ V
4846, 47mpt2ex 7136 . . . . . . . 8 (𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ↦ ((𝑎‘(2nd𝑦))(⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩(comp‘𝐷)((1st𝑛)‘(2nd𝑦)))(((2nd𝑥)(2nd𝑚)(2nd𝑦))‘𝑔))) ∈ V
4948csbex 4721 . . . . . . 7 (1st𝑦) / 𝑛(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ↦ ((𝑎‘(2nd𝑦))(⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩(comp‘𝐷)((1st𝑛)‘(2nd𝑦)))(((2nd𝑥)(2nd𝑚)(2nd𝑦))‘𝑔))) ∈ V
5049csbex 4721 . . . . . 6 (1st𝑥) / 𝑚(1st𝑦) / 𝑛(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦)) ↦ ((𝑎‘(2nd𝑦))(⟨((1st𝑚)‘(2nd𝑥)), ((1st𝑚)‘(2nd𝑦))⟩(comp‘𝐷)((1st𝑛)‘(2nd𝑦)))(((2nd𝑥)(2nd𝑚)(2nd𝑦))‘𝑔))) ∈ V
5145, 50fnmpt2i 7128 . . . . 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 7070 . . . . . . 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 5895 . . . . 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 247 . . . 4 (𝜑 → (2nd𝐸) Fn (((𝐶 Func 𝐷) × (Base‘𝐶)) × ((𝐶 Func 𝐷) × (Base‘𝐶))))
563ad2antrr 758 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝐷 ∈ Cat)
5756adantr 480 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝐷 ∈ Cat)
58 simplrl 796 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑓 ∈ (𝐶 Func 𝐷))
5930, 58, 32sylancr 694 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1st𝑓)(𝐶 Func 𝐷)(2nd𝑓))
604, 22, 59funcf1 16349 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1st𝑓):(Base‘𝐶)⟶(Base‘𝐷))
6160adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (1st𝑓):(Base‘𝐶)⟶(Base‘𝐷))
62 simplrr 797 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑢 ∈ (Base‘𝐶))
6362adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑢 ∈ (Base‘𝐶))
6461, 63ffvelrnd 6268 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((1st𝑓)‘𝑢) ∈ (Base‘𝐷))
65 simplrr 797 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑣 ∈ (Base‘𝐶))
6661, 65ffvelrnd 6268 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((1st𝑓)‘𝑣) ∈ (Base‘𝐷))
67 simprl 790 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑔 ∈ (𝐶 Func 𝐷))
68 1st2ndbr 7108 . . . . . . . . . . . . . . . . . . 19 ((Rel (𝐶 Func 𝐷) ∧ 𝑔 ∈ (𝐶 Func 𝐷)) → (1st𝑔)(𝐶 Func 𝐷)(2nd𝑔))
6930, 67, 68sylancr 694 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1st𝑔)(𝐶 Func 𝐷)(2nd𝑔))
704, 22, 69funcf1 16349 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1st𝑔):(Base‘𝐶)⟶(Base‘𝐷))
7170adantr 480 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (1st𝑔):(Base‘𝐶)⟶(Base‘𝐷))
7271, 65ffvelrnd 6268 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((1st𝑔)‘𝑣) ∈ (Base‘𝐷))
73 simprr 792 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑣 ∈ (Base‘𝐶))
744, 5, 24, 59, 62, 73funcf2 16351 . . . . . . . . . . . . . . . . 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 792 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ∈ (𝑢(Hom ‘𝐶)𝑣))
7775, 76ffvelrnd 6268 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((𝑢(2nd𝑓)𝑣)‘) ∈ (((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑓)‘𝑣)))
78 simprl 790 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔))
797, 78nat1st2nd 16434 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑎 ∈ (⟨(1st𝑓), (2nd𝑓)⟩(𝐶 Nat 𝐷)⟨(1st𝑔), (2nd𝑔)⟩))
807, 79, 4, 24, 65natcl 16436 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (𝑎𝑣) ∈ (((1st𝑓)‘𝑣)(Hom ‘𝐷)((1st𝑔)‘𝑣)))
8122, 24, 6, 57, 64, 66, 72, 77, 80catcocl 16169 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((𝑎𝑣)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑣)⟩(comp‘𝐷)((1st𝑔)‘𝑣))((𝑢(2nd𝑓)𝑣)‘)) ∈ (((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑔)‘𝑣)))
8281ralrimivva 2954 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → ∀𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔)∀ ∈ (𝑢(Hom ‘𝐶)𝑣)((𝑎𝑣)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑣)⟩(comp‘𝐷)((1st𝑔)‘𝑣))((𝑢(2nd𝑓)𝑣)‘)) ∈ (((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑔)‘𝑣)))
83 eqid 2610 . . . . . . . . . . . . . 14 (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎𝑣)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑣)⟩(comp‘𝐷)((1st𝑔)‘𝑣))((𝑢(2nd𝑓)𝑣)‘))) = (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎𝑣)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑣)⟩(comp‘𝐷)((1st𝑔)‘𝑣))((𝑢(2nd𝑓)𝑣)‘)))
8483fmpt2 7126 . . . . . . . . . . . . 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 207 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎𝑣)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑣)⟩(comp‘𝐷)((1st𝑔)‘𝑣))((𝑢(2nd𝑓)𝑣)‘))):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑔)‘𝑣)))
862ad2antrr 758 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝐶 ∈ Cat)
87 eqid 2610 . . . . . . . . . . . . . 14 (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩) = (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩)
881, 86, 56, 4, 5, 6, 7, 58, 67, 62, 73, 87evlf2 16681 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩) = (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎𝑣)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑣)⟩(comp‘𝐷)((1st𝑔)‘𝑣))((𝑢(2nd𝑓)𝑣)‘))))
8988feq1d 5943 . . . . . . . . . . . 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 246 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑔)‘𝑣)))
9119, 7fuchom 16444 . . . . . . . . . . . . 13 (𝐶 Nat 𝐷) = (Hom ‘𝑄)
9218, 20, 4, 91, 5, 58, 62, 67, 73, 23xpchom2 16649 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩) = ((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣)))
931, 86, 56, 4, 58, 62evlf1 16683 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑓(1st𝐸)𝑢) = ((1st𝑓)‘𝑢))
941, 86, 56, 4, 67, 73evlf1 16683 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑔(1st𝐸)𝑣) = ((1st𝑔)‘𝑣))
9593, 94oveq12d 6567 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → ((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)) = (((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑔)‘𝑣)))
9692, 95feq23d 5953 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)) ↔ (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑔)‘𝑣))))
9790, 96mpbird 246 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)))
9897ralrimivva 2954 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)))
9998ralrimivva 2954 . . . . . . . 8 (𝜑 → ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)))
100 oveq2 6557 . . . . . . . . . . . 12 (𝑦 = ⟨𝑔, 𝑣⟩ → (𝑥(2nd𝐸)𝑦) = (𝑥(2nd𝐸)⟨𝑔, 𝑣⟩))
101 oveq2 6557 . . . . . . . . . . . 12 (𝑦 = ⟨𝑔, 𝑣⟩ → (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) = (𝑥(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩))
102 fveq2 6103 . . . . . . . . . . . . . 14 (𝑦 = ⟨𝑔, 𝑣⟩ → ((1st𝐸)‘𝑦) = ((1st𝐸)‘⟨𝑔, 𝑣⟩))
103 df-ov 6552 . . . . . . . . . . . . . 14 (𝑔(1st𝐸)𝑣) = ((1st𝐸)‘⟨𝑔, 𝑣⟩)
104102, 103syl6eqr 2662 . . . . . . . . . . . . 13 (𝑦 = ⟨𝑔, 𝑣⟩ → ((1st𝐸)‘𝑦) = (𝑔(1st𝐸)𝑣))
105104oveq2d 6565 . . . . . . . . . . . 12 (𝑦 = ⟨𝑔, 𝑣⟩ → (((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)) = (((1st𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)))
106100, 101, 105feq123d 5947 . . . . . . . . . . 11 (𝑦 = ⟨𝑔, 𝑣⟩ → ((𝑥(2nd𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)) ↔ (𝑥(2nd𝐸)⟨𝑔, 𝑣⟩):(𝑥(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣))))
107106ralxp 5185 . . . . . . . . . 10 (∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2nd𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)) ↔ ∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(𝑥(2nd𝐸)⟨𝑔, 𝑣⟩):(𝑥(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)))
108 oveq1 6556 . . . . . . . . . . . 12 (𝑥 = ⟨𝑓, 𝑢⟩ → (𝑥(2nd𝐸)⟨𝑔, 𝑣⟩) = (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩))
109 oveq1 6556 . . . . . . . . . . . 12 (𝑥 = ⟨𝑓, 𝑢⟩ → (𝑥(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩) = (⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩))
110 fveq2 6103 . . . . . . . . . . . . . 14 (𝑥 = ⟨𝑓, 𝑢⟩ → ((1st𝐸)‘𝑥) = ((1st𝐸)‘⟨𝑓, 𝑢⟩))
111 df-ov 6552 . . . . . . . . . . . . . 14 (𝑓(1st𝐸)𝑢) = ((1st𝐸)‘⟨𝑓, 𝑢⟩)
112110, 111syl6eqr 2662 . . . . . . . . . . . . 13 (𝑥 = ⟨𝑓, 𝑢⟩ → ((1st𝐸)‘𝑥) = (𝑓(1st𝐸)𝑢))
113112oveq1d 6564 . . . . . . . . . . . 12 (𝑥 = ⟨𝑓, 𝑢⟩ → (((1st𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)) = ((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)))
114108, 109, 113feq123d 5947 . . . . . . . . . . 11 (𝑥 = ⟨𝑓, 𝑢⟩ → ((𝑥(2nd𝐸)⟨𝑔, 𝑣⟩):(𝑥(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)) ↔ (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣))))
1151142ralbidv 2972 . . . . . . . . . 10 (𝑥 = ⟨𝑓, 𝑢⟩ → (∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(𝑥(2nd𝐸)⟨𝑔, 𝑣⟩):(𝑥(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)) ↔ ∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣))))
116107, 115syl5bb 271 . . . . . . . . 9 (𝑥 = ⟨𝑓, 𝑢⟩ → (∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2nd𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)) ↔ ∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣))))
117116ralxp 5185 . . . . . . . 8 (∀𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2nd𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)) ↔ ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑔, 𝑣⟩):(⟨𝑓, 𝑢⟩(Hom ‘(𝑄 ×c 𝐶))⟨𝑔, 𝑣⟩)⟶((𝑓(1st𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st𝐸)𝑣)))
11899, 117sylibr 223 . . . . . . 7 (𝜑 → ∀𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2nd𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)))
119118r19.21bi 2916 . . . . . 6 ((𝜑𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) → ∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2nd𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)))
120119r19.21bi 2916 . . . . 5 (((𝜑𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) → (𝑥(2nd𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st𝐸)‘𝑥)(Hom ‘𝐷)((1st𝐸)‘𝑦)))
121120anasss 677 . . . 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 2610 . . . . . . . . . . 11 (Id‘𝑄) = (Id‘𝑄)
125 eqid 2610 . . . . . . . . . . 11 (Id‘𝐶) = (Id‘𝐶)
126 simprl 790 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝑓 ∈ (𝐶 Func 𝐷))
127 simprr 792 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝑢 ∈ (Base‘𝐶))
12818, 122, 123, 20, 4, 124, 125, 25, 126, 127xpcid 16652 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩) = ⟨((Id‘𝑄)‘𝑓), ((Id‘𝐶)‘𝑢)⟩)
129128fveq2d 6107 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘⟨((Id‘𝑄)‘𝑓), ((Id‘𝐶)‘𝑢)⟩))
130 df-ov 6552 . . . . . . . . 9 (((Id‘𝑄)‘𝑓)(⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)((Id‘𝐶)‘𝑢)) = ((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘⟨((Id‘𝑄)‘𝑓), ((Id‘𝐶)‘𝑢)⟩)
131129, 130syl6eqr 2662 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)) = (((Id‘𝑄)‘𝑓)(⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)((Id‘𝐶)‘𝑢)))
1323adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝐷 ∈ Cat)
133 eqid 2610 . . . . . . . . 9 (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩) = (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)
13420, 91, 124, 122, 126catidcl 16166 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝑄)‘𝑓) ∈ (𝑓(𝐶 Nat 𝐷)𝑓))
1354, 5, 125, 123, 127catidcl 16166 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝐶)‘𝑢) ∈ (𝑢(Hom ‘𝐶)𝑢))
1361, 123, 132, 4, 5, 6, 7, 126, 126, 127, 127, 133, 134, 135evlf2val 16682 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝑄)‘𝑓)(⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)((Id‘𝐶)‘𝑢)) = ((((Id‘𝑄)‘𝑓)‘𝑢)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑢)⟩(comp‘𝐷)((1st𝑓)‘𝑢))((𝑢(2nd𝑓)𝑢)‘((Id‘𝐶)‘𝑢))))
13730, 126, 32sylancr 694 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (1st𝑓)(𝐶 Func 𝐷)(2nd𝑓))
1384, 22, 137funcf1 16349 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (1st𝑓):(Base‘𝐶)⟶(Base‘𝐷))
139138, 127ffvelrnd 6268 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((1st𝑓)‘𝑢) ∈ (Base‘𝐷))
14022, 24, 26, 132, 139catidcl 16166 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝐷)‘((1st𝑓)‘𝑢)) ∈ (((1st𝑓)‘𝑢)(Hom ‘𝐷)((1st𝑓)‘𝑢)))
14122, 24, 26, 132, 139, 6, 139, 140catlid 16167 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝐷)‘((1st𝑓)‘𝑢))(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑢)⟩(comp‘𝐷)((1st𝑓)‘𝑢))((Id‘𝐷)‘((1st𝑓)‘𝑢))) = ((Id‘𝐷)‘((1st𝑓)‘𝑢)))
14219, 124, 26, 126fucid 16454 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝑄)‘𝑓) = ((Id‘𝐷) ∘ (1st𝑓)))
143142fveq1d 6105 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝑄)‘𝑓)‘𝑢) = (((Id‘𝐷) ∘ (1st𝑓))‘𝑢))
144 fvco3 6185 . . . . . . . . . . . 12 (((1st𝑓):(Base‘𝐶)⟶(Base‘𝐷) ∧ 𝑢 ∈ (Base‘𝐶)) → (((Id‘𝐷) ∘ (1st𝑓))‘𝑢) = ((Id‘𝐷)‘((1st𝑓)‘𝑢)))
145138, 127, 144syl2anc 691 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝐷) ∘ (1st𝑓))‘𝑢) = ((Id‘𝐷)‘((1st𝑓)‘𝑢)))
146143, 145eqtrd 2644 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝑄)‘𝑓)‘𝑢) = ((Id‘𝐷)‘((1st𝑓)‘𝑢)))
1474, 125, 26, 137, 127funcid 16353 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((𝑢(2nd𝑓)𝑢)‘((Id‘𝐶)‘𝑢)) = ((Id‘𝐷)‘((1st𝑓)‘𝑢)))
148146, 147oveq12d 6567 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((((Id‘𝑄)‘𝑓)‘𝑢)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑢)⟩(comp‘𝐷)((1st𝑓)‘𝑢))((𝑢(2nd𝑓)𝑢)‘((Id‘𝐶)‘𝑢))) = (((Id‘𝐷)‘((1st𝑓)‘𝑢))(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑢)⟩(comp‘𝐷)((1st𝑓)‘𝑢))((Id‘𝐷)‘((1st𝑓)‘𝑢))))
1491, 123, 132, 4, 126, 127evlf1 16683 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (𝑓(1st𝐸)𝑢) = ((1st𝑓)‘𝑢))
150149fveq2d 6107 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝐷)‘(𝑓(1st𝐸)𝑢)) = ((Id‘𝐷)‘((1st𝑓)‘𝑢)))
151141, 148, 1503eqtr4d 2654 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((((Id‘𝑄)‘𝑓)‘𝑢)(⟨((1st𝑓)‘𝑢), ((1st𝑓)‘𝑢)⟩(comp‘𝐷)((1st𝑓)‘𝑢))((𝑢(2nd𝑓)𝑢)‘((Id‘𝐶)‘𝑢))) = ((Id‘𝐷)‘(𝑓(1st𝐸)𝑢)))
152131, 136, 1513eqtrd 2648 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1st𝐸)𝑢)))
153152ralrimivva 2954 . . . . . 6 (𝜑 → ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1st𝐸)𝑢)))
154 id 22 . . . . . . . . . 10 (𝑥 = ⟨𝑓, 𝑢⟩ → 𝑥 = ⟨𝑓, 𝑢⟩)
155154, 154oveq12d 6567 . . . . . . . . 9 (𝑥 = ⟨𝑓, 𝑢⟩ → (𝑥(2nd𝐸)𝑥) = (⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩))
156 fveq2 6103 . . . . . . . . 9 (𝑥 = ⟨𝑓, 𝑢⟩ → ((Id‘(𝑄 ×c 𝐶))‘𝑥) = ((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩))
157155, 156fveq12d 6109 . . . . . . . 8 (𝑥 = ⟨𝑓, 𝑢⟩ → ((𝑥(2nd𝐸)𝑥)‘((Id‘(𝑄 ×c 𝐶))‘𝑥)) = ((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)))
158112fveq2d 6107 . . . . . . . 8 (𝑥 = ⟨𝑓, 𝑢⟩ → ((Id‘𝐷)‘((1st𝐸)‘𝑥)) = ((Id‘𝐷)‘(𝑓(1st𝐸)𝑢)))
159157, 158eqeq12d 2625 . . . . . . 7 (𝑥 = ⟨𝑓, 𝑢⟩ → (((𝑥(2nd𝐸)𝑥)‘((Id‘(𝑄 ×c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1st𝐸)‘𝑥)) ↔ ((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1st𝐸)𝑢))))
160159ralxp 5185 . . . . . 6 (∀𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))((𝑥(2nd𝐸)𝑥)‘((Id‘(𝑄 ×c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1st𝐸)‘𝑥)) ↔ ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)((⟨𝑓, 𝑢⟩(2nd𝐸)⟨𝑓, 𝑢⟩)‘((Id‘(𝑄 ×c 𝐶))‘⟨𝑓, 𝑢⟩)) = ((Id‘𝐷)‘(𝑓(1st𝐸)𝑢)))
161153, 160sylibr 223 . . . . 5 (𝜑 → ∀𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))((𝑥(2nd𝐸)𝑥)‘((Id‘(𝑄 ×c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1st𝐸)‘𝑥)))
162161r19.21bi 2916 . . . 4 ((𝜑𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) → ((𝑥(2nd𝐸)𝑥)‘((Id‘(𝑄 ×c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1st𝐸)‘𝑥)))
16323ad2ant1 1075 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝐶 ∈ Cat)
16433ad2ant1 1075 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝐷 ∈ Cat)
165 simp21 1087 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
166 1st2nd2 7096 . . . . . . . . 9 (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
167165, 166syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
168167, 165eqeltrrd 2689 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ⟨(1st𝑥), (2nd𝑥)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
169 opelxp 5070 . . . . . . 7 (⟨(1st𝑥), (2nd𝑥)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↔ ((1st𝑥) ∈ (𝐶 Func 𝐷) ∧ (2nd𝑥) ∈ (Base‘𝐶)))
170168, 169sylib 207 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st𝑥) ∈ (𝐶 Func 𝐷) ∧ (2nd𝑥) ∈ (Base‘𝐶)))
171 simp22 1088 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
172 1st2nd2 7096 . . . . . . . . 9 (𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
173171, 172syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑦 = ⟨(1st𝑦), (2nd𝑦)⟩)
174173, 171eqeltrrd 2689 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ⟨(1st𝑦), (2nd𝑦)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
175 opelxp 5070 . . . . . . 7 (⟨(1st𝑦), (2nd𝑦)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↔ ((1st𝑦) ∈ (𝐶 Func 𝐷) ∧ (2nd𝑦) ∈ (Base‘𝐶)))
176174, 175sylib 207 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st𝑦) ∈ (𝐶 Func 𝐷) ∧ (2nd𝑦) ∈ (Base‘𝐶)))
177 simp23 1089 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
178 1st2nd2 7096 . . . . . . . . 9 (𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
179177, 178syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
180179, 177eqeltrrd 2689 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ⟨(1st𝑧), (2nd𝑧)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))
181 opelxp 5070 . . . . . . 7 (⟨(1st𝑧), (2nd𝑧)⟩ ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↔ ((1st𝑧) ∈ (𝐶 Func 𝐷) ∧ (2nd𝑧) ∈ (Base‘𝐶)))
182180, 181sylib 207 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st𝑧) ∈ (𝐶 Func 𝐷) ∧ (2nd𝑧) ∈ (Base‘𝐶)))
183 simp3l 1082 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦))
18418, 21, 91, 5, 23, 165, 171xpchom 16643 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) = (((1st𝑥)(𝐶 Nat 𝐷)(1st𝑦)) × ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦))))
185183, 184eleqtrd 2690 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑓 ∈ (((1st𝑥)(𝐶 Nat 𝐷)(1st𝑦)) × ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦))))
186 1st2nd2 7096 . . . . . . . . 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 2689 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ⟨(1st𝑓), (2nd𝑓)⟩ ∈ (((1st𝑥)(𝐶 Nat 𝐷)(1st𝑦)) × ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦))))
189 opelxp 5070 . . . . . . 7 (⟨(1st𝑓), (2nd𝑓)⟩ ∈ (((1st𝑥)(𝐶 Nat 𝐷)(1st𝑦)) × ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦))) ↔ ((1st𝑓) ∈ ((1st𝑥)(𝐶 Nat 𝐷)(1st𝑦)) ∧ (2nd𝑓) ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦))))
190188, 189sylib 207 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st𝑓) ∈ ((1st𝑥)(𝐶 Nat 𝐷)(1st𝑦)) ∧ (2nd𝑓) ∈ ((2nd𝑥)(Hom ‘𝐶)(2nd𝑦))))
191 simp3r 1083 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))
19218, 21, 91, 5, 23, 171, 177xpchom 16643 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧) = (((1st𝑦)(𝐶 Nat 𝐷)(1st𝑧)) × ((2nd𝑦)(Hom ‘𝐶)(2nd𝑧))))
193191, 192eleqtrd 2690 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑔 ∈ (((1st𝑦)(𝐶 Nat 𝐷)(1st𝑧)) × ((2nd𝑦)(Hom ‘𝐶)(2nd𝑧))))
194 1st2nd2 7096 . . . . . . . . 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 2689 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ⟨(1st𝑔), (2nd𝑔)⟩ ∈ (((1st𝑦)(𝐶 Nat 𝐷)(1st𝑧)) × ((2nd𝑦)(Hom ‘𝐶)(2nd𝑧))))
197 opelxp 5070 . . . . . . 7 (⟨(1st𝑔), (2nd𝑔)⟩ ∈ (((1st𝑦)(𝐶 Nat 𝐷)(1st𝑧)) × ((2nd𝑦)(Hom ‘𝐶)(2nd𝑧))) ↔ ((1st𝑔) ∈ ((1st𝑦)(𝐶 Nat 𝐷)(1st𝑧)) ∧ (2nd𝑔) ∈ ((2nd𝑦)(Hom ‘𝐶)(2nd𝑧))))
198196, 197sylib 207 . . . . . 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 16684 . . . . 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 6567 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (𝑥(2nd𝐸)𝑧) = (⟨(1st𝑥), (2nd𝑥)⟩(2nd𝐸)⟨(1st𝑧), (2nd𝑧)⟩))
201167, 173opeq12d 4348 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ⟨𝑥, 𝑦⟩ = ⟨⟨(1st𝑥), (2nd𝑥)⟩, ⟨(1st𝑦), (2nd𝑦)⟩⟩)
202201, 179oveq12d 6567 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (⟨𝑥, 𝑦⟩(comp‘(𝑄 ×c 𝐶))𝑧) = (⟨⟨(1st𝑥), (2nd𝑥)⟩, ⟨(1st𝑦), (2nd𝑦)⟩⟩(comp‘(𝑄 ×c 𝐶))⟨(1st𝑧), (2nd𝑧)⟩))
203202, 195, 187oveq123d 6570 . . . . . 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 6109 . . . . 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 6107 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st𝐸)‘𝑥) = ((1st𝐸)‘⟨(1st𝑥), (2nd𝑥)⟩))
206173fveq2d 6107 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st𝐸)‘𝑦) = ((1st𝐸)‘⟨(1st𝑦), (2nd𝑦)⟩))
207205, 206opeq12d 4348 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ⟨((1st𝐸)‘𝑥), ((1st𝐸)‘𝑦)⟩ = ⟨((1st𝐸)‘⟨(1st𝑥), (2nd𝑥)⟩), ((1st𝐸)‘⟨(1st𝑦), (2nd𝑦)⟩)⟩)
208179fveq2d 6107 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st𝐸)‘𝑧) = ((1st𝐸)‘⟨(1st𝑧), (2nd𝑧)⟩))
209207, 208oveq12d 6567 . . . . . 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 6567 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (𝑦(2nd𝐸)𝑧) = (⟨(1st𝑦), (2nd𝑦)⟩(2nd𝐸)⟨(1st𝑧), (2nd𝑧)⟩))
211210, 195fveq12d 6109 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((𝑦(2nd𝐸)𝑧)‘𝑔) = ((⟨(1st𝑦), (2nd𝑦)⟩(2nd𝐸)⟨(1st𝑧), (2nd𝑧)⟩)‘⟨(1st𝑔), (2nd𝑔)⟩))
212167, 173oveq12d 6567 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (𝑥(2nd𝐸)𝑦) = (⟨(1st𝑥), (2nd𝑥)⟩(2nd𝐸)⟨(1st𝑦), (2nd𝑦)⟩))
213212, 187fveq12d 6109 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((𝑥(2nd𝐸)𝑦)‘𝑓) = ((⟨(1st𝑥), (2nd𝑥)⟩(2nd𝐸)⟨(1st𝑦), (2nd𝑦)⟩)‘⟨(1st𝑓), (2nd𝑓)⟩))
214209, 211, 213oveq123d 6570 . . . . 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 2654 . . . 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 16348 . . 3 (𝜑 → (1st𝐸)((𝑄 ×c 𝐶) Func 𝐷)(2nd𝐸))
217 df-br 4584 . . 3 ((1st𝐸)((𝑄 ×c 𝐶) Func 𝐷)(2nd𝐸) ↔ ⟨(1st𝐸), (2nd𝐸)⟩ ∈ ((𝑄 ×c 𝐶) Func 𝐷))
218216, 217sylib 207 . 2 (𝜑 → ⟨(1st𝐸), (2nd𝐸)⟩ ∈ ((𝑄 ×c 𝐶) Func 𝐷))
21917, 218eqeltrd 2688 1 (𝜑𝐸 ∈ ((𝑄 ×c 𝐶) Func 𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∀wral 2896  Vcvv 3173  ⦋csb 3499  ⟨cop 4131   class class class wbr 4583   × cxp 5036   ∘ ccom 5042  Rel wrel 5043   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551  1st c1st 7057  2nd c2nd 7058  Basecbs 15695  Hom chom 15779  compcco 15780  Catccat 16148  Idccid 16149   Func cfunc 16337   Nat cnat 16424   FuncCat cfuc 16425   ×c cxpc 16631   evalF cevlf 16672 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-fz 12198  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-hom 15793  df-cco 15794  df-cat 16152  df-cid 16153  df-func 16341  df-nat 16426  df-fuc 16427  df-xpc 16635  df-evlf 16676 This theorem is referenced by:  uncfcl  16698  uncf1  16699  uncf2  16700  yonedalem1  16735
 Copyright terms: Public domain W3C validator