Proof of Theorem atlatle
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | simpl13 1249 |
. . . . . 6
⊢ ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → 𝐾 ∈ AtLat) |
| 2 | | atlpos 39282 |
. . . . . 6
⊢ (𝐾 ∈ AtLat → 𝐾 ∈ Poset) |
| 3 | 1, 2 | syl 17 |
. . . . 5
⊢ ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → 𝐾 ∈ Poset) |
| 4 | | atlatle.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐾) |
| 5 | | atlatle.a |
. . . . . . 7
⊢ 𝐴 = (Atoms‘𝐾) |
| 6 | 4, 5 | atbase 39270 |
. . . . . 6
⊢ (𝑝 ∈ 𝐴 → 𝑝 ∈ 𝐵) |
| 7 | 6 | adantl 481 |
. . . . 5
⊢ ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ 𝐵) |
| 8 | | simpl2 1191 |
. . . . 5
⊢ ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → 𝑋 ∈ 𝐵) |
| 9 | | simpl3 1192 |
. . . . 5
⊢ ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → 𝑌 ∈ 𝐵) |
| 10 | | atlatle.l |
. . . . . 6
⊢ ≤ =
(le‘𝐾) |
| 11 | 4, 10 | postr 18377 |
. . . . 5
⊢ ((𝐾 ∈ Poset ∧ (𝑝 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑝 ≤ 𝑋 ∧ 𝑋 ≤ 𝑌) → 𝑝 ≤ 𝑌)) |
| 12 | 3, 7, 8, 9, 11 | syl13anc 1371 |
. . . 4
⊢ ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → ((𝑝 ≤ 𝑋 ∧ 𝑋 ≤ 𝑌) → 𝑝 ≤ 𝑌)) |
| 13 | 12 | expcomd 416 |
. . 3
⊢ ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → (𝑋 ≤ 𝑌 → (𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌))) |
| 14 | 13 | ralrimdva 3151 |
. 2
⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → ∀𝑝 ∈ 𝐴 (𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌))) |
| 15 | | ss2rab 4080 |
. . 3
⊢ ({𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋} ⊆ {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌} ↔ ∀𝑝 ∈ 𝐴 (𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌)) |
| 16 | | simpl12 1248 |
. . . . . 6
⊢ ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋} ⊆ {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌}) → 𝐾 ∈ CLat) |
| 17 | | ssrab2 4089 |
. . . . . . . 8
⊢ {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌} ⊆ 𝐴 |
| 18 | 4, 5 | atssbase 39271 |
. . . . . . . 8
⊢ 𝐴 ⊆ 𝐵 |
| 19 | 17, 18 | sstri 4004 |
. . . . . . 7
⊢ {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌} ⊆ 𝐵 |
| 20 | | eqid 2734 |
. . . . . . . 8
⊢
(lub‘𝐾) =
(lub‘𝐾) |
| 21 | 4, 10, 20 | lubss 18570 |
. . . . . . 7
⊢ ((𝐾 ∈ CLat ∧ {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌} ⊆ 𝐵 ∧ {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋} ⊆ {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌}) → ((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋}) ≤ ((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌})) |
| 22 | 19, 21 | mp3an2 1448 |
. . . . . 6
⊢ ((𝐾 ∈ CLat ∧ {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋} ⊆ {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌}) → ((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋}) ≤ ((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌})) |
| 23 | 16, 22 | sylancom 588 |
. . . . 5
⊢ ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋} ⊆ {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌}) → ((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋}) ≤ ((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌})) |
| 24 | 23 | ex 412 |
. . . 4
⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ({𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋} ⊆ {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌} → ((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋}) ≤ ((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌}))) |
| 25 | 4, 10, 20, 5 | atlatmstc 39300 |
. . . . . 6
⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵) → ((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋}) = 𝑋) |
| 26 | 25 | 3adant3 1131 |
. . . . 5
⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋}) = 𝑋) |
| 27 | 4, 10, 20, 5 | atlatmstc 39300 |
. . . . . 6
⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑌 ∈ 𝐵) → ((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌}) = 𝑌) |
| 28 | 27 | 3adant2 1130 |
. . . . 5
⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌}) = 𝑌) |
| 29 | 26, 28 | breq12d 5160 |
. . . 4
⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋}) ≤ ((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌}) ↔ 𝑋 ≤ 𝑌)) |
| 30 | 24, 29 | sylibd 239 |
. . 3
⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ({𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋} ⊆ {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌} → 𝑋 ≤ 𝑌)) |
| 31 | 15, 30 | biimtrrid 243 |
. 2
⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (∀𝑝 ∈ 𝐴 (𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌) → 𝑋 ≤ 𝑌)) |
| 32 | 14, 31 | impbid 212 |
1
⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ ∀𝑝 ∈ 𝐴 (𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌))) |
