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

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 ⊢ < = ( lt ‘ 𝐾 )
atlt.j ⊢ ∨ = ( join ‘ 𝐾 )
atlt.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion atlt ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 < ( 𝑃 ∨ 𝑄 ) ↔ 𝑃 ≠ 𝑄 ) )

Proof

Step Hyp Ref Expression
1 atlt.s ⊢ < = ( lt ‘ 𝐾 )
2 atlt.j ⊢ ∨ = ( join ‘ 𝐾 )
3 atlt.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 simp1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → 𝐾 ∈ HL )
5 simp2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → 𝑃 ∈ 𝐴 )
6 simp3 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → 𝑄 ∈ 𝐴 )
7 eqid ⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
8 1 2 3 7 atltcvr ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑃 < ( 𝑃 ∨ 𝑄 ) ↔ 𝑃 ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) )
9 4 5 5 6 8 syl13anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 < ( 𝑃 ∨ 𝑄 ) ↔ 𝑃 ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) )
10 2 7 3 atcvr1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ≠ 𝑄 ↔ 𝑃 ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) )
11 9 10 bitr4d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 < ( 𝑃 ∨ 𝑄 ) ↔ 𝑃 ≠ 𝑄 ) )