Theorem isposi

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

	Ref	Expression
Hypotheses	isposi.k	$$⊢K\in \mathrm{V}$$
	isposi.b	$$⊢B={\mathrm{Base}}_K$$
	isposi.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	isposi.1	$$⊢x\in B\to x\underset{\dot{}}{\le }x$$
	isposi.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)$$
	isposi.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	isposi	$$⊢K\in \mathrm{Poset}$$

Proof

Step	Hyp	Ref	Expression
1		isposi.k	$$⊢K\in \mathrm{V}$$
2		isposi.b	$$⊢B={\mathrm{Base}}_K$$
3		isposi.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
4		isposi.1	$$⊢x\in B\to x\underset{\dot{}}{\le }x$$
5		isposi.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		isposi.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	4	3ad2ant1	$$⊢\left(x\in B\wedge y\in B\wedge z\in B\right)\to x\underset{\dot{}}{\le }x$$
8	5	3adant3	$$⊢\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 }x\right)\to x=y\right)$$
9	7 8 6	3jca	$$⊢\left(x\in B\wedge y\in B\wedge z\in B\right)\to \left(x\underset{\dot{}}{\le }x\wedge \left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\to x=y\right)\wedge \left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)\right)$$
10	9	rgen3	$$⊢\forall x\in B\forall y\in B\forall z\in B\left(x\underset{\dot{}}{\le }x\wedge \left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\to x=y\right)\wedge \left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)\right)$$
11	2 3	ispos	$$⊢K\in \mathrm{Poset}\leftrightarrow \left(K\in \mathrm{V}\wedge \forall x\in B\forall y\in B\forall z\in B\left(x\underset{\dot{}}{\le }x\wedge \left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\to x=y\right)\wedge \left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)\right)\right)$$
12	1 10 11	mpbir2an	$$⊢K\in \mathrm{Poset}$$