Theorem isposix

Description: Properties that determine a poset (explicit structure version). Note that the numeric indices of the structure components are not mentioned explicitly in either the theorem or its proof. (Contributed by NM, 9-Nov-2012)

	Ref	Expression
Hypotheses	isposix.a	|- B e. _V
	isposix.b	|- .<_ e. _V
	isposix.k	|- K = { <. ( Base ` ndx ) , B >. , <. ( le ` ndx ) , .<_ >. }
	isposix.1	|- ( x e. B -> x .<_ x )
	isposix.2	|- ( ( x e. B /\ y e. B ) -> ( ( x .<_ y /\ y .<_ x ) -> x = y ) )
	isposix.3	|- ( ( x e. B /\ y e. B /\ z e. B ) -> ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) )
Assertion	isposix	|- K e. Poset

Proof

Step	Hyp	Ref	Expression
1		isposix.a	|- B e. _V
2		isposix.b	|- .<_ e. _V
3		isposix.k	|- K = { <. ( Base ` ndx ) , B >. , <. ( le ` ndx ) , .<_ >. }
4		isposix.1	|- ( x e. B -> x .<_ x )
5		isposix.2	|- ( ( x e. B /\ y e. B ) -> ( ( x .<_ y /\ y .<_ x ) -> x = y ) )
6		isposix.3	|- ( ( x e. B /\ y e. B /\ z e. B ) -> ( ( x .<_ y /\ y .<_ z ) -> x .<_ z ) )
7		prex	|- { <. ( Base ` ndx ) , B >. , <. ( le ` ndx ) , .<_ >. } e. _V
8	3 7	eqeltri	|- K e. _V
9		df-ple	|- le = Slot ; 1 0
10		1lt10	|- 1 < ; 1 0
11		10nn	|- ; 1 0 e. NN
12	3 9 10 11	2strbas	|- ( B e. _V -> B = ( Base ` K ) )
13	1 12	ax-mp	|- B = ( Base ` K )
14	3 9 10 11	2strop	|- ( .<_ e. _V -> .<_ = ( le ` K ) )
15	2 14	ax-mp	|- .<_ = ( le ` K )
16	8 13 15 4 5 6	isposi	|- K e. Poset