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

Metamath Proof Explorer

Theorem cvlatexchb1

Description: A version of cvlexchb1 for atoms. (Contributed by NM, 5-Nov-2012)

Ref Expression
Hypotheses cvlatexch.l ⊢ ≤ = ( le ‘ 𝐾 )
cvlatexch.j ⊢ ∨ = ( join ‘ 𝐾 )
cvlatexch.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion cvlatexchb1 ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) → ( 𝑃 ≤ ( 𝑅 ∨ 𝑄 ) ↔ ( 𝑅 ∨ 𝑃 ) = ( 𝑅 ∨ 𝑄 ) ) )

Proof

Step Hyp Ref Expression
1 cvlatexch.l ⊢ ≤ = ( le ‘ 𝐾 )
2 cvlatexch.j ⊢ ∨ = ( join ‘ 𝐾 )
3 cvlatexch.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 cvlatl ⊢ ( 𝐾 ∈ CvLat → 𝐾 ∈ AtLat )
5 4 adantr ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝐾 ∈ AtLat )
6 simpr1 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝑃 ∈ 𝐴 )
7 simpr3 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → 𝑅 ∈ 𝐴 )
8 1 3 atncmp ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( ¬ 𝑃 ≤ 𝑅 ↔ 𝑃 ≠ 𝑅 ) )
9 5 6 7 8 syl3anc ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( ¬ 𝑃 ≤ 𝑅 ↔ 𝑃 ≠ 𝑅 ) )
10 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
11 10 3 atbase ⊢ ( 𝑅 ∈ 𝐴 → 𝑅 ∈ ( Base ‘ 𝐾 ) )
12 10 1 2 3 cvlexchb1 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) ∧ ¬ 𝑃 ≤ 𝑅 ) → ( 𝑃 ≤ ( 𝑅 ∨ 𝑄 ) ↔ ( 𝑅 ∨ 𝑃 ) = ( 𝑅 ∨ 𝑄 ) ) )
13 12 3expia ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) ) → ( ¬ 𝑃 ≤ 𝑅 → ( 𝑃 ≤ ( 𝑅 ∨ 𝑄 ) ↔ ( 𝑅 ∨ 𝑃 ) = ( 𝑅 ∨ 𝑄 ) ) ) )
14 11 13 syl3anr3 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( ¬ 𝑃 ≤ 𝑅 → ( 𝑃 ≤ ( 𝑅 ∨ 𝑄 ) ↔ ( 𝑅 ∨ 𝑃 ) = ( 𝑅 ∨ 𝑄 ) ) ) )
15 9 14 sylbird ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( 𝑃 ≠ 𝑅 → ( 𝑃 ≤ ( 𝑅 ∨ 𝑄 ) ↔ ( 𝑅 ∨ 𝑃 ) = ( 𝑅 ∨ 𝑄 ) ) ) )
16 15 3impia ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) → ( 𝑃 ≤ ( 𝑅 ∨ 𝑄 ) ↔ ( 𝑅 ∨ 𝑃 ) = ( 𝑅 ∨ 𝑄 ) ) )