Theorem ispos2

Description: A poset is an antisymmetric proset.

EDITORIAL: could become the definition of poset. (Contributed by Stefan O'Rear, 1-Feb-2015)

	Ref	Expression
Hypotheses	ispos2.b	$$⊢B={\mathrm{Base}}_K$$
	ispos2.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
Assertion	ispos2	$$⊢K\in \mathrm{Poset}\leftrightarrow \left(K\in \mathrm{Proset}\wedge \forall x\in B\forall y\in B\left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\to x=y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ispos2.b	$$⊢B={\mathrm{Base}}_K$$
2		ispos2.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		3anan32	$$⊢\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)\leftrightarrow \left(\left(x\underset{\dot{}}{\le }x\wedge \left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)\right)\wedge \left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\to x=y\right)\right)$$
4	3	ralbii	$$⊢\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)\leftrightarrow \forall z\in B\left(\left(x\underset{\dot{}}{\le }x\wedge \left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)\right)\wedge \left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\to x=y\right)\right)$$
5		r19.26	$$⊢\forall z\in B\left(\left(x\underset{\dot{}}{\le }x\wedge \left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)\right)\wedge \left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\to x=y\right)\right)\leftrightarrow \left(\forall z\in B\left(x\underset{\dot{}}{\le }x\wedge \left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)\right)\wedge \forall z\in B\left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\to x=y\right)\right)$$
6	4 5	bitri	$$⊢\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)\leftrightarrow \left(\forall z\in B\left(x\underset{\dot{}}{\le }x\wedge \left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)\right)\wedge \forall z\in B\left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\to x=y\right)\right)$$
7	6	2ralbii	$$⊢\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)\leftrightarrow \forall x\in B\forall y\in B\left(\forall z\in B\left(x\underset{\dot{}}{\le }x\wedge \left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)\right)\wedge \forall z\in B\left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\to x=y\right)\right)$$
8		r19.26-2	$$⊢\forall x\in B\forall y\in B\left(\forall z\in B\left(x\underset{\dot{}}{\le }x\wedge \left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)\right)\wedge \forall z\in B\left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\to x=y\right)\right)\leftrightarrow \left(\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 }z\right)\to x\underset{\dot{}}{\le }z\right)\right)\wedge \forall x\in B\forall y\in B\forall z\in B\left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\to x=y\right)\right)$$
9		rr19.3v	$$⊢\forall y\in B\forall z\in B\left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\to x=y\right)\leftrightarrow \forall y\in B\left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\to x=y\right)$$
10	9	ralbii	$$⊢\forall x\in B\forall y\in B\forall z\in B\left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\to x=y\right)\leftrightarrow \forall x\in B\forall y\in B\left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\to x=y\right)$$
11	10	anbi2i	$$⊢\left(\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 }z\right)\to x\underset{\dot{}}{\le }z\right)\right)\wedge \forall x\in B\forall y\in B\forall z\in B\left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\to x=y\right)\right)\leftrightarrow \left(\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 }z\right)\to x\underset{\dot{}}{\le }z\right)\right)\wedge \forall x\in B\forall y\in B\left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\to x=y\right)\right)$$
12	8 11	bitri	$$⊢\forall x\in B\forall y\in B\left(\forall z\in B\left(x\underset{\dot{}}{\le }x\wedge \left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)\right)\wedge \forall z\in B\left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\to x=y\right)\right)\leftrightarrow \left(\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 }z\right)\to x\underset{\dot{}}{\le }z\right)\right)\wedge \forall x\in B\forall y\in B\left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\to x=y\right)\right)$$
13	7 12	bitri	$$⊢\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)\leftrightarrow \left(\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 }z\right)\to x\underset{\dot{}}{\le }z\right)\right)\wedge \forall x\in B\forall y\in B\left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\to x=y\right)\right)$$
14	13	anbi2i	$$⊢\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)\leftrightarrow \left(K\in \mathrm{V}\wedge \left(\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 }z\right)\to x\underset{\dot{}}{\le }z\right)\right)\wedge \forall x\in B\forall y\in B\left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\to x=y\right)\right)\right)$$
15	1 2	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)$$
16	1 2	isprs	$$⊢K\in \mathrm{Proset}\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 }z\right)\to x\underset{\dot{}}{\le }z\right)\right)\right)$$
17	16	anbi1i	$$⊢\left(K\in \mathrm{Proset}\wedge \forall x\in B\forall y\in B\left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\to x=y\right)\right)\leftrightarrow \left(\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 }z\right)\to x\underset{\dot{}}{\le }z\right)\right)\right)\wedge \forall x\in B\forall y\in B\left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\to x=y\right)\right)$$
18		anass	$$⊢\left(\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 }z\right)\to x\underset{\dot{}}{\le }z\right)\right)\right)\wedge \forall x\in B\forall y\in B\left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\to x=y\right)\right)\leftrightarrow \left(K\in \mathrm{V}\wedge \left(\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 }z\right)\to x\underset{\dot{}}{\le }z\right)\right)\wedge \forall x\in B\forall y\in B\left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\to x=y\right)\right)\right)$$
19	17 18	bitri	$$⊢\left(K\in \mathrm{Proset}\wedge \forall x\in B\forall y\in B\left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\to x=y\right)\right)\leftrightarrow \left(K\in \mathrm{V}\wedge \left(\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 }z\right)\to x\underset{\dot{}}{\le }z\right)\right)\wedge \forall x\in B\forall y\in B\left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\to x=y\right)\right)\right)$$
20	14 15 19	3bitr4i	$$⊢K\in \mathrm{Poset}\leftrightarrow \left(K\in \mathrm{Proset}\wedge \forall x\in B\forall y\in B\left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\to x=y\right)\right)$$