Metamath Proof Explorer

Theorem msubff1

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

Ref Expression
Hypotheses msubff1.v ⊢ 𝑉 = ( mVR ‘ 𝑇 )
msubff1.r ⊢ 𝑅 = ( mREx ‘ 𝑇 )
msubff1.s ⊢ 𝑆 = ( mSubst ‘ 𝑇 )
msubff1.e ⊢ 𝐸 = ( mEx ‘ 𝑇 )
Assertion msubff1 ( 𝑇 ∈ mFS → ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) : ( 𝑅 ↑m 𝑉 ) –1-1→ ( 𝐸 ↑m 𝐸 ) )

Proof

Step Hyp Ref Expression
1 msubff1.v ⊢ 𝑉 = ( mVR ‘ 𝑇 )
2 msubff1.r ⊢ 𝑅 = ( mREx ‘ 𝑇 )
3 msubff1.s ⊢ 𝑆 = ( mSubst ‘ 𝑇 )
4 msubff1.e ⊢ 𝐸 = ( mEx ‘ 𝑇 )
5 1 2 3 4 msubff ⊢ ( 𝑇 ∈ mFS → 𝑆 : ( 𝑅 ↑pm 𝑉 ) ⟶ ( 𝐸 ↑m 𝐸 ) )
6 mapsspm ⊢ ( 𝑅 ↑m 𝑉 ) ⊆ ( 𝑅 ↑pm 𝑉 )
7 6 a1i ⊢ ( 𝑇 ∈ mFS → ( 𝑅 ↑m 𝑉 ) ⊆ ( 𝑅 ↑pm 𝑉 ) )
8 5 7 fssresd ⊢ ( 𝑇 ∈ mFS → ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) : ( 𝑅 ↑m 𝑉 ) ⟶ ( 𝐸 ↑m 𝐸 ) )
9 eqid ⊢ ( mRSubst ‘ 𝑇 ) = ( mRSubst ‘ 𝑇 )
10 1 2 9 mrsubff ⊢ ( 𝑇 ∈ mFS → ( mRSubst ‘ 𝑇 ) : ( 𝑅 ↑pm 𝑉 ) ⟶ ( 𝑅 ↑m 𝑅 ) )
11 10 ad2antrr ⊢ ( ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) ) → ( mRSubst ‘ 𝑇 ) : ( 𝑅 ↑pm 𝑉 ) ⟶ ( 𝑅 ↑m 𝑅 ) )
12 simplrl ⊢ ( ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) ) → 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) )
13 6 12 sselid ⊢ ( ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) ) → 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) )
14 11 13 ffvelrnd ⊢ ( ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) ) → ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ∈ ( 𝑅 ↑m 𝑅 ) )
15 elmapi ⊢ ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ∈ ( 𝑅 ↑m 𝑅 ) → ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) : 𝑅 ⟶ 𝑅 )
16 ffn ⊢ ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) : 𝑅 ⟶ 𝑅 → ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) Fn 𝑅 )
17 14 15 16 3syl ⊢ ( ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) ) → ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) Fn 𝑅 )
18 simplrr ⊢ ( ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) ) → 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) )
19 6 18 sselid ⊢ ( ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) ) → 𝑔 ∈ ( 𝑅 ↑pm 𝑉 ) )
20 11 19 ffvelrnd ⊢ ( ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) ) → ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) ∈ ( 𝑅 ↑m 𝑅 ) )
21 elmapi ⊢ ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) ∈ ( 𝑅 ↑m 𝑅 ) → ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) : 𝑅 ⟶ 𝑅 )
22 ffn ⊢ ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) : 𝑅 ⟶ 𝑅 → ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) Fn 𝑅 )
23 20 21 22 3syl ⊢ ( ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) ) → ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) Fn 𝑅 )
24 simplrr ⊢ ( ( ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) ) ∧ 𝑟 ∈ 𝑅 ) → ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) )
25 24 fveq1d ⊢ ( ( ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) ) ∧ 𝑟 ∈ 𝑅 ) → ( ( 𝑆 ‘ 𝑓 ) ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) = ( ( 𝑆 ‘ 𝑔 ) ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) )
26 12 adantr ⊢ ( ( ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) ) ∧ 𝑟 ∈ 𝑅 ) → 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) )
27 elmapi ⊢ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) → 𝑓 : 𝑉 ⟶ 𝑅 )
28 26 27 syl ⊢ ( ( ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) ) ∧ 𝑟 ∈ 𝑅 ) → 𝑓 : 𝑉 ⟶ 𝑅 )
29 ssidd ⊢ ( ( ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) ) ∧ 𝑟 ∈ 𝑅 ) → 𝑉 ⊆ 𝑉 )
30 eqid ⊢ ( mTC ‘ 𝑇 ) = ( mTC ‘ 𝑇 )
31 eqid ⊢ ( mType ‘ 𝑇 ) = ( mType ‘ 𝑇 )
32 1 30 31 mtyf2 ⊢ ( 𝑇 ∈ mFS → ( mType ‘ 𝑇 ) : 𝑉 ⟶ ( mTC ‘ 𝑇 ) )
33 32 ad3antrrr ⊢ ( ( ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) ) ∧ 𝑟 ∈ 𝑅 ) → ( mType ‘ 𝑇 ) : 𝑉 ⟶ ( mTC ‘ 𝑇 ) )
34 simplrl ⊢ ( ( ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) ) ∧ 𝑟 ∈ 𝑅 ) → 𝑣 ∈ 𝑉 )
35 33 34 ffvelrnd ⊢ ( ( ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) ) ∧ 𝑟 ∈ 𝑅 ) → ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) ∈ ( mTC ‘ 𝑇 ) )
36 opelxpi ⊢ ( ( ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) ∈ ( mTC ‘ 𝑇 ) ∧ 𝑟 ∈ 𝑅 ) → ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ∈ ( ( mTC ‘ 𝑇 ) × 𝑅 ) )
37 35 36 sylancom ⊢ ( ( ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) ) ∧ 𝑟 ∈ 𝑅 ) → ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ∈ ( ( mTC ‘ 𝑇 ) × 𝑅 ) )
38 30 4 2 mexval ⊢ 𝐸 = ( ( mTC ‘ 𝑇 ) × 𝑅 )
39 37 38 eleqtrrdi ⊢ ( ( ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) ) ∧ 𝑟 ∈ 𝑅 ) → ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ∈ 𝐸 )
40 1 2 3 4 9 msubval ⊢ ( ( 𝑓 : 𝑉 ⟶ 𝑅 ∧ 𝑉 ⊆ 𝑉 ∧ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ∈ 𝐸 ) → ( ( 𝑆 ‘ 𝑓 ) ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) = ⟨ ( 1st ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2nd ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) ) ⟩ )
41 28 29 39 40 syl3anc ⊢ ( ( ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) ) ∧ 𝑟 ∈ 𝑅 ) → ( ( 𝑆 ‘ 𝑓 ) ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) = ⟨ ( 1st ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2nd ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) ) ⟩ )
42 18 adantr ⊢ ( ( ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) ) ∧ 𝑟 ∈ 𝑅 ) → 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) )
43 elmapi ⊢ ( 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) → 𝑔 : 𝑉 ⟶ 𝑅 )
44 42 43 syl ⊢ ( ( ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) ) ∧ 𝑟 ∈ 𝑅 ) → 𝑔 : 𝑉 ⟶ 𝑅 )
45 1 2 3 4 9 msubval ⊢ ( ( 𝑔 : 𝑉 ⟶ 𝑅 ∧ 𝑉 ⊆ 𝑉 ∧ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ∈ 𝐸 ) → ( ( 𝑆 ‘ 𝑔 ) ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) = ⟨ ( 1st ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) ‘ ( 2nd ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) ) ⟩ )
46 44 29 39 45 syl3anc ⊢ ( ( ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) ) ∧ 𝑟 ∈ 𝑅 ) → ( ( 𝑆 ‘ 𝑔 ) ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) = ⟨ ( 1st ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) ‘ ( 2nd ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) ) ⟩ )
47 25 41 46 3eqtr3d ⊢ ( ( ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) ) ∧ 𝑟 ∈ 𝑅 ) → ⟨ ( 1st ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2nd ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) ) ⟩ = ⟨ ( 1st ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) ‘ ( 2nd ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) ) ⟩ )
48 fvex ⊢ ( 1st ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) ∈ V
49 fvex ⊢ ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2nd ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) ) ∈ V
50 48 49 opth ⊢ ( ⟨ ( 1st ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2nd ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) ) ⟩ = ⟨ ( 1st ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) ‘ ( 2nd ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) ) ⟩ ↔ ( ( 1st ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) = ( 1st ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) ∧ ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2nd ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) ) = ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) ‘ ( 2nd ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) ) ) )
51 50 simprbi ⊢ ( ⟨ ( 1st ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2nd ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) ) ⟩ = ⟨ ( 1st ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) ‘ ( 2nd ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) ) ⟩ → ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2nd ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) ) = ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) ‘ ( 2nd ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) ) )
52 47 51 syl ⊢ ( ( ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) ) ∧ 𝑟 ∈ 𝑅 ) → ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2nd ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) ) = ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) ‘ ( 2nd ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) ) )
53 fvex ⊢ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) ∈ V
54 vex ⊢ 𝑟 ∈ V
55 53 54 op2nd ⊢ ( 2nd ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) = 𝑟
56 55 fveq2i ⊢ ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2nd ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) ) = ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ 𝑟 )
57 55 fveq2i ⊢ ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) ‘ ( 2nd ‘ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , 𝑟 ⟩ ) ) = ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) ‘ 𝑟 )
58 52 56 57 3eqtr3g ⊢ ( ( ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) ) ∧ 𝑟 ∈ 𝑅 ) → ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ 𝑟 ) = ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) ‘ 𝑟 ) )
59 17 23 58 eqfnfvd ⊢ ( ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) ) → ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) = ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) )
60 1 2 9 mrsubff1 ⊢ ( 𝑇 ∈ mFS → ( ( mRSubst ‘ 𝑇 ) ↾ ( 𝑅 ↑m 𝑉 ) ) : ( 𝑅 ↑m 𝑉 ) –1-1→ ( 𝑅 ↑m 𝑅 ) )
61 f1fveq ⊢ ( ( ( ( mRSubst ‘ 𝑇 ) ↾ ( 𝑅 ↑m 𝑉 ) ) : ( 𝑅 ↑m 𝑉 ) –1-1→ ( 𝑅 ↑m 𝑅 ) ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( ( ( ( mRSubst ‘ 𝑇 ) ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑓 ) = ( ( ( mRSubst ‘ 𝑇 ) ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑔 ) ↔ 𝑓 = 𝑔 ) )
62 60 61 sylan ⊢ ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( ( ( ( mRSubst ‘ 𝑇 ) ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑓 ) = ( ( ( mRSubst ‘ 𝑇 ) ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑔 ) ↔ 𝑓 = 𝑔 ) )
63 fvres ⊢ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) → ( ( ( mRSubst ‘ 𝑇 ) ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑓 ) = ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) )
64 fvres ⊢ ( 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) → ( ( ( mRSubst ‘ 𝑇 ) ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑔 ) = ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) )
65 63 64 eqeqan12d ⊢ ( ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( ( ( ( mRSubst ‘ 𝑇 ) ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑓 ) = ( ( ( mRSubst ‘ 𝑇 ) ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑔 ) ↔ ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) = ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) ) )
66 65 adantl ⊢ ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( ( ( ( mRSubst ‘ 𝑇 ) ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑓 ) = ( ( ( mRSubst ‘ 𝑇 ) ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑔 ) ↔ ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) = ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) ) )
67 62 66 bitr3d ⊢ ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝑓 = 𝑔 ↔ ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) = ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) ) )
68 67 adantr ⊢ ( ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) ) → ( 𝑓 = 𝑔 ↔ ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) = ( ( mRSubst ‘ 𝑇 ) ‘ 𝑔 ) ) )
69 59 68 mpbird ⊢ ( ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) ) → 𝑓 = 𝑔 )
70 69 fveq1d ⊢ ( ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( 𝑣 ∈ 𝑉 ∧ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) ) → ( 𝑓 ‘ 𝑣 ) = ( 𝑔 ‘ 𝑣 ) )
71 70 expr ⊢ ( ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) → ( 𝑓 ‘ 𝑣 ) = ( 𝑔 ‘ 𝑣 ) ) )
72 71 ralrimdva ⊢ ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) → ∀ 𝑣 ∈ 𝑉 ( 𝑓 ‘ 𝑣 ) = ( 𝑔 ‘ 𝑣 ) ) )
73 fvres ⊢ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) → ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑓 ) = ( 𝑆 ‘ 𝑓 ) )
74 fvres ⊢ ( 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) → ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑔 ) = ( 𝑆 ‘ 𝑔 ) )
75 73 74 eqeqan12d ⊢ ( ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑓 ) = ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑔 ) ↔ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) )
76 75 adantl ⊢ ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑓 ) = ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑔 ) ↔ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) )
77 ffn ⊢ ( 𝑓 : 𝑉 ⟶ 𝑅 → 𝑓 Fn 𝑉 )
78 ffn ⊢ ( 𝑔 : 𝑉 ⟶ 𝑅 → 𝑔 Fn 𝑉 )
79 eqfnfv ⊢ ( ( 𝑓 Fn 𝑉 ∧ 𝑔 Fn 𝑉 ) → ( 𝑓 = 𝑔 ↔ ∀ 𝑣 ∈ 𝑉 ( 𝑓 ‘ 𝑣 ) = ( 𝑔 ‘ 𝑣 ) ) )
80 77 78 79 syl2an ⊢ ( ( 𝑓 : 𝑉 ⟶ 𝑅 ∧ 𝑔 : 𝑉 ⟶ 𝑅 ) → ( 𝑓 = 𝑔 ↔ ∀ 𝑣 ∈ 𝑉 ( 𝑓 ‘ 𝑣 ) = ( 𝑔 ‘ 𝑣 ) ) )
81 27 43 80 syl2an ⊢ ( ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( 𝑓 = 𝑔 ↔ ∀ 𝑣 ∈ 𝑉 ( 𝑓 ‘ 𝑣 ) = ( 𝑔 ‘ 𝑣 ) ) )
82 81 adantl ⊢ ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝑓 = 𝑔 ↔ ∀ 𝑣 ∈ 𝑉 ( 𝑓 ‘ 𝑣 ) = ( 𝑔 ‘ 𝑣 ) ) )
83 72 76 82 3imtr4d ⊢ ( ( 𝑇 ∈ mFS ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑓 ) = ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑔 ) → 𝑓 = 𝑔 ) )
84 83 ralrimivva ⊢ ( 𝑇 ∈ mFS → ∀ 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∀ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ( ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑓 ) = ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑔 ) → 𝑓 = 𝑔 ) )
85 dff13 ⊢ ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) : ( 𝑅 ↑m 𝑉 ) –1-1→ ( 𝐸 ↑m 𝐸 ) ↔ ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) : ( 𝑅 ↑m 𝑉 ) ⟶ ( 𝐸 ↑m 𝐸 ) ∧ ∀ 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∀ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ( ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑓 ) = ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑔 ) → 𝑓 = 𝑔 ) ) )
86 8 84 85 sylanbrc ⊢ ( 𝑇 ∈ mFS → ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) : ( 𝑅 ↑m 𝑉 ) –1-1→ ( 𝐸 ↑m 𝐸 ) )