This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ≤ = ( le ‘ 𝐾 )
lhp2a.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
lhp2a.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion lhpexnle ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 ¬ 𝑝 ≤ 𝑊 )

Proof

Step Hyp Ref Expression
1 lhp2a.l ⊢ ≤ = ( le ‘ 𝐾 )
2 lhp2a.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3 lhp2a.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 eqid ⊢ ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
5 eqid ⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
6 4 5 3 lhp1cvr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑊 ( ⋖ ‘ 𝐾 ) ( 1. ‘ 𝐾 ) )
7 simpl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐾 ∈ HL )
8 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
9 8 3 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
10 9 adantl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
11 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
12 8 4 op1cl ⊢ ( 𝐾 ∈ OP → ( 1. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
13 11 12 syl ⊢ ( 𝐾 ∈ HL → ( 1. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
14 13 adantr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 1. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
15 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
16 8 1 15 5 2 cvrval3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ∧ ( 1. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑊 ( ⋖ ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ↔ ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝑊 ( join ‘ 𝐾 ) 𝑝 ) = ( 1. ‘ 𝐾 ) ) ) )
17 7 10 14 16 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑊 ( ⋖ ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ↔ ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝑊 ( join ‘ 𝐾 ) 𝑝 ) = ( 1. ‘ 𝐾 ) ) ) )
18 6 17 mpbid ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝑊 ( join ‘ 𝐾 ) 𝑝 ) = ( 1. ‘ 𝐾 ) ) )
19 simpl ⊢ ( ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝑊 ( join ‘ 𝐾 ) 𝑝 ) = ( 1. ‘ 𝐾 ) ) → ¬ 𝑝 ≤ 𝑊 )
20 19 reximi ⊢ ( ∃ 𝑝 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 ∧ ( 𝑊 ( join ‘ 𝐾 ) 𝑝 ) = ( 1. ‘ 𝐾 ) ) → ∃ 𝑝 ∈ 𝐴 ¬ 𝑝 ≤ 𝑊 )
21 18 20 syl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 ¬ 𝑝 ≤ 𝑊 )