Theorem posasymb

Description: A poset ordering is asymmetric. (Contributed by NM, 21-Oct-2011)

	Ref	Expression
Hypotheses	posi.b	$$⊢B={\mathrm{Base}}_K$$
	posi.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
Assertion	posasymb	$$⊢\left(K\in \mathrm{Poset}\wedge X\in B\wedge Y\in B\right)\to \left(\left(X\underset{\dot{}}{\le }Y\wedge Y\underset{\dot{}}{\le }X\right)\leftrightarrow X=Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		posi.b	$$⊢B={\mathrm{Base}}_K$$
2		posi.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		simp1	$$⊢\left(K\in \mathrm{Poset}\wedge X\in B\wedge Y\in B\right)\to K\in \mathrm{Poset}$$
4		simp2	$$⊢\left(K\in \mathrm{Poset}\wedge X\in B\wedge Y\in B\right)\to X\in B$$
5		simp3	$$⊢\left(K\in \mathrm{Poset}\wedge X\in B\wedge Y\in B\right)\to Y\in B$$
6	1 2	posi	$$⊢\left(K\in \mathrm{Poset}\wedge \left(X\in B\wedge Y\in B\wedge Y\in B\right)\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 }Y\right)\to X\underset{\dot{}}{\le }Y\right)\right)$$
7	3 4 5 5 6	syl13anc	$$⊢\left(K\in \mathrm{Poset}\wedge X\in B\wedge Y\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 }Y\right)\to X\underset{\dot{}}{\le }Y\right)\right)$$
8	7	simp2d	$$⊢\left(K\in \mathrm{Poset}\wedge 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)$$
9	1 2	posref	$$⊢\left(K\in \mathrm{Poset}\wedge X\in B\right)\to X\underset{\dot{}}{\le }X$$
10		breq2	$$⊢X=Y\to \left(X\underset{\dot{}}{\le }X\leftrightarrow X\underset{\dot{}}{\le }Y\right)$$
11	9 10	syl5ibcom	$$⊢\left(K\in \mathrm{Poset}\wedge X\in B\right)\to \left(X=Y\to X\underset{\dot{}}{\le }Y\right)$$
12		breq1	$$⊢X=Y\to \left(X\underset{\dot{}}{\le }X\leftrightarrow Y\underset{\dot{}}{\le }X\right)$$
13	9 12	syl5ibcom	$$⊢\left(K\in \mathrm{Poset}\wedge X\in B\right)\to \left(X=Y\to Y\underset{\dot{}}{\le }X\right)$$
14	11 13	jcad	$$⊢\left(K\in \mathrm{Poset}\wedge X\in B\right)\to \left(X=Y\to \left(X\underset{\dot{}}{\le }Y\wedge Y\underset{\dot{}}{\le }X\right)\right)$$
15	14	3adant3	$$⊢\left(K\in \mathrm{Poset}\wedge X\in B\wedge Y\in B\right)\to \left(X=Y\to \left(X\underset{\dot{}}{\le }Y\wedge Y\underset{\dot{}}{\le }X\right)\right)$$
16	8 15	impbid	$$⊢\left(K\in \mathrm{Poset}\wedge X\in B\wedge Y\in B\right)\to \left(\left(X\underset{\dot{}}{\le }Y\wedge Y\underset{\dot{}}{\le }X\right)\leftrightarrow X=Y\right)$$