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