Metamath Proof Explorer


Theorem 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 HL p A q A p 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 HL x Base K 0. K < K x x < K 1. K
7 simpl K HL x Base K K HL
8 hlop K HL K OP
9 8 adantr K HL x Base K K OP
10 2 4 op0cl K OP 0. K Base K
11 9 10 syl K HL x Base K 0. K Base K
12 simpr K HL x Base K x Base K
13 eqid K = K
14 2 13 3 1 hlrelat1 K HL 0. K Base K x Base K 0. K < K x p A ¬ p K 0. K p K x
15 7 11 12 14 syl3anc K HL x Base K 0. K < K x p A ¬ p K 0. K p K x
16 2 5 op1cl K OP 1. K Base K
17 9 16 syl K HL x Base K 1. K Base K
18 2 13 3 1 hlrelat1 K HL x Base K 1. K Base K x < K 1. K q A ¬ q K x q K 1. K
19 17 18 mpd3an3 K HL x Base K x < K 1. K q A ¬ q K x q K 1. K
20 15 19 anim12d K HL x Base K 0. K < K x x < K 1. K p A ¬ p K 0. K p K x q A ¬ q K x q K 1. K
21 reeanv p A q A ¬ p K 0. K p K x ¬ q K x q K 1. K p A ¬ p K 0. K p K x q A ¬ q K x q K 1. K
22 nbrne2 p K x ¬ q K x p q
23 22 ad2ant2lr ¬ p K 0. K p K x ¬ q K x q K 1. K p q
24 23 reximi q A ¬ p K 0. K p K x ¬ q K x q K 1. K q A p q
25 24 reximi p A q A ¬ p K 0. K p K x ¬ q K x q K 1. K p A q A p q
26 21 25 sylbir p A ¬ p K 0. K p K x q A ¬ q K x q K 1. K p A q A p q
27 20 26 syl6 K HL x Base K 0. K < K x x < K 1. K p A q A p q
28 27 rexlimdva K HL x Base K 0. K < K x x < K 1. K p A q A p q
29 6 28 mpd K HL p A q A p q