| Step | Hyp | Ref
| Expression |
| 1 | | drsprs 18349 |
. . 3
⊢ (𝐾 ∈ Dirset → 𝐾 ∈ Proset
) |
| 2 | | simpl 482 |
. . . . 5
⊢ ((𝐾 ∈ Dirset ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → 𝐾 ∈ Dirset) |
| 3 | | elinel1 4201 |
. . . . . . 7
⊢ (𝑥 ∈ (𝒫 𝐵 ∩ Fin) → 𝑥 ∈ 𝒫 𝐵) |
| 4 | 3 | elpwid 4609 |
. . . . . 6
⊢ (𝑥 ∈ (𝒫 𝐵 ∩ Fin) → 𝑥 ⊆ 𝐵) |
| 5 | 4 | adantl 481 |
. . . . 5
⊢ ((𝐾 ∈ Dirset ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑥 ⊆ 𝐵) |
| 6 | | elinel2 4202 |
. . . . . 6
⊢ (𝑥 ∈ (𝒫 𝐵 ∩ Fin) → 𝑥 ∈ Fin) |
| 7 | 6 | adantl 481 |
. . . . 5
⊢ ((𝐾 ∈ Dirset ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑥 ∈ Fin) |
| 8 | | drsbn0.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐾) |
| 9 | | drsdirfi.l |
. . . . . 6
⊢ ≤ =
(le‘𝐾) |
| 10 | 8, 9 | drsdirfi 18351 |
. . . . 5
⊢ ((𝐾 ∈ Dirset ∧ 𝑥 ⊆ 𝐵 ∧ 𝑥 ∈ Fin) → ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) |
| 11 | 2, 5, 7, 10 | syl3anc 1373 |
. . . 4
⊢ ((𝐾 ∈ Dirset ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) |
| 12 | 11 | ralrimiva 3146 |
. . 3
⊢ (𝐾 ∈ Dirset →
∀𝑥 ∈ (𝒫
𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) |
| 13 | 1, 12 | jca 511 |
. 2
⊢ (𝐾 ∈ Dirset → (𝐾 ∈ Proset ∧
∀𝑥 ∈ (𝒫
𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦)) |
| 14 | | simpl 482 |
. . 3
⊢ ((𝐾 ∈ Proset ∧
∀𝑥 ∈ (𝒫
𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) → 𝐾 ∈ Proset ) |
| 15 | | 0elpw 5356 |
. . . . . . 7
⊢ ∅
∈ 𝒫 𝐵 |
| 16 | | 0fi 9082 |
. . . . . . 7
⊢ ∅
∈ Fin |
| 17 | 15, 16 | elini 4199 |
. . . . . 6
⊢ ∅
∈ (𝒫 𝐵 ∩
Fin) |
| 18 | | raleq 3323 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 ↔ ∀𝑧 ∈ ∅ 𝑧 ≤ 𝑦)) |
| 19 | 18 | rexbidv 3179 |
. . . . . . 7
⊢ (𝑥 = ∅ → (∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 ↔ ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ ∅ 𝑧 ≤ 𝑦)) |
| 20 | 19 | rspcv 3618 |
. . . . . 6
⊢ (∅
∈ (𝒫 𝐵 ∩
Fin) → (∀𝑥
∈ (𝒫 𝐵 ∩
Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 → ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ ∅ 𝑧 ≤ 𝑦)) |
| 21 | 17, 20 | ax-mp 5 |
. . . . 5
⊢
(∀𝑥 ∈
(𝒫 𝐵 ∩
Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 → ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ ∅ 𝑧 ≤ 𝑦) |
| 22 | | rexn0 4511 |
. . . . 5
⊢
(∃𝑦 ∈
𝐵 ∀𝑧 ∈ ∅ 𝑧 ≤ 𝑦 → 𝐵 ≠ ∅) |
| 23 | 21, 22 | syl 17 |
. . . 4
⊢
(∀𝑥 ∈
(𝒫 𝐵 ∩
Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 → 𝐵 ≠ ∅) |
| 24 | 23 | adantl 481 |
. . 3
⊢ ((𝐾 ∈ Proset ∧
∀𝑥 ∈ (𝒫
𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) → 𝐵 ≠ ∅) |
| 25 | | raleq 3323 |
. . . . . . 7
⊢ (𝑥 = {𝑎, 𝑏} → (∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 ↔ ∀𝑧 ∈ {𝑎, 𝑏}𝑧 ≤ 𝑦)) |
| 26 | 25 | rexbidv 3179 |
. . . . . 6
⊢ (𝑥 = {𝑎, 𝑏} → (∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 ↔ ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ {𝑎, 𝑏}𝑧 ≤ 𝑦)) |
| 27 | | simplr 769 |
. . . . . 6
⊢ (((𝐾 ∈ Proset ∧
∀𝑥 ∈ (𝒫
𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ∀𝑥 ∈ (𝒫 𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) |
| 28 | | prelpwi 5452 |
. . . . . . . 8
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → {𝑎, 𝑏} ∈ 𝒫 𝐵) |
| 29 | | prfi 9363 |
. . . . . . . . 9
⊢ {𝑎, 𝑏} ∈ Fin |
| 30 | 29 | a1i 11 |
. . . . . . . 8
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → {𝑎, 𝑏} ∈ Fin) |
| 31 | 28, 30 | elind 4200 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → {𝑎, 𝑏} ∈ (𝒫 𝐵 ∩ Fin)) |
| 32 | 31 | adantl 481 |
. . . . . 6
⊢ (((𝐾 ∈ Proset ∧
∀𝑥 ∈ (𝒫
𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → {𝑎, 𝑏} ∈ (𝒫 𝐵 ∩ Fin)) |
| 33 | 26, 27, 32 | rspcdva 3623 |
. . . . 5
⊢ (((𝐾 ∈ Proset ∧
∀𝑥 ∈ (𝒫
𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ {𝑎, 𝑏}𝑧 ≤ 𝑦) |
| 34 | | vex 3484 |
. . . . . . 7
⊢ 𝑎 ∈ V |
| 35 | | vex 3484 |
. . . . . . 7
⊢ 𝑏 ∈ V |
| 36 | | breq1 5146 |
. . . . . . 7
⊢ (𝑧 = 𝑎 → (𝑧 ≤ 𝑦 ↔ 𝑎 ≤ 𝑦)) |
| 37 | | breq1 5146 |
. . . . . . 7
⊢ (𝑧 = 𝑏 → (𝑧 ≤ 𝑦 ↔ 𝑏 ≤ 𝑦)) |
| 38 | 34, 35, 36, 37 | ralpr 4700 |
. . . . . 6
⊢
(∀𝑧 ∈
{𝑎, 𝑏}𝑧 ≤ 𝑦 ↔ (𝑎 ≤ 𝑦 ∧ 𝑏 ≤ 𝑦)) |
| 39 | 38 | rexbii 3094 |
. . . . 5
⊢
(∃𝑦 ∈
𝐵 ∀𝑧 ∈ {𝑎, 𝑏}𝑧 ≤ 𝑦 ↔ ∃𝑦 ∈ 𝐵 (𝑎 ≤ 𝑦 ∧ 𝑏 ≤ 𝑦)) |
| 40 | 33, 39 | sylib 218 |
. . . 4
⊢ (((𝐾 ∈ Proset ∧
∀𝑥 ∈ (𝒫
𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ∃𝑦 ∈ 𝐵 (𝑎 ≤ 𝑦 ∧ 𝑏 ≤ 𝑦)) |
| 41 | 40 | ralrimivva 3202 |
. . 3
⊢ ((𝐾 ∈ Proset ∧
∀𝑥 ∈ (𝒫
𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) → ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 (𝑎 ≤ 𝑦 ∧ 𝑏 ≤ 𝑦)) |
| 42 | 8, 9 | isdrs 18347 |
. . 3
⊢ (𝐾 ∈ Dirset ↔ (𝐾 ∈ Proset ∧ 𝐵 ≠ ∅ ∧
∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 (𝑎 ≤ 𝑦 ∧ 𝑏 ≤ 𝑦))) |
| 43 | 14, 24, 41, 42 | syl3anbrc 1344 |
. 2
⊢ ((𝐾 ∈ Proset ∧
∀𝑥 ∈ (𝒫
𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) → 𝐾 ∈ Dirset) |
| 44 | 13, 43 | impbii 209 |
1
⊢ (𝐾 ∈ Dirset ↔ (𝐾 ∈ Proset ∧
∀𝑥 ∈ (𝒫
𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦)) |