# Metamath Proof Explorer

## Theorem swopo

Description: A strict weak order is a partial order. (Contributed by Mario Carneiro, 9-Jul-2014)

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

### Proof

Step Hyp Ref Expression
1 swopo.1 ${⊢}\left({\phi }\wedge \left({y}\in {A}\wedge {z}\in {A}\right)\right)\to \left({y}{R}{z}\to ¬{z}{R}{y}\right)$
2 swopo.2 ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {y}\in {A}\wedge {z}\in {A}\right)\right)\to \left({x}{R}{y}\to \left({x}{R}{z}\vee {z}{R}{y}\right)\right)$
3 id ${⊢}{x}\in {A}\to {x}\in {A}$
4 3 ancli ${⊢}{x}\in {A}\to \left({x}\in {A}\wedge {x}\in {A}\right)$
5 1 ralrimivva ${⊢}{\phi }\to \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}{R}{z}\to ¬{z}{R}{y}\right)$
6 breq1 ${⊢}{y}={x}\to \left({y}{R}{z}↔{x}{R}{z}\right)$
7 breq2 ${⊢}{y}={x}\to \left({z}{R}{y}↔{z}{R}{x}\right)$
8 7 notbid ${⊢}{y}={x}\to \left(¬{z}{R}{y}↔¬{z}{R}{x}\right)$
9 6 8 imbi12d ${⊢}{y}={x}\to \left(\left({y}{R}{z}\to ¬{z}{R}{y}\right)↔\left({x}{R}{z}\to ¬{z}{R}{x}\right)\right)$
10 breq2 ${⊢}{z}={x}\to \left({x}{R}{z}↔{x}{R}{x}\right)$
11 breq1 ${⊢}{z}={x}\to \left({z}{R}{x}↔{x}{R}{x}\right)$
12 11 notbid ${⊢}{z}={x}\to \left(¬{z}{R}{x}↔¬{x}{R}{x}\right)$
13 10 12 imbi12d ${⊢}{z}={x}\to \left(\left({x}{R}{z}\to ¬{z}{R}{x}\right)↔\left({x}{R}{x}\to ¬{x}{R}{x}\right)\right)$
14 9 13 rspc2va ${⊢}\left(\left({x}\in {A}\wedge {x}\in {A}\right)\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}{R}{z}\to ¬{z}{R}{y}\right)\right)\to \left({x}{R}{x}\to ¬{x}{R}{x}\right)$
15 4 5 14 syl2anr ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({x}{R}{x}\to ¬{x}{R}{x}\right)$
16 15 pm2.01d ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to ¬{x}{R}{x}$
17 1 3adantr1 ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {y}\in {A}\wedge {z}\in {A}\right)\right)\to \left({y}{R}{z}\to ¬{z}{R}{y}\right)$
18 2 imp ${⊢}\left(\left({\phi }\wedge \left({x}\in {A}\wedge {y}\in {A}\wedge {z}\in {A}\right)\right)\wedge {x}{R}{y}\right)\to \left({x}{R}{z}\vee {z}{R}{y}\right)$
19 18 orcomd ${⊢}\left(\left({\phi }\wedge \left({x}\in {A}\wedge {y}\in {A}\wedge {z}\in {A}\right)\right)\wedge {x}{R}{y}\right)\to \left({z}{R}{y}\vee {x}{R}{z}\right)$
20 19 ord ${⊢}\left(\left({\phi }\wedge \left({x}\in {A}\wedge {y}\in {A}\wedge {z}\in {A}\right)\right)\wedge {x}{R}{y}\right)\to \left(¬{z}{R}{y}\to {x}{R}{z}\right)$
21 20 expimpd ${⊢}\left({\phi }\wedge \left({x}\in {A}\wedge {y}\in {A}\wedge {z}\in {A}\right)\right)\to \left(\left({x}{R}{y}\wedge ¬{z}{R}{y}\right)\to {x}{R}{z}\right)$
22 17 21 sylan2d ${⊢}\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)$
23 16 22 ispod ${⊢}{\phi }\to {R}\mathrm{Po}{A}$