# 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}\subseteq {B}\to \left({R}\mathrm{Po}{B}\to {R}\mathrm{Po}{A}\right)$

### Proof

Step Hyp Ref Expression
1 ssralv ${⊢}{A}\subseteq {B}\to \left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left(¬{x}{R}{x}\wedge \left(\left({x}{R}{y}\wedge {y}{R}{z}\right)\to {x}{R}{z}\right)\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left(¬{x}{R}{x}\wedge \left(\left({x}{R}{y}\wedge {y}{R}{z}\right)\to {x}{R}{z}\right)\right)\right)$
2 ss2ralv ${⊢}{A}\subseteq {B}\to \left(\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left(¬{x}{R}{x}\wedge \left(\left({x}{R}{y}\wedge {y}{R}{z}\right)\to {x}{R}{z}\right)\right)\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{x}{R}{x}\wedge \left(\left({x}{R}{y}\wedge {y}{R}{z}\right)\to {x}{R}{z}\right)\right)\right)$
3 2 ralimdv ${⊢}{A}\subseteq {B}\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left(¬{x}{R}{x}\wedge \left(\left({x}{R}{y}\wedge {y}{R}{z}\right)\to {x}{R}{z}\right)\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{x}{R}{x}\wedge \left(\left({x}{R}{y}\wedge {y}{R}{z}\right)\to {x}{R}{z}\right)\right)\right)$
4 1 3 syld ${⊢}{A}\subseteq {B}\to \left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left(¬{x}{R}{x}\wedge \left(\left({x}{R}{y}\wedge {y}{R}{z}\right)\to {x}{R}{z}\right)\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{x}{R}{x}\wedge \left(\left({x}{R}{y}\wedge {y}{R}{z}\right)\to {x}{R}{z}\right)\right)\right)$
5 df-po ${⊢}{R}\mathrm{Po}{B}↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\left(¬{x}{R}{x}\wedge \left(\left({x}{R}{y}\wedge {y}{R}{z}\right)\to {x}{R}{z}\right)\right)$
6 df-po ${⊢}{R}\mathrm{Po}{A}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left(¬{x}{R}{x}\wedge \left(\left({x}{R}{y}\wedge {y}{R}{z}\right)\to {x}{R}{z}\right)\right)$
7 4 5 6 3imtr4g ${⊢}{A}\subseteq {B}\to \left({R}\mathrm{Po}{B}\to {R}\mathrm{Po}{A}\right)$