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

Theorem prf2nd 17445
 Description: Cancellation of pairing with second projection. (Contributed by Mario Carneiro, 12-Jan-2017.)
Hypotheses
Ref Expression
prf1st.p 𝑃 = (𝐹 ⟨,⟩F 𝐺)
prf1st.c (𝜑𝐹 ∈ (𝐶 Func 𝐷))
prf1st.d (𝜑𝐺 ∈ (𝐶 Func 𝐸))
Assertion
Ref Expression
prf2nd (𝜑 → ((𝐷 2ndF 𝐸) ∘func 𝑃) = 𝐺)

Proof of Theorem prf2nd
Dummy variables 𝑓 𝑥 𝑦 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2826 . . . . . . 7 (𝐷 ×c 𝐸) = (𝐷 ×c 𝐸)
2 eqid 2826 . . . . . . . 8 (Base‘𝐷) = (Base‘𝐷)
3 eqid 2826 . . . . . . . 8 (Base‘𝐸) = (Base‘𝐸)
41, 2, 3xpcbas 17418 . . . . . . 7 ((Base‘𝐷) × (Base‘𝐸)) = (Base‘(𝐷 ×c 𝐸))
5 eqid 2826 . . . . . . 7 (Hom ‘(𝐷 ×c 𝐸)) = (Hom ‘(𝐷 ×c 𝐸))
6 prf1st.c . . . . . . . . . 10 (𝜑𝐹 ∈ (𝐶 Func 𝐷))
7 funcrcl 17123 . . . . . . . . . 10 (𝐹 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
86, 7syl 17 . . . . . . . . 9 (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
98simprd 496 . . . . . . . 8 (𝜑𝐷 ∈ Cat)
109adantr 481 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝐷 ∈ Cat)
11 prf1st.d . . . . . . . . . 10 (𝜑𝐺 ∈ (𝐶 Func 𝐸))
12 funcrcl 17123 . . . . . . . . . 10 (𝐺 ∈ (𝐶 Func 𝐸) → (𝐶 ∈ Cat ∧ 𝐸 ∈ Cat))
1311, 12syl 17 . . . . . . . . 9 (𝜑 → (𝐶 ∈ Cat ∧ 𝐸 ∈ Cat))
1413simprd 496 . . . . . . . 8 (𝜑𝐸 ∈ Cat)
1514adantr 481 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝐶)) → 𝐸 ∈ Cat)
16 eqid 2826 . . . . . . 7 (𝐷 2ndF 𝐸) = (𝐷 2ndF 𝐸)
17 eqid 2826 . . . . . . . . . 10 (Base‘𝐶) = (Base‘𝐶)
18 relfunc 17122 . . . . . . . . . . 11 Rel (𝐶 Func 𝐷)
19 1st2ndbr 7732 . . . . . . . . . . 11 ((Rel (𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
2018, 6, 19sylancr 587 . . . . . . . . . 10 (𝜑 → (1st𝐹)(𝐶 Func 𝐷)(2nd𝐹))
2117, 2, 20funcf1 17126 . . . . . . . . 9 (𝜑 → (1st𝐹):(Base‘𝐶)⟶(Base‘𝐷))
2221ffvelrnda 6847 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((1st𝐹)‘𝑥) ∈ (Base‘𝐷))
23 relfunc 17122 . . . . . . . . . . 11 Rel (𝐶 Func 𝐸)
24 1st2ndbr 7732 . . . . . . . . . . 11 ((Rel (𝐶 Func 𝐸) ∧ 𝐺 ∈ (𝐶 Func 𝐸)) → (1st𝐺)(𝐶 Func 𝐸)(2nd𝐺))
2523, 11, 24sylancr 587 . . . . . . . . . 10 (𝜑 → (1st𝐺)(𝐶 Func 𝐸)(2nd𝐺))
2617, 3, 25funcf1 17126 . . . . . . . . 9 (𝜑 → (1st𝐺):(Base‘𝐶)⟶(Base‘𝐸))
2726ffvelrnda 6847 . . . . . . . 8 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((1st𝐺)‘𝑥) ∈ (Base‘𝐸))
2822, 27opelxpd 5592 . . . . . . 7 ((𝜑𝑥 ∈ (Base‘𝐶)) → ⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩ ∈ ((Base‘𝐷) × (Base‘𝐸)))
291, 4, 5, 10, 15, 16, 282ndf1 17435 . . . . . 6 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((1st ‘(𝐷 2ndF 𝐸))‘⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩) = (2nd ‘⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩))
30 fvex 6680 . . . . . . 7 ((1st𝐹)‘𝑥) ∈ V
31 fvex 6680 . . . . . . 7 ((1st𝐺)‘𝑥) ∈ V
3230, 31op2nd 7689 . . . . . 6 (2nd ‘⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩) = ((1st𝐺)‘𝑥)
3329, 32syl6eq 2877 . . . . 5 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((1st ‘(𝐷 2ndF 𝐸))‘⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩) = ((1st𝐺)‘𝑥))
3433mpteq2dva 5158 . . . 4 (𝜑 → (𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘(𝐷 2ndF 𝐸))‘⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩)) = (𝑥 ∈ (Base‘𝐶) ↦ ((1st𝐺)‘𝑥)))
35 prf1st.p . . . . . . 7 𝑃 = (𝐹 ⟨,⟩F 𝐺)
36 eqid 2826 . . . . . . 7 (Hom ‘𝐶) = (Hom ‘𝐶)
3735, 17, 36, 6, 11prfval 17439 . . . . . 6 (𝜑𝑃 = ⟨(𝑥 ∈ (Base‘𝐶) ↦ ⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ( ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩))⟩)
38 fvex 6680 . . . . . . . 8 (Base‘𝐶) ∈ V
3938mptex 6981 . . . . . . 7 (𝑥 ∈ (Base‘𝐶) ↦ ⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩) ∈ V
4038, 38mpoex 7768 . . . . . . 7 (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ( ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩)) ∈ V
4139, 40op1std 7690 . . . . . 6 (𝑃 = ⟨(𝑥 ∈ (Base‘𝐶) ↦ ⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ( ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ⟨((𝑥(2nd𝐹)𝑦)‘), ((𝑥(2nd𝐺)𝑦)‘)⟩))⟩ → (1st𝑃) = (𝑥 ∈ (Base‘𝐶) ↦ ⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩))
4237, 41syl 17 . . . . 5 (𝜑 → (1st𝑃) = (𝑥 ∈ (Base‘𝐶) ↦ ⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩))
43 relfunc 17122 . . . . . . . 8 Rel ((𝐷 ×c 𝐸) Func 𝐸)
441, 9, 14, 162ndfcl 17438 . . . . . . . 8 (𝜑 → (𝐷 2ndF 𝐸) ∈ ((𝐷 ×c 𝐸) Func 𝐸))
45 1st2ndbr 7732 . . . . . . . 8 ((Rel ((𝐷 ×c 𝐸) Func 𝐸) ∧ (𝐷 2ndF 𝐸) ∈ ((𝐷 ×c 𝐸) Func 𝐸)) → (1st ‘(𝐷 2ndF 𝐸))((𝐷 ×c 𝐸) Func 𝐸)(2nd ‘(𝐷 2ndF 𝐸)))
4643, 44, 45sylancr 587 . . . . . . 7 (𝜑 → (1st ‘(𝐷 2ndF 𝐸))((𝐷 ×c 𝐸) Func 𝐸)(2nd ‘(𝐷 2ndF 𝐸)))
474, 3, 46funcf1 17126 . . . . . 6 (𝜑 → (1st ‘(𝐷 2ndF 𝐸)):((Base‘𝐷) × (Base‘𝐸))⟶(Base‘𝐸))
4847feqmptd 6730 . . . . 5 (𝜑 → (1st ‘(𝐷 2ndF 𝐸)) = (𝑢 ∈ ((Base‘𝐷) × (Base‘𝐸)) ↦ ((1st ‘(𝐷 2ndF 𝐸))‘𝑢)))
49 fveq2 6667 . . . . 5 (𝑢 = ⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩ → ((1st ‘(𝐷 2ndF 𝐸))‘𝑢) = ((1st ‘(𝐷 2ndF 𝐸))‘⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩))
5028, 42, 48, 49fmptco 6887 . . . 4 (𝜑 → ((1st ‘(𝐷 2ndF 𝐸)) ∘ (1st𝑃)) = (𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘(𝐷 2ndF 𝐸))‘⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩)))
5126feqmptd 6730 . . . 4 (𝜑 → (1st𝐺) = (𝑥 ∈ (Base‘𝐶) ↦ ((1st𝐺)‘𝑥)))
5234, 50, 513eqtr4d 2871 . . 3 (𝜑 → ((1st ‘(𝐷 2ndF 𝐸)) ∘ (1st𝑃)) = (1st𝐺))
539ad2antrr 722 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝐷 ∈ Cat)
5414ad2antrr 722 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝐸 ∈ Cat)
55 relfunc 17122 . . . . . . . . . . . . . . . 16 Rel (𝐶 Func (𝐷 ×c 𝐸))
5635, 1, 6, 11prfcl 17443 . . . . . . . . . . . . . . . 16 (𝜑𝑃 ∈ (𝐶 Func (𝐷 ×c 𝐸)))
57 1st2ndbr 7732 . . . . . . . . . . . . . . . 16 ((Rel (𝐶 Func (𝐷 ×c 𝐸)) ∧ 𝑃 ∈ (𝐶 Func (𝐷 ×c 𝐸))) → (1st𝑃)(𝐶 Func (𝐷 ×c 𝐸))(2nd𝑃))
5855, 56, 57sylancr 587 . . . . . . . . . . . . . . 15 (𝜑 → (1st𝑃)(𝐶 Func (𝐷 ×c 𝐸))(2nd𝑃))
5917, 4, 58funcf1 17126 . . . . . . . . . . . . . 14 (𝜑 → (1st𝑃):(Base‘𝐶)⟶((Base‘𝐷) × (Base‘𝐸)))
6059ffvelrnda 6847 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (Base‘𝐶)) → ((1st𝑃)‘𝑥) ∈ ((Base‘𝐷) × (Base‘𝐸)))
6160adantrr 713 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st𝑃)‘𝑥) ∈ ((Base‘𝐷) × (Base‘𝐸)))
6261adantr 481 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((1st𝑃)‘𝑥) ∈ ((Base‘𝐷) × (Base‘𝐸)))
6359ffvelrnda 6847 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ (Base‘𝐶)) → ((1st𝑃)‘𝑦) ∈ ((Base‘𝐷) × (Base‘𝐸)))
6463adantrl 712 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st𝑃)‘𝑦) ∈ ((Base‘𝐷) × (Base‘𝐸)))
6564adantr 481 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((1st𝑃)‘𝑦) ∈ ((Base‘𝐷) × (Base‘𝐸)))
661, 4, 5, 53, 54, 16, 62, 652ndf2 17436 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (((1st𝑃)‘𝑥)(2nd ‘(𝐷 2ndF 𝐸))((1st𝑃)‘𝑦)) = (2nd ↾ (((1st𝑃)‘𝑥)(Hom ‘(𝐷 ×c 𝐸))((1st𝑃)‘𝑦))))
6766fveq1d 6669 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((((1st𝑃)‘𝑥)(2nd ‘(𝐷 2ndF 𝐸))((1st𝑃)‘𝑦))‘((𝑥(2nd𝑃)𝑦)‘𝑓)) = ((2nd ↾ (((1st𝑃)‘𝑥)(Hom ‘(𝐷 ×c 𝐸))((1st𝑃)‘𝑦)))‘((𝑥(2nd𝑃)𝑦)‘𝑓)))
6858adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st𝑃)(𝐶 Func (𝐷 ×c 𝐸))(2nd𝑃))
69 simprl 767 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑥 ∈ (Base‘𝐶))
70 simprr 769 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑦 ∈ (Base‘𝐶))
7117, 36, 5, 68, 69, 70funcf2 17128 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd𝑃)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st𝑃)‘𝑥)(Hom ‘(𝐷 ×c 𝐸))((1st𝑃)‘𝑦)))
7271ffvelrnda 6847 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑥(2nd𝑃)𝑦)‘𝑓) ∈ (((1st𝑃)‘𝑥)(Hom ‘(𝐷 ×c 𝐸))((1st𝑃)‘𝑦)))
7372fvresd 6687 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((2nd ↾ (((1st𝑃)‘𝑥)(Hom ‘(𝐷 ×c 𝐸))((1st𝑃)‘𝑦)))‘((𝑥(2nd𝑃)𝑦)‘𝑓)) = (2nd ‘((𝑥(2nd𝑃)𝑦)‘𝑓)))
746ad2antrr 722 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝐹 ∈ (𝐶 Func 𝐷))
7511ad2antrr 722 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝐺 ∈ (𝐶 Func 𝐸))
7669adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑥 ∈ (Base‘𝐶))
7770adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑦 ∈ (Base‘𝐶))
78 simpr 485 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
7935, 17, 36, 74, 75, 76, 77, 78prf2 17442 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑥(2nd𝑃)𝑦)‘𝑓) = ⟨((𝑥(2nd𝐹)𝑦)‘𝑓), ((𝑥(2nd𝐺)𝑦)‘𝑓)⟩)
8079fveq2d 6671 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (2nd ‘((𝑥(2nd𝑃)𝑦)‘𝑓)) = (2nd ‘⟨((𝑥(2nd𝐹)𝑦)‘𝑓), ((𝑥(2nd𝐺)𝑦)‘𝑓)⟩))
81 fvex 6680 . . . . . . . . . . 11 ((𝑥(2nd𝐹)𝑦)‘𝑓) ∈ V
82 fvex 6680 . . . . . . . . . . 11 ((𝑥(2nd𝐺)𝑦)‘𝑓) ∈ V
8381, 82op2nd 7689 . . . . . . . . . 10 (2nd ‘⟨((𝑥(2nd𝐹)𝑦)‘𝑓), ((𝑥(2nd𝐺)𝑦)‘𝑓)⟩) = ((𝑥(2nd𝐺)𝑦)‘𝑓)
8480, 83syl6eq 2877 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (2nd ‘((𝑥(2nd𝑃)𝑦)‘𝑓)) = ((𝑥(2nd𝐺)𝑦)‘𝑓))
8567, 73, 843eqtrd 2865 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((((1st𝑃)‘𝑥)(2nd ‘(𝐷 2ndF 𝐸))((1st𝑃)‘𝑦))‘((𝑥(2nd𝑃)𝑦)‘𝑓)) = ((𝑥(2nd𝐺)𝑦)‘𝑓))
8685mpteq2dva 5158 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ((((1st𝑃)‘𝑥)(2nd ‘(𝐷 2ndF 𝐸))((1st𝑃)‘𝑦))‘((𝑥(2nd𝑃)𝑦)‘𝑓))) = (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ((𝑥(2nd𝐺)𝑦)‘𝑓)))
87 eqid 2826 . . . . . . . . 9 (Hom ‘𝐸) = (Hom ‘𝐸)
8846adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘(𝐷 2ndF 𝐸))((𝐷 ×c 𝐸) Func 𝐸)(2nd ‘(𝐷 2ndF 𝐸)))
894, 5, 87, 88, 61, 64funcf2 17128 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (((1st𝑃)‘𝑥)(2nd ‘(𝐷 2ndF 𝐸))((1st𝑃)‘𝑦)):(((1st𝑃)‘𝑥)(Hom ‘(𝐷 ×c 𝐸))((1st𝑃)‘𝑦))⟶(((1st ‘(𝐷 2ndF 𝐸))‘((1st𝑃)‘𝑥))(Hom ‘𝐸)((1st ‘(𝐷 2ndF 𝐸))‘((1st𝑃)‘𝑦))))
90 fcompt 6891 . . . . . . . 8 (((((1st𝑃)‘𝑥)(2nd ‘(𝐷 2ndF 𝐸))((1st𝑃)‘𝑦)):(((1st𝑃)‘𝑥)(Hom ‘(𝐷 ×c 𝐸))((1st𝑃)‘𝑦))⟶(((1st ‘(𝐷 2ndF 𝐸))‘((1st𝑃)‘𝑥))(Hom ‘𝐸)((1st ‘(𝐷 2ndF 𝐸))‘((1st𝑃)‘𝑦))) ∧ (𝑥(2nd𝑃)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st𝑃)‘𝑥)(Hom ‘(𝐷 ×c 𝐸))((1st𝑃)‘𝑦))) → ((((1st𝑃)‘𝑥)(2nd ‘(𝐷 2ndF 𝐸))((1st𝑃)‘𝑦)) ∘ (𝑥(2nd𝑃)𝑦)) = (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ((((1st𝑃)‘𝑥)(2nd ‘(𝐷 2ndF 𝐸))((1st𝑃)‘𝑦))‘((𝑥(2nd𝑃)𝑦)‘𝑓))))
9189, 71, 90syl2anc 584 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((((1st𝑃)‘𝑥)(2nd ‘(𝐷 2ndF 𝐸))((1st𝑃)‘𝑦)) ∘ (𝑥(2nd𝑃)𝑦)) = (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ((((1st𝑃)‘𝑥)(2nd ‘(𝐷 2ndF 𝐸))((1st𝑃)‘𝑦))‘((𝑥(2nd𝑃)𝑦)‘𝑓))))
9225adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st𝐺)(𝐶 Func 𝐸)(2nd𝐺))
9317, 36, 87, 92, 69, 70funcf2 17128 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd𝐺)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st𝐺)‘𝑥)(Hom ‘𝐸)((1st𝐺)‘𝑦)))
9493feqmptd 6730 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd𝐺)𝑦) = (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ((𝑥(2nd𝐺)𝑦)‘𝑓)))
9586, 91, 943eqtr4d 2871 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((((1st𝑃)‘𝑥)(2nd ‘(𝐷 2ndF 𝐸))((1st𝑃)‘𝑦)) ∘ (𝑥(2nd𝑃)𝑦)) = (𝑥(2nd𝐺)𝑦))
96953impb 1109 . . . . 5 ((𝜑𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) → ((((1st𝑃)‘𝑥)(2nd ‘(𝐷 2ndF 𝐸))((1st𝑃)‘𝑦)) ∘ (𝑥(2nd𝑃)𝑦)) = (𝑥(2nd𝐺)𝑦))
9796mpoeq3dva 7223 . . . 4 (𝜑 → (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝑃)‘𝑥)(2nd ‘(𝐷 2ndF 𝐸))((1st𝑃)‘𝑦)) ∘ (𝑥(2nd𝑃)𝑦))) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑥(2nd𝐺)𝑦)))
9817, 25funcfn2 17129 . . . . 5 (𝜑 → (2nd𝐺) Fn ((Base‘𝐶) × (Base‘𝐶)))
99 fnov 7272 . . . . 5 ((2nd𝐺) Fn ((Base‘𝐶) × (Base‘𝐶)) ↔ (2nd𝐺) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑥(2nd𝐺)𝑦)))
10098, 99sylib 219 . . . 4 (𝜑 → (2nd𝐺) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑥(2nd𝐺)𝑦)))
10197, 100eqtr4d 2864 . . 3 (𝜑 → (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝑃)‘𝑥)(2nd ‘(𝐷 2ndF 𝐸))((1st𝑃)‘𝑦)) ∘ (𝑥(2nd𝑃)𝑦))) = (2nd𝐺))
10252, 101opeq12d 4810 . 2 (𝜑 → ⟨((1st ‘(𝐷 2ndF 𝐸)) ∘ (1st𝑃)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝑃)‘𝑥)(2nd ‘(𝐷 2ndF 𝐸))((1st𝑃)‘𝑦)) ∘ (𝑥(2nd𝑃)𝑦)))⟩ = ⟨(1st𝐺), (2nd𝐺)⟩)
10317, 56, 44cofuval 17142 . 2 (𝜑 → ((𝐷 2ndF 𝐸) ∘func 𝑃) = ⟨((1st ‘(𝐷 2ndF 𝐸)) ∘ (1st𝑃)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st𝑃)‘𝑥)(2nd ‘(𝐷 2ndF 𝐸))((1st𝑃)‘𝑦)) ∘ (𝑥(2nd𝑃)𝑦)))⟩)
104 1st2nd 7729 . . 3 ((Rel (𝐶 Func 𝐸) ∧ 𝐺 ∈ (𝐶 Func 𝐸)) → 𝐺 = ⟨(1st𝐺), (2nd𝐺)⟩)
10523, 11, 104sylancr 587 . 2 (𝜑𝐺 = ⟨(1st𝐺), (2nd𝐺)⟩)
106102, 103, 1053eqtr4d 2871 1 (𝜑 → ((𝐷 2ndF 𝐸) ∘func 𝑃) = 𝐺)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 396   = wceq 1530   ∈ wcel 2107  ⟨cop 4570   class class class wbr 5063   ↦ cmpt 5143   × cxp 5552   ↾ cres 5556   ∘ ccom 5558  Rel wrel 5559   Fn wfn 6347  ⟶wf 6348  ‘cfv 6352  (class class class)co 7148   ∈ cmpo 7150  1st c1st 7678  2nd c2nd 7679  Basecbs 16473  Hom chom 16566  Catccat 16925   Func cfunc 17114   ∘func ccofu 17116   ×c cxpc 17408   2ndF c2ndf 17410   ⟨,⟩F cprf 17411 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7451  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-fal 1543  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-nel 3129  df-ral 3148  df-rex 3149  df-reu 3150  df-rmo 3151  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-int 4875  df-iun 4919  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6146  df-ord 6192  df-on 6193  df-lim 6194  df-suc 6195  df-iota 6312  df-fun 6354  df-fn 6355  df-f 6356  df-f1 6357  df-fo 6358  df-f1o 6359  df-fv 6360  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7569  df-1st 7680  df-2nd 7681  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-1o 8093  df-oadd 8097  df-er 8279  df-map 8398  df-ixp 8451  df-en 8499  df-dom 8500  df-sdom 8501  df-fin 8502  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11628  df-2 11689  df-3 11690  df-4 11691  df-5 11692  df-6 11693  df-7 11694  df-8 11695  df-9 11696  df-n0 11887  df-z 11971  df-dec 12088  df-uz 12233  df-fz 12883  df-struct 16475  df-ndx 16476  df-slot 16477  df-base 16479  df-hom 16579  df-cco 16580  df-cat 16929  df-cid 16930  df-func 17118  df-cofu 17120  df-xpc 17412  df-2ndf 17414  df-prf 17415 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator