Theorem isposi

Description: Properties that determine a poset (implicit structure version). (Contributed by NM, 11-Sep-2011)

	Ref	Expression
Hypotheses	isposi.k	|- K e. _V
	isposi.b	|- B = ( Base ` K )
	isposi.l	|- .<_ = ( le ` K )
	isposi.1	|- ( x e. B -> x .<_ x )
	isposi.2	|- ( ( x e. B /\ y e. B ) -> ( ( x .<_ y /\ y .<_ x ) -> x = y ) )
	isposi.3	|- ( ( x e. B /\ y e. B /\ z e. B ) -> ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) )
Assertion	isposi	|- K e. Poset

Proof

Step	Hyp	Ref	Expression
1		isposi.k	|- K e. _V
2		isposi.b	|- B = ( Base ` K )
3		isposi.l	|- .<_ = ( le ` K )
4		isposi.1	|- ( x e. B -> x .<_ x )
5		isposi.2	|- ( ( x e. B /\ y e. B ) -> ( ( x .<_ y /\ y .<_ x ) -> x = y ) )
6		isposi.3	|- ( ( x e. B /\ y e. B /\ z e. B ) -> ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) )
7	4	3ad2ant1	|- ( ( x e. B /\ y e. B /\ z e. B ) -> x .<_ x )
8	5	3adant3	|- ( ( x e. B /\ y e. B /\ z e. B ) -> ( ( x .<_ y /\ y .<_ x ) -> x = y ) )
9	7 8 6	3jca	|- ( ( x e. B /\ y e. B /\ z e. B ) -> ( x .<_ x /\ ( ( x .<_ y /\ y .<_ x ) -> x = y ) /\ ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) ) )
10	9	rgen3	|- 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 ) )
11	2 3	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 ) ) ) )
12	1 10 11	mpbir2an	|- K e. Poset