Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . . 7
⊢
(Base‘𝐶) =
(Base‘𝐶) |
2 | | eqid 2733 |
. . . . . . 7
⊢
(Base‘𝐷) =
(Base‘𝐷) |
3 | | relfunc 17753 |
. . . . . . . 8
⊢ Rel
(𝐶 Func 𝐷) |
4 | | fuclid.r |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺)) |
5 | | fuclid.n |
. . . . . . . . . . 11
⊢ 𝑁 = (𝐶 Nat 𝐷) |
6 | 5 | natrcl 17842 |
. . . . . . . . . 10
⊢ (𝑅 ∈ (𝐹𝑁𝐺) → (𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷))) |
7 | 4, 6 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷))) |
8 | 7 | simpld 496 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) |
9 | | 1st2ndbr 7975 |
. . . . . . . 8
⊢ ((Rel
(𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) |
10 | 3, 8, 9 | sylancr 588 |
. . . . . . 7
⊢ (𝜑 → (1st
‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) |
11 | 1, 2, 10 | funcf1 17757 |
. . . . . 6
⊢ (𝜑 → (1st
‘𝐹):(Base‘𝐶)⟶(Base‘𝐷)) |
12 | | fvco3 6941 |
. . . . . 6
⊢
(((1st ‘𝐹):(Base‘𝐶)⟶(Base‘𝐷) ∧ 𝑥 ∈ (Base‘𝐶)) → (( 1 ∘ (1st
‘𝐹))‘𝑥) = ( 1 ‘((1st
‘𝐹)‘𝑥))) |
13 | 11, 12 | sylan 581 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (( 1 ∘ (1st
‘𝐹))‘𝑥) = ( 1 ‘((1st
‘𝐹)‘𝑥))) |
14 | 13 | oveq2d 7374 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑅‘𝑥)(⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐹)‘𝑥)⟩(comp‘𝐷)((1st ‘𝐺)‘𝑥))(( 1 ∘ (1st
‘𝐹))‘𝑥)) = ((𝑅‘𝑥)(⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐹)‘𝑥)⟩(comp‘𝐷)((1st ‘𝐺)‘𝑥))( 1 ‘((1st
‘𝐹)‘𝑥)))) |
15 | | eqid 2733 |
. . . . 5
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
16 | | fuclid.1 |
. . . . 5
⊢ 1 =
(Id‘𝐷) |
17 | | funcrcl 17754 |
. . . . . . . 8
⊢ (𝐹 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
18 | 8, 17 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
19 | 18 | simprd 497 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ Cat) |
20 | 19 | adantr 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐷 ∈ Cat) |
21 | 11 | ffvelcdmda 7036 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘𝐹)‘𝑥) ∈ (Base‘𝐷)) |
22 | | eqid 2733 |
. . . . 5
⊢
(comp‘𝐷) =
(comp‘𝐷) |
23 | 7 | simprd 497 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷)) |
24 | | 1st2ndbr 7975 |
. . . . . . . 8
⊢ ((Rel
(𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷)) → (1st ‘𝐺)(𝐶 Func 𝐷)(2nd ‘𝐺)) |
25 | 3, 23, 24 | sylancr 588 |
. . . . . . 7
⊢ (𝜑 → (1st
‘𝐺)(𝐶 Func 𝐷)(2nd ‘𝐺)) |
26 | 1, 2, 25 | funcf1 17757 |
. . . . . 6
⊢ (𝜑 → (1st
‘𝐺):(Base‘𝐶)⟶(Base‘𝐷)) |
27 | 26 | ffvelcdmda 7036 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘𝐺)‘𝑥) ∈ (Base‘𝐷)) |
28 | 5, 4 | nat1st2nd 17843 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ (⟨(1st ‘𝐹), (2nd ‘𝐹)⟩𝑁⟨(1st ‘𝐺), (2nd ‘𝐺)⟩)) |
29 | 28 | adantr 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑅 ∈ (⟨(1st ‘𝐹), (2nd ‘𝐹)⟩𝑁⟨(1st ‘𝐺), (2nd ‘𝐺)⟩)) |
30 | | simpr 486 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶)) |
31 | 5, 29, 1, 15, 30 | natcl 17845 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑅‘𝑥) ∈ (((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐺)‘𝑥))) |
32 | 2, 15, 16, 20, 21, 22, 27, 31 | catrid 17569 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑅‘𝑥)(⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐹)‘𝑥)⟩(comp‘𝐷)((1st ‘𝐺)‘𝑥))( 1 ‘((1st
‘𝐹)‘𝑥))) = (𝑅‘𝑥)) |
33 | 14, 32 | eqtrd 2773 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑅‘𝑥)(⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐹)‘𝑥)⟩(comp‘𝐷)((1st ‘𝐺)‘𝑥))(( 1 ∘ (1st
‘𝐹))‘𝑥)) = (𝑅‘𝑥)) |
34 | 33 | mpteq2dva 5206 |
. 2
⊢ (𝜑 → (𝑥 ∈ (Base‘𝐶) ↦ ((𝑅‘𝑥)(⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐹)‘𝑥)⟩(comp‘𝐷)((1st ‘𝐺)‘𝑥))(( 1 ∘ (1st
‘𝐹))‘𝑥))) = (𝑥 ∈ (Base‘𝐶) ↦ (𝑅‘𝑥))) |
35 | | fuclid.q |
. . 3
⊢ 𝑄 = (𝐶 FuncCat 𝐷) |
36 | | fuclid.x |
. . 3
⊢ ∙ =
(comp‘𝑄) |
37 | 35, 5, 16, 8 | fucidcl 17859 |
. . 3
⊢ (𝜑 → ( 1 ∘ (1st
‘𝐹)) ∈ (𝐹𝑁𝐹)) |
38 | 35, 5, 1, 22, 36, 37, 4 | fucco 17856 |
. 2
⊢ (𝜑 → (𝑅(⟨𝐹, 𝐹⟩ ∙ 𝐺)( 1 ∘ (1st
‘𝐹))) = (𝑥 ∈ (Base‘𝐶) ↦ ((𝑅‘𝑥)(⟨((1st ‘𝐹)‘𝑥), ((1st ‘𝐹)‘𝑥)⟩(comp‘𝐷)((1st ‘𝐺)‘𝑥))(( 1 ∘ (1st
‘𝐹))‘𝑥)))) |
39 | 5, 28, 1 | natfn 17846 |
. . 3
⊢ (𝜑 → 𝑅 Fn (Base‘𝐶)) |
40 | | dffn5 6902 |
. . 3
⊢ (𝑅 Fn (Base‘𝐶) ↔ 𝑅 = (𝑥 ∈ (Base‘𝐶) ↦ (𝑅‘𝑥))) |
41 | 39, 40 | sylib 217 |
. 2
⊢ (𝜑 → 𝑅 = (𝑥 ∈ (Base‘𝐶) ↦ (𝑅‘𝑥))) |
42 | 34, 38, 41 | 3eqtr4d 2783 |
1
⊢ (𝜑 → (𝑅(⟨𝐹, 𝐹⟩ ∙ 𝐺)( 1 ∘ (1st
‘𝐹))) = 𝑅) |