This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 bitrid ⊢ ( 𝑆 ∈ 𝑉 → ( [ 𝑆 / 𝑥 ] ∃ 𝑙 ∈ ℕ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 𝑆 )