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 ∧ 𝑊𝐻 ) → ∃ 𝑝𝐴 ¬ 𝑝 𝑊 )