Proof of Theorem isfuncd
Step | Hyp | Ref
| Expression |
1 | | isfuncd.1 |
. 2
⊢ (𝜑 → 𝐹:𝐵⟶𝐶) |
2 | | isfuncd.2 |
. . . 4
⊢ (𝜑 → 𝐺 Fn (𝐵 × 𝐵)) |
3 | | isfunc.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐷) |
4 | | fvex 6201 |
. . . . . 6
⊢
(Base‘𝐷)
∈ V |
5 | 3, 4 | eqeltri 2697 |
. . . . 5
⊢ 𝐵 ∈ V |
6 | 5, 5 | xpex 6962 |
. . . 4
⊢ (𝐵 × 𝐵) ∈ V |
7 | | fnex 6481 |
. . . 4
⊢ ((𝐺 Fn (𝐵 × 𝐵) ∧ (𝐵 × 𝐵) ∈ V) → 𝐺 ∈ V) |
8 | 2, 6, 7 | sylancl 694 |
. . 3
⊢ (𝜑 → 𝐺 ∈ V) |
9 | | isfuncd.3 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)𝐽(𝐹‘𝑦))) |
10 | | ovex 6678 |
. . . . . . 7
⊢ ((𝐹‘𝑥)𝐽(𝐹‘𝑦)) ∈ V |
11 | | ovex 6678 |
. . . . . . 7
⊢ (𝑥𝐻𝑦) ∈ V |
12 | 10, 11 | elmap 7886 |
. . . . . 6
⊢ ((𝑥𝐺𝑦) ∈ (((𝐹‘𝑥)𝐽(𝐹‘𝑦)) ↑𝑚 (𝑥𝐻𝑦)) ↔ (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)𝐽(𝐹‘𝑦))) |
13 | 9, 12 | sylibr 224 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥𝐺𝑦) ∈ (((𝐹‘𝑥)𝐽(𝐹‘𝑦)) ↑𝑚 (𝑥𝐻𝑦))) |
14 | 13 | ralrimivva 2971 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐺𝑦) ∈ (((𝐹‘𝑥)𝐽(𝐹‘𝑦)) ↑𝑚 (𝑥𝐻𝑦))) |
15 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐺‘𝑧) = (𝐺‘〈𝑥, 𝑦〉)) |
16 | | df-ov 6653 |
. . . . . . 7
⊢ (𝑥𝐺𝑦) = (𝐺‘〈𝑥, 𝑦〉) |
17 | 15, 16 | syl6eqr 2674 |
. . . . . 6
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐺‘𝑧) = (𝑥𝐺𝑦)) |
18 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
19 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
20 | 18, 19 | op1std 7178 |
. . . . . . . . 9
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (1st ‘𝑧) = 𝑥) |
21 | 20 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐹‘(1st ‘𝑧)) = (𝐹‘𝑥)) |
22 | 18, 19 | op2ndd 7179 |
. . . . . . . . 9
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (2nd ‘𝑧) = 𝑦) |
23 | 22 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐹‘(2nd ‘𝑧)) = (𝐹‘𝑦)) |
24 | 21, 23 | oveq12d 6668 |
. . . . . . 7
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) = ((𝐹‘𝑥)𝐽(𝐹‘𝑦))) |
25 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐻‘𝑧) = (𝐻‘〈𝑥, 𝑦〉)) |
26 | | df-ov 6653 |
. . . . . . . 8
⊢ (𝑥𝐻𝑦) = (𝐻‘〈𝑥, 𝑦〉) |
27 | 25, 26 | syl6eqr 2674 |
. . . . . . 7
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐻‘𝑧) = (𝑥𝐻𝑦)) |
28 | 24, 27 | oveq12d 6668 |
. . . . . 6
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) = (((𝐹‘𝑥)𝐽(𝐹‘𝑦)) ↑𝑚 (𝑥𝐻𝑦))) |
29 | 17, 28 | eleq12d 2695 |
. . . . 5
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ↔ (𝑥𝐺𝑦) ∈ (((𝐹‘𝑥)𝐽(𝐹‘𝑦)) ↑𝑚 (𝑥𝐻𝑦)))) |
30 | 29 | ralxp 5263 |
. . . 4
⊢
(∀𝑧 ∈
(𝐵 × 𝐵)(𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐺𝑦) ∈ (((𝐹‘𝑥)𝐽(𝐹‘𝑦)) ↑𝑚 (𝑥𝐻𝑦))) |
31 | 14, 30 | sylibr 224 |
. . 3
⊢ (𝜑 → ∀𝑧 ∈ (𝐵 × 𝐵)(𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) |
32 | | elixp2 7912 |
. . 3
⊢ (𝐺 ∈ X𝑧 ∈
(𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ↔ (𝐺 ∈ V ∧ 𝐺 Fn (𝐵 × 𝐵) ∧ ∀𝑧 ∈ (𝐵 × 𝐵)(𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)))) |
33 | 8, 2, 31, 32 | syl3anbrc 1246 |
. 2
⊢ (𝜑 → 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) |
34 | | isfuncd.4 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥))) |
35 | | isfuncd.5 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑚 ∈ (𝑥𝐻𝑦) ∧ 𝑛 ∈ (𝑦𝐻𝑧))) → ((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))) |
36 | 35 | 3expia 1267 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑚 ∈ (𝑥𝐻𝑦) ∧ 𝑛 ∈ (𝑦𝐻𝑧)) → ((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))) |
37 | 36 | 3exp2 1285 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐵 → (𝑦 ∈ 𝐵 → (𝑧 ∈ 𝐵 → ((𝑚 ∈ (𝑥𝐻𝑦) ∧ 𝑛 ∈ (𝑦𝐻𝑧)) → ((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))))) |
38 | 37 | imp43 621 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑚 ∈ (𝑥𝐻𝑦) ∧ 𝑛 ∈ (𝑦𝐻𝑧)) → ((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))) |
39 | 38 | ralrimivv 2970 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))) |
40 | 39 | ralrimivva 2971 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))) |
41 | 34, 40 | jca 554 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))) |
42 | 41 | ralrimiva 2966 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))) |
43 | | isfunc.c |
. . 3
⊢ 𝐶 = (Base‘𝐸) |
44 | | isfunc.h |
. . 3
⊢ 𝐻 = (Hom ‘𝐷) |
45 | | isfunc.j |
. . 3
⊢ 𝐽 = (Hom ‘𝐸) |
46 | | isfunc.1 |
. . 3
⊢ 1 =
(Id‘𝐷) |
47 | | isfunc.i |
. . 3
⊢ 𝐼 = (Id‘𝐸) |
48 | | isfunc.x |
. . 3
⊢ · =
(comp‘𝐷) |
49 | | isfunc.o |
. . 3
⊢ 𝑂 = (comp‘𝐸) |
50 | | isfunc.d |
. . 3
⊢ (𝜑 → 𝐷 ∈ Cat) |
51 | | isfunc.e |
. . 3
⊢ (𝜑 → 𝐸 ∈ Cat) |
52 | 3, 43, 44, 45, 46, 47, 48, 49, 50, 51 | isfunc 16524 |
. 2
⊢ (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ (𝐹:𝐵⟶𝐶 ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))))) |
53 | 1, 33, 42, 52 | mpbir3and 1245 |
1
⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) |