# Metamath Proof Explorer

## Theorem mrsubff

Description: A substitution is a function from R to R . (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mrsubvr.v 𝑉 = ( mVR ‘ 𝑇 )
mrsubvr.r 𝑅 = ( mREx ‘ 𝑇 )
mrsubvr.s 𝑆 = ( mRSubst ‘ 𝑇 )
Assertion mrsubff ( 𝑇𝑊𝑆 : ( 𝑅pm 𝑉 ) ⟶ ( 𝑅m 𝑅 ) )

### Proof

Step Hyp Ref Expression
1 mrsubvr.v 𝑉 = ( mVR ‘ 𝑇 )
2 mrsubvr.r 𝑅 = ( mREx ‘ 𝑇 )
3 mrsubvr.s 𝑆 = ( mRSubst ‘ 𝑇 )
4 fvex ( mCN ‘ 𝑇 ) ∈ V
5 1 fvexi 𝑉 ∈ V
6 4 5 unex ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ∈ V
7 eqid ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) = ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) )
8 7 frmdmnd ( ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ∈ V → ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) ∈ Mnd )
9 6 8 mp1i ( ( ( 𝑇𝑊𝑓 ∈ ( 𝑅pm 𝑉 ) ) ∧ 𝑒𝑅 ) → ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) ∈ Mnd )
10 simpr ( ( ( 𝑇𝑊𝑓 ∈ ( 𝑅pm 𝑉 ) ) ∧ 𝑒𝑅 ) → 𝑒𝑅 )
11 eqid ( mCN ‘ 𝑇 ) = ( mCN ‘ 𝑇 )
12 11 1 2 mrexval ( 𝑇𝑊𝑅 = Word ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) )
13 12 ad2antrr ( ( ( 𝑇𝑊𝑓 ∈ ( 𝑅pm 𝑉 ) ) ∧ 𝑒𝑅 ) → 𝑅 = Word ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) )
14 10 13 eleqtrd ( ( ( 𝑇𝑊𝑓 ∈ ( 𝑅pm 𝑉 ) ) ∧ 𝑒𝑅 ) → 𝑒 ∈ Word ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) )
15 elpmi ( 𝑓 ∈ ( 𝑅pm 𝑉 ) → ( 𝑓 : dom 𝑓𝑅 ∧ dom 𝑓𝑉 ) )
16 15 simpld ( 𝑓 ∈ ( 𝑅pm 𝑉 ) → 𝑓 : dom 𝑓𝑅 )
17 16 ad3antlr ( ( ( ( 𝑇𝑊𝑓 ∈ ( 𝑅pm 𝑉 ) ) ∧ 𝑒𝑅 ) ∧ 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) → 𝑓 : dom 𝑓𝑅 )
18 17 ffvelrnda ( ( ( ( ( 𝑇𝑊𝑓 ∈ ( 𝑅pm 𝑉 ) ) ∧ 𝑒𝑅 ) ∧ 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) ∧ 𝑣 ∈ dom 𝑓 ) → ( 𝑓𝑣 ) ∈ 𝑅 )
19 13 ad2antrr ( ( ( ( ( 𝑇𝑊𝑓 ∈ ( 𝑅pm 𝑉 ) ) ∧ 𝑒𝑅 ) ∧ 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) ∧ 𝑣 ∈ dom 𝑓 ) → 𝑅 = Word ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) )
20 18 19 eleqtrd ( ( ( ( ( 𝑇𝑊𝑓 ∈ ( 𝑅pm 𝑉 ) ) ∧ 𝑒𝑅 ) ∧ 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) ∧ 𝑣 ∈ dom 𝑓 ) → ( 𝑓𝑣 ) ∈ Word ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) )
21 simplr ( ( ( ( ( 𝑇𝑊𝑓 ∈ ( 𝑅pm 𝑉 ) ) ∧ 𝑒𝑅 ) ∧ 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) ∧ ¬ 𝑣 ∈ dom 𝑓 ) → 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) )
22 21 s1cld ( ( ( ( ( 𝑇𝑊𝑓 ∈ ( 𝑅pm 𝑉 ) ) ∧ 𝑒𝑅 ) ∧ 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) ∧ ¬ 𝑣 ∈ dom 𝑓 ) → ⟨“ 𝑣 ”⟩ ∈ Word ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) )
23 20 22 ifclda ( ( ( ( 𝑇𝑊𝑓 ∈ ( 𝑅pm 𝑉 ) ) ∧ 𝑒𝑅 ) ∧ 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) → if ( 𝑣 ∈ dom 𝑓 , ( 𝑓𝑣 ) , ⟨“ 𝑣 ”⟩ ) ∈ Word ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) )
24 23 fmpttd ( ( ( 𝑇𝑊𝑓 ∈ ( 𝑅pm 𝑉 ) ) ∧ 𝑒𝑅 ) → ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) : ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ⟶ Word ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) )
25 wrdco ( ( 𝑒 ∈ Word ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ∧ ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) : ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ⟶ Word ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) → ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ∈ Word Word ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) )
26 14 24 25 syl2anc ( ( ( 𝑇𝑊𝑓 ∈ ( 𝑅pm 𝑉 ) ) ∧ 𝑒𝑅 ) → ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ∈ Word Word ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) )
27 eqid ( Base ‘ ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) ) = ( Base ‘ ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) )
28 7 27 frmdbas ( ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ∈ V → ( Base ‘ ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) ) = Word ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) )
29 6 28 ax-mp ( Base ‘ ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) ) = Word ( ( mCN ‘ 𝑇 ) ∪ 𝑉 )
30 29 eqcomi Word ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) = ( Base ‘ ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) )
31 30 gsumwcl ( ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) ∈ Mnd ∧ ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ∈ Word Word ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) → ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ∈ Word ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) )
32 9 26 31 syl2anc ( ( ( 𝑇𝑊𝑓 ∈ ( 𝑅pm 𝑉 ) ) ∧ 𝑒𝑅 ) → ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ∈ Word ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) )
33 32 13 eleqtrrd ( ( ( 𝑇𝑊𝑓 ∈ ( 𝑅pm 𝑉 ) ) ∧ 𝑒𝑅 ) → ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ∈ 𝑅 )
34 33 fmpttd ( ( 𝑇𝑊𝑓 ∈ ( 𝑅pm 𝑉 ) ) → ( 𝑒𝑅 ↦ ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) : 𝑅𝑅 )
35 2 fvexi 𝑅 ∈ V
36 35 35 elmap ( ( 𝑒𝑅 ↦ ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) ∈ ( 𝑅m 𝑅 ) ↔ ( 𝑒𝑅 ↦ ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) : 𝑅𝑅 )
37 34 36 sylibr ( ( 𝑇𝑊𝑓 ∈ ( 𝑅pm 𝑉 ) ) → ( 𝑒𝑅 ↦ ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) ∈ ( 𝑅m 𝑅 ) )
38 37 fmpttd ( 𝑇𝑊 → ( 𝑓 ∈ ( 𝑅pm 𝑉 ) ↦ ( 𝑒𝑅 ↦ ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) ) : ( 𝑅pm 𝑉 ) ⟶ ( 𝑅m 𝑅 ) )
39 11 1 2 3 7 mrsubffval ( 𝑇𝑊𝑆 = ( 𝑓 ∈ ( 𝑅pm 𝑉 ) ↦ ( 𝑒𝑅 ↦ ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) ) )
40 39 feq1d ( 𝑇𝑊 → ( 𝑆 : ( 𝑅pm 𝑉 ) ⟶ ( 𝑅m 𝑅 ) ↔ ( 𝑓 ∈ ( 𝑅pm 𝑉 ) ↦ ( 𝑒𝑅 ↦ ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ 𝑉 ) ↦ if ( 𝑣 ∈ dom 𝑓 , ( 𝑓𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ 𝑒 ) ) ) ) : ( 𝑅pm 𝑉 ) ⟶ ( 𝑅m 𝑅 ) ) )
41 38 40 mpbird ( 𝑇𝑊𝑆 : ( 𝑅pm 𝑉 ) ⟶ ( 𝑅m 𝑅 ) )