Step |
Hyp |
Ref |
Expression |
1 |
|
df-word |
⊢ Word 𝑥 = { 𝑤 ∣ ∃ 𝑙 ∈ ℕ0 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑥 } |
2 |
1
|
csbeq2i |
⊢ ⦋ 𝑆 / 𝑥 ⦌ Word 𝑥 = ⦋ 𝑆 / 𝑥 ⦌ { 𝑤 ∣ ∃ 𝑙 ∈ ℕ0 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑥 } |
3 |
|
sbcrex |
⊢ ( [ 𝑆 / 𝑥 ] ∃ 𝑙 ∈ ℕ0 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑥 ↔ ∃ 𝑙 ∈ ℕ0 [ 𝑆 / 𝑥 ] 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑥 ) |
4 |
|
sbcfg |
⊢ ( 𝑆 ∈ 𝑉 → ( [ 𝑆 / 𝑥 ] 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑥 ↔ ⦋ 𝑆 / 𝑥 ⦌ 𝑤 : ⦋ 𝑆 / 𝑥 ⦌ ( 0 ..^ 𝑙 ) ⟶ ⦋ 𝑆 / 𝑥 ⦌ 𝑥 ) ) |
5 |
|
csbconstg |
⊢ ( 𝑆 ∈ 𝑉 → ⦋ 𝑆 / 𝑥 ⦌ 𝑤 = 𝑤 ) |
6 |
|
csbconstg |
⊢ ( 𝑆 ∈ 𝑉 → ⦋ 𝑆 / 𝑥 ⦌ ( 0 ..^ 𝑙 ) = ( 0 ..^ 𝑙 ) ) |
7 |
|
csbvarg |
⊢ ( 𝑆 ∈ 𝑉 → ⦋ 𝑆 / 𝑥 ⦌ 𝑥 = 𝑆 ) |
8 |
5 6 7
|
feq123d |
⊢ ( 𝑆 ∈ 𝑉 → ( ⦋ 𝑆 / 𝑥 ⦌ 𝑤 : ⦋ 𝑆 / 𝑥 ⦌ ( 0 ..^ 𝑙 ) ⟶ ⦋ 𝑆 / 𝑥 ⦌ 𝑥 ↔ 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 ) ) |
9 |
4 8
|
bitrd |
⊢ ( 𝑆 ∈ 𝑉 → ( [ 𝑆 / 𝑥 ] 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑥 ↔ 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 ) ) |
10 |
9
|
rexbidv |
⊢ ( 𝑆 ∈ 𝑉 → ( ∃ 𝑙 ∈ ℕ0 [ 𝑆 / 𝑥 ] 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑥 ↔ ∃ 𝑙 ∈ ℕ0 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 ) ) |
11 |
3 10
|
syl5bb |
⊢ ( 𝑆 ∈ 𝑉 → ( [ 𝑆 / 𝑥 ] ∃ 𝑙 ∈ ℕ0 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑥 ↔ ∃ 𝑙 ∈ ℕ0 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 ) ) |
12 |
11
|
abbidv |
⊢ ( 𝑆 ∈ 𝑉 → { 𝑤 ∣ [ 𝑆 / 𝑥 ] ∃ 𝑙 ∈ ℕ0 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑥 } = { 𝑤 ∣ ∃ 𝑙 ∈ ℕ0 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 } ) |
13 |
|
csbab |
⊢ ⦋ 𝑆 / 𝑥 ⦌ { 𝑤 ∣ ∃ 𝑙 ∈ ℕ0 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑥 } = { 𝑤 ∣ [ 𝑆 / 𝑥 ] ∃ 𝑙 ∈ ℕ0 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑥 } |
14 |
|
df-word |
⊢ Word 𝑆 = { 𝑤 ∣ ∃ 𝑙 ∈ ℕ0 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑆 } |
15 |
12 13 14
|
3eqtr4g |
⊢ ( 𝑆 ∈ 𝑉 → ⦋ 𝑆 / 𝑥 ⦌ { 𝑤 ∣ ∃ 𝑙 ∈ ℕ0 𝑤 : ( 0 ..^ 𝑙 ) ⟶ 𝑥 } = Word 𝑆 ) |
16 |
2 15
|
eqtrid |
⊢ ( 𝑆 ∈ 𝑉 → ⦋ 𝑆 / 𝑥 ⦌ Word 𝑥 = Word 𝑆 ) |