This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 Word S \subseteq Word T$

Proof

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