Step | Hyp | Ref
| Expression |
1 | | isfunc.d |
. . . 4
⊢ (𝜑 → 𝐷 ∈ Cat) |
2 | | isfunc.e |
. . . 4
⊢ (𝜑 → 𝐸 ∈ Cat) |
3 | | fvex 6113 |
. . . . . . . 8
⊢
(Base‘𝑑)
∈ V |
4 | 3 | a1i 11 |
. . . . . . 7
⊢ ((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) → (Base‘𝑑) ∈ V) |
5 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) → 𝑑 = 𝐷) |
6 | 5 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) → (Base‘𝑑) = (Base‘𝐷)) |
7 | | isfunc.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐷) |
8 | 6, 7 | syl6eqr 2662 |
. . . . . . 7
⊢ ((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) → (Base‘𝑑) = 𝐵) |
9 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵) |
10 | | simplr 788 |
. . . . . . . . . . . . 13
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → 𝑒 = 𝐸) |
11 | 10 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Base‘𝑒) = (Base‘𝐸)) |
12 | | isfunc.c |
. . . . . . . . . . . 12
⊢ 𝐶 = (Base‘𝐸) |
13 | 11, 12 | syl6eqr 2662 |
. . . . . . . . . . 11
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Base‘𝑒) = 𝐶) |
14 | 9, 13 | feq23d 5953 |
. . . . . . . . . 10
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑓:𝑏⟶(Base‘𝑒) ↔ 𝑓:𝐵⟶𝐶)) |
15 | | fvex 6113 |
. . . . . . . . . . . 12
⊢
(Base‘𝐸)
∈ V |
16 | 12, 15 | eqeltri 2684 |
. . . . . . . . . . 11
⊢ 𝐶 ∈ V |
17 | | fvex 6113 |
. . . . . . . . . . . 12
⊢
(Base‘𝐷)
∈ V |
18 | 7, 17 | eqeltri 2684 |
. . . . . . . . . . 11
⊢ 𝐵 ∈ V |
19 | 16, 18 | elmap 7772 |
. . . . . . . . . 10
⊢ (𝑓 ∈ (𝐶 ↑𝑚 𝐵) ↔ 𝑓:𝐵⟶𝐶) |
20 | 14, 19 | syl6bbr 277 |
. . . . . . . . 9
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑓:𝑏⟶(Base‘𝑒) ↔ 𝑓 ∈ (𝐶 ↑𝑚 𝐵))) |
21 | 9 | sqxpeqd 5065 |
. . . . . . . . . . . 12
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑏 × 𝑏) = (𝐵 × 𝐵)) |
22 | 21 | ixpeq1d 7806 |
. . . . . . . . . . 11
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑𝑚
((Hom ‘𝑑)‘𝑧)) = X𝑧 ∈
(𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑𝑚
((Hom ‘𝑑)‘𝑧))) |
23 | 10 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Hom ‘𝑒) = (Hom ‘𝐸)) |
24 | | isfunc.j |
. . . . . . . . . . . . . . 15
⊢ 𝐽 = (Hom ‘𝐸) |
25 | 23, 24 | syl6eqr 2662 |
. . . . . . . . . . . . . 14
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Hom ‘𝑒) = 𝐽) |
26 | 25 | oveqd 6566 |
. . . . . . . . . . . . 13
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) = ((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧)))) |
27 | | simpll 786 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → 𝑑 = 𝐷) |
28 | 27 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Hom ‘𝑑) = (Hom ‘𝐷)) |
29 | | isfunc.h |
. . . . . . . . . . . . . . 15
⊢ 𝐻 = (Hom ‘𝐷) |
30 | 28, 29 | syl6eqr 2662 |
. . . . . . . . . . . . . 14
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Hom ‘𝑑) = 𝐻) |
31 | 30 | fveq1d 6105 |
. . . . . . . . . . . . 13
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((Hom ‘𝑑)‘𝑧) = (𝐻‘𝑧)) |
32 | 26, 31 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑𝑚
((Hom ‘𝑑)‘𝑧)) = (((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) |
33 | 32 | ixpeq2dv 7810 |
. . . . . . . . . . 11
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑𝑚
((Hom ‘𝑑)‘𝑧)) = X𝑧 ∈
(𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) |
34 | 22, 33 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑𝑚
((Hom ‘𝑑)‘𝑧)) = X𝑧 ∈
(𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) |
35 | 34 | eleq2d 2673 |
. . . . . . . . 9
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑𝑚
((Hom ‘𝑑)‘𝑧)) ↔ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)))) |
36 | 27 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Id‘𝑑) = (Id‘𝐷)) |
37 | | isfunc.1 |
. . . . . . . . . . . . . . 15
⊢ 1 =
(Id‘𝐷) |
38 | 36, 37 | syl6eqr 2662 |
. . . . . . . . . . . . . 14
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Id‘𝑑) = 1 ) |
39 | 38 | fveq1d 6105 |
. . . . . . . . . . . . 13
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((Id‘𝑑)‘𝑥) = ( 1 ‘𝑥)) |
40 | 39 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((𝑥𝑔𝑥)‘( 1 ‘𝑥))) |
41 | 10 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Id‘𝑒) = (Id‘𝐸)) |
42 | | isfunc.i |
. . . . . . . . . . . . . 14
⊢ 𝐼 = (Id‘𝐸) |
43 | 41, 42 | syl6eqr 2662 |
. . . . . . . . . . . . 13
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (Id‘𝑒) = 𝐼) |
44 | 43 | fveq1d 6105 |
. . . . . . . . . . . 12
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((Id‘𝑒)‘(𝑓‘𝑥)) = (𝐼‘(𝑓‘𝑥))) |
45 | 40, 44 | eqeq12d 2625 |
. . . . . . . . . . 11
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓‘𝑥)) ↔ ((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)))) |
46 | 30 | oveqd 6566 |
. . . . . . . . . . . . . 14
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑥(Hom ‘𝑑)𝑦) = (𝑥𝐻𝑦)) |
47 | 30 | oveqd 6566 |
. . . . . . . . . . . . . . 15
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑦(Hom ‘𝑑)𝑧) = (𝑦𝐻𝑧)) |
48 | 27 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (comp‘𝑑) = (comp‘𝐷)) |
49 | | isfunc.x |
. . . . . . . . . . . . . . . . . . . 20
⊢ · =
(comp‘𝐷) |
50 | 48, 49 | syl6eqr 2662 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (comp‘𝑑) = · ) |
51 | 50 | oveqd 6566 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (〈𝑥, 𝑦〉(comp‘𝑑)𝑧) = (〈𝑥, 𝑦〉 · 𝑧)) |
52 | 51 | oveqd 6566 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (𝑛(〈𝑥, 𝑦〉(comp‘𝑑)𝑧)𝑚) = (𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) |
53 | 52 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝑑)𝑧)𝑚)) = ((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚))) |
54 | 10 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (comp‘𝑒) = (comp‘𝐸)) |
55 | | isfunc.o |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑂 = (comp‘𝐸) |
56 | 54, 55 | syl6eqr 2662 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (comp‘𝑒) = 𝑂) |
57 | 56 | oveqd 6566 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝑒)(𝑓‘𝑧)) = (〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))) |
58 | 57 | oveqd 6566 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))) |
59 | 53, 58 | eqeq12d 2625 |
. . . . . . . . . . . . . . 15
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) |
60 | 47, 59 | raleqbidv 3129 |
. . . . . . . . . . . . . 14
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) |
61 | 46, 60 | raleqbidv 3129 |
. . . . . . . . . . . . 13
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) |
62 | 9, 61 | raleqbidv 3129 |
. . . . . . . . . . . 12
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) |
63 | 9, 62 | raleqbidv 3129 |
. . . . . . . . . . 11
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) |
64 | 45, 63 | anbi12d 743 |
. . . . . . . . . 10
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))) |
65 | 9, 64 | raleqbidv 3129 |
. . . . . . . . 9
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → (∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))) |
66 | 20, 35, 65 | 3anbi123d 1391 |
. . . . . . . 8
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((𝑓:𝑏⟶(Base‘𝑒) ∧ 𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑𝑚
((Hom ‘𝑑)‘𝑧)) ∧ ∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ (𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))) |
67 | | df-3an 1033 |
. . . . . . . 8
⊢ ((𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))) |
68 | 66, 67 | syl6bb 275 |
. . . . . . 7
⊢ (((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) ∧ 𝑏 = 𝐵) → ((𝑓:𝑏⟶(Base‘𝑒) ∧ 𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑𝑚
((Hom ‘𝑑)‘𝑧)) ∧ ∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))) |
69 | 4, 8, 68 | sbcied2 3440 |
. . . . . 6
⊢ ((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) → ([(Base‘𝑑) / 𝑏](𝑓:𝑏⟶(Base‘𝑒) ∧ 𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑𝑚
((Hom ‘𝑑)‘𝑧)) ∧ ∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ ((𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))) |
70 | 69 | opabbidv 4648 |
. . . . 5
⊢ ((𝑑 = 𝐷 ∧ 𝑒 = 𝐸) → {〈𝑓, 𝑔〉 ∣ [(Base‘𝑑) / 𝑏](𝑓:𝑏⟶(Base‘𝑒) ∧ 𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑𝑚
((Hom ‘𝑑)‘𝑧)) ∧ ∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))} = {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))}) |
71 | | df-func 16341 |
. . . . 5
⊢ Func =
(𝑑 ∈ Cat, 𝑒 ∈ Cat ↦ {〈𝑓, 𝑔〉 ∣ [(Base‘𝑑) / 𝑏](𝑓:𝑏⟶(Base‘𝑒) ∧ 𝑔 ∈ X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st ‘𝑧))(Hom ‘𝑒)(𝑓‘(2nd ‘𝑧))) ↑𝑚
((Hom ‘𝑑)‘𝑧)) ∧ ∀𝑥 ∈ 𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑑)‘𝑥)) = ((Id‘𝑒)‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑚 ∈ (𝑥(Hom ‘𝑑)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑑)𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉(comp‘𝑑)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉(comp‘𝑒)(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))}) |
72 | | ovex 6577 |
. . . . . . 7
⊢ (𝐶 ↑𝑚
𝐵) ∈
V |
73 | | snex 4835 |
. . . . . . . 8
⊢ {𝑓} ∈ V |
74 | | ovex 6577 |
. . . . . . . . . 10
⊢ (((𝑓‘(1st
‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ∈ V |
75 | 74 | rgenw 2908 |
. . . . . . . . 9
⊢
∀𝑧 ∈
(𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ∈ V |
76 | | ixpexg 7818 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
(𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ∈ V → X𝑧 ∈
(𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ∈ V) |
77 | 75, 76 | ax-mp 5 |
. . . . . . . 8
⊢ X𝑧 ∈
(𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ∈ V |
78 | 73, 77 | xpex 6860 |
. . . . . . 7
⊢ ({𝑓} × X𝑧 ∈
(𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) ∈ V |
79 | 72, 78 | iunex 7039 |
. . . . . 6
⊢ ∪ 𝑓 ∈ (𝐶 ↑𝑚 𝐵)({𝑓} × X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) ∈ V |
80 | | simpl 472 |
. . . . . . . . . 10
⊢ (((𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) → (𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)))) |
81 | 80 | anim2i 591 |
. . . . . . . . 9
⊢ ((𝑑 = 〈𝑓, 𝑔〉 ∧ ((𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))) → (𝑑 = 〈𝑓, 𝑔〉 ∧ (𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))))) |
82 | 81 | 2eximi 1753 |
. . . . . . . 8
⊢
(∃𝑓∃𝑔(𝑑 = 〈𝑓, 𝑔〉 ∧ ((𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))) → ∃𝑓∃𝑔(𝑑 = 〈𝑓, 𝑔〉 ∧ (𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))))) |
83 | | elopab 4908 |
. . . . . . . 8
⊢ (𝑑 ∈ {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))} ↔ ∃𝑓∃𝑔(𝑑 = 〈𝑓, 𝑔〉 ∧ ((𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))))) |
84 | | eliunxp 5181 |
. . . . . . . 8
⊢ (𝑑 ∈ ∪ 𝑓 ∈ (𝐶 ↑𝑚 𝐵)({𝑓} × X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) ↔ ∃𝑓∃𝑔(𝑑 = 〈𝑓, 𝑔〉 ∧ (𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))))) |
85 | 82, 83, 84 | 3imtr4i 280 |
. . . . . . 7
⊢ (𝑑 ∈ {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))} → 𝑑 ∈ ∪
𝑓 ∈ (𝐶 ↑𝑚 𝐵)({𝑓} × X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)))) |
86 | 85 | ssriv 3572 |
. . . . . 6
⊢
{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))} ⊆ ∪ 𝑓 ∈ (𝐶 ↑𝑚 𝐵)({𝑓} × X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) |
87 | 79, 86 | ssexi 4731 |
. . . . 5
⊢
{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))} ∈ V |
88 | 70, 71, 87 | ovmpt2a 6689 |
. . . 4
⊢ ((𝐷 ∈ Cat ∧ 𝐸 ∈ Cat) → (𝐷 Func 𝐸) = {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))}) |
89 | 1, 2, 88 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝐷 Func 𝐸) = {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))}) |
90 | 89 | breqd 4594 |
. 2
⊢ (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ 𝐹{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))}𝐺)) |
91 | | brabv 6597 |
. . . 4
⊢ (𝐹{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))}𝐺 → (𝐹 ∈ V ∧ 𝐺 ∈ V)) |
92 | | elex 3185 |
. . . . . 6
⊢ (𝐹 ∈ (𝐶 ↑𝑚 𝐵) → 𝐹 ∈ V) |
93 | | elex 3185 |
. . . . . 6
⊢ (𝐺 ∈ X𝑧 ∈
(𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) → 𝐺 ∈ V) |
94 | 92, 93 | anim12i 588 |
. . . . 5
⊢ ((𝐹 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) → (𝐹 ∈ V ∧ 𝐺 ∈ V)) |
95 | 94 | 3adant3 1074 |
. . . 4
⊢ ((𝐹 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))) → (𝐹 ∈ V ∧ 𝐺 ∈ V)) |
96 | | simpl 472 |
. . . . . . . 8
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → 𝑓 = 𝐹) |
97 | 96 | eleq1d 2672 |
. . . . . . 7
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓 ∈ (𝐶 ↑𝑚 𝐵) ↔ 𝐹 ∈ (𝐶 ↑𝑚 𝐵))) |
98 | | simpr 476 |
. . . . . . . 8
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺) |
99 | 96 | fveq1d 6105 |
. . . . . . . . . . 11
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓‘(1st ‘𝑧)) = (𝐹‘(1st ‘𝑧))) |
100 | 96 | fveq1d 6105 |
. . . . . . . . . . 11
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓‘(2nd ‘𝑧)) = (𝐹‘(2nd ‘𝑧))) |
101 | 99, 100 | oveq12d 6567 |
. . . . . . . . . 10
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) = ((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧)))) |
102 | 101 | oveq1d 6564 |
. . . . . . . . 9
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) = (((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) |
103 | 102 | ixpeq2dv 7810 |
. . . . . . . 8
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) = X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) |
104 | 98, 103 | eleq12d 2682 |
. . . . . . 7
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ↔ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)))) |
105 | 98 | oveqd 6566 |
. . . . . . . . . . 11
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑥𝑔𝑥) = (𝑥𝐺𝑥)) |
106 | 105 | fveq1d 6105 |
. . . . . . . . . 10
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = ((𝑥𝐺𝑥)‘( 1 ‘𝑥))) |
107 | 96 | fveq1d 6105 |
. . . . . . . . . . 11
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓‘𝑥) = (𝐹‘𝑥)) |
108 | 107 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝐼‘(𝑓‘𝑥)) = (𝐼‘(𝐹‘𝑥))) |
109 | 106, 108 | eqeq12d 2625 |
. . . . . . . . 9
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ↔ ((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)))) |
110 | 98 | oveqd 6566 |
. . . . . . . . . . . . 13
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑥𝑔𝑧) = (𝑥𝐺𝑧)) |
111 | 110 | fveq1d 6105 |
. . . . . . . . . . . 12
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = ((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚))) |
112 | 96 | fveq1d 6105 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓‘𝑦) = (𝐹‘𝑦)) |
113 | 107, 112 | opeq12d 4348 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → 〈(𝑓‘𝑥), (𝑓‘𝑦)〉 = 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) |
114 | 96 | fveq1d 6105 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑓‘𝑧) = (𝐹‘𝑧)) |
115 | 113, 114 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧)) = (〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))) |
116 | 98 | oveqd 6566 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑦𝑔𝑧) = (𝑦𝐺𝑧)) |
117 | 116 | fveq1d 6105 |
. . . . . . . . . . . . 13
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑦𝑔𝑧)‘𝑛) = ((𝑦𝐺𝑧)‘𝑛)) |
118 | 98 | oveqd 6566 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (𝑥𝑔𝑦) = (𝑥𝐺𝑦)) |
119 | 118 | fveq1d 6105 |
. . . . . . . . . . . . 13
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑥𝑔𝑦)‘𝑚) = ((𝑥𝐺𝑦)‘𝑚)) |
120 | 115, 117,
119 | oveq123d 6570 |
. . . . . . . . . . . 12
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))) |
121 | 111, 120 | eqeq12d 2625 |
. . . . . . . . . . 11
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))) |
122 | 121 | 2ralbidv 2972 |
. . . . . . . . . 10
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))) |
123 | 122 | 2ralbidv 2972 |
. . . . . . . . 9
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)) ↔ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))) |
124 | 109, 123 | anbi12d 743 |
. . . . . . . 8
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))) |
125 | 124 | ralbidv 2969 |
. . . . . . 7
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))) ↔ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))) |
126 | 97, 104, 125 | 3anbi123d 1391 |
. . . . . 6
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → ((𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ (𝐹 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))))) |
127 | 67, 126 | syl5bbr 273 |
. . . . 5
⊢ ((𝑓 = 𝐹 ∧ 𝑔 = 𝐺) → (((𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚)))) ↔ (𝐹 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))))) |
128 | | eqid 2610 |
. . . . 5
⊢
{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))} = {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))} |
129 | 127, 128 | brabga 4914 |
. . . 4
⊢ ((𝐹 ∈ V ∧ 𝐺 ∈ V) → (𝐹{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))}𝐺 ↔ (𝐹 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))))) |
130 | 91, 95, 129 | pm5.21nii 367 |
. . 3
⊢ (𝐹{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))}𝐺 ↔ (𝐹 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))) |
131 | 16, 18 | elmap 7772 |
. . . 4
⊢ (𝐹 ∈ (𝐶 ↑𝑚 𝐵) ↔ 𝐹:𝐵⟶𝐶) |
132 | 131 | 3anbi1i 1246 |
. . 3
⊢ ((𝐹 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))) ↔ (𝐹:𝐵⟶𝐶 ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))) |
133 | 130, 132 | bitri 263 |
. 2
⊢ (𝐹{〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ (𝐶 ↑𝑚 𝐵) ∧ 𝑔 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝑓‘(1st ‘𝑧))𝐽(𝑓‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧))) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝑔𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝑓‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝑔𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(〈(𝑓‘𝑥), (𝑓‘𝑦)〉𝑂(𝑓‘𝑧))((𝑥𝑔𝑦)‘𝑚))))}𝐺 ↔ (𝐹:𝐵⟶𝐶 ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))) |
134 | 90, 133 | syl6bb 275 |
1
⊢ (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ (𝐹:𝐵⟶𝐶 ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑𝑚
(𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))))) |