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 | ⊢ ( 𝑆 ⊆ 𝑇 → Word 𝑆 ⊆ Word 𝑇 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fss | ⊢ ( ( 𝑤 : ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ⟶ 𝑆 ∧ 𝑆 ⊆ 𝑇 ) → 𝑤 : ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ⟶ 𝑇 ) | |
| 2 | 1 | expcom | ⊢ ( 𝑆 ⊆ 𝑇 → ( 𝑤 : ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ⟶ 𝑆 → 𝑤 : ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ⟶ 𝑇 ) ) |
| 3 | iswrdb | ⊢ ( 𝑤 ∈ Word 𝑆 ↔ 𝑤 : ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ⟶ 𝑆 ) | |
| 4 | iswrdb | ⊢ ( 𝑤 ∈ Word 𝑇 ↔ 𝑤 : ( 0 ..^ ( ♯ ‘ 𝑤 ) ) ⟶ 𝑇 ) | |
| 5 | 2 3 4 | 3imtr4g | ⊢ ( 𝑆 ⊆ 𝑇 → ( 𝑤 ∈ Word 𝑆 → 𝑤 ∈ Word 𝑇 ) ) |
| 6 | 5 | ssrdv | ⊢ ( 𝑆 ⊆ 𝑇 → Word 𝑆 ⊆ Word 𝑇 ) |