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 𝐴 ) )