Theorem oposlem

Description: Lemma for orthoposet properties. (Contributed by NM, 20-Oct-2011)

	Ref	Expression
Hypotheses	oposlem.b	$$⊢B={\mathrm{Base}}_K$$
	oposlem.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	oposlem.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{oc}\left(K\right)$$
	oposlem.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	oposlem.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	oposlem.f	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
	oposlem.u	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\left(K\right)$$
Assertion	oposlem	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\wedge Y\in B\right)\to \left(\left(\underset{\dot{}}{\perp }\left(X\right)\in B\wedge \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(X\right)\right)=X\wedge \left(X\underset{\dot{}}{\le }Y\to \underset{\dot{}}{\perp }\left(Y\right)\underset{\dot{}}{\le }\underset{\dot{}}{\perp }\left(X\right)\right)\right)\wedge X\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(X\right)=\underset{\dot{}}{1}\wedge X\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(X\right)=\underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		oposlem.b	$$⊢B={\mathrm{Base}}_K$$
2		oposlem.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		oposlem.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{oc}\left(K\right)$$
4		oposlem.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
5		oposlem.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
6		oposlem.f	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
7		oposlem.u	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\left(K\right)$$
8		eqid	$$⊢\mathrm{lub}\left(K\right)=\mathrm{lub}\left(K\right)$$
9		eqid	$$⊢\mathrm{glb}\left(K\right)=\mathrm{glb}\left(K\right)$$
10	1 8 9 2 3 4 5 6 7	isopos	$$⊢K\in \mathrm{OP}\leftrightarrow \left(\left(K\in \mathrm{Poset}\wedge B\in \mathrm{dom}\mathrm{lub}\left(K\right)\wedge B\in \mathrm{dom}\mathrm{glb}\left(K\right)\right)\wedge \forall x\in B\forall y\in B\left(\left(\underset{\dot{}}{\perp }\left(x\right)\in B\wedge \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(x\right)\right)=x\wedge \left(x\underset{\dot{}}{\le }y\to \underset{\dot{}}{\perp }\left(y\right)\underset{\dot{}}{\le }\underset{\dot{}}{\perp }\left(x\right)\right)\right)\wedge x\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(x\right)=\underset{\dot{}}{1}\wedge x\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(x\right)=\underset{\dot{}}{0}\right)\right)$$
11	10	simprbi	$$⊢K\in \mathrm{OP}\to \forall x\in B\forall y\in B\left(\left(\underset{\dot{}}{\perp }\left(x\right)\in B\wedge \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(x\right)\right)=x\wedge \left(x\underset{\dot{}}{\le }y\to \underset{\dot{}}{\perp }\left(y\right)\underset{\dot{}}{\le }\underset{\dot{}}{\perp }\left(x\right)\right)\right)\wedge x\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(x\right)=\underset{\dot{}}{1}\wedge x\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(x\right)=\underset{\dot{}}{0}\right)$$
12		fveq2	$$⊢x=X\to \underset{\dot{}}{\perp }\left(x\right)=\underset{\dot{}}{\perp }\left(X\right)$$
13	12	eleq1d	$$⊢x=X\to \left(\underset{\dot{}}{\perp }\left(x\right)\in B\leftrightarrow \underset{\dot{}}{\perp }\left(X\right)\in B\right)$$
14		2fveq3	$$⊢x=X\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(x\right)\right)=\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(X\right)\right)$$
15		id	$$⊢x=X\to x=X$$
16	14 15	eqeq12d	$$⊢x=X\to \left(\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(x\right)\right)=x\leftrightarrow \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(X\right)\right)=X\right)$$
17		breq1	$$⊢x=X\to \left(x\underset{\dot{}}{\le }y\leftrightarrow X\underset{\dot{}}{\le }y\right)$$
18	12	breq2d	$$⊢x=X\to \left(\underset{\dot{}}{\perp }\left(y\right)\underset{\dot{}}{\le }\underset{\dot{}}{\perp }\left(x\right)\leftrightarrow \underset{\dot{}}{\perp }\left(y\right)\underset{\dot{}}{\le }\underset{\dot{}}{\perp }\left(X\right)\right)$$
19	17 18	imbi12d	$$⊢x=X\to \left(\left(x\underset{\dot{}}{\le }y\to \underset{\dot{}}{\perp }\left(y\right)\underset{\dot{}}{\le }\underset{\dot{}}{\perp }\left(x\right)\right)\leftrightarrow \left(X\underset{\dot{}}{\le }y\to \underset{\dot{}}{\perp }\left(y\right)\underset{\dot{}}{\le }\underset{\dot{}}{\perp }\left(X\right)\right)\right)$$
20	13 16 19	3anbi123d	$$⊢x=X\to \left(\left(\underset{\dot{}}{\perp }\left(x\right)\in B\wedge \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(x\right)\right)=x\wedge \left(x\underset{\dot{}}{\le }y\to \underset{\dot{}}{\perp }\left(y\right)\underset{\dot{}}{\le }\underset{\dot{}}{\perp }\left(x\right)\right)\right)\leftrightarrow \left(\underset{\dot{}}{\perp }\left(X\right)\in B\wedge \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(X\right)\right)=X\wedge \left(X\underset{\dot{}}{\le }y\to \underset{\dot{}}{\perp }\left(y\right)\underset{\dot{}}{\le }\underset{\dot{}}{\perp }\left(X\right)\right)\right)\right)$$
21	15 12	oveq12d	$$⊢x=X\to x\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(x\right)=X\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(X\right)$$
22	21	eqeq1d	$$⊢x=X\to \left(x\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(x\right)=\underset{\dot{}}{1}\leftrightarrow X\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(X\right)=\underset{\dot{}}{1}\right)$$
23	15 12	oveq12d	$$⊢x=X\to x\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(x\right)=X\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(X\right)$$
24	23	eqeq1d	$$⊢x=X\to \left(x\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(x\right)=\underset{\dot{}}{0}\leftrightarrow X\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(X\right)=\underset{\dot{}}{0}\right)$$
25	20 22 24	3anbi123d	$$⊢x=X\to \left(\left(\left(\underset{\dot{}}{\perp }\left(x\right)\in B\wedge \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(x\right)\right)=x\wedge \left(x\underset{\dot{}}{\le }y\to \underset{\dot{}}{\perp }\left(y\right)\underset{\dot{}}{\le }\underset{\dot{}}{\perp }\left(x\right)\right)\right)\wedge x\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(x\right)=\underset{\dot{}}{1}\wedge x\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(x\right)=\underset{\dot{}}{0}\right)\leftrightarrow \left(\left(\underset{\dot{}}{\perp }\left(X\right)\in B\wedge \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(X\right)\right)=X\wedge \left(X\underset{\dot{}}{\le }y\to \underset{\dot{}}{\perp }\left(y\right)\underset{\dot{}}{\le }\underset{\dot{}}{\perp }\left(X\right)\right)\right)\wedge X\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(X\right)=\underset{\dot{}}{1}\wedge X\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(X\right)=\underset{\dot{}}{0}\right)\right)$$
26		breq2	$$⊢y=Y\to \left(X\underset{\dot{}}{\le }y\leftrightarrow X\underset{\dot{}}{\le }Y\right)$$
27		fveq2	$$⊢y=Y\to \underset{\dot{}}{\perp }\left(y\right)=\underset{\dot{}}{\perp }\left(Y\right)$$
28	27	breq1d	$$⊢y=Y\to \left(\underset{\dot{}}{\perp }\left(y\right)\underset{\dot{}}{\le }\underset{\dot{}}{\perp }\left(X\right)\leftrightarrow \underset{\dot{}}{\perp }\left(Y\right)\underset{\dot{}}{\le }\underset{\dot{}}{\perp }\left(X\right)\right)$$
29	26 28	imbi12d	$$⊢y=Y\to \left(\left(X\underset{\dot{}}{\le }y\to \underset{\dot{}}{\perp }\left(y\right)\underset{\dot{}}{\le }\underset{\dot{}}{\perp }\left(X\right)\right)\leftrightarrow \left(X\underset{\dot{}}{\le }Y\to \underset{\dot{}}{\perp }\left(Y\right)\underset{\dot{}}{\le }\underset{\dot{}}{\perp }\left(X\right)\right)\right)$$
30	29	3anbi3d	$$⊢y=Y\to \left(\left(\underset{\dot{}}{\perp }\left(X\right)\in B\wedge \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(X\right)\right)=X\wedge \left(X\underset{\dot{}}{\le }y\to \underset{\dot{}}{\perp }\left(y\right)\underset{\dot{}}{\le }\underset{\dot{}}{\perp }\left(X\right)\right)\right)\leftrightarrow \left(\underset{\dot{}}{\perp }\left(X\right)\in B\wedge \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(X\right)\right)=X\wedge \left(X\underset{\dot{}}{\le }Y\to \underset{\dot{}}{\perp }\left(Y\right)\underset{\dot{}}{\le }\underset{\dot{}}{\perp }\left(X\right)\right)\right)\right)$$
31	30	3anbi1d	$$⊢y=Y\to \left(\left(\left(\underset{\dot{}}{\perp }\left(X\right)\in B\wedge \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(X\right)\right)=X\wedge \left(X\underset{\dot{}}{\le }y\to \underset{\dot{}}{\perp }\left(y\right)\underset{\dot{}}{\le }\underset{\dot{}}{\perp }\left(X\right)\right)\right)\wedge X\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(X\right)=\underset{\dot{}}{1}\wedge X\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(X\right)=\underset{\dot{}}{0}\right)\leftrightarrow \left(\left(\underset{\dot{}}{\perp }\left(X\right)\in B\wedge \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(X\right)\right)=X\wedge \left(X\underset{\dot{}}{\le }Y\to \underset{\dot{}}{\perp }\left(Y\right)\underset{\dot{}}{\le }\underset{\dot{}}{\perp }\left(X\right)\right)\right)\wedge X\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(X\right)=\underset{\dot{}}{1}\wedge X\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(X\right)=\underset{\dot{}}{0}\right)\right)$$
32	25 31	rspc2v	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(\forall x\in B\forall y\in B\left(\left(\underset{\dot{}}{\perp }\left(x\right)\in B\wedge \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(x\right)\right)=x\wedge \left(x\underset{\dot{}}{\le }y\to \underset{\dot{}}{\perp }\left(y\right)\underset{\dot{}}{\le }\underset{\dot{}}{\perp }\left(x\right)\right)\right)\wedge x\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(x\right)=\underset{\dot{}}{1}\wedge x\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(x\right)=\underset{\dot{}}{0}\right)\to \left(\left(\underset{\dot{}}{\perp }\left(X\right)\in B\wedge \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(X\right)\right)=X\wedge \left(X\underset{\dot{}}{\le }Y\to \underset{\dot{}}{\perp }\left(Y\right)\underset{\dot{}}{\le }\underset{\dot{}}{\perp }\left(X\right)\right)\right)\wedge X\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(X\right)=\underset{\dot{}}{1}\wedge X\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(X\right)=\underset{\dot{}}{0}\right)\right)$$
33	11 32	mpan9	$$⊢\left(K\in \mathrm{OP}\wedge \left(X\in B\wedge Y\in B\right)\right)\to \left(\left(\underset{\dot{}}{\perp }\left(X\right)\in B\wedge \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(X\right)\right)=X\wedge \left(X\underset{\dot{}}{\le }Y\to \underset{\dot{}}{\perp }\left(Y\right)\underset{\dot{}}{\le }\underset{\dot{}}{\perp }\left(X\right)\right)\right)\wedge X\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(X\right)=\underset{\dot{}}{1}\wedge X\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(X\right)=\underset{\dot{}}{0}\right)$$
34	33	3impb	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\wedge Y\in B\right)\to \left(\left(\underset{\dot{}}{\perp }\left(X\right)\in B\wedge \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(X\right)\right)=X\wedge \left(X\underset{\dot{}}{\le }Y\to \underset{\dot{}}{\perp }\left(Y\right)\underset{\dot{}}{\le }\underset{\dot{}}{\perp }\left(X\right)\right)\right)\wedge X\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(X\right)=\underset{\dot{}}{1}\wedge X\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(X\right)=\underset{\dot{}}{0}\right)$$