Metamath Proof Explorer

Theorem mrsubcv

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

Ref Expression
Hypotheses mrsubffval.c ⊢ C = mCN ⁡ T
mrsubffval.v ⊢ V = mVR ⁡ T
mrsubffval.r ⊢ R = mREx ⁡ T
mrsubffval.s ⊢ S = mRSubst ⁡ T
Assertion mrsubcv ⊢ F : A ⟶ R ∧ A ⊆ V ∧ X ∈ C ∪ V → S ⁡ F ⁡ ⟨“ X ”⟩ = if X ∈ A F ⁡ X ⟨“ X ”⟩

Proof

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