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

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 ) → ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑋 )