Step |
Hyp |
Ref |
Expression |
1 |
|
mrsubvr.v |
⊢ 𝑉 = ( mVR ‘ 𝑇 ) |
2 |
|
mrsubvr.r |
⊢ 𝑅 = ( mREx ‘ 𝑇 ) |
3 |
|
mrsubvr.s |
⊢ 𝑆 = ( mRSubst ‘ 𝑇 ) |
4 |
1 2 3
|
mrsubff |
⊢ ( 𝑇 ∈ 𝑊 → 𝑆 : ( 𝑅 ↑pm 𝑉 ) ⟶ ( 𝑅 ↑m 𝑅 ) ) |
5 |
|
mapsspm |
⊢ ( 𝑅 ↑m 𝑉 ) ⊆ ( 𝑅 ↑pm 𝑉 ) |
6 |
5
|
a1i |
⊢ ( 𝑇 ∈ 𝑊 → ( 𝑅 ↑m 𝑉 ) ⊆ ( 𝑅 ↑pm 𝑉 ) ) |
7 |
4 6
|
fssresd |
⊢ ( 𝑇 ∈ 𝑊 → ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) : ( 𝑅 ↑m 𝑉 ) ⟶ ( 𝑅 ↑m 𝑅 ) ) |
8 |
|
fveq1 |
⊢ ( ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) → ( ( 𝑆 ‘ 𝑓 ) ‘ 〈“ 𝑣 ”〉 ) = ( ( 𝑆 ‘ 𝑔 ) ‘ 〈“ 𝑣 ”〉 ) ) |
9 |
|
simplrl |
⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ) |
10 |
|
elmapi |
⊢ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) → 𝑓 : 𝑉 ⟶ 𝑅 ) |
11 |
9 10
|
syl |
⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑓 : 𝑉 ⟶ 𝑅 ) |
12 |
|
ssidd |
⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑉 ⊆ 𝑉 ) |
13 |
|
simpr |
⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ 𝑉 ) |
14 |
1 2 3
|
mrsubvr |
⊢ ( ( 𝑓 : 𝑉 ⟶ 𝑅 ∧ 𝑉 ⊆ 𝑉 ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝑆 ‘ 𝑓 ) ‘ 〈“ 𝑣 ”〉 ) = ( 𝑓 ‘ 𝑣 ) ) |
15 |
11 12 13 14
|
syl3anc |
⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝑆 ‘ 𝑓 ) ‘ 〈“ 𝑣 ”〉 ) = ( 𝑓 ‘ 𝑣 ) ) |
16 |
|
simplrr |
⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) |
17 |
|
elmapi |
⊢ ( 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) → 𝑔 : 𝑉 ⟶ 𝑅 ) |
18 |
16 17
|
syl |
⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑔 : 𝑉 ⟶ 𝑅 ) |
19 |
1 2 3
|
mrsubvr |
⊢ ( ( 𝑔 : 𝑉 ⟶ 𝑅 ∧ 𝑉 ⊆ 𝑉 ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝑆 ‘ 𝑔 ) ‘ 〈“ 𝑣 ”〉 ) = ( 𝑔 ‘ 𝑣 ) ) |
20 |
18 12 13 19
|
syl3anc |
⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝑆 ‘ 𝑔 ) ‘ 〈“ 𝑣 ”〉 ) = ( 𝑔 ‘ 𝑣 ) ) |
21 |
15 20
|
eqeq12d |
⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( ( 𝑆 ‘ 𝑓 ) ‘ 〈“ 𝑣 ”〉 ) = ( ( 𝑆 ‘ 𝑔 ) ‘ 〈“ 𝑣 ”〉 ) ↔ ( 𝑓 ‘ 𝑣 ) = ( 𝑔 ‘ 𝑣 ) ) ) |
22 |
8 21
|
syl5ib |
⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) → ( 𝑓 ‘ 𝑣 ) = ( 𝑔 ‘ 𝑣 ) ) ) |
23 |
22
|
ralrimdva |
⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) → ∀ 𝑣 ∈ 𝑉 ( 𝑓 ‘ 𝑣 ) = ( 𝑔 ‘ 𝑣 ) ) ) |
24 |
|
fvres |
⊢ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) → ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑓 ) = ( 𝑆 ‘ 𝑓 ) ) |
25 |
|
fvres |
⊢ ( 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) → ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑔 ) = ( 𝑆 ‘ 𝑔 ) ) |
26 |
24 25
|
eqeqan12d |
⊢ ( ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑓 ) = ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑔 ) ↔ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) ) |
27 |
26
|
adantl |
⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑓 ) = ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑔 ) ↔ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) ) |
28 |
|
ffn |
⊢ ( 𝑓 : 𝑉 ⟶ 𝑅 → 𝑓 Fn 𝑉 ) |
29 |
|
ffn |
⊢ ( 𝑔 : 𝑉 ⟶ 𝑅 → 𝑔 Fn 𝑉 ) |
30 |
|
eqfnfv |
⊢ ( ( 𝑓 Fn 𝑉 ∧ 𝑔 Fn 𝑉 ) → ( 𝑓 = 𝑔 ↔ ∀ 𝑣 ∈ 𝑉 ( 𝑓 ‘ 𝑣 ) = ( 𝑔 ‘ 𝑣 ) ) ) |
31 |
28 29 30
|
syl2an |
⊢ ( ( 𝑓 : 𝑉 ⟶ 𝑅 ∧ 𝑔 : 𝑉 ⟶ 𝑅 ) → ( 𝑓 = 𝑔 ↔ ∀ 𝑣 ∈ 𝑉 ( 𝑓 ‘ 𝑣 ) = ( 𝑔 ‘ 𝑣 ) ) ) |
32 |
10 17 31
|
syl2an |
⊢ ( ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( 𝑓 = 𝑔 ↔ ∀ 𝑣 ∈ 𝑉 ( 𝑓 ‘ 𝑣 ) = ( 𝑔 ‘ 𝑣 ) ) ) |
33 |
32
|
adantl |
⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝑓 = 𝑔 ↔ ∀ 𝑣 ∈ 𝑉 ( 𝑓 ‘ 𝑣 ) = ( 𝑔 ‘ 𝑣 ) ) ) |
34 |
23 27 33
|
3imtr4d |
⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑓 ) = ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑔 ) → 𝑓 = 𝑔 ) ) |
35 |
34
|
ralrimivva |
⊢ ( 𝑇 ∈ 𝑊 → ∀ 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∀ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ( ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑓 ) = ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑔 ) → 𝑓 = 𝑔 ) ) |
36 |
|
dff13 |
⊢ ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) : ( 𝑅 ↑m 𝑉 ) –1-1→ ( 𝑅 ↑m 𝑅 ) ↔ ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) : ( 𝑅 ↑m 𝑉 ) ⟶ ( 𝑅 ↑m 𝑅 ) ∧ ∀ 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∀ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ( ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑓 ) = ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑔 ) → 𝑓 = 𝑔 ) ) ) |
37 |
7 35 36
|
sylanbrc |
⊢ ( 𝑇 ∈ 𝑊 → ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) : ( 𝑅 ↑m 𝑉 ) –1-1→ ( 𝑅 ↑m 𝑅 ) ) |