Theorem prslem

Description: Lemma for prsref and prstr . (Contributed by Mario Carneiro, 1-Feb-2015)

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

Proof

Step	Hyp	Ref	Expression
1		isprs.b	$$⊢B={\mathrm{Base}}_K$$
2		isprs.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3	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)$$
4	3	simprbi	$$⊢K\in \mathrm{Proset}\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 }z\right)\to x\underset{\dot{}}{\le }z\right)\right)$$
5		breq12	$$⊢\left(x=X\wedge x=X\right)\to \left(x\underset{\dot{}}{\le }x\leftrightarrow X\underset{\dot{}}{\le }X\right)$$
6	5	anidms	$$⊢x=X\to \left(x\underset{\dot{}}{\le }x\leftrightarrow X\underset{\dot{}}{\le }X\right)$$
7		breq1	$$⊢x=X\to \left(x\underset{\dot{}}{\le }y\leftrightarrow X\underset{\dot{}}{\le }y\right)$$
8	7	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)$$
9		breq1	$$⊢x=X\to \left(x\underset{\dot{}}{\le }z\leftrightarrow X\underset{\dot{}}{\le }z\right)$$
10	8 9	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)$$
11	6 10	anbi12d	$$⊢x=X\to \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)\leftrightarrow \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)$$
12		breq2	$$⊢y=Y\to \left(X\underset{\dot{}}{\le }y\leftrightarrow X\underset{\dot{}}{\le }Y\right)$$
13		breq1	$$⊢y=Y\to \left(y\underset{\dot{}}{\le }z\leftrightarrow Y\underset{\dot{}}{\le }z\right)$$
14	12 13	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)$$
15	14	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)$$
16	15	anbi2d	$$⊢y=Y\to \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)\leftrightarrow \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		breq2	$$⊢z=Z\to \left(Y\underset{\dot{}}{\le }z\leftrightarrow Y\underset{\dot{}}{\le }Z\right)$$
18	17	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)$$
19		breq2	$$⊢z=Z\to \left(X\underset{\dot{}}{\le }z\leftrightarrow X\underset{\dot{}}{\le }Z\right)$$
20	18 19	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)$$
21	20	anbi2d	$$⊢z=Z\to \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)\leftrightarrow \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)$$
22	11 16 21	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 }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 }Z\right)\to X\underset{\dot{}}{\le }Z\right)\right)\right)$$
23	4 22	mpan9	$$⊢\left(K\in \mathrm{Proset}\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 }Z\right)\to X\underset{\dot{}}{\le }Z\right)\right)$$