Proof of Theorem atlatle
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | simpl13 1246 |
. . . . . 6
⊢ ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → 𝐾 ∈ AtLat) |
| 2 | | atlpos 36439 |
. . . . . 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 36427 |
. . . . . 6
⊢ (𝑝 ∈ 𝐴 → 𝑝 ∈ 𝐵) |
| 7 | 6 | adantl 484 |
. . . . 5
⊢ ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ 𝐵) |
| 8 | | simpl2 1188 |
. . . . 5
⊢ ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → 𝑋 ∈ 𝐵) |
| 9 | | simpl3 1189 |
. . . . 5
⊢ ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → 𝑌 ∈ 𝐵) |
| 10 | | atlatle.l |
. . . . . 6
⊢ ≤ =
(le‘𝐾) |
| 11 | 4, 10 | postr 17565 |
. . . . 5
⊢ ((𝐾 ∈ Poset ∧ (𝑝 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑝 ≤ 𝑋 ∧ 𝑋 ≤ 𝑌) → 𝑝 ≤ 𝑌)) |
| 12 | 3, 7, 8, 9, 11 | syl13anc 1368 |
. . . 4
⊢ ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → ((𝑝 ≤ 𝑋 ∧ 𝑋 ≤ 𝑌) → 𝑝 ≤ 𝑌)) |
| 13 | 12 | expcomd 419 |
. . 3
⊢ ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑝 ∈ 𝐴) → (𝑋 ≤ 𝑌 → (𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌))) |
| 14 | 13 | ralrimdva 3191 |
. 2
⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → ∀𝑝 ∈ 𝐴 (𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌))) |
| 15 | | ss2rab 4049 |
. . 3
⊢ ({𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋} ⊆ {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌} ↔ ∀𝑝 ∈ 𝐴 (𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌)) |
| 16 | | simpl12 1245 |
. . . . . 6
⊢ ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋} ⊆ {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌}) → 𝐾 ∈ CLat) |
| 17 | | ssrab2 4058 |
. . . . . . . 8
⊢ {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌} ⊆ 𝐴 |
| 18 | 4, 5 | atssbase 36428 |
. . . . . . . 8
⊢ 𝐴 ⊆ 𝐵 |
| 19 | 17, 18 | sstri 3978 |
. . . . . . 7
⊢ {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌} ⊆ 𝐵 |
| 20 | | eqid 2823 |
. . . . . . . 8
⊢
(lub‘𝐾) =
(lub‘𝐾) |
| 21 | 4, 10, 20 | lubss 17733 |
. . . . . . 7
⊢ ((𝐾 ∈ CLat ∧ {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌} ⊆ 𝐵 ∧ {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋} ⊆ {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌}) → ((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋}) ≤ ((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌})) |
| 22 | 19, 21 | mp3an2 1445 |
. . . . . 6
⊢ ((𝐾 ∈ CLat ∧ {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋} ⊆ {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌}) → ((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋}) ≤ ((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌})) |
| 23 | 16, 22 | sylancom 590 |
. . . . 5
⊢ ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋} ⊆ {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌}) → ((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋}) ≤ ((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌})) |
| 24 | 23 | ex 415 |
. . . 4
⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ({𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋} ⊆ {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌} → ((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋}) ≤ ((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌}))) |
| 25 | 4, 10, 20, 5 | atlatmstc 36457 |
. . . . . 6
⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵) → ((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋}) = 𝑋) |
| 26 | 25 | 3adant3 1128 |
. . . . 5
⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋}) = 𝑋) |
| 27 | 4, 10, 20, 5 | atlatmstc 36457 |
. . . . . 6
⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑌 ∈ 𝐵) → ((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌}) = 𝑌) |
| 28 | 27 | 3adant2 1127 |
. . . . 5
⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌}) = 𝑌) |
| 29 | 26, 28 | breq12d 5081 |
. . . 4
⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋}) ≤ ((lub‘𝐾)‘{𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌}) ↔ 𝑋 ≤ 𝑌)) |
| 30 | 24, 29 | sylibd 241 |
. . 3
⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ({𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑋} ⊆ {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ 𝑌} → 𝑋 ≤ 𝑌)) |
| 31 | 15, 30 | syl5bir 245 |
. 2
⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (∀𝑝 ∈ 𝐴 (𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌) → 𝑋 ≤ 𝑌)) |
| 32 | 14, 31 | impbid 214 |
1
⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ ∀𝑝 ∈ 𝐴 (𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌))) |
