Metamath Proof Explorer


Theorem lpadlem1

Description: Lemma for the leftpad theorems. (Contributed by Thierry Arnoux, 7-Aug-2023)

Ref Expression
Hypothesis lpadlem1.1 φCS
Assertion lpadlem1 φ0..^LW×CWordS

Proof

Step Hyp Ref Expression
1 lpadlem1.1 φCS
2 fconst6g CS0..^LW×C:0..^LWS
3 iswrdi 0..^LW×C:0..^LWS0..^LW×CWordS
4 1 2 3 3syl φ0..^LW×CWordS