Metamath Proof Explorer


Theorem posn

Description: Partial ordering of a singleton. (Contributed by NM, 27-Apr-2009) (Revised by Mario Carneiro, 23-Apr-2015)

Ref Expression
Assertion posn Rel R R Po A ¬ A R A

Proof

Step Hyp Ref Expression
1 po0 R Po
2 snprc ¬ A V A =
3 poeq2 A = R Po A R Po
4 2 3 sylbi ¬ A V R Po A R Po
5 1 4 mpbiri ¬ A V R Po A
6 5 adantl Rel R ¬ A V R Po A
7 brrelex1 Rel R A R A A V
8 7 stoic1a Rel R ¬ A V ¬ A R A
9 6 8 2thd Rel R ¬ A V R Po A ¬ A R A
10 9 ex Rel R ¬ A V R Po A ¬ A R A
11 df-po R Po A x A y A z A ¬ x R x x R y y R z x R z
12 breq2 z = A y R z y R A
13 12 anbi2d z = A x R y y R z x R y y R A
14 breq2 z = A x R z x R A
15 13 14 imbi12d z = A x R y y R z x R z x R y y R A x R A
16 15 anbi2d z = A ¬ x R x x R y y R z x R z ¬ x R x x R y y R A x R A
17 16 ralsng A V z A ¬ x R x x R y y R z x R z ¬ x R x x R y y R A x R A
18 17 ralbidv A V y A z A ¬ x R x x R y y R z x R z y A ¬ x R x x R y y R A x R A
19 simpl x R y y R A x R y
20 breq2 y = A x R y x R A
21 19 20 syl5ib y = A x R y y R A x R A
22 21 biantrud y = A ¬ x R x ¬ x R x x R y y R A x R A
23 22 bicomd y = A ¬ x R x x R y y R A x R A ¬ x R x
24 23 ralsng A V y A ¬ x R x x R y y R A x R A ¬ x R x
25 18 24 bitrd A V y A z A ¬ x R x x R y y R z x R z ¬ x R x
26 25 ralbidv A V x A y A z A ¬ x R x x R y y R z x R z x A ¬ x R x
27 breq12 x = A x = A x R x A R A
28 27 anidms x = A x R x A R A
29 28 notbid x = A ¬ x R x ¬ A R A
30 29 ralsng A V x A ¬ x R x ¬ A R A
31 26 30 bitrd A V x A y A z A ¬ x R x x R y y R z x R z ¬ A R A
32 11 31 bitrid A V R Po A ¬ A R A
33 10 32 pm2.61d2 Rel R R Po A ¬ A R A