Step | Hyp | Ref
| Expression |
1 | | mrsubvr.v |
. . . 4
⊢ 𝑉 = (mVR‘𝑇) |
2 | | mrsubvr.r |
. . . 4
⊢ 𝑅 = (mREx‘𝑇) |
3 | | mrsubvr.s |
. . . 4
⊢ 𝑆 = (mRSubst‘𝑇) |
4 | 1, 2, 3 | mrsubff 30663 |
. . 3
⊢ (𝑇 ∈ 𝑊 → 𝑆:(𝑅 ↑pm 𝑉)⟶(𝑅 ↑𝑚 𝑅)) |
5 | | mapsspm 7777 |
. . . 4
⊢ (𝑅 ↑𝑚
𝑉) ⊆ (𝑅 ↑pm
𝑉) |
6 | 5 | a1i 11 |
. . 3
⊢ (𝑇 ∈ 𝑊 → (𝑅 ↑𝑚 𝑉) ⊆ (𝑅 ↑pm 𝑉)) |
7 | 4, 6 | fssresd 5984 |
. 2
⊢ (𝑇 ∈ 𝑊 → (𝑆 ↾ (𝑅 ↑𝑚 𝑉)):(𝑅 ↑𝑚 𝑉)⟶(𝑅 ↑𝑚 𝑅)) |
8 | | fveq1 6102 |
. . . . . 6
⊢ ((𝑆‘𝑓) = (𝑆‘𝑔) → ((𝑆‘𝑓)‘〈“𝑣”〉) = ((𝑆‘𝑔)‘〈“𝑣”〉)) |
9 | | simplrl 796 |
. . . . . . . . 9
⊢ (((𝑇 ∈ 𝑊 ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑣 ∈ 𝑉) → 𝑓 ∈ (𝑅 ↑𝑚 𝑉)) |
10 | | elmapi 7765 |
. . . . . . . . 9
⊢ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) → 𝑓:𝑉⟶𝑅) |
11 | 9, 10 | syl 17 |
. . . . . . . 8
⊢ (((𝑇 ∈ 𝑊 ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑣 ∈ 𝑉) → 𝑓:𝑉⟶𝑅) |
12 | | ssid 3587 |
. . . . . . . . 9
⊢ 𝑉 ⊆ 𝑉 |
13 | 12 | a1i 11 |
. . . . . . . 8
⊢ (((𝑇 ∈ 𝑊 ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑣 ∈ 𝑉) → 𝑉 ⊆ 𝑉) |
14 | | simpr 476 |
. . . . . . . 8
⊢ (((𝑇 ∈ 𝑊 ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑣 ∈ 𝑉) → 𝑣 ∈ 𝑉) |
15 | 1, 2, 3 | mrsubvr 30662 |
. . . . . . . 8
⊢ ((𝑓:𝑉⟶𝑅 ∧ 𝑉 ⊆ 𝑉 ∧ 𝑣 ∈ 𝑉) → ((𝑆‘𝑓)‘〈“𝑣”〉) = (𝑓‘𝑣)) |
16 | 11, 13, 14, 15 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝑇 ∈ 𝑊 ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑣 ∈ 𝑉) → ((𝑆‘𝑓)‘〈“𝑣”〉) = (𝑓‘𝑣)) |
17 | | simplrr 797 |
. . . . . . . . 9
⊢ (((𝑇 ∈ 𝑊 ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑣 ∈ 𝑉) → 𝑔 ∈ (𝑅 ↑𝑚 𝑉)) |
18 | | elmapi 7765 |
. . . . . . . . 9
⊢ (𝑔 ∈ (𝑅 ↑𝑚 𝑉) → 𝑔:𝑉⟶𝑅) |
19 | 17, 18 | syl 17 |
. . . . . . . 8
⊢ (((𝑇 ∈ 𝑊 ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑣 ∈ 𝑉) → 𝑔:𝑉⟶𝑅) |
20 | 1, 2, 3 | mrsubvr 30662 |
. . . . . . . 8
⊢ ((𝑔:𝑉⟶𝑅 ∧ 𝑉 ⊆ 𝑉 ∧ 𝑣 ∈ 𝑉) → ((𝑆‘𝑔)‘〈“𝑣”〉) = (𝑔‘𝑣)) |
21 | 19, 13, 14, 20 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝑇 ∈ 𝑊 ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑣 ∈ 𝑉) → ((𝑆‘𝑔)‘〈“𝑣”〉) = (𝑔‘𝑣)) |
22 | 16, 21 | eqeq12d 2625 |
. . . . . 6
⊢ (((𝑇 ∈ 𝑊 ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑣 ∈ 𝑉) → (((𝑆‘𝑓)‘〈“𝑣”〉) = ((𝑆‘𝑔)‘〈“𝑣”〉) ↔ (𝑓‘𝑣) = (𝑔‘𝑣))) |
23 | 8, 22 | syl5ib 233 |
. . . . 5
⊢ (((𝑇 ∈ 𝑊 ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑣 ∈ 𝑉) → ((𝑆‘𝑓) = (𝑆‘𝑔) → (𝑓‘𝑣) = (𝑔‘𝑣))) |
24 | 23 | ralrimdva 2952 |
. . . 4
⊢ ((𝑇 ∈ 𝑊 ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) → ((𝑆‘𝑓) = (𝑆‘𝑔) → ∀𝑣 ∈ 𝑉 (𝑓‘𝑣) = (𝑔‘𝑣))) |
25 | | fvres 6117 |
. . . . . 6
⊢ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) → ((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑓) = (𝑆‘𝑓)) |
26 | | fvres 6117 |
. . . . . 6
⊢ (𝑔 ∈ (𝑅 ↑𝑚 𝑉) → ((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑔) = (𝑆‘𝑔)) |
27 | 25, 26 | eqeqan12d 2626 |
. . . . 5
⊢ ((𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉)) → (((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑓) = ((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑔) ↔ (𝑆‘𝑓) = (𝑆‘𝑔))) |
28 | 27 | adantl 481 |
. . . 4
⊢ ((𝑇 ∈ 𝑊 ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) → (((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑓) = ((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑔) ↔ (𝑆‘𝑓) = (𝑆‘𝑔))) |
29 | | ffn 5958 |
. . . . . . 7
⊢ (𝑓:𝑉⟶𝑅 → 𝑓 Fn 𝑉) |
30 | | ffn 5958 |
. . . . . . 7
⊢ (𝑔:𝑉⟶𝑅 → 𝑔 Fn 𝑉) |
31 | | eqfnfv 6219 |
. . . . . . 7
⊢ ((𝑓 Fn 𝑉 ∧ 𝑔 Fn 𝑉) → (𝑓 = 𝑔 ↔ ∀𝑣 ∈ 𝑉 (𝑓‘𝑣) = (𝑔‘𝑣))) |
32 | 29, 30, 31 | syl2an 493 |
. . . . . 6
⊢ ((𝑓:𝑉⟶𝑅 ∧ 𝑔:𝑉⟶𝑅) → (𝑓 = 𝑔 ↔ ∀𝑣 ∈ 𝑉 (𝑓‘𝑣) = (𝑔‘𝑣))) |
33 | 10, 18, 32 | syl2an 493 |
. . . . 5
⊢ ((𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉)) → (𝑓 = 𝑔 ↔ ∀𝑣 ∈ 𝑉 (𝑓‘𝑣) = (𝑔‘𝑣))) |
34 | 33 | adantl 481 |
. . . 4
⊢ ((𝑇 ∈ 𝑊 ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑓 = 𝑔 ↔ ∀𝑣 ∈ 𝑉 (𝑓‘𝑣) = (𝑔‘𝑣))) |
35 | 24, 28, 34 | 3imtr4d 282 |
. . 3
⊢ ((𝑇 ∈ 𝑊 ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) → (((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑓) = ((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑔) → 𝑓 = 𝑔)) |
36 | 35 | ralrimivva 2954 |
. 2
⊢ (𝑇 ∈ 𝑊 → ∀𝑓 ∈ (𝑅 ↑𝑚 𝑉)∀𝑔 ∈ (𝑅 ↑𝑚 𝑉)(((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑓) = ((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑔) → 𝑓 = 𝑔)) |
37 | | dff13 6416 |
. 2
⊢ ((𝑆 ↾ (𝑅 ↑𝑚 𝑉)):(𝑅 ↑𝑚 𝑉)–1-1→(𝑅 ↑𝑚 𝑅) ↔ ((𝑆 ↾ (𝑅 ↑𝑚 𝑉)):(𝑅 ↑𝑚 𝑉)⟶(𝑅 ↑𝑚 𝑅) ∧ ∀𝑓 ∈ (𝑅 ↑𝑚 𝑉)∀𝑔 ∈ (𝑅 ↑𝑚 𝑉)(((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑓) = ((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑔) → 𝑓 = 𝑔))) |
38 | 7, 36, 37 | sylanbrc 695 |
1
⊢ (𝑇 ∈ 𝑊 → (𝑆 ↾ (𝑅 ↑𝑚 𝑉)):(𝑅 ↑𝑚 𝑉)–1-1→(𝑅 ↑𝑚 𝑅)) |