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

Metamath Proof Explorer

Theorem cvlexch3

Description: An atomic covering lattice has the exchange property. ( atexch analog.) (Contributed by NM, 5-Nov-2012)

Ref Expression
Hypotheses cvlexch3.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cvlexch3.l ⊢ ≤ = ( le ‘ 𝐾 )
cvlexch3.j ⊢ ∨ = ( join ‘ 𝐾 )
cvlexch3.m ⊢ ∧ = ( meet ‘ 𝐾 )
cvlexch3.z ⊢ 0 = ( 0. ‘ 𝐾 )
cvlexch3.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion cvlexch3 ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∧ 𝑋 ) = 0 ) → ( 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) → 𝑄 ≤ ( 𝑋 ∨ 𝑃 ) ) )

Proof

Step Hyp Ref Expression
1 cvlexch3.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cvlexch3.l ⊢ ≤ = ( le ‘ 𝐾 )
3 cvlexch3.j ⊢ ∨ = ( join ‘ 𝐾 )
4 cvlexch3.m ⊢ ∧ = ( meet ‘ 𝐾 )
5 cvlexch3.z ⊢ 0 = ( 0. ‘ 𝐾 )
6 cvlexch3.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
7 cvlatl ⊢ ( 𝐾 ∈ CvLat → 𝐾 ∈ AtLat )
8 7 adantr ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ) → 𝐾 ∈ AtLat )
9 simpr1 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ) → 𝑃 ∈ 𝐴 )
10 simpr3 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
11 1 2 4 5 6 atnle ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( ¬ 𝑃 ≤ 𝑋 ↔ ( 𝑃 ∧ 𝑋 ) = 0 ) )
12 8 9 10 11 syl3anc ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ) → ( ¬ 𝑃 ≤ 𝑋 ↔ ( 𝑃 ∧ 𝑋 ) = 0 ) )
13 1 2 3 6 cvlexch1 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 𝑃 ≤ 𝑋 ) → ( 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) → 𝑄 ≤ ( 𝑋 ∨ 𝑃 ) ) )
14 13 3expia ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ) → ( ¬ 𝑃 ≤ 𝑋 → ( 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) → 𝑄 ≤ ( 𝑋 ∨ 𝑃 ) ) ) )
15 12 14 sylbird ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑃 ∧ 𝑋 ) = 0 → ( 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) → 𝑄 ≤ ( 𝑋 ∨ 𝑃 ) ) ) )
16 15 3impia ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑃 ∧ 𝑋 ) = 0 ) → ( 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) → 𝑄 ≤ ( 𝑋 ∨ 𝑃 ) ) )