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\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		df-ple	$$⊢\mathrm{le}=\mathrm{Slot}10$$
10		1lt10	$$⊢1<10$$
11		10nn	$$⊢10\in \mathbb{N}$$
12	3 9 10 11	2strbas	$$⊢B\in \mathrm{V}\to B={\mathrm{Base}}_K$$
13	1 12	ax-mp	$$⊢B={\mathrm{Base}}_K$$
14	3 9 10 11	2strop	$$⊢\underset{\dot{}}{\le }\in \mathrm{V}\to \underset{\dot{}}{\le }={\le }_K$$
15	2 14	ax-mp	$$⊢\underset{\dot{}}{\le }={\le }_K$$
16	8 13 15 4 5 6	isposi	$$⊢K\in \mathrm{Poset}$$