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	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 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 ) )