hl2at

Description: A Hilbert lattice has at least 2 atoms. (Contributed by NM, 5-Dec-2011)

		Ref	Expression
	Hypothesis	hl2atom.a	$⊢ A = Atoms (K)$
	Assertion	hl2at	$⊢ K \in HL \to \exists p \in A \exists q \in A p \neq q$

Proof

Step	Hyp	Ref	Expression
1		hl2atom.a	$⊢ A = Atoms (K)$
2		eqid	$⊢ {Base}_{K} = {Base}_{K}$
3		eqid	$⊢ <_{K} = <_{K}$
4		eqid	$⊢ 0. (K) = 0. (K)$
5		eqid	$⊢ 1. (K) = 1. (K)$
6	2 3 4 5	hlhgt2	$⊢ K \in HL \to \exists x \in {Base}_{K} (0. (K) <_{K} x \land x <_{K} 1. (K))$
7		simpl	$⊢ (K \in HL \land x \in {Base}_{K}) \to K \in HL$
8		hlop	$⊢ K \in HL \to K \in OP$
9	8	adantr	$⊢ (K \in HL \land x \in {Base}_{K}) \to K \in OP$
10	2 4	op0cl	$⊢ K \in OP \to 0. (K) \in {Base}_{K}$
11	9 10	syl	$⊢ (K \in HL \land x \in {Base}_{K}) \to 0. (K) \in {Base}_{K}$
12		simpr	$⊢ (K \in HL \land x \in {Base}_{K}) \to x \in {Base}_{K}$
13		eqid	$⊢ \leq_{K} = \leq_{K}$
14	2 13 3 1	hlrelat1	$⊢ (K \in HL \land 0. (K) \in {Base}_{K} \land x \in {Base}_{K}) \to (0. (K) <_{K} x \to \exists p \in A (\neg p \leq_{K} 0. (K) \land p \leq_{K} x))$
15	7 11 12 14	syl3anc	$⊢ (K \in HL \land x \in {Base}_{K}) \to (0. (K) <_{K} x \to \exists p \in A (\neg p \leq_{K} 0. (K) \land p \leq_{K} x))$
16	2 5	op1cl	$⊢ K \in OP \to 1. (K) \in {Base}_{K}$
17	9 16	syl	$⊢ (K \in HL \land x \in {Base}_{K}) \to 1. (K) \in {Base}_{K}$
18	2 13 3 1	hlrelat1	$⊢ (K \in HL \land x \in {Base}_{K} \land 1. (K) \in {Base}_{K}) \to (x <_{K} 1. (K) \to \exists q \in A (\neg q \leq_{K} x \land q \leq_{K} 1. (K)))$
19	17 18	mpd3an3	$⊢ (K \in HL \land x \in {Base}_{K}) \to (x <_{K} 1. (K) \to \exists q \in A (\neg q \leq_{K} x \land q \leq_{K} 1. (K)))$
20	15 19	anim12d	$⊢ (K \in HL \land x \in {Base}_{K}) \to ((0. (K) <_{K} x \land x <_{K} 1. (K)) \to (\exists p \in A (\neg p \leq_{K} 0. (K) \land p \leq_{K} x) \land \exists q \in A (\neg q \leq_{K} x \land q \leq_{K} 1. (K))))$
21		reeanv	$⊢ \exists p \in A \exists q \in A ((\neg p \leq_{K} 0. (K) \land p \leq_{K} x) \land (\neg q \leq_{K} x \land q \leq_{K} 1. (K))) \leftrightarrow (\exists p \in A (\neg p \leq_{K} 0. (K) \land p \leq_{K} x) \land \exists q \in A (\neg q \leq_{K} x \land q \leq_{K} 1. (K)))$
22		nbrne2	$⊢ (p \leq_{K} x \land \neg q \leq_{K} x) \to p \neq q$
23	22	ad2ant2lr	$⊢ ((\neg p \leq_{K} 0. (K) \land p \leq_{K} x) \land (\neg q \leq_{K} x \land q \leq_{K} 1. (K))) \to p \neq q$
24	23	reximi	$⊢ \exists q \in A ((\neg p \leq_{K} 0. (K) \land p \leq_{K} x) \land (\neg q \leq_{K} x \land q \leq_{K} 1. (K))) \to \exists q \in A p \neq q$
25	24	reximi	$⊢ \exists p \in A \exists q \in A ((\neg p \leq_{K} 0. (K) \land p \leq_{K} x) \land (\neg q \leq_{K} x \land q \leq_{K} 1. (K))) \to \exists p \in A \exists q \in A p \neq q$
26	21 25	sylbir	$⊢ (\exists p \in A (\neg p \leq_{K} 0. (K) \land p \leq_{K} x) \land \exists q \in A (\neg q \leq_{K} x \land q \leq_{K} 1. (K))) \to \exists p \in A \exists q \in A p \neq q$
27	20 26	syl6	$⊢ (K \in HL \land x \in {Base}_{K}) \to ((0. (K) <_{K} x \land x <_{K} 1. (K)) \to \exists p \in A \exists q \in A p \neq q)$
28	27	rexlimdva	$⊢ K \in HL \to (\exists x \in {Base}_{K} (0. (K) <_{K} x \land x <_{K} 1. (K)) \to \exists p \in A \exists q \in A p \neq q)$
29	6 28	mpd	$⊢ K \in HL \to \exists p \in A \exists q \in A p \neq q$

Metamath Proof Explorer

Theorem hl2at

Proof