Theorem hl0lt1N

Description: Lattice 0 is less than lattice 1 in a Hilbert lattice. (Contributed by NM, 4-Dec-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hl0lt1.s	$$⊢\underset{\dot{}}{<}={<}_K$$
	hl0lt1.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
	hl0lt1.u	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\left(K\right)$$
Assertion	hl0lt1N	$$⊢K\in \mathrm{HL}\to \underset{\dot{}}{0}\underset{\dot{}}{<}\underset{\dot{}}{1}$$

Proof

Step	Hyp	Ref	Expression
1		hl0lt1.s	$$⊢\underset{\dot{}}{<}={<}_K$$
2		hl0lt1.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
3		hl0lt1.u	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\left(K\right)$$
4		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
5	4 1 2 3	hlhgt2	$$⊢K\in \mathrm{HL}\to \exists x\in {\mathrm{Base}}_K\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\wedge x\underset{\dot{}}{<}\underset{\dot{}}{1}\right)$$
6		hlpos	$$⊢K\in \mathrm{HL}\to K\in \mathrm{Poset}$$
7	6	adantr	$$⊢\left(K\in \mathrm{HL}\wedge x\in {\mathrm{Base}}_K\right)\to K\in \mathrm{Poset}$$
8		hlop	$$⊢K\in \mathrm{HL}\to K\in \mathrm{OP}$$
9	8	adantr	$$⊢\left(K\in \mathrm{HL}\wedge x\in {\mathrm{Base}}_K\right)\to K\in \mathrm{OP}$$
10	4 2	op0cl	$$⊢K\in \mathrm{OP}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_K$$
11	9 10	syl	$$⊢\left(K\in \mathrm{HL}\wedge x\in {\mathrm{Base}}_K\right)\to \underset{\dot{}}{0}\in {\mathrm{Base}}_K$$
12		simpr	$$⊢\left(K\in \mathrm{HL}\wedge x\in {\mathrm{Base}}_K\right)\to x\in {\mathrm{Base}}_K$$
13	4 3	op1cl	$$⊢K\in \mathrm{OP}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_K$$
14	9 13	syl	$$⊢\left(K\in \mathrm{HL}\wedge x\in {\mathrm{Base}}_K\right)\to \underset{\dot{}}{1}\in {\mathrm{Base}}_K$$
15	4 1	plttr	$$⊢\left(K\in \mathrm{Poset}\wedge \left(\underset{\dot{}}{0}\in {\mathrm{Base}}_K\wedge x\in {\mathrm{Base}}_K\wedge \underset{\dot{}}{1}\in {\mathrm{Base}}_K\right)\right)\to \left(\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\wedge x\underset{\dot{}}{<}\underset{\dot{}}{1}\right)\to \underset{\dot{}}{0}\underset{\dot{}}{<}\underset{\dot{}}{1}\right)$$
16	7 11 12 14 15	syl13anc	$$⊢\left(K\in \mathrm{HL}\wedge x\in {\mathrm{Base}}_K\right)\to \left(\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\wedge x\underset{\dot{}}{<}\underset{\dot{}}{1}\right)\to \underset{\dot{}}{0}\underset{\dot{}}{<}\underset{\dot{}}{1}\right)$$
17	16	rexlimdva	$$⊢K\in \mathrm{HL}\to \left(\exists x\in {\mathrm{Base}}_K\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\wedge x\underset{\dot{}}{<}\underset{\dot{}}{1}\right)\to \underset{\dot{}}{0}\underset{\dot{}}{<}\underset{\dot{}}{1}\right)$$
18	5 17	mpd	$$⊢K\in \mathrm{HL}\to \underset{\dot{}}{0}\underset{\dot{}}{<}\underset{\dot{}}{1}$$