# Metamath Proof Explorer

## Theorem ispod

Description: Sufficient conditions for a partial order. (Contributed by NM, 9-Jul-2014)

Ref Expression
Hypotheses ispod.1 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to ¬{x}{R}{x}$
ispod.2 ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {y}\in {A}\wedge {z}\in {A}\right)\right)\to \left(\left({x}{R}{y}\wedge {y}{R}{z}\right)\to {x}{R}{z}\right)$
Assertion ispod ${⊢}{\phi }\to {R}\mathrm{Po}{A}$

### Proof

Step Hyp Ref Expression
1 ispod.1 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to ¬{x}{R}{x}$
2 ispod.2 ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {y}\in {A}\wedge {z}\in {A}\right)\right)\to \left(\left({x}{R}{y}\wedge {y}{R}{z}\right)\to {x}{R}{z}\right)$
3 1 3ad2antr1 ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {y}\in {A}\wedge {z}\in {A}\right)\right)\to ¬{x}{R}{x}$
4 3 2 jca ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {y}\in {A}\wedge {z}\in {A}\right)\right)\to \left(¬{x}{R}{x}\wedge \left(\left({x}{R}{y}\wedge {y}{R}{z}\right)\to {x}{R}{z}\right)\right)$
5 4 ralrimivvva ${⊢}{\phi }\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)$
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 5 6 sylibr ${⊢}{\phi }\to {R}\mathrm{Po}{A}$