Metamath Proof Explorer

Theorem 2atjlej

Description: Two atoms are different if their join majorizes the join of two different atoms. (Contributed by NM, 4-Jun-2013)

Ref Expression
Hypotheses ps1.l ⊢ ≤ = ( le ‘ 𝐾 )
ps1.j ⊢ ∨ = ( join ‘ 𝐾 )
ps1.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion 2atjlej ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) ) ) → 𝑅 ≠ 𝑆 )

Proof

Step Hyp Ref Expression
1 ps1.l ⊢ ≤ = ( le ‘ 𝐾 )
2 ps1.j ⊢ ∨ = ( join ‘ 𝐾 )
3 ps1.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 simp33 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) ) ) → ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) )
5 simp1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) ) ) → 𝐾 ∈ HL )
6 simp21 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) ) ) → 𝑃 ∈ 𝐴 )
7 simp22 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) ) ) → 𝑄 ∈ 𝐴 )
8 simp23 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) ) ) → 𝑃 ≠ 𝑄 )
9 simp31 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) ) ) → 𝑅 ∈ 𝐴 )
10 simp32 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) ) ) → 𝑆 ∈ 𝐴 )
11 1 2 3 ps-1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) ↔ ( 𝑃 ∨ 𝑄 ) = ( 𝑅 ∨ 𝑆 ) ) )
12 5 6 7 8 9 10 11 syl132anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) ↔ ( 𝑃 ∨ 𝑄 ) = ( 𝑅 ∨ 𝑆 ) ) )
13 4 12 mpbid ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) ) ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑅 ∨ 𝑆 ) )
14 2 3 lnnat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ≠ 𝑄 ↔ ¬ ( 𝑃 ∨ 𝑄 ) ∈ 𝐴 ) )
15 5 6 7 14 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) ) ) → ( 𝑃 ≠ 𝑄 ↔ ¬ ( 𝑃 ∨ 𝑄 ) ∈ 𝐴 ) )
16 8 15 mpbid ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) ) ) → ¬ ( 𝑃 ∨ 𝑄 ) ∈ 𝐴 )
17 13 16 eqneltrrd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) ) ) → ¬ ( 𝑅 ∨ 𝑆 ) ∈ 𝐴 )
18 2 3 lnnat ⊢ ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ( 𝑅 ≠ 𝑆 ↔ ¬ ( 𝑅 ∨ 𝑆 ) ∈ 𝐴 ) )
19 5 9 10 18 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) ) ) → ( 𝑅 ≠ 𝑆 ↔ ¬ ( 𝑅 ∨ 𝑆 ) ∈ 𝐴 ) )
20 17 19 mpbird ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) ) ) → 𝑅 ≠ 𝑆 )