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