Metamath Proof Explorer


Theorem csbwrdg

Description: Class substitution for the symbols of a word. (Contributed by Alexander van der Vekens, 15-Jul-2018)

Ref Expression
Assertion csbwrdg ( 𝑆𝑉 𝑆 / 𝑥 Word 𝑥 = Word 𝑆 )

Proof

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