Theorem posi

Description: Lemma for poset properties. (Contributed by NM, 11-Sep-2011)

	Ref	Expression
Hypotheses	posi.b	$$⊢B={\mathrm{Base}}_K$$
	posi.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
Assertion	posi	$$⊢\left(K\in \mathrm{Poset}\wedge \left(X\in B\wedge Y\in B\wedge Z\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 }Z\right)\to X\underset{\dot{}}{\le }Z\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		posi.b	$$⊢B={\mathrm{Base}}_K$$
2		posi.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3	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)$$
4	3	simprbi	$$⊢K\in \mathrm{Poset}\to \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)$$
5		breq1	$$⊢x=X\to \left(x\underset{\dot{}}{\le }x\leftrightarrow X\underset{\dot{}}{\le }x\right)$$
6		breq2	$$⊢x=X\to \left(X\underset{\dot{}}{\le }x\leftrightarrow X\underset{\dot{}}{\le }X\right)$$
7	5 6	bitrd	$$⊢x=X\to \left(x\underset{\dot{}}{\le }x\leftrightarrow X\underset{\dot{}}{\le }X\right)$$
8		breq1	$$⊢x=X\to \left(x\underset{\dot{}}{\le }y\leftrightarrow X\underset{\dot{}}{\le }y\right)$$
9		breq2	$$⊢x=X\to \left(y\underset{\dot{}}{\le }x\leftrightarrow y\underset{\dot{}}{\le }X\right)$$
10	8 9	anbi12d	$$⊢x=X\to \left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\leftrightarrow \left(X\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }X\right)\right)$$
11		eqeq1	$$⊢x=X\to \left(x=y\leftrightarrow X=y\right)$$
12	10 11	imbi12d	$$⊢x=X\to \left(\left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }x\right)\to x=y\right)\leftrightarrow \left(\left(X\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }X\right)\to X=y\right)\right)$$
13	8	anbi1d	$$⊢x=X\to \left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }z\right)\leftrightarrow \left(X\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }z\right)\right)$$
14		breq1	$$⊢x=X\to \left(x\underset{\dot{}}{\le }z\leftrightarrow X\underset{\dot{}}{\le }z\right)$$
15	13 14	imbi12d	$$⊢x=X\to \left(\left(\left(x\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }z\right)\to x\underset{\dot{}}{\le }z\right)\leftrightarrow \left(\left(X\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }z\right)\to X\underset{\dot{}}{\le }z\right)\right)$$
16	7 12 15	3anbi123d	$$⊢x=X\to \left(\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(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)$$
17		breq2	$$⊢y=Y\to \left(X\underset{\dot{}}{\le }y\leftrightarrow X\underset{\dot{}}{\le }Y\right)$$
18		breq1	$$⊢y=Y\to \left(y\underset{\dot{}}{\le }X\leftrightarrow Y\underset{\dot{}}{\le }X\right)$$
19	17 18	anbi12d	$$⊢y=Y\to \left(\left(X\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }X\right)\leftrightarrow \left(X\underset{\dot{}}{\le }Y\wedge Y\underset{\dot{}}{\le }X\right)\right)$$
20		eqeq2	$$⊢y=Y\to \left(X=y\leftrightarrow X=Y\right)$$
21	19 20	imbi12d	$$⊢y=Y\to \left(\left(\left(X\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }X\right)\to X=y\right)\leftrightarrow \left(\left(X\underset{\dot{}}{\le }Y\wedge Y\underset{\dot{}}{\le }X\right)\to X=Y\right)\right)$$
22		breq1	$$⊢y=Y\to \left(y\underset{\dot{}}{\le }z\leftrightarrow Y\underset{\dot{}}{\le }z\right)$$
23	17 22	anbi12d	$$⊢y=Y\to \left(\left(X\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }z\right)\leftrightarrow \left(X\underset{\dot{}}{\le }Y\wedge Y\underset{\dot{}}{\le }z\right)\right)$$
24	23	imbi1d	$$⊢y=Y\to \left(\left(\left(X\underset{\dot{}}{\le }y\wedge y\underset{\dot{}}{\le }z\right)\to X\underset{\dot{}}{\le }z\right)\leftrightarrow \left(\left(X\underset{\dot{}}{\le }Y\wedge Y\underset{\dot{}}{\le }z\right)\to X\underset{\dot{}}{\le }z\right)\right)$$
25	21 24	3anbi23d	$$⊢y=Y\to \left(\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(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)$$
26		breq2	$$⊢z=Z\to \left(Y\underset{\dot{}}{\le }z\leftrightarrow Y\underset{\dot{}}{\le }Z\right)$$
27	26	anbi2d	$$⊢z=Z\to \left(\left(X\underset{\dot{}}{\le }Y\wedge Y\underset{\dot{}}{\le }z\right)\leftrightarrow \left(X\underset{\dot{}}{\le }Y\wedge Y\underset{\dot{}}{\le }Z\right)\right)$$
28		breq2	$$⊢z=Z\to \left(X\underset{\dot{}}{\le }z\leftrightarrow X\underset{\dot{}}{\le }Z\right)$$
29	27 28	imbi12d	$$⊢z=Z\to \left(\left(\left(X\underset{\dot{}}{\le }Y\wedge Y\underset{\dot{}}{\le }z\right)\to X\underset{\dot{}}{\le }z\right)\leftrightarrow \left(\left(X\underset{\dot{}}{\le }Y\wedge Y\underset{\dot{}}{\le }Z\right)\to X\underset{\dot{}}{\le }Z\right)\right)$$
30	29	3anbi3d	$$⊢z=Z\to \left(\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(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)$$
31	16 25 30	rspc3v	$$⊢\left(X\in B\wedge Y\in B\wedge Z\in B\right)\to \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 }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)\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)\right)$$
32	4 31	mpan9	$$⊢\left(K\in \mathrm{Poset}\wedge \left(X\in B\wedge Y\in B\wedge Z\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 }Z\right)\to X\underset{\dot{}}{\le }Z\right)\right)$$