poss

Description: Subset theorem for the partial ordering predicate. (Contributed by NM, 27-Mar-1997) (Proof shortened by Mario Carneiro, 18-Nov-2016)

		Ref	Expression
	Assertion	poss	$⊢ A \subseteq B \to (R Po B \to R Po A)$

Step	Hyp	Ref	Expression
1		ssralv	$⊢ A \subseteq B \to (\forall x \in B \forall y \in B \forall z \in B (\neg x R x \land ((x R y \land y R z) \to x R z)) \to \forall x \in A \forall y \in B \forall z \in B (\neg x R x \land ((x R y \land y R z) \to x R z)))$
2		ss2ralv	$⊢ A \subseteq B \to (\forall y \in B \forall z \in B (\neg x R x \land ((x R y \land y R z) \to x R z)) \to \forall y \in A \forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z)))$
3	2	ralimdv	$⊢ A \subseteq B \to (\forall x \in A \forall y \in B \forall z \in B (\neg x R x \land ((x R y \land y R z) \to x R z)) \to \forall x \in A \forall y \in A \forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z)))$
4	1 3	syld	$⊢ A \subseteq B \to (\forall x \in B \forall y \in B \forall z \in B (\neg x R x \land ((x R y \land y R z) \to x R z)) \to \forall x \in A \forall y \in A \forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z)))$
5		df-po	$⊢ R Po B \leftrightarrow \forall x \in B \forall y \in B \forall z \in B (\neg x R x \land ((x R y \land y R z) \to x R z))$
6		df-po	$⊢ R Po A \leftrightarrow \forall x \in A \forall y \in A \forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z))$
7	4 5 6	3imtr4g	$⊢ A \subseteq B \to (R Po B \to R Po A)$

Metamath Proof Explorer