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

Theorem prfcl 18091
Description: The pairing of functors 𝐹:𝐶𝐷 and 𝐺:𝐶𝐷 is a functor 𝐹, 𝐺⟩:𝐶⟶(𝐷 × 𝐸). (Contributed by Mario Carneiro, 12-Jan-2017.)
Hypotheses
Ref Expression
prfcl.p 𝑃 = (𝐹 ⟨,⟩F 𝐺)
prfcl.t 𝑇 = (𝐷 ×c 𝐸)
prfcl.c (𝜑𝐹 ∈ (𝐶 Func 𝐷))
prfcl.d (𝜑𝐺 ∈ (𝐶 Func 𝐸))
Assertion
Ref Expression
prfcl (𝜑𝑃 ∈ (𝐶 Func 𝑇))

Proof of Theorem prfcl
Dummy variables 𝑓 𝑔 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prfcl.p . . . 4 𝑃 = (𝐹 ⟨,⟩F 𝐺)
2 eqid 2736 . . . 4 (Base‘𝐶) = (Base‘𝐶)
3 eqid 2736 . . . 4 (Hom ‘𝐶) = (Hom ‘𝐶)
4 prfcl.c . . . 4 (𝜑𝐹 ∈ (𝐶 Func 𝐷))
5 prfcl.d . . . 4 (𝜑𝐺 ∈ (𝐶 Func 𝐸))
61, 2, 3, 4, 5prfval 18087 . . 3 (𝜑𝑃 = ⟨(𝑥 ∈ (Base‘𝐶) ↦ ⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ( ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩))⟩)
7 fvex 6855 . . . . . . 7 (Base‘𝐶) ∈ V
87mptex 7173 . . . . . 6 (𝑥 ∈ (Base‘𝐶) ↦ ⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩) ∈ V
97, 7mpoex 8012 . . . . . 6 (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ( ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩)) ∈ V
108, 9op1std 7931 . . . . 5 (𝑃 = ⟨(𝑥 ∈ (Base‘𝐶) ↦ ⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ( ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩))⟩ → (1st𝑃) = (𝑥 ∈ (Base‘𝐶) ↦ ⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩))
116, 10syl 17 . . . 4 (𝜑 → (1st𝑃) = (𝑥 ∈ (Base‘𝐶) ↦ ⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩))
128, 9op2ndd 7932 . . . . 5 (𝑃 = ⟨(𝑥 ∈ (Base‘𝐶) ↦ ⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ( ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩))⟩ → (2nd𝑃) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ( ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩)))
136, 12syl 17 . . . 4 (𝜑 → (2nd𝑃) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ( ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩)))
1411, 13opeq12d 4838 . . 3 (𝜑 → ⟨(1st𝑃), (2nd𝑃)⟩ = ⟨(𝑥 ∈ (Base‘𝐶) ↦ ⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ( ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩))⟩)
156, 14eqtr4d 2779 . 2 (𝜑𝑃 = ⟨(1st𝑃), (2nd𝑃)⟩)
16 prfcl.t . . . . 5 𝑇 = (𝐷 ×c 𝐸)
17 eqid 2736 . . . . 5 (Base‘𝐷) = (Base‘𝐷)
18 eqid 2736 . . . . 5 (Base‘𝐸) = (Base‘𝐸)
1916, 17, 18xpcbas 18066 . . . 4 ((Base‘𝐷) × (Base‘𝐸)) = (Base‘𝑇)
20 eqid 2736 . . . 4 (Hom ‘𝑇) = (Hom ‘𝑇)
21 eqid 2736 . . . 4 (Id‘𝐶) = (Id‘𝐶)
22 eqid 2736 . . . 4 (Id‘𝑇) = (Id‘𝑇)
23 eqid 2736 . . . 4 (comp‘𝐶) = (comp‘𝐶)
24 eqid 2736 . . . 4 (comp‘𝑇) = (comp‘𝑇)
25 funcrcl 17749 . . . . . 6 (𝐹 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
264, 25syl 17 . . . . 5 (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
2726simpld 495 . . . 4 (𝜑𝐶 ∈ Cat)
2826simprd 496 . . . . 5 (𝜑𝐷 ∈ Cat)
29 funcrcl 17749 . . . . . . 7 (𝐺 ∈ (𝐶 Func 𝐸) → (𝐶 ∈ Cat ∧ 𝐸 ∈ Cat))
305, 29syl 17 . . . . . 6 (𝜑 → (𝐶 ∈ Cat ∧ 𝐸 ∈ Cat))
3130simprd 496 . . . . 5 (𝜑𝐸 ∈ Cat)
3216, 28, 31xpccat 18078 . . . 4 (𝜑𝑇 ∈ Cat)
33 relfunc 17748 . . . . . . . . 9 Rel (𝐶 Func 𝐷)
34 1st2ndbr 7974 . . . . . . . . 9 ((Rel (𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
3533, 4, 34sylancr 587 . . . . . . . 8 (𝜑 → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
362, 17, 35funcf1 17752 . . . . . . 7 (𝜑 → (1st𝐹):(Base‘𝐶)⟶(Base‘𝐷))
3736ffvelcdmda 7035 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((1st𝐹)‘𝑥) ∈ (Base‘𝐷))
38 relfunc 17748 . . . . . . . . 9 Rel (𝐶 Func 𝐸)
39 1st2ndbr 7974 . . . . . . . . 9 ((Rel (𝐶 Func 𝐸) ∧ 𝐺 ∈ (𝐶 Func 𝐸)) → (1st𝐺)(𝐶 Func 𝐸)(2nd𝐺))
4038, 5, 39sylancr 587 . . . . . . . 8 (𝜑 → (1st𝐺)(𝐶 Func 𝐸)(2nd𝐺))
412, 18, 40funcf1 17752 . . . . . . 7 (𝜑 → (1st𝐺):(Base‘𝐶)⟶(Base‘𝐸))
4241ffvelcdmda 7035 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((1st𝐺)‘𝑥) ∈ (Base‘𝐸))
4337, 42opelxpd 5671 . . . . 5 ((𝜑𝑥 ∈ (Base‘𝐶)) → ⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩ ∈ ((Base‘𝐷) × (Base‘𝐸)))
4411, 43fmpt3d 7064 . . . 4 (𝜑 → (1st𝑃):(Base‘𝐶)⟶((Base‘𝐷) × (Base‘𝐸)))
45 eqid 2736 . . . . . 6 (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ( ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩)) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ( ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩))
46 ovex 7390 . . . . . . 7 (𝑥(Hom ‘𝐶)𝑦) ∈ V
4746mptex 7173 . . . . . 6 ( ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩) ∈ V
4845, 47fnmpoi 8002 . . . . 5 (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ( ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩)) Fn ((Base‘𝐶) × (Base‘𝐶))
4913fneq1d 6595 . . . . 5 (𝜑 → ((2nd𝑃) Fn ((Base‘𝐶) × (Base‘𝐶)) ↔ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ( ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩)) Fn ((Base‘𝐶) × (Base‘𝐶))))
5048, 49mpbiri 257 . . . 4 (𝜑 → (2nd𝑃) Fn ((Base‘𝐶) × (Base‘𝐶)))
5113oveqd 7374 . . . . . 6 (𝜑 → (𝑥(2nd𝑃)𝑦) = (𝑥(𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ( ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩))𝑦))
5245ovmpt4g 7502 . . . . . . 7 ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ ( ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩) ∈ V) → (𝑥(𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ( ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩))𝑦) = ( ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩))
5347, 52mp3an3 1450 . . . . . 6 ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑥(𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ( ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩))𝑦) = ( ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩))
5451, 53sylan9eq 2796 . . . . 5 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd𝑃)𝑦) = ( ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩))
55 eqid 2736 . . . . . . . . 9 (Hom ‘𝐷) = (Hom ‘𝐷)
5635adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
57 simprl 769 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑥 ∈ (Base‘𝐶))
58 simprr 771 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑦 ∈ (Base‘𝐶))
592, 3, 55, 56, 57, 58funcf2 17754 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
6059ffvelcdmda 7035 . . . . . . 7 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑥(2nd𝐹)𝑦)‘) ∈ (((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
61 eqid 2736 . . . . . . . . 9 (Hom ‘𝐸) = (Hom ‘𝐸)
6240adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st𝐺)(𝐶 Func 𝐸)(2nd𝐺))
632, 3, 61, 62, 57, 58funcf2 17754 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd𝐺)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st𝐺)‘𝑥)(Hom ‘𝐸)((1st𝐺)‘𝑦)))
6463ffvelcdmda 7035 . . . . . . 7 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑥(2nd𝐺)𝑦)‘) ∈ (((1st𝐺)‘𝑥)(Hom ‘𝐸)((1st𝐺)‘𝑦)))
6560, 64opelxpd 5671 . . . . . 6 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ ∈ (𝑥(Hom ‘𝐶)𝑦)) → ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩ ∈ ((((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)) × (((1st𝐺)‘𝑥)(Hom ‘𝐸)((1st𝐺)‘𝑦))))
664adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐹 ∈ (𝐶 Func 𝐷))
675adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐺 ∈ (𝐶 Func 𝐸))
681, 2, 3, 66, 67, 57prf1 18088 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st𝑃)‘𝑥) = ⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩)
691, 2, 3, 66, 67, 58prf1 18088 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st𝑃)‘𝑦) = ⟨((1st𝐹)‘𝑦), ((1st𝐺)‘𝑦)⟩)
7068, 69oveq12d 7375 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (((1st𝑃)‘𝑥)(Hom ‘𝑇)((1st𝑃)‘𝑦)) = (⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩(Hom ‘𝑇)⟨((1st𝐹)‘𝑦), ((1st𝐺)‘𝑦)⟩))
7137adantrr 715 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st𝐹)‘𝑥) ∈ (Base‘𝐷))
7242adantrr 715 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st𝐺)‘𝑥) ∈ (Base‘𝐸))
7336ffvelcdmda 7035 . . . . . . . . . 10 ((𝜑𝑦 ∈ (Base‘𝐶)) → ((1st𝐹)‘𝑦) ∈ (Base‘𝐷))
7473adantrl 714 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st𝐹)‘𝑦) ∈ (Base‘𝐷))
7541ffvelcdmda 7035 . . . . . . . . . 10 ((𝜑𝑦 ∈ (Base‘𝐶)) → ((1st𝐺)‘𝑦) ∈ (Base‘𝐸))
7675adantrl 714 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st𝐺)‘𝑦) ∈ (Base‘𝐸))
7716, 17, 18, 55, 61, 71, 72, 74, 76, 20xpchom2 18074 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩(Hom ‘𝑇)⟨((1st𝐹)‘𝑦), ((1st𝐺)‘𝑦)⟩) = ((((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)) × (((1st𝐺)‘𝑥)(Hom ‘𝐸)((1st𝐺)‘𝑦))))
7870, 77eqtrd 2776 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (((1st𝑃)‘𝑥)(Hom ‘𝑇)((1st𝑃)‘𝑦)) = ((((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)) × (((1st𝐺)‘𝑥)(Hom ‘𝐸)((1st𝐺)‘𝑦))))
7978adantr 481 . . . . . 6 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ ∈ (𝑥(Hom ‘𝐶)𝑦)) → (((1st𝑃)‘𝑥)(Hom ‘𝑇)((1st𝑃)‘𝑦)) = ((((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)) × (((1st𝐺)‘𝑥)(Hom ‘𝐸)((1st𝐺)‘𝑦))))
8065, 79eleqtrrd 2841 . . . . 5 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ ∈ (𝑥(Hom ‘𝐶)𝑦)) → ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩ ∈ (((1st𝑃)‘𝑥)(Hom ‘𝑇)((1st𝑃)‘𝑦)))
8154, 80fmpt3d 7064 . . . 4 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd𝑃)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st𝑃)‘𝑥)(Hom ‘𝑇)((1st𝑃)‘𝑦)))
82 eqid 2736 . . . . . . 7 (Id‘𝐷) = (Id‘𝐷)
8335adantr 481 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝐶)) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
84 simpr 485 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
852, 21, 82, 83, 84funcid 17756 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd𝐹)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘((1st𝐹)‘𝑥)))
86 eqid 2736 . . . . . . 7 (Id‘𝐸) = (Id‘𝐸)
8740adantr 481 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝐶)) → (1st𝐺)(𝐶 Func 𝐸)(2nd𝐺))
882, 21, 86, 87, 84funcid 17756 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd𝐺)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐸)‘((1st𝐺)‘𝑥)))
8985, 88opeq12d 4838 . . . . 5 ((𝜑𝑥 ∈ (Base‘𝐶)) → ⟨((𝑥(2nd𝐹)𝑥)‘((Id‘𝐶)‘𝑥)), ((𝑥(2nd𝐺)𝑥)‘((Id‘𝐶)‘𝑥))⟩ = ⟨((Id‘𝐷)‘((1st𝐹)‘𝑥)), ((Id‘𝐸)‘((1st𝐺)‘𝑥))⟩)
904adantr 481 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝐹 ∈ (𝐶 Func 𝐷))
915adantr 481 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝐺 ∈ (𝐶 Func 𝐸))
9227adantr 481 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝐶 ∈ Cat)
932, 3, 21, 92, 84catidcl 17562 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘𝑥) ∈ (𝑥(Hom ‘𝐶)𝑥))
941, 2, 3, 90, 91, 84, 84, 93prf2 18090 . . . . 5 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd𝑃)𝑥)‘((Id‘𝐶)‘𝑥)) = ⟨((𝑥(2nd𝐹)𝑥)‘((Id‘𝐶)‘𝑥)), ((𝑥(2nd𝐺)𝑥)‘((Id‘𝐶)‘𝑥))⟩)
951, 2, 3, 90, 91, 84prf1 18088 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((1st𝑃)‘𝑥) = ⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩)
9695fveq2d 6846 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((Id‘𝑇)‘((1st𝑃)‘𝑥)) = ((Id‘𝑇)‘⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩))
9728adantr 481 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝐷 ∈ Cat)
9831adantr 481 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝐸 ∈ Cat)
9916, 97, 98, 17, 18, 82, 86, 22, 37, 42xpcid 18077 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((Id‘𝑇)‘⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩) = ⟨((Id‘𝐷)‘((1st𝐹)‘𝑥)), ((Id‘𝐸)‘((1st𝐺)‘𝑥))⟩)
10096, 99eqtrd 2776 . . . . 5 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((Id‘𝑇)‘((1st𝑃)‘𝑥)) = ⟨((Id‘𝐷)‘((1st𝐹)‘𝑥)), ((Id‘𝐸)‘((1st𝐺)‘𝑥))⟩)
10189, 94, 1003eqtr4d 2786 . . . 4 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd𝑃)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝑇)‘((1st𝑃)‘𝑥)))
102 eqid 2736 . . . . . . 7 (comp‘𝐷) = (comp‘𝐷)
103353ad2ant1 1133 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
104 simp21 1206 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑥 ∈ (Base‘𝐶))
105 simp22 1207 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑦 ∈ (Base‘𝐶))
106 simp23 1208 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑧 ∈ (Base‘𝐶))
107 simp3l 1201 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
108 simp3r 1202 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))
1092, 3, 23, 102, 103, 104, 105, 106, 107, 108funcco 17757 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd𝐹)𝑧)‘𝑔)(⟨((1st𝐹)‘𝑥), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑥(2nd𝐹)𝑦)‘𝑓)))
110 eqid 2736 . . . . . . 7 (comp‘𝐸) = (comp‘𝐸)
11153ad2ant1 1133 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝐺 ∈ (𝐶 Func 𝐸))
11238, 111, 39sylancr 587 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1st𝐺)(𝐶 Func 𝐸)(2nd𝐺))
1132, 3, 23, 110, 112, 104, 105, 106, 107, 108funcco 17757 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd𝐺)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd𝐺)𝑧)‘𝑔)(⟨((1st𝐺)‘𝑥), ((1st𝐺)‘𝑦)⟩(comp‘𝐸)((1st𝐺)‘𝑧))((𝑥(2nd𝐺)𝑦)‘𝑓)))
114109, 113opeq12d 4838 . . . . 5 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ⟨((𝑥(2nd𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)), ((𝑥(2nd𝐺)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))⟩ = ⟨(((𝑦(2nd𝐹)𝑧)‘𝑔)(⟨((1st𝐹)‘𝑥), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑥(2nd𝐹)𝑦)‘𝑓)), (((𝑦(2nd𝐺)𝑧)‘𝑔)(⟨((1st𝐺)‘𝑥), ((1st𝐺)‘𝑦)⟩(comp‘𝐸)((1st𝐺)‘𝑧))((𝑥(2nd𝐺)𝑦)‘𝑓))⟩)
11543ad2ant1 1133 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝐹 ∈ (𝐶 Func 𝐷))
116273ad2ant1 1133 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝐶 ∈ Cat)
1172, 3, 23, 116, 104, 105, 106, 107, 108catcocl 17565 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧))
1181, 2, 3, 115, 111, 104, 106, 117prf2 18090 . . . . 5 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd𝑃)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = ⟨((𝑥(2nd𝐹)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)), ((𝑥(2nd𝐺)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓))⟩)
1191, 2, 3, 115, 111, 104prf1 18088 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st𝑃)‘𝑥) = ⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩)
1201, 2, 3, 115, 111, 105prf1 18088 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st𝑃)‘𝑦) = ⟨((1st𝐹)‘𝑦), ((1st𝐺)‘𝑦)⟩)
121119, 120opeq12d 4838 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ⟨((1st𝑃)‘𝑥), ((1st𝑃)‘𝑦)⟩ = ⟨⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩, ⟨((1st𝐹)‘𝑦), ((1st𝐺)‘𝑦)⟩⟩)
1221, 2, 3, 115, 111, 106prf1 18088 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st𝑃)‘𝑧) = ⟨((1st𝐹)‘𝑧), ((1st𝐺)‘𝑧)⟩)
123121, 122oveq12d 7375 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (⟨((1st𝑃)‘𝑥), ((1st𝑃)‘𝑦)⟩(comp‘𝑇)((1st𝑃)‘𝑧)) = (⟨⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩, ⟨((1st𝐹)‘𝑦), ((1st𝐺)‘𝑦)⟩⟩(comp‘𝑇)⟨((1st𝐹)‘𝑧), ((1st𝐺)‘𝑧)⟩))
1241, 2, 3, 115, 111, 105, 106, 108prf2 18090 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2nd𝑃)𝑧)‘𝑔) = ⟨((𝑦(2nd𝐹)𝑧)‘𝑔), ((𝑦(2nd𝐺)𝑧)‘𝑔)⟩)
1251, 2, 3, 115, 111, 104, 105, 107prf2 18090 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd𝑃)𝑦)‘𝑓) = ⟨((𝑥(2nd𝐹)𝑦)‘𝑓), ((𝑥(2nd𝐺)𝑦)‘𝑓)⟩)
126123, 124, 125oveq123d 7378 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑦(2nd𝑃)𝑧)‘𝑔)(⟨((1st𝑃)‘𝑥), ((1st𝑃)‘𝑦)⟩(comp‘𝑇)((1st𝑃)‘𝑧))((𝑥(2nd𝑃)𝑦)‘𝑓)) = (⟨((𝑦(2nd𝐹)𝑧)‘𝑔), ((𝑦(2nd𝐺)𝑧)‘𝑔)⟩(⟨⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩, ⟨((1st𝐹)‘𝑦), ((1st𝐺)‘𝑦)⟩⟩(comp‘𝑇)⟨((1st𝐹)‘𝑧), ((1st𝐺)‘𝑧)⟩)⟨((𝑥(2nd𝐹)𝑦)‘𝑓), ((𝑥(2nd𝐺)𝑦)‘𝑓)⟩))
127363ad2ant1 1133 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1st𝐹):(Base‘𝐶)⟶(Base‘𝐷))
128127, 104ffvelcdmd 7036 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st𝐹)‘𝑥) ∈ (Base‘𝐷))
129413ad2ant1 1133 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1st𝐺):(Base‘𝐶)⟶(Base‘𝐸))
130129, 104ffvelcdmd 7036 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st𝐺)‘𝑥) ∈ (Base‘𝐸))
131127, 105ffvelcdmd 7036 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st𝐹)‘𝑦) ∈ (Base‘𝐷))
132129, 105ffvelcdmd 7036 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st𝐺)‘𝑦) ∈ (Base‘𝐸))
133127, 106ffvelcdmd 7036 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st𝐹)‘𝑧) ∈ (Base‘𝐷))
134129, 106ffvelcdmd 7036 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st𝐺)‘𝑧) ∈ (Base‘𝐸))
1352, 3, 55, 103, 104, 105funcf2 17754 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑥(2nd𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
136135, 107ffvelcdmd 7036 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd𝐹)𝑦)‘𝑓) ∈ (((1st𝐹)‘𝑥)(Hom ‘𝐷)((1st𝐹)‘𝑦)))
1372, 3, 61, 112, 104, 105funcf2 17754 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑥(2nd𝐺)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st𝐺)‘𝑥)(Hom ‘𝐸)((1st𝐺)‘𝑦)))
138137, 107ffvelcdmd 7036 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd𝐺)𝑦)‘𝑓) ∈ (((1st𝐺)‘𝑥)(Hom ‘𝐸)((1st𝐺)‘𝑦)))
1392, 3, 55, 103, 105, 106funcf2 17754 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑦(2nd𝐹)𝑧):(𝑦(Hom ‘𝐶)𝑧)⟶(((1st𝐹)‘𝑦)(Hom ‘𝐷)((1st𝐹)‘𝑧)))
140139, 108ffvelcdmd 7036 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2nd𝐹)𝑧)‘𝑔) ∈ (((1st𝐹)‘𝑦)(Hom ‘𝐷)((1st𝐹)‘𝑧)))
1412, 3, 61, 112, 105, 106funcf2 17754 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑦(2nd𝐺)𝑧):(𝑦(Hom ‘𝐶)𝑧)⟶(((1st𝐺)‘𝑦)(Hom ‘𝐸)((1st𝐺)‘𝑧)))
142141, 108ffvelcdmd 7036 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2nd𝐺)𝑧)‘𝑔) ∈ (((1st𝐺)‘𝑦)(Hom ‘𝐸)((1st𝐺)‘𝑧)))
14316, 17, 18, 55, 61, 128, 130, 131, 132, 102, 110, 24, 133, 134, 136, 138, 140, 142xpcco2 18075 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (⟨((𝑦(2nd𝐹)𝑧)‘𝑔), ((𝑦(2nd𝐺)𝑧)‘𝑔)⟩(⟨⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩, ⟨((1st𝐹)‘𝑦), ((1st𝐺)‘𝑦)⟩⟩(comp‘𝑇)⟨((1st𝐹)‘𝑧), ((1st𝐺)‘𝑧)⟩)⟨((𝑥(2nd𝐹)𝑦)‘𝑓), ((𝑥(2nd𝐺)𝑦)‘𝑓)⟩) = ⟨(((𝑦(2nd𝐹)𝑧)‘𝑔)(⟨((1st𝐹)‘𝑥), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑥(2nd𝐹)𝑦)‘𝑓)), (((𝑦(2nd𝐺)𝑧)‘𝑔)(⟨((1st𝐺)‘𝑥), ((1st𝐺)‘𝑦)⟩(comp‘𝐸)((1st𝐺)‘𝑧))((𝑥(2nd𝐺)𝑦)‘𝑓))⟩)
144126, 143eqtrd 2776 . . . . 5 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑦(2nd𝑃)𝑧)‘𝑔)(⟨((1st𝑃)‘𝑥), ((1st𝑃)‘𝑦)⟩(comp‘𝑇)((1st𝑃)‘𝑧))((𝑥(2nd𝑃)𝑦)‘𝑓)) = ⟨(((𝑦(2nd𝐹)𝑧)‘𝑔)(⟨((1st𝐹)‘𝑥), ((1st𝐹)‘𝑦)⟩(comp‘𝐷)((1st𝐹)‘𝑧))((𝑥(2nd𝐹)𝑦)‘𝑓)), (((𝑦(2nd𝐺)𝑧)‘𝑔)(⟨((1st𝐺)‘𝑥), ((1st𝐺)‘𝑦)⟩(comp‘𝐸)((1st𝐺)‘𝑧))((𝑥(2nd𝐺)𝑦)‘𝑓))⟩)
145114, 118, 1443eqtr4d 2786 . . . 4 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd𝑃)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd𝑃)𝑧)‘𝑔)(⟨((1st𝑃)‘𝑥), ((1st𝑃)‘𝑦)⟩(comp‘𝑇)((1st𝑃)‘𝑧))((𝑥(2nd𝑃)𝑦)‘𝑓)))
1462, 19, 3, 20, 21, 22, 23, 24, 27, 32, 44, 50, 81, 101, 145isfuncd 17751 . . 3 (𝜑 → (1st𝑃)(𝐶 Func 𝑇)(2nd𝑃))
147 df-br 5106 . . 3 ((1st𝑃)(𝐶 Func 𝑇)(2nd𝑃) ↔ ⟨(1st𝑃), (2nd𝑃)⟩ ∈ (𝐶 Func 𝑇))
148146, 147sylib 217 . 2 (𝜑 → ⟨(1st𝑃), (2nd𝑃)⟩ ∈ (𝐶 Func 𝑇))
14915, 148eqeltrd 2838 1 (𝜑𝑃 ∈ (𝐶 Func 𝑇))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1087   = wceq 1541  wcel 2106  Vcvv 3445  cop 4592   class class class wbr 5105  cmpt 5188   × cxp 5631  Rel wrel 5638   Fn wfn 6491  wf 6492  cfv 6496  (class class class)co 7357  cmpo 7359  1st c1st 7919  2nd c2nd 7920  Basecbs 17083  Hom chom 17144  compcco 17145  Catccat 17544  Idccid 17545   Func cfunc 17740   ×c cxpc 18056   ⟨,⟩F cprf 18059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-map 8767  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-fz 13425  df-struct 17019  df-slot 17054  df-ndx 17066  df-base 17084  df-hom 17157  df-cco 17158  df-cat 17548  df-cid 17549  df-func 17744  df-xpc 18060  df-prf 18063
This theorem is referenced by:  prf1st  18092  prf2nd  18093  uncfcl  18124  uncf1  18125  uncf2  18126  yonedalem1  18161  yonedalem21  18162  yonedalem22  18167
  Copyright terms: Public domain W3C validator