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

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 ( 𝐴 ⊆ 𝐵 → ( 𝑅 Or 𝐵 → 𝑅 Or 𝐴 ) )

Proof

Step Hyp Ref Expression
1 poss ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑅 Po 𝐵 → 𝑅 Po 𝐴 ) )
2 ss2ralv ⊢ ( 𝐴 ⊆ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
3 1 2 anim12d ⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝑅 Po 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) → ( 𝑅 Po 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) ) )
4 df-so ⊢ ( 𝑅 Or 𝐵 ↔ ( 𝑅 Po 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
5 df-so ⊢ ( 𝑅 Or 𝐴 ↔ ( 𝑅 Po 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
6 3 4 5 3imtr4g ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑅 Or 𝐵 → 𝑅 Or 𝐴 ) )