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 C_ T -> Word S C_ Word T ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fss | |- ( ( w : ( 0 ..^ ( # ` w ) ) --> S /\ S C_ T ) -> w : ( 0 ..^ ( # ` w ) ) --> T ) |
|
| 2 | 1 | expcom | |- ( S C_ T -> ( w : ( 0 ..^ ( # ` w ) ) --> S -> w : ( 0 ..^ ( # ` w ) ) --> T ) ) |
| 3 | iswrdb | |- ( w e. Word S <-> w : ( 0 ..^ ( # ` w ) ) --> S ) |
|
| 4 | iswrdb | |- ( w e. Word T <-> w : ( 0 ..^ ( # ` w ) ) --> T ) |
|
| 5 | 2 3 4 | 3imtr4g | |- ( S C_ T -> ( w e. Word S -> w e. Word T ) ) |
| 6 | 5 | ssrdv | |- ( S C_ T -> Word S C_ Word T ) |