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