Metamath Proof Explorer

Theorem lhpexnle

Description: There exists an atom not under a co-atom. (Contributed by NM, 12-Apr-2013)

Ref Expression
Hypotheses lhp2a.l ⊢ ≤ ˙ = ≤ K
lhp2a.a ⊢ A = Atoms ⁡ K
lhp2a.h ⊢ H = LHyp ⁡ K
Assertion lhpexnle ⊢ K ∈ HL ∧ W ∈ H → ∃ p ∈ A ¬ p ≤ ˙ W

Proof

Step Hyp Ref Expression
1 lhp2a.l ⊢ ≤ ˙ = ≤ K
2 lhp2a.a ⊢ A = Atoms ⁡ K
3 lhp2a.h ⊢ H = LHyp ⁡ K
4 eqid ⊢ 1. ⁡ K = 1. ⁡ K
5 eqid ⊢ ⋖ K = ⋖ K
6 4 5 3 lhp1cvr ⊢ K ∈ HL ∧ W ∈ H → W ⋖ K 1. ⁡ K
7 simpl ⊢ K ∈ HL ∧ W ∈ H → K ∈ HL
8 eqid ⊢ Base K = Base K
9 8 3 lhpbase ⊢ W ∈ H → W ∈ Base K
10 9 adantl ⊢ K ∈ HL ∧ W ∈ H → W ∈ Base K
11 hlop ⊢ K ∈ HL → K ∈ OP
12 8 4 op1cl ⊢ K ∈ OP → 1. ⁡ K ∈ Base K
13 11 12 syl ⊢ K ∈ HL → 1. ⁡ K ∈ Base K
14 13 adantr ⊢ K ∈ HL ∧ W ∈ H → 1. ⁡ K ∈ Base K
15 eqid ⊢ join ⁡ K = join ⁡ K
16 8 1 15 5 2 cvrval3 ⊢ K ∈ HL ∧ W ∈ Base K ∧ 1. ⁡ K ∈ Base K → W ⋖ K 1. ⁡ K ↔ ∃ p ∈ A ¬ p ≤ ˙ W ∧ W join ⁡ K p = 1. ⁡ K
17 7 10 14 16 syl3anc ⊢ K ∈ HL ∧ W ∈ H → W ⋖ K 1. ⁡ K ↔ ∃ p ∈ A ¬ p ≤ ˙ W ∧ W join ⁡ K p = 1. ⁡ K
18 6 17 mpbid ⊢ K ∈ HL ∧ W ∈ H → ∃ p ∈ A ¬ p ≤ ˙ W ∧ W join ⁡ K p = 1. ⁡ K
19 simpl ⊢ ¬ p ≤ ˙ W ∧ W join ⁡ K p = 1. ⁡ K → ¬ p ≤ ˙ W
20 19 reximi ⊢ ∃ p ∈ A ¬ p ≤ ˙ W ∧ W join ⁡ K p = 1. ⁡ K → ∃ p ∈ A ¬ p ≤ ˙ W
21 18 20 syl ⊢ K ∈ HL ∧ W ∈ H → ∃ p ∈ A ¬ p ≤ ˙ W