Metamath Proof Explorer


Theorem mrsubff1

Description: When restricted to complete mappings, the substitution-producing function is one-to-one. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mrsubvr.v 𝑉 = ( mVR ‘ 𝑇 )
mrsubvr.r 𝑅 = ( mREx ‘ 𝑇 )
mrsubvr.s 𝑆 = ( mRSubst ‘ 𝑇 )
Assertion mrsubff1 ( 𝑇𝑊 → ( 𝑆 ↾ ( 𝑅m 𝑉 ) ) : ( 𝑅m 𝑉 ) –1-1→ ( 𝑅m 𝑅 ) )

Proof

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 𝑅 ) )