Metamath Proof Explorer

Theorem soss

Description: Subset theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997) (Proof shortened by Andrew Salmon, 25-Jul-2011)

Ref Expression
Assertion soss ⊢ A ⊆ B → R Or B → R Or A

Proof

Step Hyp Ref Expression
1 poss ⊢ A ⊆ B → R Po B → R Po A
2 ss2ralv ⊢ A ⊆ B → ∀ x ∈ B ∀ y ∈ B x R y ∨ x = y ∨ y R x → ∀ x ∈ A ∀ y ∈ A x R y ∨ x = y ∨ y R x
3 1 2 anim12d ⊢ A ⊆ B → R Po B ∧ ∀ x ∈ B ∀ y ∈ B x R y ∨ x = y ∨ y R x → R Po A ∧ ∀ x ∈ A ∀ y ∈ A x R y ∨ x = y ∨ y R x
4 df-so ⊢ R Or B ↔ R Po B ∧ ∀ x ∈ B ∀ y ∈ B x R y ∨ x = y ∨ y R x
5 df-so ⊢ R Or A ↔ R Po A ∧ ∀ x ∈ A ∀ y ∈ A x R y ∨ x = y ∨ y R x
6 3 4 5 3imtr4g ⊢ A ⊆ B → R Or B → R Or A