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 ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion hl2at ( 𝐾 ∈ HL → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 𝑝 ≠ 𝑞 )

Proof

Step Hyp Ref Expression
1 hl2atom.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
3 eqid ⊢ ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
4 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
5 eqid ⊢ ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
6 2 3 4 5 hlhgt2 ⊢ ( 𝐾 ∈ HL → ∃ 𝑥 ∈ ( Base ‘ 𝐾 ) ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) )
7 simpl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → 𝐾 ∈ HL )
8 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
9 8 adantr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → 𝐾 ∈ OP )
10 2 4 op0cl ⊢ ( 𝐾 ∈ OP → ( 0. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
11 9 10 syl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( 0. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
12 simpr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → 𝑥 ∈ ( Base ‘ 𝐾 ) )
13 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
14 2 13 3 1 hlrelat1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 0. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 → ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 0. ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑥 ) ) )
15 7 11 12 14 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 → ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 0. ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑥 ) ) )
16 2 5 op1cl ⊢ ( 𝐾 ∈ OP → ( 1. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
17 9 16 syl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( 1. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
18 2 13 3 1 hlrelat1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ ( 1. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑥 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) → ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑥 ∧ 𝑞 ( le ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) )
19 17 18 mpd3an3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑥 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) → ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑥 ∧ 𝑞 ( le ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) )
20 15 19 anim12d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) → ( ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 0. ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑥 ) ∧ ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑥 ∧ 𝑞 ( le ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ) )
21 reeanv ⊢ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 0. ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑥 ) ∧ ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑥 ∧ 𝑞 ( le ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) ↔ ( ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 0. ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑥 ) ∧ ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑥 ∧ 𝑞 ( le ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) )
22 nbrne2 ⊢ ( ( 𝑝 ( le ‘ 𝐾 ) 𝑥 ∧ ¬ 𝑞 ( le ‘ 𝐾 ) 𝑥 ) → 𝑝 ≠ 𝑞 )
23 22 ad2ant2lr ⊢ ( ( ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 0. ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑥 ) ∧ ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑥 ∧ 𝑞 ( le ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) → 𝑝 ≠ 𝑞 )
24 23 reximi ⊢ ( ∃ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 0. ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑥 ) ∧ ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑥 ∧ 𝑞 ( le ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) → ∃ 𝑞 ∈ 𝐴 𝑝 ≠ 𝑞 )
25 24 reximi ⊢ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 0. ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑥 ) ∧ ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑥 ∧ 𝑞 ( le ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 𝑝 ≠ 𝑞 )
26 21 25 sylbir ⊢ ( ( ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 0. ‘ 𝐾 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑥 ) ∧ ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑥 ∧ 𝑞 ( le ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 𝑝 ≠ 𝑞 )
27 20 26 syl6 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 𝑝 ≠ 𝑞 ) )
28 27 rexlimdva ⊢ ( 𝐾 ∈ HL → ( ∃ 𝑥 ∈ ( Base ‘ 𝐾 ) ( ( 0. ‘ 𝐾 ) ( lt ‘ 𝐾 ) 𝑥 ∧ 𝑥 ( lt ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 𝑝 ≠ 𝑞 ) )
29 6 28 mpd ⊢ ( 𝐾 ∈ HL → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 𝑝 ≠ 𝑞 )