Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . . . . . 7
⊢
(Base‘𝐶) =
(Base‘𝐶) |
2 | | eqid 2738 |
. . . . . . 7
⊢
(Base‘𝐷) =
(Base‘𝐷) |
3 | | relfunc 17566 |
. . . . . . . 8
⊢ Rel
(𝐶 Func 𝐷) |
4 | | fuclid.r |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ (𝐹𝑁𝐺)) |
5 | | fuclid.n |
. . . . . . . . . . 11
⊢ 𝑁 = (𝐶 Nat 𝐷) |
6 | 5 | natrcl 17655 |
. . . . . . . . . 10
⊢ (𝑅 ∈ (𝐹𝑁𝐺) → (𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷))) |
7 | 4, 6 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷))) |
8 | 7 | simpld 495 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) |
9 | | 1st2ndbr 7874 |
. . . . . . . 8
⊢ ((Rel
(𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) |
10 | 3, 8, 9 | sylancr 587 |
. . . . . . 7
⊢ (𝜑 → (1st
‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) |
11 | 1, 2, 10 | funcf1 17570 |
. . . . . 6
⊢ (𝜑 → (1st
‘𝐹):(Base‘𝐶)⟶(Base‘𝐷)) |
12 | | fvco3 6861 |
. . . . . 6
⊢
(((1st ‘𝐹):(Base‘𝐶)⟶(Base‘𝐷) ∧ 𝑥 ∈ (Base‘𝐶)) → (( 1 ∘ (1st
‘𝐹))‘𝑥) = ( 1 ‘((1st
‘𝐹)‘𝑥))) |
13 | 11, 12 | sylan 580 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (( 1 ∘ (1st
‘𝐹))‘𝑥) = ( 1 ‘((1st
‘𝐹)‘𝑥))) |
14 | 13 | oveq2d 7285 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑅‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐹)‘𝑥)〉(comp‘𝐷)((1st ‘𝐺)‘𝑥))(( 1 ∘ (1st
‘𝐹))‘𝑥)) = ((𝑅‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐹)‘𝑥)〉(comp‘𝐷)((1st ‘𝐺)‘𝑥))( 1 ‘((1st
‘𝐹)‘𝑥)))) |
15 | | eqid 2738 |
. . . . 5
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
16 | | fuclid.1 |
. . . . 5
⊢ 1 =
(Id‘𝐷) |
17 | | funcrcl 17567 |
. . . . . . . 8
⊢ (𝐹 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
18 | 8, 17 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
19 | 18 | simprd 496 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ Cat) |
20 | 19 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐷 ∈ Cat) |
21 | 11 | ffvelrnda 6955 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘𝐹)‘𝑥) ∈ (Base‘𝐷)) |
22 | | eqid 2738 |
. . . . 5
⊢
(comp‘𝐷) =
(comp‘𝐷) |
23 | 7 | simprd 496 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐷)) |
24 | | 1st2ndbr 7874 |
. . . . . . . 8
⊢ ((Rel
(𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷)) → (1st ‘𝐺)(𝐶 Func 𝐷)(2nd ‘𝐺)) |
25 | 3, 23, 24 | sylancr 587 |
. . . . . . 7
⊢ (𝜑 → (1st
‘𝐺)(𝐶 Func 𝐷)(2nd ‘𝐺)) |
26 | 1, 2, 25 | funcf1 17570 |
. . . . . 6
⊢ (𝜑 → (1st
‘𝐺):(Base‘𝐶)⟶(Base‘𝐷)) |
27 | 26 | ffvelrnda 6955 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘𝐺)‘𝑥) ∈ (Base‘𝐷)) |
28 | 5, 4 | nat1st2nd 17656 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ (〈(1st ‘𝐹), (2nd ‘𝐹)〉𝑁〈(1st ‘𝐺), (2nd ‘𝐺)〉)) |
29 | 28 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑅 ∈ (〈(1st ‘𝐹), (2nd ‘𝐹)〉𝑁〈(1st ‘𝐺), (2nd ‘𝐺)〉)) |
30 | | simpr 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶)) |
31 | 5, 29, 1, 15, 30 | natcl 17658 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑅‘𝑥) ∈ (((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐺)‘𝑥))) |
32 | 2, 15, 16, 20, 21, 22, 27, 31 | catrid 17382 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑅‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐹)‘𝑥)〉(comp‘𝐷)((1st ‘𝐺)‘𝑥))( 1 ‘((1st
‘𝐹)‘𝑥))) = (𝑅‘𝑥)) |
33 | 14, 32 | eqtrd 2778 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑅‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐹)‘𝑥)〉(comp‘𝐷)((1st ‘𝐺)‘𝑥))(( 1 ∘ (1st
‘𝐹))‘𝑥)) = (𝑅‘𝑥)) |
34 | 33 | mpteq2dva 5175 |
. 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 17672 |
. . 3
⊢ (𝜑 → ( 1 ∘ (1st
‘𝐹)) ∈ (𝐹𝑁𝐹)) |
38 | 35, 5, 1, 22, 36, 37, 4 | fucco 17669 |
. 2
⊢ (𝜑 → (𝑅(〈𝐹, 𝐹〉 ∙ 𝐺)( 1 ∘ (1st
‘𝐹))) = (𝑥 ∈ (Base‘𝐶) ↦ ((𝑅‘𝑥)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐹)‘𝑥)〉(comp‘𝐷)((1st ‘𝐺)‘𝑥))(( 1 ∘ (1st
‘𝐹))‘𝑥)))) |
39 | 5, 28, 1 | natfn 17659 |
. . 3
⊢ (𝜑 → 𝑅 Fn (Base‘𝐶)) |
40 | | dffn5 6822 |
. . 3
⊢ (𝑅 Fn (Base‘𝐶) ↔ 𝑅 = (𝑥 ∈ (Base‘𝐶) ↦ (𝑅‘𝑥))) |
41 | 39, 40 | sylib 217 |
. 2
⊢ (𝜑 → 𝑅 = (𝑥 ∈ (Base‘𝐶) ↦ (𝑅‘𝑥))) |
42 | 34, 38, 41 | 3eqtr4d 2788 |
1
⊢ (𝜑 → (𝑅(〈𝐹, 𝐹〉 ∙ 𝐺)( 1 ∘ (1st
‘𝐹))) = 𝑅) |