Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . . . 7
⊢ (𝐷 ×c
𝐸) = (𝐷 ×c 𝐸) |
2 | | eqid 2622 |
. . . . . . . 8
⊢
(Base‘𝐷) =
(Base‘𝐷) |
3 | | eqid 2622 |
. . . . . . . 8
⊢
(Base‘𝐸) =
(Base‘𝐸) |
4 | 1, 2, 3 | xpcbas 16818 |
. . . . . . 7
⊢
((Base‘𝐷)
× (Base‘𝐸)) =
(Base‘(𝐷
×c 𝐸)) |
5 | | eqid 2622 |
. . . . . . 7
⊢ (Hom
‘(𝐷
×c 𝐸)) = (Hom ‘(𝐷 ×c 𝐸)) |
6 | | prf1st.c |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) |
7 | | funcrcl 16523 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
8 | 6, 7 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
9 | 8 | simprd 479 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ Cat) |
10 | 9 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐷 ∈ Cat) |
11 | | prf1st.d |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) |
12 | | funcrcl 16523 |
. . . . . . . . . 10
⊢ (𝐺 ∈ (𝐶 Func 𝐸) → (𝐶 ∈ Cat ∧ 𝐸 ∈ Cat)) |
13 | 11, 12 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 ∈ Cat ∧ 𝐸 ∈ Cat)) |
14 | 13 | simprd 479 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ Cat) |
15 | 14 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐸 ∈ Cat) |
16 | | eqid 2622 |
. . . . . . 7
⊢ (𝐷
2ndF 𝐸) = (𝐷 2ndF 𝐸) |
17 | | eqid 2622 |
. . . . . . . . . 10
⊢
(Base‘𝐶) =
(Base‘𝐶) |
18 | | relfunc 16522 |
. . . . . . . . . . 11
⊢ Rel
(𝐶 Func 𝐷) |
19 | | 1st2ndbr 7217 |
. . . . . . . . . . 11
⊢ ((Rel
(𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) |
20 | 18, 6, 19 | sylancr 695 |
. . . . . . . . . 10
⊢ (𝜑 → (1st
‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) |
21 | 17, 2, 20 | funcf1 16526 |
. . . . . . . . 9
⊢ (𝜑 → (1st
‘𝐹):(Base‘𝐶)⟶(Base‘𝐷)) |
22 | 21 | ffvelrnda 6359 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘𝐹)‘𝑥) ∈ (Base‘𝐷)) |
23 | | relfunc 16522 |
. . . . . . . . . . 11
⊢ Rel
(𝐶 Func 𝐸) |
24 | | 1st2ndbr 7217 |
. . . . . . . . . . 11
⊢ ((Rel
(𝐶 Func 𝐸) ∧ 𝐺 ∈ (𝐶 Func 𝐸)) → (1st ‘𝐺)(𝐶 Func 𝐸)(2nd ‘𝐺)) |
25 | 23, 11, 24 | sylancr 695 |
. . . . . . . . . 10
⊢ (𝜑 → (1st
‘𝐺)(𝐶 Func 𝐸)(2nd ‘𝐺)) |
26 | 17, 3, 25 | funcf1 16526 |
. . . . . . . . 9
⊢ (𝜑 → (1st
‘𝐺):(Base‘𝐶)⟶(Base‘𝐸)) |
27 | 26 | ffvelrnda 6359 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘𝐺)‘𝑥) ∈ (Base‘𝐸)) |
28 | | opelxpi 5148 |
. . . . . . . 8
⊢
((((1st ‘𝐹)‘𝑥) ∈ (Base‘𝐷) ∧ ((1st ‘𝐺)‘𝑥) ∈ (Base‘𝐸)) → 〈((1st
‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉 ∈ ((Base‘𝐷) × (Base‘𝐸))) |
29 | 22, 27, 28 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 〈((1st
‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉 ∈ ((Base‘𝐷) × (Base‘𝐸))) |
30 | 1, 4, 5, 10, 15, 16, 29 | 2ndf1 16835 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘(𝐷
2ndF 𝐸))‘〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉) = (2nd
‘〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉)) |
31 | | fvex 6201 |
. . . . . . 7
⊢
((1st ‘𝐹)‘𝑥) ∈ V |
32 | | fvex 6201 |
. . . . . . 7
⊢
((1st ‘𝐺)‘𝑥) ∈ V |
33 | 31, 32 | op2nd 7177 |
. . . . . 6
⊢
(2nd ‘〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉) = ((1st ‘𝐺)‘𝑥) |
34 | 30, 33 | syl6eq 2672 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘(𝐷
2ndF 𝐸))‘〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉) = ((1st ‘𝐺)‘𝑥)) |
35 | 34 | mpteq2dva 4744 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘(𝐷
2ndF 𝐸))‘〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉)) = (𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘𝐺)‘𝑥))) |
36 | | prf1st.p |
. . . . . . 7
⊢ 𝑃 = (𝐹 〈,〉F 𝐺) |
37 | | eqid 2622 |
. . . . . . 7
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
38 | 36, 17, 37, 6, 11 | prfval 16839 |
. . . . . 6
⊢ (𝜑 → 𝑃 = 〈(𝑥 ∈ (Base‘𝐶) ↦ 〈((1st
‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉))〉) |
39 | | fvex 6201 |
. . . . . . . 8
⊢
(Base‘𝐶)
∈ V |
40 | 39 | mptex 6486 |
. . . . . . 7
⊢ (𝑥 ∈ (Base‘𝐶) ↦ 〈((1st
‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉) ∈ V |
41 | 39, 39 | mpt2ex 7247 |
. . . . . . 7
⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉)) ∈ V |
42 | 40, 41 | op1std 7178 |
. . . . . 6
⊢ (𝑃 = 〈(𝑥 ∈ (Base‘𝐶) ↦ 〈((1st
‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉))〉 → (1st
‘𝑃) = (𝑥 ∈ (Base‘𝐶) ↦ 〈((1st
‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉)) |
43 | 38, 42 | syl 17 |
. . . . 5
⊢ (𝜑 → (1st
‘𝑃) = (𝑥 ∈ (Base‘𝐶) ↦ 〈((1st
‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉)) |
44 | | relfunc 16522 |
. . . . . . . 8
⊢ Rel
((𝐷
×c 𝐸) Func 𝐸) |
45 | 1, 9, 14, 16 | 2ndfcl 16838 |
. . . . . . . 8
⊢ (𝜑 → (𝐷 2ndF 𝐸) ∈ ((𝐷 ×c 𝐸) Func 𝐸)) |
46 | | 1st2ndbr 7217 |
. . . . . . . 8
⊢ ((Rel
((𝐷
×c 𝐸) Func 𝐸) ∧ (𝐷 2ndF 𝐸) ∈ ((𝐷 ×c 𝐸) Func 𝐸)) → (1st ‘(𝐷
2ndF 𝐸))((𝐷 ×c 𝐸) Func 𝐸)(2nd ‘(𝐷 2ndF 𝐸))) |
47 | 44, 45, 46 | sylancr 695 |
. . . . . . 7
⊢ (𝜑 → (1st
‘(𝐷
2ndF 𝐸))((𝐷 ×c 𝐸) Func 𝐸)(2nd ‘(𝐷 2ndF 𝐸))) |
48 | 4, 3, 47 | funcf1 16526 |
. . . . . 6
⊢ (𝜑 → (1st
‘(𝐷
2ndF 𝐸)):((Base‘𝐷) × (Base‘𝐸))⟶(Base‘𝐸)) |
49 | 48 | feqmptd 6249 |
. . . . 5
⊢ (𝜑 → (1st
‘(𝐷
2ndF 𝐸)) = (𝑢 ∈ ((Base‘𝐷) × (Base‘𝐸)) ↦ ((1st ‘(𝐷
2ndF 𝐸))‘𝑢))) |
50 | | fveq2 6191 |
. . . . 5
⊢ (𝑢 = 〈((1st
‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉 → ((1st ‘(𝐷
2ndF 𝐸))‘𝑢) = ((1st ‘(𝐷
2ndF 𝐸))‘〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉)) |
51 | 29, 43, 49, 50 | fmptco 6396 |
. . . 4
⊢ (𝜑 → ((1st
‘(𝐷
2ndF 𝐸)) ∘ (1st ‘𝑃)) = (𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘(𝐷
2ndF 𝐸))‘〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉))) |
52 | 26 | feqmptd 6249 |
. . . 4
⊢ (𝜑 → (1st
‘𝐺) = (𝑥 ∈ (Base‘𝐶) ↦ ((1st
‘𝐺)‘𝑥))) |
53 | 35, 51, 52 | 3eqtr4d 2666 |
. . 3
⊢ (𝜑 → ((1st
‘(𝐷
2ndF 𝐸)) ∘ (1st ‘𝑃)) = (1st
‘𝐺)) |
54 | 9 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝐷 ∈ Cat) |
55 | 14 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝐸 ∈ Cat) |
56 | | relfunc 16522 |
. . . . . . . . . . . . . . . 16
⊢ Rel
(𝐶 Func (𝐷 ×c 𝐸)) |
57 | 36, 1, 6, 11 | prfcl 16843 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑃 ∈ (𝐶 Func (𝐷 ×c 𝐸))) |
58 | | 1st2ndbr 7217 |
. . . . . . . . . . . . . . . 16
⊢ ((Rel
(𝐶 Func (𝐷 ×c 𝐸)) ∧ 𝑃 ∈ (𝐶 Func (𝐷 ×c 𝐸))) → (1st
‘𝑃)(𝐶 Func (𝐷 ×c 𝐸))(2nd ‘𝑃)) |
59 | 56, 57, 58 | sylancr 695 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1st
‘𝑃)(𝐶 Func (𝐷 ×c 𝐸))(2nd ‘𝑃)) |
60 | 17, 4, 59 | funcf1 16526 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (1st
‘𝑃):(Base‘𝐶)⟶((Base‘𝐷) × (Base‘𝐸))) |
61 | 60 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘𝑃)‘𝑥) ∈ ((Base‘𝐷) × (Base‘𝐸))) |
62 | 61 | adantrr 753 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝑃)‘𝑥) ∈ ((Base‘𝐷) × (Base‘𝐸))) |
63 | 62 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((1st ‘𝑃)‘𝑥) ∈ ((Base‘𝐷) × (Base‘𝐸))) |
64 | 60 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐶)) → ((1st ‘𝑃)‘𝑦) ∈ ((Base‘𝐷) × (Base‘𝐸))) |
65 | 64 | adantrl 752 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝑃)‘𝑦) ∈ ((Base‘𝐷) × (Base‘𝐸))) |
66 | 65 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((1st ‘𝑃)‘𝑦) ∈ ((Base‘𝐷) × (Base‘𝐸))) |
67 | 1, 4, 5, 54, 55, 16, 63, 66 | 2ndf2 16836 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (((1st ‘𝑃)‘𝑥)(2nd ‘(𝐷 2ndF 𝐸))((1st ‘𝑃)‘𝑦)) = (2nd ↾
(((1st ‘𝑃)‘𝑥)(Hom ‘(𝐷 ×c 𝐸))((1st ‘𝑃)‘𝑦)))) |
68 | 67 | fveq1d 6193 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((((1st ‘𝑃)‘𝑥)(2nd ‘(𝐷 2ndF 𝐸))((1st ‘𝑃)‘𝑦))‘((𝑥(2nd ‘𝑃)𝑦)‘𝑓)) = ((2nd ↾
(((1st ‘𝑃)‘𝑥)(Hom ‘(𝐷 ×c 𝐸))((1st ‘𝑃)‘𝑦)))‘((𝑥(2nd ‘𝑃)𝑦)‘𝑓))) |
69 | 59 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘𝑃)(𝐶 Func (𝐷 ×c 𝐸))(2nd ‘𝑃)) |
70 | | simprl 794 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑥 ∈ (Base‘𝐶)) |
71 | | simprr 796 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑦 ∈ (Base‘𝐶)) |
72 | 17, 37, 5, 69, 70, 71 | funcf2 16528 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘𝑃)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝑃)‘𝑥)(Hom ‘(𝐷 ×c 𝐸))((1st ‘𝑃)‘𝑦))) |
73 | 72 | ffvelrnda 6359 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑥(2nd ‘𝑃)𝑦)‘𝑓) ∈ (((1st ‘𝑃)‘𝑥)(Hom ‘(𝐷 ×c 𝐸))((1st ‘𝑃)‘𝑦))) |
74 | | fvres 6207 |
. . . . . . . . . 10
⊢ (((𝑥(2nd ‘𝑃)𝑦)‘𝑓) ∈ (((1st ‘𝑃)‘𝑥)(Hom ‘(𝐷 ×c 𝐸))((1st ‘𝑃)‘𝑦)) → ((2nd ↾
(((1st ‘𝑃)‘𝑥)(Hom ‘(𝐷 ×c 𝐸))((1st ‘𝑃)‘𝑦)))‘((𝑥(2nd ‘𝑃)𝑦)‘𝑓)) = (2nd ‘((𝑥(2nd ‘𝑃)𝑦)‘𝑓))) |
75 | 73, 74 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((2nd ↾
(((1st ‘𝑃)‘𝑥)(Hom ‘(𝐷 ×c 𝐸))((1st ‘𝑃)‘𝑦)))‘((𝑥(2nd ‘𝑃)𝑦)‘𝑓)) = (2nd ‘((𝑥(2nd ‘𝑃)𝑦)‘𝑓))) |
76 | 6 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝐹 ∈ (𝐶 Func 𝐷)) |
77 | 11 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝐺 ∈ (𝐶 Func 𝐸)) |
78 | 70 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑥 ∈ (Base‘𝐶)) |
79 | 71 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑦 ∈ (Base‘𝐶)) |
80 | | simpr 477 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) |
81 | 36, 17, 37, 76, 77, 78, 79, 80 | prf2 16842 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑥(2nd ‘𝑃)𝑦)‘𝑓) = 〈((𝑥(2nd ‘𝐹)𝑦)‘𝑓), ((𝑥(2nd ‘𝐺)𝑦)‘𝑓)〉) |
82 | 81 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (2nd ‘((𝑥(2nd ‘𝑃)𝑦)‘𝑓)) = (2nd ‘〈((𝑥(2nd ‘𝐹)𝑦)‘𝑓), ((𝑥(2nd ‘𝐺)𝑦)‘𝑓)〉)) |
83 | | fvex 6201 |
. . . . . . . . . . 11
⊢ ((𝑥(2nd ‘𝐹)𝑦)‘𝑓) ∈ V |
84 | | fvex 6201 |
. . . . . . . . . . 11
⊢ ((𝑥(2nd ‘𝐺)𝑦)‘𝑓) ∈ V |
85 | 83, 84 | op2nd 7177 |
. . . . . . . . . 10
⊢
(2nd ‘〈((𝑥(2nd ‘𝐹)𝑦)‘𝑓), ((𝑥(2nd ‘𝐺)𝑦)‘𝑓)〉) = ((𝑥(2nd ‘𝐺)𝑦)‘𝑓) |
86 | 82, 85 | syl6eq 2672 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (2nd ‘((𝑥(2nd ‘𝑃)𝑦)‘𝑓)) = ((𝑥(2nd ‘𝐺)𝑦)‘𝑓)) |
87 | 68, 75, 86 | 3eqtrd 2660 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((((1st ‘𝑃)‘𝑥)(2nd ‘(𝐷 2ndF 𝐸))((1st ‘𝑃)‘𝑦))‘((𝑥(2nd ‘𝑃)𝑦)‘𝑓)) = ((𝑥(2nd ‘𝐺)𝑦)‘𝑓)) |
88 | 87 | mpteq2dva 4744 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ((((1st ‘𝑃)‘𝑥)(2nd ‘(𝐷 2ndF 𝐸))((1st ‘𝑃)‘𝑦))‘((𝑥(2nd ‘𝑃)𝑦)‘𝑓))) = (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ((𝑥(2nd ‘𝐺)𝑦)‘𝑓))) |
89 | | eqid 2622 |
. . . . . . . . 9
⊢ (Hom
‘𝐸) = (Hom
‘𝐸) |
90 | 47 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘(𝐷
2ndF 𝐸))((𝐷 ×c 𝐸) Func 𝐸)(2nd ‘(𝐷 2ndF 𝐸))) |
91 | 4, 5, 89, 90, 62, 65 | funcf2 16528 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (((1st ‘𝑃)‘𝑥)(2nd ‘(𝐷 2ndF 𝐸))((1st ‘𝑃)‘𝑦)):(((1st ‘𝑃)‘𝑥)(Hom ‘(𝐷 ×c 𝐸))((1st ‘𝑃)‘𝑦))⟶(((1st ‘(𝐷
2ndF 𝐸))‘((1st ‘𝑃)‘𝑥))(Hom ‘𝐸)((1st ‘(𝐷 2ndF 𝐸))‘((1st
‘𝑃)‘𝑦)))) |
92 | | fcompt 6400 |
. . . . . . . 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 ‘𝑃)𝑦)‘𝑓)))) |
93 | 91, 72, 92 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((((1st ‘𝑃)‘𝑥)(2nd ‘(𝐷 2ndF 𝐸))((1st ‘𝑃)‘𝑦)) ∘ (𝑥(2nd ‘𝑃)𝑦)) = (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ((((1st ‘𝑃)‘𝑥)(2nd ‘(𝐷 2ndF 𝐸))((1st ‘𝑃)‘𝑦))‘((𝑥(2nd ‘𝑃)𝑦)‘𝑓)))) |
94 | 25 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘𝐺)(𝐶 Func 𝐸)(2nd ‘𝐺)) |
95 | 17, 37, 89, 94, 70, 71 | funcf2 16528 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘𝐺)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐺)‘𝑥)(Hom ‘𝐸)((1st ‘𝐺)‘𝑦))) |
96 | 95 | feqmptd 6249 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘𝐺)𝑦) = (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ ((𝑥(2nd ‘𝐺)𝑦)‘𝑓))) |
97 | 88, 93, 96 | 3eqtr4d 2666 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((((1st ‘𝑃)‘𝑥)(2nd ‘(𝐷 2ndF 𝐸))((1st ‘𝑃)‘𝑦)) ∘ (𝑥(2nd ‘𝑃)𝑦)) = (𝑥(2nd ‘𝐺)𝑦)) |
98 | 97 | 3impb 1260 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) → ((((1st ‘𝑃)‘𝑥)(2nd ‘(𝐷 2ndF 𝐸))((1st ‘𝑃)‘𝑦)) ∘ (𝑥(2nd ‘𝑃)𝑦)) = (𝑥(2nd ‘𝐺)𝑦)) |
99 | 98 | mpt2eq3dva 6719 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝑃)‘𝑥)(2nd ‘(𝐷 2ndF 𝐸))((1st ‘𝑃)‘𝑦)) ∘ (𝑥(2nd ‘𝑃)𝑦))) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑥(2nd ‘𝐺)𝑦))) |
100 | 17, 25 | funcfn2 16529 |
. . . . 5
⊢ (𝜑 → (2nd
‘𝐺) Fn
((Base‘𝐶) ×
(Base‘𝐶))) |
101 | | fnov 6768 |
. . . . 5
⊢
((2nd ‘𝐺) Fn ((Base‘𝐶) × (Base‘𝐶)) ↔ (2nd ‘𝐺) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑥(2nd ‘𝐺)𝑦))) |
102 | 100, 101 | sylib 208 |
. . . 4
⊢ (𝜑 → (2nd
‘𝐺) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (𝑥(2nd ‘𝐺)𝑦))) |
103 | 99, 102 | eqtr4d 2659 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝑃)‘𝑥)(2nd ‘(𝐷 2ndF 𝐸))((1st ‘𝑃)‘𝑦)) ∘ (𝑥(2nd ‘𝑃)𝑦))) = (2nd ‘𝐺)) |
104 | 53, 103 | opeq12d 4410 |
. 2
⊢ (𝜑 → 〈((1st
‘(𝐷
2ndF 𝐸)) ∘ (1st ‘𝑃)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝑃)‘𝑥)(2nd ‘(𝐷 2ndF 𝐸))((1st ‘𝑃)‘𝑦)) ∘ (𝑥(2nd ‘𝑃)𝑦)))〉 = 〈(1st
‘𝐺), (2nd
‘𝐺)〉) |
105 | 17, 57, 45 | cofuval 16542 |
. 2
⊢ (𝜑 → ((𝐷 2ndF 𝐸) ∘func
𝑃) = 〈((1st
‘(𝐷
2ndF 𝐸)) ∘ (1st ‘𝑃)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝑃)‘𝑥)(2nd ‘(𝐷 2ndF 𝐸))((1st ‘𝑃)‘𝑦)) ∘ (𝑥(2nd ‘𝑃)𝑦)))〉) |
106 | | 1st2nd 7214 |
. . 3
⊢ ((Rel
(𝐶 Func 𝐸) ∧ 𝐺 ∈ (𝐶 Func 𝐸)) → 𝐺 = 〈(1st ‘𝐺), (2nd ‘𝐺)〉) |
107 | 23, 11, 106 | sylancr 695 |
. 2
⊢ (𝜑 → 𝐺 = 〈(1st ‘𝐺), (2nd ‘𝐺)〉) |
108 | 104, 105,
107 | 3eqtr4d 2666 |
1
⊢ (𝜑 → ((𝐷 2ndF 𝐸) ∘func
𝑃) = 𝐺) |