Theorem ispos2

Description: A poset is an antisymmetric proset.

EDITORIAL: could become the definition of poset. (Contributed by Stefan O'Rear, 1-Feb-2015)

	Ref	Expression
Hypotheses	ispos2.b	|- B = ( Base ` K )
	ispos2.l	|- .<_ = ( le ` K )
Assertion	ispos2	|- ( K e. Poset <-> ( K e. Proset /\ A. x e. B A. y e. B ( ( x .<_ y /\ y .<_ x ) -> x = y ) ) )

Proof

Step	Hyp	Ref	Expression
1		ispos2.b	|- B = ( Base ` K )
2		ispos2.l	|- .<_ = ( le ` K )
3		3anan32	|- ( ( x .<_ x /\ ( ( x .<_ y /\ y .<_ x ) -> x = y ) /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) <-> ( ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) /\ ( ( x .<_ y /\ y .<_ x ) -> x = y ) ) )
4	3	ralbii	|- ( A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ x ) -> x = y ) /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) <-> A. z e. B ( ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) /\ ( ( x .<_ y /\ y .<_ x ) -> x = y ) ) )
5		r19.26	|- ( A. z e. B ( ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) /\ ( ( x .<_ y /\ y .<_ x ) -> x = y ) ) <-> ( A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) /\ A. z e. B ( ( x .<_ y /\ y .<_ x ) -> x = y ) ) )
6	4 5	bitri	|- ( A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ x ) -> x = y ) /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) <-> ( A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) /\ A. z e. B ( ( x .<_ y /\ y .<_ x ) -> x = y ) ) )
7	6	2ralbii	|- ( A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ x ) -> x = y ) /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) <-> A. x e. B A. y e. B ( A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) /\ A. z e. B ( ( x .<_ y /\ y .<_ x ) -> x = y ) ) )
8		r19.26-2	|- ( A. x e. B A. y e. B ( A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) /\ A. z e. B ( ( x .<_ y /\ y .<_ x ) -> x = y ) ) <-> ( A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) /\ A. x e. B A. y e. B A. z e. B ( ( x .<_ y /\ y .<_ x ) -> x = y ) ) )
9		rr19.3v	|- ( A. y e. B A. z e. B ( ( x .<_ y /\ y .<_ x ) -> x = y ) <-> A. y e. B ( ( x .<_ y /\ y .<_ x ) -> x = y ) )
10	9	ralbii	|- ( A. x e. B A. y e. B A. z e. B ( ( x .<_ y /\ y .<_ x ) -> x = y ) <-> A. x e. B A. y e. B ( ( x .<_ y /\ y .<_ x ) -> x = y ) )
11	10	anbi2i	|- ( ( A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) /\ A. x e. B A. y e. B A. z e. B ( ( x .<_ y /\ y .<_ x ) -> x = y ) ) <-> ( A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) /\ A. x e. B A. y e. B ( ( x .<_ y /\ y .<_ x ) -> x = y ) ) )
12	8 11	bitri	|- ( A. x e. B A. y e. B ( A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) /\ A. z e. B ( ( x .<_ y /\ y .<_ x ) -> x = y ) ) <-> ( A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) /\ A. x e. B A. y e. B ( ( x .<_ y /\ y .<_ x ) -> x = y ) ) )
13	7 12	bitri	|- ( A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ x ) -> x = y ) /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) <-> ( A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) /\ A. x e. B A. y e. B ( ( x .<_ y /\ y .<_ x ) -> x = y ) ) )
14	13	anbi2i	|- ( ( K e. _V /\ A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ x ) -> x = y ) /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) <-> ( K e. _V /\ ( A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) /\ A. x e. B A. y e. B ( ( x .<_ y /\ y .<_ x ) -> x = y ) ) ) )
15	1 2	ispos	|- ( K e. Poset <-> ( K e. _V /\ A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ x ) -> x = y ) /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) )
16	1 2	isprs	|- ( K e. Proset <-> ( K e. _V /\ A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) )
17	16	anbi1i	|- ( ( K e. Proset /\ A. x e. B A. y e. B ( ( x .<_ y /\ y .<_ x ) -> x = y ) ) <-> ( ( K e. _V /\ A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) /\ A. x e. B A. y e. B ( ( x .<_ y /\ y .<_ x ) -> x = y ) ) )
18		anass	|- ( ( ( K e. _V /\ A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) ) /\ A. x e. B A. y e. B ( ( x .<_ y /\ y .<_ x ) -> x = y ) ) <-> ( K e. _V /\ ( A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) /\ A. x e. B A. y e. B ( ( x .<_ y /\ y .<_ x ) -> x = y ) ) ) )
19	17 18	bitri	|- ( ( K e. Proset /\ A. x e. B A. y e. B ( ( x .<_ y /\ y .<_ x ) -> x = y ) ) <-> ( K e. _V /\ ( A. x e. B A. y e. B A. z e. B ( x .<_ x /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) /\ A. x e. B A. y e. B ( ( x .<_ y /\ y .<_ x ) -> x = y ) ) ) )
20	14 15 19	3bitr4i	|- ( K e. Poset <-> ( K e. Proset /\ A. x e. B A. y e. B ( ( x .<_ y /\ y .<_ x ) -> x = y ) ) )