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

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 e. _V <-> { A } = (/) )
3 poeq2 
 |-  ( { A } = (/) -> ( R Po { A } <-> R Po (/) ) )
4 2 3 sylbi 
 |-  ( -. A e. _V -> ( R Po { A } <-> R Po (/) ) )
5 1 4 mpbiri 
 |-  ( -. A e. _V -> R Po { A } )
6 5 adantl 
 |-  ( ( Rel R /\ -. A e. _V ) -> R Po { A } )
7 brrelex1 
 |-  ( ( Rel R /\ A R A ) -> A e. _V )
8 7 stoic1a 
 |-  ( ( Rel R /\ -. A e. _V ) -> -. A R A )
9 6 8 2thd 
 |-  ( ( Rel R /\ -. A e. _V ) -> ( R Po { A } <-> -. A R A ) )
10 9 ex 
 |-  ( Rel R -> ( -. A e. _V -> ( R Po { A } <-> -. A R A ) ) )
11 df-po 
 |-  ( R Po { A } <-> A. x e. { A } A. y e. { A } A. z e. { 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 e. _V -> ( A. z e. { 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 e. _V -> ( A. y e. { A } A. z e. { A } ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) <-> A. y e. { 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 imbitrid 
 |-  ( 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 e. _V -> ( A. y e. { A } ( -. x R x /\ ( ( x R y /\ y R A ) -> x R A ) ) <-> -. x R x ) )
25 18 24 bitrd 
 |-  ( A e. _V -> ( A. y e. { A } A. z e. { A } ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) <-> -. x R x ) )
26 25 ralbidv 
 |-  ( A e. _V -> ( A. x e. { A } A. y e. { A } A. z e. { A } ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) <-> A. x e. { 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 e. _V -> ( A. x e. { A } -. x R x <-> -. A R A ) )
31 26 30 bitrd 
 |-  ( A e. _V -> ( A. x e. { A } A. y e. { A } A. z e. { A } ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) <-> -. A R A ) )
32 11 31 bitrid 
 |-  ( A e. _V -> ( R Po { A } <-> -. A R A ) )
33 10 32 pm2.61d2 
 |-  ( Rel R -> ( R Po { A } <-> -. A R A ) )