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\in \mathrm{V}$$
	isposix.b	$$⊢\underset{\dot{}}{\le }\in \mathrm{V}$$
	isposix.k	$$⊢K=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩\right\}$$
	isposix.1	$$⊢x\in B\to x\underset{\dot{}}{\le }x$$
	isposix.2	$$⊢\left(x\in B\wedge y\in B\right)\to \left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\to x=y\right)$$
	isposix.3	$$⊢\left(x\in B\wedge y\in B\wedge z\in B\right)\to \left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)$$
Assertion	isposix	$$⊢K\in \mathrm{Poset}$$

Proof

Step	Hyp	Ref	Expression
1		isposix.a	$$⊢B\in \mathrm{V}$$
2		isposix.b	$$⊢\underset{\dot{}}{\le }\in \mathrm{V}$$
3		isposix.k	$$⊢K=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩\right\}$$
4		isposix.1	$$⊢x\in B\to x\underset{\dot{}}{\le }x$$
5		isposix.2	$$⊢\left(x\in B\wedge y\in B\right)\to \left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\to x=y\right)$$
6		isposix.3	$$⊢\left(x\in B\wedge y\in B\wedge z\in B\right)\to \left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)$$
7		prex	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩\right\}\in \mathrm{V}$$
8	3 7	eqeltri	$$⊢K\in \mathrm{V}$$
9		basendxltplendx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}<{\le }_{\mathrm{ndx}}$$
10		plendxnn	$$⊢{\le }_{\mathrm{ndx}}\in \mathbb{N}$$
11	3 9 10	2strbas1	$$⊢B\in \mathrm{V}\to B={\mathrm{Base}}_K$$
12	1 11	ax-mp	$$⊢B={\mathrm{Base}}_K$$
13		pleid	$$⊢\mathrm{le}=\mathrm{Slot}{\le }_{\mathrm{ndx}}$$
14	3 9 10 13	2strop1	$$⊢\underset{\dot{}}{\le }\in \mathrm{V}\to \underset{\dot{}}{\le }={\le }_K$$
15	2 14	ax-mp	$$⊢\underset{\dot{}}{\le }={\le }_K$$
16	8 12 15 4 5 6	isposi	$$⊢K\in \mathrm{Poset}$$