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

Metamath Proof Explorer

Theorem cvlexch1

Description: An atomic covering lattice has the exchange property. (Contributed by NM, 6-Nov-2011)

Ref Expression
Hypotheses cvlexch.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cvlexch.l ⊢ ≤ = ( le ‘ 𝐾 )
cvlexch.j ⊢ ∨ = ( join ‘ 𝐾 )
cvlexch.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion cvlexch1 ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 𝑃 ≤ 𝑋 ) → ( 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) → 𝑄 ≤ ( 𝑋 ∨ 𝑃 ) ) )

Proof

Step Hyp Ref Expression
1 cvlexch.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cvlexch.l ⊢ ≤ = ( le ‘ 𝐾 )
3 cvlexch.j ⊢ ∨ = ( join ‘ 𝐾 )
4 cvlexch.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 1 2 3 4 iscvlat ⊢ ( 𝐾 ∈ CvLat ↔ ( 𝐾 ∈ AtLat ∧ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ∀ 𝑥 ∈ 𝐵 ( ( ¬ 𝑝 ≤ 𝑥 ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑞 ) ) → 𝑞 ≤ ( 𝑥 ∨ 𝑝 ) ) ) )
6 5 simprbi ⊢ ( 𝐾 ∈ CvLat → ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ∀ 𝑥 ∈ 𝐵 ( ( ¬ 𝑝 ≤ 𝑥 ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑞 ) ) → 𝑞 ≤ ( 𝑥 ∨ 𝑝 ) ) )
7 breq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 ≤ 𝑥 ↔ 𝑃 ≤ 𝑥 ) )
8 7 notbid ⊢ ( 𝑝 = 𝑃 → ( ¬ 𝑝 ≤ 𝑥 ↔ ¬ 𝑃 ≤ 𝑥 ) )
9 breq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 ≤ ( 𝑥 ∨ 𝑞 ) ↔ 𝑃 ≤ ( 𝑥 ∨ 𝑞 ) ) )
10 8 9 anbi12d ⊢ ( 𝑝 = 𝑃 → ( ( ¬ 𝑝 ≤ 𝑥 ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑞 ) ) ↔ ( ¬ 𝑃 ≤ 𝑥 ∧ 𝑃 ≤ ( 𝑥 ∨ 𝑞 ) ) ) )
11 oveq2 ⊢ ( 𝑝 = 𝑃 → ( 𝑥 ∨ 𝑝 ) = ( 𝑥 ∨ 𝑃 ) )
12 11 breq2d ⊢ ( 𝑝 = 𝑃 → ( 𝑞 ≤ ( 𝑥 ∨ 𝑝 ) ↔ 𝑞 ≤ ( 𝑥 ∨ 𝑃 ) ) )
13 10 12 imbi12d ⊢ ( 𝑝 = 𝑃 → ( ( ( ¬ 𝑝 ≤ 𝑥 ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑞 ) ) → 𝑞 ≤ ( 𝑥 ∨ 𝑝 ) ) ↔ ( ( ¬ 𝑃 ≤ 𝑥 ∧ 𝑃 ≤ ( 𝑥 ∨ 𝑞 ) ) → 𝑞 ≤ ( 𝑥 ∨ 𝑃 ) ) ) )
14 oveq2 ⊢ ( 𝑞 = 𝑄 → ( 𝑥 ∨ 𝑞 ) = ( 𝑥 ∨ 𝑄 ) )
15 14 breq2d ⊢ ( 𝑞 = 𝑄 → ( 𝑃 ≤ ( 𝑥 ∨ 𝑞 ) ↔ 𝑃 ≤ ( 𝑥 ∨ 𝑄 ) ) )
16 15 anbi2d ⊢ ( 𝑞 = 𝑄 → ( ( ¬ 𝑃 ≤ 𝑥 ∧ 𝑃 ≤ ( 𝑥 ∨ 𝑞 ) ) ↔ ( ¬ 𝑃 ≤ 𝑥 ∧ 𝑃 ≤ ( 𝑥 ∨ 𝑄 ) ) ) )
17 breq1 ⊢ ( 𝑞 = 𝑄 → ( 𝑞 ≤ ( 𝑥 ∨ 𝑃 ) ↔ 𝑄 ≤ ( 𝑥 ∨ 𝑃 ) ) )
18 16 17 imbi12d ⊢ ( 𝑞 = 𝑄 → ( ( ( ¬ 𝑃 ≤ 𝑥 ∧ 𝑃 ≤ ( 𝑥 ∨ 𝑞 ) ) → 𝑞 ≤ ( 𝑥 ∨ 𝑃 ) ) ↔ ( ( ¬ 𝑃 ≤ 𝑥 ∧ 𝑃 ≤ ( 𝑥 ∨ 𝑄 ) ) → 𝑄 ≤ ( 𝑥 ∨ 𝑃 ) ) ) )
19 breq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑃 ≤ 𝑥 ↔ 𝑃 ≤ 𝑋 ) )
20 19 notbid ⊢ ( 𝑥 = 𝑋 → ( ¬ 𝑃 ≤ 𝑥 ↔ ¬ 𝑃 ≤ 𝑋 ) )
21 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∨ 𝑄 ) = ( 𝑋 ∨ 𝑄 ) )
22 21 breq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑃 ≤ ( 𝑥 ∨ 𝑄 ) ↔ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) )
23 20 22 anbi12d ⊢ ( 𝑥 = 𝑋 → ( ( ¬ 𝑃 ≤ 𝑥 ∧ 𝑃 ≤ ( 𝑥 ∨ 𝑄 ) ) ↔ ( ¬ 𝑃 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) ) )
24 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∨ 𝑃 ) = ( 𝑋 ∨ 𝑃 ) )
25 24 breq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑄 ≤ ( 𝑥 ∨ 𝑃 ) ↔ 𝑄 ≤ ( 𝑋 ∨ 𝑃 ) ) )
26 23 25 imbi12d ⊢ ( 𝑥 = 𝑋 → ( ( ( ¬ 𝑃 ≤ 𝑥 ∧ 𝑃 ≤ ( 𝑥 ∨ 𝑄 ) ) → 𝑄 ≤ ( 𝑥 ∨ 𝑃 ) ) ↔ ( ( ¬ 𝑃 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → 𝑄 ≤ ( 𝑋 ∨ 𝑃 ) ) ) )
27 13 18 26 rspc3v ⊢ ( ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐴 ∀ 𝑥 ∈ 𝐵 ( ( ¬ 𝑝 ≤ 𝑥 ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑞 ) ) → 𝑞 ≤ ( 𝑥 ∨ 𝑝 ) ) → ( ( ¬ 𝑃 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → 𝑄 ≤ ( 𝑋 ∨ 𝑃 ) ) ) )
28 6 27 mpan9 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( ¬ 𝑃 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → 𝑄 ≤ ( 𝑋 ∨ 𝑃 ) ) )
29 28 exp4b ⊢ ( 𝐾 ∈ CvLat → ( ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( ¬ 𝑃 ≤ 𝑋 → ( 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) → 𝑄 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) )
30 29 3imp ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 𝑃 ≤ 𝑋 ) → ( 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) → 𝑄 ≤ ( 𝑋 ∨ 𝑃 ) ) )