Metamath Proof Explorer

Theorem mrsub0

Description: The value of the substituted empty string. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypothesis mrsubccat.s ⊢ 𝑆 = ( mRSubst ‘ 𝑇 )
Assertion mrsub0 ( 𝐹 ∈ ran 𝑆 → ( 𝐹 ‘ ∅ ) = ∅ )

Proof

Step Hyp Ref Expression
1 mrsubccat.s ⊢ 𝑆 = ( mRSubst ‘ 𝑇 )
2 n0i ⊢ ( 𝐹 ∈ ran 𝑆 → ¬ ran 𝑆 = ∅ )
3 1 rnfvprc ⊢ ( ¬ 𝑇 ∈ V → ran 𝑆 = ∅ )
4 2 3 nsyl2 ⊢ ( 𝐹 ∈ ran 𝑆 → 𝑇 ∈ V )
5 eqid ⊢ ( mVR ‘ 𝑇 ) = ( mVR ‘ 𝑇 )
6 eqid ⊢ ( mREx ‘ 𝑇 ) = ( mREx ‘ 𝑇 )
7 5 6 1 mrsubff ⊢ ( 𝑇 ∈ V → 𝑆 : ( ( mREx ‘ 𝑇 ) ↑pm ( mVR ‘ 𝑇 ) ) ⟶ ( ( mREx ‘ 𝑇 ) ↑m ( mREx ‘ 𝑇 ) ) )
8 ffun ⊢ ( 𝑆 : ( ( mREx ‘ 𝑇 ) ↑pm ( mVR ‘ 𝑇 ) ) ⟶ ( ( mREx ‘ 𝑇 ) ↑m ( mREx ‘ 𝑇 ) ) → Fun 𝑆 )
9 4 7 8 3syl ⊢ ( 𝐹 ∈ ran 𝑆 → Fun 𝑆 )
10 5 6 1 mrsubrn ⊢ ran 𝑆 = ( 𝑆 “ ( ( mREx ‘ 𝑇 ) ↑m ( mVR ‘ 𝑇 ) ) )
11 10 eleq2i ⊢ ( 𝐹 ∈ ran 𝑆 ↔ 𝐹 ∈ ( 𝑆 “ ( ( mREx ‘ 𝑇 ) ↑m ( mVR ‘ 𝑇 ) ) ) )
12 11 biimpi ⊢ ( 𝐹 ∈ ran 𝑆 → 𝐹 ∈ ( 𝑆 “ ( ( mREx ‘ 𝑇 ) ↑m ( mVR ‘ 𝑇 ) ) ) )
13 fvelima ⊢ ( ( Fun 𝑆 ∧ 𝐹 ∈ ( 𝑆 “ ( ( mREx ‘ 𝑇 ) ↑m ( mVR ‘ 𝑇 ) ) ) ) → ∃ 𝑓 ∈ ( ( mREx ‘ 𝑇 ) ↑m ( mVR ‘ 𝑇 ) ) ( 𝑆 ‘ 𝑓 ) = 𝐹 )
14 9 12 13 syl2anc ⊢ ( 𝐹 ∈ ran 𝑆 → ∃ 𝑓 ∈ ( ( mREx ‘ 𝑇 ) ↑m ( mVR ‘ 𝑇 ) ) ( 𝑆 ‘ 𝑓 ) = 𝐹 )
15 elmapi ⊢ ( 𝑓 ∈ ( ( mREx ‘ 𝑇 ) ↑m ( mVR ‘ 𝑇 ) ) → 𝑓 : ( mVR ‘ 𝑇 ) ⟶ ( mREx ‘ 𝑇 ) )
16 15 adantl ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( ( mREx ‘ 𝑇 ) ↑m ( mVR ‘ 𝑇 ) ) ) → 𝑓 : ( mVR ‘ 𝑇 ) ⟶ ( mREx ‘ 𝑇 ) )
17 ssidd ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( ( mREx ‘ 𝑇 ) ↑m ( mVR ‘ 𝑇 ) ) ) → ( mVR ‘ 𝑇 ) ⊆ ( mVR ‘ 𝑇 ) )
18 wrd0 ⊢ ∅ ∈ Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) )
19 eqid ⊢ ( mCN ‘ 𝑇 ) = ( mCN ‘ 𝑇 )
20 19 5 6 mrexval ⊢ ( 𝑇 ∈ V → ( mREx ‘ 𝑇 ) = Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) )
21 20 adantr ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( ( mREx ‘ 𝑇 ) ↑m ( mVR ‘ 𝑇 ) ) ) → ( mREx ‘ 𝑇 ) = Word ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) )
22 18 21 eleqtrrid ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( ( mREx ‘ 𝑇 ) ↑m ( mVR ‘ 𝑇 ) ) ) → ∅ ∈ ( mREx ‘ 𝑇 ) )
23 eqid ⊢ ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) = ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) )
24 19 5 6 1 23 mrsubval ⊢ ( ( 𝑓 : ( mVR ‘ 𝑇 ) ⟶ ( mREx ‘ 𝑇 ) ∧ ( mVR ‘ 𝑇 ) ⊆ ( mVR ‘ 𝑇 ) ∧ ∅ ∈ ( mREx ‘ 𝑇 ) ) → ( ( 𝑆 ‘ 𝑓 ) ‘ ∅ ) = ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ↦ if ( 𝑣 ∈ ( mVR ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ ∅ ) ) )
25 16 17 22 24 syl3anc ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( ( mREx ‘ 𝑇 ) ↑m ( mVR ‘ 𝑇 ) ) ) → ( ( 𝑆 ‘ 𝑓 ) ‘ ∅ ) = ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ↦ if ( 𝑣 ∈ ( mVR ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ ∅ ) ) )
26 co02 ⊢ ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ↦ if ( 𝑣 ∈ ( mVR ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ ∅ ) = ∅
27 26 oveq2i ⊢ ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ↦ if ( 𝑣 ∈ ( mVR ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ ∅ ) ) = ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) Σg ∅ )
28 23 frmd0 ⊢ ∅ = ( 0g ‘ ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) )
29 28 gsum0 ⊢ ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) Σg ∅ ) = ∅
30 27 29 eqtri ⊢ ( ( freeMnd ‘ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ) Σg ( ( 𝑣 ∈ ( ( mCN ‘ 𝑇 ) ∪ ( mVR ‘ 𝑇 ) ) ↦ if ( 𝑣 ∈ ( mVR ‘ 𝑇 ) , ( 𝑓 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ ∅ ) ) = ∅
31 25 30 eqtrdi ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( ( mREx ‘ 𝑇 ) ↑m ( mVR ‘ 𝑇 ) ) ) → ( ( 𝑆 ‘ 𝑓 ) ‘ ∅ ) = ∅ )
32 fveq1 ⊢ ( ( 𝑆 ‘ 𝑓 ) = 𝐹 → ( ( 𝑆 ‘ 𝑓 ) ‘ ∅ ) = ( 𝐹 ‘ ∅ ) )
33 32 eqeq1d ⊢ ( ( 𝑆 ‘ 𝑓 ) = 𝐹 → ( ( ( 𝑆 ‘ 𝑓 ) ‘ ∅ ) = ∅ ↔ ( 𝐹 ‘ ∅ ) = ∅ ) )
34 31 33 syl5ibcom ⊢ ( ( 𝑇 ∈ V ∧ 𝑓 ∈ ( ( mREx ‘ 𝑇 ) ↑m ( mVR ‘ 𝑇 ) ) ) → ( ( 𝑆 ‘ 𝑓 ) = 𝐹 → ( 𝐹 ‘ ∅ ) = ∅ ) )
35 34 rexlimdva ⊢ ( 𝑇 ∈ V → ( ∃ 𝑓 ∈ ( ( mREx ‘ 𝑇 ) ↑m ( mVR ‘ 𝑇 ) ) ( 𝑆 ‘ 𝑓 ) = 𝐹 → ( 𝐹 ‘ ∅ ) = ∅ ) )
36 4 14 35 sylc ⊢ ( 𝐹 ∈ ran 𝑆 → ( 𝐹 ‘ ∅ ) = ∅ )