# Metamath Proof Explorer

## Theorem 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 ⊆ B → R Po B → R Po A$

### Proof

Step Hyp Ref Expression
1 ssralv $⊢ A ⊆ B → ∀ x ∈ B ∀ y ∈ B ∀ z ∈ B ¬ x R x ∧ x R y ∧ y R z → x R z → ∀ x ∈ A ∀ y ∈ B ∀ z ∈ B ¬ x R x ∧ x R y ∧ y R z → x R z$
2 ss2ralv $⊢ A ⊆ B → ∀ y ∈ B ∀ z ∈ B ¬ x R x ∧ x R y ∧ y R z → x R z → ∀ y ∈ A ∀ z ∈ A ¬ x R x ∧ x R y ∧ y R z → x R z$
3 2 ralimdv $⊢ A ⊆ B → ∀ x ∈ A ∀ y ∈ B ∀ z ∈ B ¬ x R x ∧ x R y ∧ y R z → x R z → ∀ x ∈ A ∀ y ∈ A ∀ z ∈ A ¬ x R x ∧ x R y ∧ y R z → x R z$
4 1 3 syld $⊢ A ⊆ B → ∀ x ∈ B ∀ y ∈ B ∀ z ∈ B ¬ x R x ∧ x R y ∧ y R z → x R z → ∀ x ∈ A ∀ y ∈ A ∀ z ∈ A ¬ x R x ∧ x R y ∧ y R z → x R z$
5 df-po $⊢ R Po B ↔ ∀ x ∈ B ∀ y ∈ B ∀ z ∈ B ¬ x R x ∧ x R y ∧ y R z → x R z$
6 df-po $⊢ R Po A ↔ ∀ x ∈ A ∀ y ∈ A ∀ z ∈ A ¬ x R x ∧ x R y ∧ y R z → x R z$
7 4 5 6 3imtr4g $⊢ A ⊆ B → R Po B → R Po A$