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	syl5eq	⊢ ( 𝑆 ∈ 𝑉 → ⦋ 𝑆 / 𝑥 ⦌ Word 𝑥 = Word 𝑆 )