Proof of Theorem exatleN
Step | Hyp | Ref
| Expression |
1 | | simpl32 1143 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ 𝑅 ≠ 𝑃) → ¬ 𝑄 ≤ 𝑋) |
2 | | atomle.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐾) |
3 | | atomle.l |
. . . . . . 7
⊢ ≤ =
(le‘𝐾) |
4 | | simp11l 1172 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋) → 𝐾 ∈ HL) |
5 | | hllat 34650 |
. . . . . . . 8
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
6 | 4, 5 | syl 17 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋) → 𝐾 ∈ Lat) |
7 | | simp122 1194 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋) → 𝑄 ∈ 𝐴) |
8 | | atomle.a |
. . . . . . . . 9
⊢ 𝐴 = (Atoms‘𝐾) |
9 | 2, 8 | atbase 34576 |
. . . . . . . 8
⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵) |
10 | 7, 9 | syl 17 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋) → 𝑄 ∈ 𝐵) |
11 | | simp121 1193 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋) → 𝑃 ∈ 𝐴) |
12 | 2, 8 | atbase 34576 |
. . . . . . . . 9
⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵) |
13 | 11, 12 | syl 17 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋) → 𝑃 ∈ 𝐵) |
14 | | simp123 1195 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋) → 𝑅 ∈ 𝐴) |
15 | 2, 8 | atbase 34576 |
. . . . . . . . 9
⊢ (𝑅 ∈ 𝐴 → 𝑅 ∈ 𝐵) |
16 | 14, 15 | syl 17 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋) → 𝑅 ∈ 𝐵) |
17 | | atomle.j |
. . . . . . . . 9
⊢ ∨ =
(join‘𝐾) |
18 | 2, 17 | latjcl 17051 |
. . . . . . . 8
⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑅 ∈ 𝐵) → (𝑃 ∨ 𝑅) ∈ 𝐵) |
19 | 6, 13, 16, 18 | syl3anc 1326 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋) → (𝑃 ∨ 𝑅) ∈ 𝐵) |
20 | | simp11r 1173 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋) → 𝑋 ∈ 𝐵) |
21 | 14, 7, 11 | 3jca 1242 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋) → (𝑅 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴)) |
22 | | simp2 1062 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋) → 𝑅 ≠ 𝑃) |
23 | 4, 21, 22 | 3jca 1242 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋) → (𝐾 ∈ HL ∧ (𝑅 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) ∧ 𝑅 ≠ 𝑃)) |
24 | | simp133 1198 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋) → 𝑅 ≤ (𝑃 ∨ 𝑄)) |
25 | 3, 17, 8 | hlatexch1 34681 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ (𝑅 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) ∧ 𝑅 ≠ 𝑃) → (𝑅 ≤ (𝑃 ∨ 𝑄) → 𝑄 ≤ (𝑃 ∨ 𝑅))) |
26 | 23, 24, 25 | sylc 65 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋) → 𝑄 ≤ (𝑃 ∨ 𝑅)) |
27 | | simp131 1196 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋) → 𝑃 ≤ 𝑋) |
28 | | simp3 1063 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋) → 𝑅 ≤ 𝑋) |
29 | 2, 3, 17 | latjle12 17062 |
. . . . . . . . 9
⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ 𝐵 ∧ 𝑅 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵)) → ((𝑃 ≤ 𝑋 ∧ 𝑅 ≤ 𝑋) ↔ (𝑃 ∨ 𝑅) ≤ 𝑋)) |
30 | 6, 13, 16, 20, 29 | syl13anc 1328 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋) → ((𝑃 ≤ 𝑋 ∧ 𝑅 ≤ 𝑋) ↔ (𝑃 ∨ 𝑅) ≤ 𝑋)) |
31 | 27, 28, 30 | mpbi2and 956 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋) → (𝑃 ∨ 𝑅) ≤ 𝑋) |
32 | 2, 3, 6, 10, 19, 20, 26, 31 | lattrd 17058 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ 𝑅 ≠ 𝑃 ∧ 𝑅 ≤ 𝑋) → 𝑄 ≤ 𝑋) |
33 | 32 | 3expia 1267 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ 𝑅 ≠ 𝑃) → (𝑅 ≤ 𝑋 → 𝑄 ≤ 𝑋)) |
34 | 1, 33 | mtod 189 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ 𝑅 ≠ 𝑃) → ¬ 𝑅 ≤ 𝑋) |
35 | 34 | ex 450 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑅 ≠ 𝑃 → ¬ 𝑅 ≤ 𝑋)) |
36 | 35 | necon4ad 2813 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑅 ≤ 𝑋 → 𝑅 = 𝑃)) |
37 | | simp31 1097 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → 𝑃 ≤ 𝑋) |
38 | | breq1 4656 |
. . 3
⊢ (𝑅 = 𝑃 → (𝑅 ≤ 𝑋 ↔ 𝑃 ≤ 𝑋)) |
39 | 37, 38 | syl5ibrcom 237 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑅 = 𝑃 → 𝑅 ≤ 𝑋)) |
40 | 36, 39 | impbid 202 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑅 ≤ 𝑋 ↔ 𝑅 = 𝑃)) |