Metamath Proof Explorer

Theorem mrsubrn

Description: Although it is defined for partial mappings of variables, every partial substitution is a substitution on some complete mapping of the variables. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mrsubvr.v ⊢ 𝑉 = ( mVR ‘ 𝑇 )
mrsubvr.r ⊢ 𝑅 = ( mREx ‘ 𝑇 )
mrsubvr.s ⊢ 𝑆 = ( mRSubst ‘ 𝑇 )
Assertion mrsubrn ran 𝑆 = ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) )

Proof

Step Hyp Ref Expression
1 mrsubvr.v ⊢ 𝑉 = ( mVR ‘ 𝑇 )
2 mrsubvr.r ⊢ 𝑅 = ( mREx ‘ 𝑇 )
3 mrsubvr.s ⊢ 𝑆 = ( mRSubst ‘ 𝑇 )
4 1 2 3 mrsubff ⊢ ( 𝑇 ∈ V → 𝑆 : ( 𝑅 ↑pm 𝑉 ) ⟶ ( 𝑅 ↑m 𝑅 ) )
5 4 ffnd ⊢ ( 𝑇 ∈ V → 𝑆 Fn ( 𝑅 ↑pm 𝑉 ) )
6 eleq1w ⊢ ( 𝑥 = 𝑣 → ( 𝑥 ∈ dom 𝑓 ↔ 𝑣 ∈ dom 𝑓 ) )
7 fveq2 ⊢ ( 𝑥 = 𝑣 → ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑣 ) )
8 s1eq ⊢ ( 𝑥 = 𝑣 → ⟨“ 𝑥 ”⟩ = ⟨“ 𝑣 ”⟩ )
9 6 7 8 ifbieq12d ⊢ ( 𝑥 = 𝑣 → if ( 𝑥 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑥 ) , ⟨“ 𝑥 ”⟩ ) = if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) )
10 eqid ⊢ ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑥 ) , ⟨“ 𝑥 ”⟩ ) ) = ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑥 ) , ⟨“ 𝑥 ”⟩ ) )
11 fvex ⊢ ( 𝑓 ‘ 𝑣 ) ∈ V
12 s1cli ⊢ ⟨“ 𝑣 ”⟩ ∈ Word V
13 12 elexi ⊢ ⟨“ 𝑣 ”⟩ ∈ V
14 11 13 ifex ⊢ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ∈ V
15 9 10 14 fvmpt ⊢ ( 𝑣 ∈ 𝑉 → ( ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑥 ) , ⟨“ 𝑥 ”⟩ ) ) ‘ 𝑣 ) = if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) )
16 15 adantl ⊢ ( ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑥 ) , ⟨“ 𝑥 ”⟩ ) ) ‘ 𝑣 ) = if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) )
17 16 ifeq1da ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) → if ( 𝑣 ∈ 𝑉 , ( ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑥 ) , ⟨“ 𝑥 ”⟩ ) ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) = if ( 𝑣 ∈ 𝑉 , if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) , ⟨“ 𝑣 ”⟩ ) )
18 ifan ⊢ if ( ( 𝑣 ∈ 𝑉 ∧ 𝑣 ∈ dom 𝑓 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) = if ( 𝑣 ∈ 𝑉 , if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) , ⟨“ 𝑣 ”⟩ )
19 17 18 eqtr4di ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) → if ( 𝑣 ∈ 𝑉 , ( ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑥 ) , ⟨“ 𝑥 ”⟩ ) ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) = if ( ( 𝑣 ∈ 𝑉 ∧ 𝑣 ∈ dom 𝑓 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) )
20 elpmi ⊢ ( 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) → ( 𝑓 : dom 𝑓 ⟶ 𝑅 ∧ dom 𝑓 ⊆ 𝑉 ) )
21 20 adantl ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) → ( 𝑓 : dom 𝑓 ⟶ 𝑅 ∧ dom 𝑓 ⊆ 𝑉 ) )
22 21 simprd ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) → dom 𝑓 ⊆ 𝑉 )
23 22 sseld ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) → ( 𝑣 ∈ dom 𝑓 → 𝑣 ∈ 𝑉 ) )
24 23 pm4.71rd ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) → ( 𝑣 ∈ dom 𝑓 ↔ ( 𝑣 ∈ 𝑉 ∧ 𝑣 ∈ dom 𝑓 ) ) )
25 24 bicomd ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) → ( ( 𝑣 ∈ 𝑉 ∧ 𝑣 ∈ dom 𝑓 ) ↔ 𝑣 ∈ dom 𝑓 ) )
26 25 ifbid ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) → if ( ( 𝑣 ∈ 𝑉 ∧ 𝑣 ∈ dom 𝑓 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) = if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) )
27 19 26 eqtr2d ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) → if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) = if ( 𝑣 ∈ 𝑉 , ( ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑥 ) , ⟨“ 𝑥 ”⟩ ) ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) )
28 27 mpteq2dv ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) → ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) = ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝑉 , ( ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑥 ) , ⟨“ 𝑥 ”⟩ ) ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) )
29 28 coeq1d ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) → ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) = ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝑉 , ( ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑥 ) , ⟨“ 𝑥 ”⟩ ) ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) )
30 29 oveq2d ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) → ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) = ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝑉 , ( ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑥 ) , ⟨“ 𝑥 ”⟩ ) ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) )
31 30 mpteq2dv ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) → ( 𝑒 ∈ 𝑅 ↦ ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) = ( 𝑒 ∈ 𝑅 ↦ ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝑉 , ( ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑥 ) , ⟨“ 𝑥 ”⟩ ) ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) )
32 eqid ⊢ ( mCN ‘ 𝑇 ) = ( mCN ‘ 𝑇 )
33 eqid ⊢ ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) = ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) )
34 32 1 2 3 33 mrsubfval ⊢ ( ( 𝑓 : dom 𝑓 ⟶ 𝑅 ∧ dom 𝑓 ⊆ 𝑉 ) → ( 𝑆 ‘ 𝑓 ) = ( 𝑒 ∈ 𝑅 ↦ ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) )
35 21 34 syl ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) → ( 𝑆 ‘ 𝑓 ) = ( 𝑒 ∈ 𝑅 ↦ ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) )
36 21 simpld ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) → 𝑓 : dom 𝑓 ⟶ 𝑅 )
37 36 adantr ⊢ ( ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) ∧ 𝑥 ∈ 𝑉 ) → 𝑓 : dom 𝑓 ⟶ 𝑅 )
38 37 ffvelrnda ⊢ ( ( ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) ∧ 𝑥 ∈ 𝑉 ) ∧ 𝑥 ∈ dom 𝑓 ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝑅 )
39 elun2 ⊢ ( 𝑥 ∈ 𝑉 → 𝑥 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) )
40 39 ad2antlr ⊢ ( ( ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) ∧ 𝑥 ∈ 𝑉 ) ∧ ¬ 𝑥 ∈ dom 𝑓 ) → 𝑥 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) )
41 40 s1cld ⊢ ( ( ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) ∧ 𝑥 ∈ 𝑉 ) ∧ ¬ 𝑥 ∈ dom 𝑓 ) → ⟨“ 𝑥 ”⟩ ∈ Word ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) )
42 32 1 2 mrexval ⊢ ( 𝑇 ∈ V → 𝑅 = Word ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) )
43 42 ad3antrrr ⊢ ( ( ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) ∧ 𝑥 ∈ 𝑉 ) ∧ ¬ 𝑥 ∈ dom 𝑓 ) → 𝑅 = Word ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) )
44 41 43 eleqtrrd ⊢ ( ( ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) ∧ 𝑥 ∈ 𝑉 ) ∧ ¬ 𝑥 ∈ dom 𝑓 ) → ⟨“ 𝑥 ”⟩ ∈ 𝑅 )
45 38 44 ifclda ⊢ ( ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) ∧ 𝑥 ∈ 𝑉 ) → if ( 𝑥 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑥 ) , ⟨“ 𝑥 ”⟩ ) ∈ 𝑅 )
46 45 fmpttd ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) → ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑥 ) , ⟨“ 𝑥 ”⟩ ) ) : 𝑉 ⟶ 𝑅 )
47 ssid ⊢ 𝑉 ⊆ 𝑉
48 32 1 2 3 33 mrsubfval ⊢ ( ( ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑥 ) , ⟨“ 𝑥 ”⟩ ) ) : 𝑉 ⟶ 𝑅 ∧ 𝑉 ⊆ 𝑉 ) → ( 𝑆 ‘ ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑥 ) , ⟨“ 𝑥 ”⟩ ) ) ) = ( 𝑒 ∈ 𝑅 ↦ ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝑉 , ( ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑥 ) , ⟨“ 𝑥 ”⟩ ) ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) )
49 46 47 48 sylancl ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) → ( 𝑆 ‘ ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑥 ) , ⟨“ 𝑥 ”⟩ ) ) ) = ( 𝑒 ∈ 𝑅 ↦ ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝑉 , ( ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑥 ) , ⟨“ 𝑥 ”⟩ ) ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) )
50 31 35 49 3eqtr4d ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) → ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑥 ) , ⟨“ 𝑥 ”⟩ ) ) ) )
51 5 adantr ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) → 𝑆 Fn ( 𝑅 ↑pm 𝑉 ) )
52 mapsspm ⊢ ( 𝑅 ↑m 𝑉 ) ⊆ ( 𝑅 ↑pm 𝑉 )
53 52 a1i ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) → ( 𝑅 ↑m 𝑉 ) ⊆ ( 𝑅 ↑pm 𝑉 ) )
54 2 fvexi ⊢ 𝑅 ∈ V
55 1 fvexi ⊢ 𝑉 ∈ V
56 54 55 elmap ⊢ ( ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑥 ) , ⟨“ 𝑥 ”⟩ ) ) ∈ ( 𝑅 ↑m 𝑉 ) ↔ ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑥 ) , ⟨“ 𝑥 ”⟩ ) ) : 𝑉 ⟶ 𝑅 )
57 46 56 sylibr ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) → ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑥 ) , ⟨“ 𝑥 ”⟩ ) ) ∈ ( 𝑅 ↑m 𝑉 ) )
58 fnfvima ⊢ ( ( 𝑆 Fn ( 𝑅 ↑pm 𝑉 ) ∧ ( 𝑅 ↑m 𝑉 ) ⊆ ( 𝑅 ↑pm 𝑉 ) ∧ ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑥 ) , ⟨“ 𝑥 ”⟩ ) ) ∈ ( 𝑅 ↑m 𝑉 ) ) → ( 𝑆 ‘ ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑥 ) , ⟨“ 𝑥 ”⟩ ) ) ) ∈ ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) ) )
59 51 53 57 58 syl3anc ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) → ( 𝑆 ‘ ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 ∈ dom 𝑓 , ( 𝑓 ‘ 𝑥 ) , ⟨“ 𝑥 ”⟩ ) ) ) ∈ ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) ) )
60 50 59 eqeltrd ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ) → ( 𝑆 ‘ 𝑓 ) ∈ ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) ) )
61 60 ralrimiva ⊢ ( 𝑇 ∈ V → ∀ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ( 𝑆 ‘ 𝑓 ) ∈ ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) ) )
62 ffnfv ⊢ ( 𝑆 : ( 𝑅 ↑pm 𝑉 ) ⟶ ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) ) ↔ ( 𝑆 Fn ( 𝑅 ↑pm 𝑉 ) ∧ ∀ 𝑓 ∈ ( 𝑅 ↑pm 𝑉 ) ( 𝑆 ‘ 𝑓 ) ∈ ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) ) ) )
63 5 61 62 sylanbrc ⊢ ( 𝑇 ∈ V → 𝑆 : ( 𝑅 ↑pm 𝑉 ) ⟶ ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) ) )
64 63 frnd ⊢ ( 𝑇 ∈ V → ran 𝑆 ⊆ ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) ) )
65 3 rnfvprc ⊢ ( ¬ 𝑇 ∈ V → ran 𝑆 = ∅ )
66 0ss ⊢ ∅ ⊆ ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) )
67 65 66 eqsstrdi ⊢ ( ¬ 𝑇 ∈ V → ran 𝑆 ⊆ ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) ) )
68 64 67 pm2.61i ⊢ ran 𝑆 ⊆ ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) )
69 imassrn ⊢ ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) ) ⊆ ran 𝑆
70 68 69 eqssi ⊢ ran 𝑆 = ( 𝑆 “ ( 𝑅 ↑m 𝑉 ) )