Metamath Proof Explorer


Theorem atlt

Description: Two atoms are unequal iff their join is greater than one of them. (Contributed by NM, 6-May-2012)

Ref Expression
Hypotheses atlt.s < ˙ = < K
atlt.j ˙ = join K
atlt.a A = Atoms K
Assertion atlt K HL P A Q A P < ˙ P ˙ Q P Q

Proof

Step Hyp Ref Expression
1 atlt.s < ˙ = < K
2 atlt.j ˙ = join K
3 atlt.a A = Atoms K
4 simp1 K HL P A Q A K HL
5 simp2 K HL P A Q A P A
6 simp3 K HL P A Q A Q A
7 eqid K = K
8 1 2 3 7 atltcvr K HL P A P A Q A P < ˙ P ˙ Q P K P ˙ Q
9 4 5 5 6 8 syl13anc K HL P A Q A P < ˙ P ˙ Q P K P ˙ Q
10 2 7 3 atcvr1 K HL P A Q A P Q P K P ˙ Q
11 9 10 bitr4d K HL P A Q A P < ˙ P ˙ Q P Q