Metamath Proof Explorer

Theorem mrsubcv

Description: The value of a substituted singleton. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mrsubffval.c ⊢ 𝐶 = ( mCN ‘ 𝑇 )
mrsubffval.v ⊢ 𝑉 = ( mVR ‘ 𝑇 )
mrsubffval.r ⊢ 𝑅 = ( mREx ‘ 𝑇 )
mrsubffval.s ⊢ 𝑆 = ( mRSubst ‘ 𝑇 )
Assertion mrsubcv ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ ( 𝐶 ∪ 𝑉 ) ) → ( ( 𝑆 ‘ 𝐹 ) ‘ ⟨“ 𝑋 ”⟩ ) = if ( 𝑋 ∈ 𝐴 , ( 𝐹 ‘ 𝑋 ) , ⟨“ 𝑋 ”⟩ ) )

Proof

Step Hyp Ref Expression
1 mrsubffval.c ⊢ 𝐶 = ( mCN ‘ 𝑇 )
2 mrsubffval.v ⊢ 𝑉 = ( mVR ‘ 𝑇 )
3 mrsubffval.r ⊢ 𝑅 = ( mREx ‘ 𝑇 )
4 mrsubffval.s ⊢ 𝑆 = ( mRSubst ‘ 𝑇 )
5 simp3 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ ( 𝐶 ∪ 𝑉 ) ) → 𝑋 ∈ ( 𝐶 ∪ 𝑉 ) )
6 5 s1cld ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ ( 𝐶 ∪ 𝑉 ) ) → ⟨“ 𝑋 ”⟩ ∈ Word ( 𝐶 ∪ 𝑉 ) )
7 elun ⊢ ( 𝑋 ∈ ( 𝐶 ∪ 𝑉 ) ↔ ( 𝑋 ∈ 𝐶 ∨ 𝑋 ∈ 𝑉 ) )
8 elfvex ⊢ ( 𝑋 ∈ ( mCN ‘ 𝑇 ) → 𝑇 ∈ V )
9 8 1 eleq2s ⊢ ( 𝑋 ∈ 𝐶 → 𝑇 ∈ V )
10 elfvex ⊢ ( 𝑋 ∈ ( mVR ‘ 𝑇 ) → 𝑇 ∈ V )
11 10 2 eleq2s ⊢ ( 𝑋 ∈ 𝑉 → 𝑇 ∈ V )
12 9 11 jaoi ⊢ ( ( 𝑋 ∈ 𝐶 ∨ 𝑋 ∈ 𝑉 ) → 𝑇 ∈ V )
13 7 12 sylbi ⊢ ( 𝑋 ∈ ( 𝐶 ∪ 𝑉 ) → 𝑇 ∈ V )
14 13 3ad2ant3 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ ( 𝐶 ∪ 𝑉 ) ) → 𝑇 ∈ V )
15 1 2 3 mrexval ⊢ ( 𝑇 ∈ V → 𝑅 = Word ( 𝐶 ∪ 𝑉 ) )
16 14 15 syl ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ ( 𝐶 ∪ 𝑉 ) ) → 𝑅 = Word ( 𝐶 ∪ 𝑉 ) )
17 6 16 eleqtrrd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ ( 𝐶 ∪ 𝑉 ) ) → ⟨“ 𝑋 ”⟩ ∈ 𝑅 )
18 eqid ⊢ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) = ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) )
19 1 2 3 4 18 mrsubval ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ ⟨“ 𝑋 ”⟩ ∈ 𝑅 ) → ( ( 𝑆 ‘ 𝐹 ) ‘ ⟨“ 𝑋 ”⟩ ) = ( ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ ⟨“ 𝑋 ”⟩ ) ) )
20 17 19 syld3an3 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ ( 𝐶 ∪ 𝑉 ) ) → ( ( 𝑆 ‘ 𝐹 ) ‘ ⟨“ 𝑋 ”⟩ ) = ( ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ ⟨“ 𝑋 ”⟩ ) ) )
21 simpl1 ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ ( 𝐶 ∪ 𝑉 ) ) ∧ 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ) → 𝐹 : 𝐴 ⟶ 𝑅 )
22 21 ffvelcdmda ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ ( 𝐶 ∪ 𝑉 ) ) ∧ 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ) ∧ 𝑣 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑣 ) ∈ 𝑅 )
23 16 ad2antrr ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ ( 𝐶 ∪ 𝑉 ) ) ∧ 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ) ∧ 𝑣 ∈ 𝐴 ) → 𝑅 = Word ( 𝐶 ∪ 𝑉 ) )
24 22 23 eleqtrd ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ ( 𝐶 ∪ 𝑉 ) ) ∧ 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ) ∧ 𝑣 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑣 ) ∈ Word ( 𝐶 ∪ 𝑉 ) )
25 simplr ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ ( 𝐶 ∪ 𝑉 ) ) ∧ 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ) ∧ ¬ 𝑣 ∈ 𝐴 ) → 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) )
26 25 s1cld ⊢ ( ( ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ ( 𝐶 ∪ 𝑉 ) ) ∧ 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ) ∧ ¬ 𝑣 ∈ 𝐴 ) → ⟨“ 𝑣 ”⟩ ∈ Word ( 𝐶 ∪ 𝑉 ) )
27 24 26 ifclda ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ ( 𝐶 ∪ 𝑉 ) ) ∧ 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ) → if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ∈ Word ( 𝐶 ∪ 𝑉 ) )
28 27 fmpttd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ ( 𝐶 ∪ 𝑉 ) ) → ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) : ( 𝐶 ∪ 𝑉 ) ⟶ Word ( 𝐶 ∪ 𝑉 ) )
29 s1co ⊢ ( ( 𝑋 ∈ ( 𝐶 ∪ 𝑉 ) ∧ ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) : ( 𝐶 ∪ 𝑉 ) ⟶ Word ( 𝐶 ∪ 𝑉 ) ) → ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ ⟨“ 𝑋 ”⟩ ) = ⟨“ ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ‘ 𝑋 ) ”⟩ )
30 5 28 29 syl2anc ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ ( 𝐶 ∪ 𝑉 ) ) → ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ ⟨“ 𝑋 ”⟩ ) = ⟨“ ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ‘ 𝑋 ) ”⟩ )
31 eleq1 ⊢ ( 𝑣 = 𝑋 → ( 𝑣 ∈ 𝐴 ↔ 𝑋 ∈ 𝐴 ) )
32 fveq2 ⊢ ( 𝑣 = 𝑋 → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑋 ) )
33 s1eq ⊢ ( 𝑣 = 𝑋 → ⟨“ 𝑣 ”⟩ = ⟨“ 𝑋 ”⟩ )
34 31 32 33 ifbieq12d ⊢ ( 𝑣 = 𝑋 → if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) = if ( 𝑋 ∈ 𝐴 , ( 𝐹 ‘ 𝑋 ) , ⟨“ 𝑋 ”⟩ ) )
35 eqid ⊢ ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) = ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) )
36 fvex ⊢ ( 𝐹 ‘ 𝑋 ) ∈ V
37 s1cli ⊢ ⟨“ 𝑋 ”⟩ ∈ Word V
38 37 elexi ⊢ ⟨“ 𝑋 ”⟩ ∈ V
39 36 38 ifex ⊢ if ( 𝑋 ∈ 𝐴 , ( 𝐹 ‘ 𝑋 ) , ⟨“ 𝑋 ”⟩ ) ∈ V
40 34 35 39 fvmpt ⊢ ( 𝑋 ∈ ( 𝐶 ∪ 𝑉 ) → ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ‘ 𝑋 ) = if ( 𝑋 ∈ 𝐴 , ( 𝐹 ‘ 𝑋 ) , ⟨“ 𝑋 ”⟩ ) )
41 40 3ad2ant3 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ ( 𝐶 ∪ 𝑉 ) ) → ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ‘ 𝑋 ) = if ( 𝑋 ∈ 𝐴 , ( 𝐹 ‘ 𝑋 ) , ⟨“ 𝑋 ”⟩ ) )
42 41 s1eqd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ ( 𝐶 ∪ 𝑉 ) ) → ⟨“ ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ‘ 𝑋 ) ”⟩ = ⟨“ if ( 𝑋 ∈ 𝐴 , ( 𝐹 ‘ 𝑋 ) , ⟨“ 𝑋 ”⟩ ) ”⟩ )
43 30 42 eqtrd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ ( 𝐶 ∪ 𝑉 ) ) → ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ ⟨“ 𝑋 ”⟩ ) = ⟨“ if ( 𝑋 ∈ 𝐴 , ( 𝐹 ‘ 𝑋 ) , ⟨“ 𝑋 ”⟩ ) ”⟩ )
44 43 oveq2d ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ ( 𝐶 ∪ 𝑉 ) ) → ( ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) Σg ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ∘ ⟨“ 𝑋 ”⟩ ) ) = ( ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) Σg ⟨“ if ( 𝑋 ∈ 𝐴 , ( 𝐹 ‘ 𝑋 ) , ⟨“ 𝑋 ”⟩ ) ”⟩ ) )
45 28 5 ffvelcdmd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ ( 𝐶 ∪ 𝑉 ) ) → ( ( 𝑣 ∈ ( 𝐶 ∪ 𝑉 ) ↦ if ( 𝑣 ∈ 𝐴 , ( 𝐹 ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ) ) ‘ 𝑋 ) ∈ Word ( 𝐶 ∪ 𝑉 ) )
46 41 45 eqeltrrd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ ( 𝐶 ∪ 𝑉 ) ) → if ( 𝑋 ∈ 𝐴 , ( 𝐹 ‘ 𝑋 ) , ⟨“ 𝑋 ”⟩ ) ∈ Word ( 𝐶 ∪ 𝑉 ) )
47 1 fvexi ⊢ 𝐶 ∈ V
48 2 fvexi ⊢ 𝑉 ∈ V
49 47 48 unex ⊢ ( 𝐶 ∪ 𝑉 ) ∈ V
50 eqid ⊢ ( Base ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) = ( Base ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) )
51 18 50 frmdbas ⊢ ( ( 𝐶 ∪ 𝑉 ) ∈ V → ( Base ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) = Word ( 𝐶 ∪ 𝑉 ) )
52 49 51 ax-mp ⊢ ( Base ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) ) = Word ( 𝐶 ∪ 𝑉 )
53 52 eqcomi ⊢ Word ( 𝐶 ∪ 𝑉 ) = ( Base ‘ ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) )
54 53 gsumws1 ⊢ ( if ( 𝑋 ∈ 𝐴 , ( 𝐹 ‘ 𝑋 ) , ⟨“ 𝑋 ”⟩ ) ∈ Word ( 𝐶 ∪ 𝑉 ) → ( ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) Σg ⟨“ if ( 𝑋 ∈ 𝐴 , ( 𝐹 ‘ 𝑋 ) , ⟨“ 𝑋 ”⟩ ) ”⟩ ) = if ( 𝑋 ∈ 𝐴 , ( 𝐹 ‘ 𝑋 ) , ⟨“ 𝑋 ”⟩ ) )
55 46 54 syl ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ ( 𝐶 ∪ 𝑉 ) ) → ( ( freeMnd ‘ ( 𝐶 ∪ 𝑉 ) ) Σg ⟨“ if ( 𝑋 ∈ 𝐴 , ( 𝐹 ‘ 𝑋 ) , ⟨“ 𝑋 ”⟩ ) ”⟩ ) = if ( 𝑋 ∈ 𝐴 , ( 𝐹 ‘ 𝑋 ) , ⟨“ 𝑋 ”⟩ ) )
56 20 44 55 3eqtrd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ 𝐴 ⊆ 𝑉 ∧ 𝑋 ∈ ( 𝐶 ∪ 𝑉 ) ) → ( ( 𝑆 ‘ 𝐹 ) ‘ ⟨“ 𝑋 ”⟩ ) = if ( 𝑋 ∈ 𝐴 , ( 𝐹 ‘ 𝑋 ) , ⟨“ 𝑋 ”⟩ ) )