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