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

Metamath Proof Explorer

Theorem lhpexle

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

Ref Expression
Hypotheses lhp2a.l ⊢ ≤ = ( le ‘ 𝐾 )
lhp2a.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
lhp2a.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion lhpexle ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 𝑝 ≤ 𝑊 )

Proof

Step Hyp Ref Expression
1 lhp2a.l ⊢ ≤ = ( le ‘ 𝐾 )
2 lhp2a.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3 lhp2a.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 simpl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐾 ∈ HL )
5 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
6 5 3 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
7 6 adantl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
8 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
9 8 3 lhpn0 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑊 ≠ ( 0. ‘ 𝐾 ) )
10 5 1 8 2 atle ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ≠ ( 0. ‘ 𝐾 ) ) → ∃ 𝑝 ∈ 𝐴 𝑝 ≤ 𝑊 )
11 4 7 9 10 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 𝑝 ≤ 𝑊 )