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