Metamath Proof Explorer


Theorem atlex

Description: Every nonzero element of an atomic lattice is greater than or equal to an atom. ( hatomic analog.) (Contributed by NM, 21-Oct-2011)

Ref Expression
Hypotheses atlex.b 𝐵 = ( Base ‘ 𝐾 )
atlex.l = ( le ‘ 𝐾 )
atlex.z 0 = ( 0. ‘ 𝐾 )
atlex.a 𝐴 = ( Atoms ‘ 𝐾 )
Assertion atlex ( ( 𝐾 ∈ AtLat ∧ 𝑋𝐵𝑋0 ) → ∃ 𝑦𝐴 𝑦 𝑋 )

Proof

Step Hyp Ref Expression
1 atlex.b 𝐵 = ( Base ‘ 𝐾 )
2 atlex.l = ( le ‘ 𝐾 )
3 atlex.z 0 = ( 0. ‘ 𝐾 )
4 atlex.a 𝐴 = ( Atoms ‘ 𝐾 )
5 eqid ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 )
6 1 5 2 3 4 isatl ( 𝐾 ∈ AtLat ↔ ( 𝐾 ∈ Lat ∧ 𝐵 ∈ dom ( glb ‘ 𝐾 ) ∧ ∀ 𝑥𝐵 ( 𝑥0 → ∃ 𝑦𝐴 𝑦 𝑥 ) ) )
7 6 simp3bi ( 𝐾 ∈ AtLat → ∀ 𝑥𝐵 ( 𝑥0 → ∃ 𝑦𝐴 𝑦 𝑥 ) )
8 neeq1 ( 𝑥 = 𝑋 → ( 𝑥0𝑋0 ) )
9 breq2 ( 𝑥 = 𝑋 → ( 𝑦 𝑥𝑦 𝑋 ) )
10 9 rexbidv ( 𝑥 = 𝑋 → ( ∃ 𝑦𝐴 𝑦 𝑥 ↔ ∃ 𝑦𝐴 𝑦 𝑋 ) )
11 8 10 imbi12d ( 𝑥 = 𝑋 → ( ( 𝑥0 → ∃ 𝑦𝐴 𝑦 𝑥 ) ↔ ( 𝑋0 → ∃ 𝑦𝐴 𝑦 𝑋 ) ) )
12 11 rspccv ( ∀ 𝑥𝐵 ( 𝑥0 → ∃ 𝑦𝐴 𝑦 𝑥 ) → ( 𝑋𝐵 → ( 𝑋0 → ∃ 𝑦𝐴 𝑦 𝑋 ) ) )
13 7 12 syl ( 𝐾 ∈ AtLat → ( 𝑋𝐵 → ( 𝑋0 → ∃ 𝑦𝐴 𝑦 𝑋 ) ) )
14 13 3imp ( ( 𝐾 ∈ AtLat ∧ 𝑋𝐵𝑋0 ) → ∃ 𝑦𝐴 𝑦 𝑋 )