Metamath Proof Explorer


Theorem 2atneat

Description: The join of two distinct atoms is not an atom. (Contributed by NM, 12-Oct-2012)

Ref Expression
Hypotheses 2atneat.j ˙ = join K
2atneat.a A = Atoms K
Assertion 2atneat K HL P A Q A P Q ¬ P ˙ Q A

Proof

Step Hyp Ref Expression
1 2atneat.j ˙ = join K
2 2atneat.a A = Atoms K
3 simpl K HL P A Q A P Q K HL
4 simpr1 K HL P A Q A P Q P A
5 simpr2 K HL P A Q A P Q Q A
6 simpr3 K HL P A Q A P Q P Q
7 eqid LLines K = LLines K
8 1 2 7 llni2 K HL P A Q A P Q P ˙ Q LLines K
9 3 4 5 6 8 syl31anc K HL P A Q A P Q P ˙ Q LLines K
10 2 7 llnneat K HL P ˙ Q LLines K ¬ P ˙ Q A
11 9 10 syldan K HL P A Q A P Q ¬ P ˙ Q A