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) (Proof shortened by AV, 30-Oct-2024)

	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		basendxltplendx	|- ( Base ` ndx ) < ( le ` ndx )
10		plendxnn	|- ( le ` ndx ) e. NN
11	3 9 10	2strbas1	|- ( B e. _V -> B = ( Base ` K ) )
12	1 11	ax-mp	|- B = ( Base ` K )
13		pleid	|- le = Slot ( le ` ndx )
14	3 9 10 13	2strop1	|- ( .<_ e. _V -> .<_ = ( le ` K ) )
15	2 14	ax-mp	|- .<_ = ( le ` K )
16	8 12 15 4 5 6	isposi	|- K e. Poset