Step | Hyp | Ref
| Expression |
1 | | funcid.x |
. 2
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
2 | | funcid.f |
. . . . 5
⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) |
3 | | funcid.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐷) |
4 | | eqid 2610 |
. . . . . 6
⊢
(Base‘𝐸) =
(Base‘𝐸) |
5 | | eqid 2610 |
. . . . . 6
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
6 | | eqid 2610 |
. . . . . 6
⊢ (Hom
‘𝐸) = (Hom
‘𝐸) |
7 | | funcid.1 |
. . . . . 6
⊢ 1 =
(Id‘𝐷) |
8 | | funcid.i |
. . . . . 6
⊢ 𝐼 = (Id‘𝐸) |
9 | | eqid 2610 |
. . . . . 6
⊢
(comp‘𝐷) =
(comp‘𝐷) |
10 | | eqid 2610 |
. . . . . 6
⊢
(comp‘𝐸) =
(comp‘𝐸) |
11 | | df-br 4584 |
. . . . . . . . 9
⊢ (𝐹(𝐷 Func 𝐸)𝐺 ↔ 〈𝐹, 𝐺〉 ∈ (𝐷 Func 𝐸)) |
12 | 2, 11 | sylib 207 |
. . . . . . . 8
⊢ (𝜑 → 〈𝐹, 𝐺〉 ∈ (𝐷 Func 𝐸)) |
13 | | funcrcl 16346 |
. . . . . . . 8
⊢
(〈𝐹, 𝐺〉 ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat)) |
14 | 12, 13 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat)) |
15 | 14 | simpld 474 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ Cat) |
16 | 14 | simprd 478 |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈ Cat) |
17 | 3, 4, 5, 6, 7, 8, 9, 10, 15, 16 | isfunc 16347 |
. . . . 5
⊢ (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ (𝐹:𝐵⟶(Base‘𝐸) ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))(Hom ‘𝐸)(𝐹‘(2nd ‘𝑧))) ↑𝑚
((Hom ‘𝐷)‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝐸)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))))) |
18 | 2, 17 | mpbid 221 |
. . . 4
⊢ (𝜑 → (𝐹:𝐵⟶(Base‘𝐸) ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))(Hom ‘𝐸)(𝐹‘(2nd ‘𝑧))) ↑𝑚
((Hom ‘𝐷)‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝐸)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))) |
19 | 18 | simp3d 1068 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝐸)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))) |
20 | | simpl 472 |
. . . 4
⊢ ((((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝐸)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))) → ((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥))) |
21 | 20 | ralimi 2936 |
. . 3
⊢
(∀𝑥 ∈
𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥(Hom ‘𝐷)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝐷)𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝐷)𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝐸)(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))) → ∀𝑥 ∈ 𝐵 ((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥))) |
22 | 19, 21 | syl 17 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥))) |
23 | | id 22 |
. . . . . 6
⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋) |
24 | 23, 23 | oveq12d 6567 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝑥𝐺𝑥) = (𝑋𝐺𝑋)) |
25 | | fveq2 6103 |
. . . . 5
⊢ (𝑥 = 𝑋 → ( 1 ‘𝑥) = ( 1 ‘𝑋)) |
26 | 24, 25 | fveq12d 6109 |
. . . 4
⊢ (𝑥 = 𝑋 → ((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = ((𝑋𝐺𝑋)‘( 1 ‘𝑋))) |
27 | | fveq2 6103 |
. . . . 5
⊢ (𝑥 = 𝑋 → (𝐹‘𝑥) = (𝐹‘𝑋)) |
28 | 27 | fveq2d 6107 |
. . . 4
⊢ (𝑥 = 𝑋 → (𝐼‘(𝐹‘𝑥)) = (𝐼‘(𝐹‘𝑋))) |
29 | 26, 28 | eqeq12d 2625 |
. . 3
⊢ (𝑥 = 𝑋 → (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ↔ ((𝑋𝐺𝑋)‘( 1 ‘𝑋)) = (𝐼‘(𝐹‘𝑋)))) |
30 | 29 | rspcv 3278 |
. 2
⊢ (𝑋 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 ((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) → ((𝑋𝐺𝑋)‘( 1 ‘𝑋)) = (𝐼‘(𝐹‘𝑋)))) |
31 | 1, 22, 30 | sylc 63 |
1
⊢ (𝜑 → ((𝑋𝐺𝑋)‘( 1 ‘𝑋)) = (𝐼‘(𝐹‘𝑋))) |