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

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

Proof

Step Hyp Ref Expression
1 ssralv ⊢ ( 𝐴 ⊆ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ) )
2 ss2ralv ⊢ ( 𝐴 ⊆ 𝐵 → ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) → ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ) )
3 2 ralimdv ⊢ ( 𝐴 ⊆ 𝐵 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ) )
4 1 3 syld ⊢ ( 𝐴 ⊆ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ) )
5 df-po ⊢ ( 𝑅 Po 𝐵 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
6 df-po ⊢ ( 𝑅 Po 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
7 4 5 6 3imtr4g ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑅 Po 𝐵 → 𝑅 Po 𝐴 ) )