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

Metamath Proof Explorer

Theorem llnneat

Description: A lattice line is not an atom. (Contributed by NM, 19-Jun-2012)

Ref Expression
Hypotheses llnneat.a ⊢ A = Atoms ⁡ K
llnneat.n ⊢ N = LLines ⁡ K
Assertion llnneat ⊢ K ∈ HL ∧ X ∈ N → ¬ X ∈ A

Proof

Step Hyp Ref Expression
1 llnneat.a ⊢ A = Atoms ⁡ K
2 llnneat.n ⊢ N = LLines ⁡ K
3 hllat ⊢ K ∈ HL → K ∈ Lat
4 eqid ⊢ Base K = Base K
5 4 2 llnbase ⊢ X ∈ N → X ∈ Base K
6 eqid ⊢ ≤ K = ≤ K
7 4 6 latref ⊢ K ∈ Lat ∧ X ∈ Base K → X ≤ K X
8 3 5 7 syl2an ⊢ K ∈ HL ∧ X ∈ N → X ≤ K X
9 6 1 2 llnnleat ⊢ K ∈ HL ∧ X ∈ N ∧ X ∈ A → ¬ X ≤ K X
10 9 3expia ⊢ K ∈ HL ∧ X ∈ N → X ∈ A → ¬ X ≤ K X
11 8 10 mt2d ⊢ K ∈ HL ∧ X ∈ N → ¬ X ∈ A