Theorem sswrd

Description: The set of words respects ordering on the base set. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by Mario Carneiro, 26-Feb-2016) (Proof shortened by AV, 13-May-2020)

	Ref	Expression
Assertion	sswrd	$$⊢S\subseteq T\to \mathrm{Word}S\subseteq \mathrm{Word}T$$

Proof

Step	Hyp	Ref	Expression
1		fss	$$⊢\left(w:\left(0..^\left|w\right|\right)⟶S\wedge S\subseteq T\right)\to w:\left(0..^\left|w\right|\right)⟶T$$
2	1	expcom	$$⊢S\subseteq T\to \left(w:\left(0..^\left|w\right|\right)⟶S\to w:\left(0..^\left|w\right|\right)⟶T\right)$$
3		iswrdb	$$⊢w\in \mathrm{Word}S\leftrightarrow w:\left(0..^\left|w\right|\right)⟶S$$
4		iswrdb	$$⊢w\in \mathrm{Word}T\leftrightarrow w:\left(0..^\left|w\right|\right)⟶T$$
5	2 3 4	3imtr4g	$$⊢S\subseteq T\to \left(w\in \mathrm{Word}S\to w\in \mathrm{Word}T\right)$$
6	5	ssrdv	$$⊢S\subseteq T\to \mathrm{Word}S\subseteq \mathrm{Word}T$$