Step | Hyp | Ref
| Expression |
1 | | drsprs 17655 |
. . 3
⊢ (𝐾 ∈ Dirset → 𝐾 ∈ Proset
) |
2 | | simpl 486 |
. . . . 5
⊢ ((𝐾 ∈ Dirset ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → 𝐾 ∈ Dirset) |
3 | | elinel1 4083 |
. . . . . . 7
⊢ (𝑥 ∈ (𝒫 𝐵 ∩ Fin) → 𝑥 ∈ 𝒫 𝐵) |
4 | 3 | elpwid 4496 |
. . . . . 6
⊢ (𝑥 ∈ (𝒫 𝐵 ∩ Fin) → 𝑥 ⊆ 𝐵) |
5 | 4 | adantl 485 |
. . . . 5
⊢ ((𝐾 ∈ Dirset ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑥 ⊆ 𝐵) |
6 | | elinel2 4084 |
. . . . . 6
⊢ (𝑥 ∈ (𝒫 𝐵 ∩ Fin) → 𝑥 ∈ Fin) |
7 | 6 | adantl 485 |
. . . . 5
⊢ ((𝐾 ∈ Dirset ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑥 ∈ Fin) |
8 | | drsbn0.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐾) |
9 | | drsdirfi.l |
. . . . . 6
⊢ ≤ =
(le‘𝐾) |
10 | 8, 9 | drsdirfi 17657 |
. . . . 5
⊢ ((𝐾 ∈ Dirset ∧ 𝑥 ⊆ 𝐵 ∧ 𝑥 ∈ Fin) → ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) |
11 | 2, 5, 7, 10 | syl3anc 1372 |
. . . 4
⊢ ((𝐾 ∈ Dirset ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) |
12 | 11 | ralrimiva 3096 |
. . 3
⊢ (𝐾 ∈ Dirset →
∀𝑥 ∈ (𝒫
𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) |
13 | 1, 12 | jca 515 |
. 2
⊢ (𝐾 ∈ Dirset → (𝐾 ∈ Proset ∧
∀𝑥 ∈ (𝒫
𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦)) |
14 | | simpl 486 |
. . 3
⊢ ((𝐾 ∈ Proset ∧
∀𝑥 ∈ (𝒫
𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) → 𝐾 ∈ Proset ) |
15 | | 0elpw 5219 |
. . . . . . 7
⊢ ∅
∈ 𝒫 𝐵 |
16 | | 0fin 8763 |
. . . . . . 7
⊢ ∅
∈ Fin |
17 | 15, 16 | elini 4081 |
. . . . . 6
⊢ ∅
∈ (𝒫 𝐵 ∩
Fin) |
18 | | raleq 3309 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 ↔ ∀𝑧 ∈ ∅ 𝑧 ≤ 𝑦)) |
19 | 18 | rexbidv 3206 |
. . . . . . 7
⊢ (𝑥 = ∅ → (∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 ↔ ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ ∅ 𝑧 ≤ 𝑦)) |
20 | 19 | rspcv 3519 |
. . . . . 6
⊢ (∅
∈ (𝒫 𝐵 ∩
Fin) → (∀𝑥
∈ (𝒫 𝐵 ∩
Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 → ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ ∅ 𝑧 ≤ 𝑦)) |
21 | 17, 20 | ax-mp 5 |
. . . . 5
⊢
(∀𝑥 ∈
(𝒫 𝐵 ∩
Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 → ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ ∅ 𝑧 ≤ 𝑦) |
22 | | rexn0 4394 |
. . . . 5
⊢
(∃𝑦 ∈
𝐵 ∀𝑧 ∈ ∅ 𝑧 ≤ 𝑦 → 𝐵 ≠ ∅) |
23 | 21, 22 | syl 17 |
. . . 4
⊢
(∀𝑥 ∈
(𝒫 𝐵 ∩
Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 → 𝐵 ≠ ∅) |
24 | 23 | adantl 485 |
. . 3
⊢ ((𝐾 ∈ Proset ∧
∀𝑥 ∈ (𝒫
𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) → 𝐵 ≠ ∅) |
25 | | raleq 3309 |
. . . . . . 7
⊢ (𝑥 = {𝑎, 𝑏} → (∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 ↔ ∀𝑧 ∈ {𝑎, 𝑏}𝑧 ≤ 𝑦)) |
26 | 25 | rexbidv 3206 |
. . . . . 6
⊢ (𝑥 = {𝑎, 𝑏} → (∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 ↔ ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ {𝑎, 𝑏}𝑧 ≤ 𝑦)) |
27 | | simplr 769 |
. . . . . 6
⊢ (((𝐾 ∈ Proset ∧
∀𝑥 ∈ (𝒫
𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ∀𝑥 ∈ (𝒫 𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) |
28 | | prelpwi 5303 |
. . . . . . . 8
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → {𝑎, 𝑏} ∈ 𝒫 𝐵) |
29 | | prfi 8860 |
. . . . . . . . 9
⊢ {𝑎, 𝑏} ∈ Fin |
30 | 29 | a1i 11 |
. . . . . . . 8
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → {𝑎, 𝑏} ∈ Fin) |
31 | 28, 30 | elind 4082 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → {𝑎, 𝑏} ∈ (𝒫 𝐵 ∩ Fin)) |
32 | 31 | adantl 485 |
. . . . . 6
⊢ (((𝐾 ∈ Proset ∧
∀𝑥 ∈ (𝒫
𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → {𝑎, 𝑏} ∈ (𝒫 𝐵 ∩ Fin)) |
33 | 26, 27, 32 | rspcdva 3526 |
. . . . 5
⊢ (((𝐾 ∈ Proset ∧
∀𝑥 ∈ (𝒫
𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ {𝑎, 𝑏}𝑧 ≤ 𝑦) |
34 | | vex 3401 |
. . . . . . 7
⊢ 𝑎 ∈ V |
35 | | vex 3401 |
. . . . . . 7
⊢ 𝑏 ∈ V |
36 | | breq1 5030 |
. . . . . . 7
⊢ (𝑧 = 𝑎 → (𝑧 ≤ 𝑦 ↔ 𝑎 ≤ 𝑦)) |
37 | | breq1 5030 |
. . . . . . 7
⊢ (𝑧 = 𝑏 → (𝑧 ≤ 𝑦 ↔ 𝑏 ≤ 𝑦)) |
38 | 34, 35, 36, 37 | ralpr 4588 |
. . . . . 6
⊢
(∀𝑧 ∈
{𝑎, 𝑏}𝑧 ≤ 𝑦 ↔ (𝑎 ≤ 𝑦 ∧ 𝑏 ≤ 𝑦)) |
39 | 38 | rexbii 3160 |
. . . . 5
⊢
(∃𝑦 ∈
𝐵 ∀𝑧 ∈ {𝑎, 𝑏}𝑧 ≤ 𝑦 ↔ ∃𝑦 ∈ 𝐵 (𝑎 ≤ 𝑦 ∧ 𝑏 ≤ 𝑦)) |
40 | 33, 39 | sylib 221 |
. . . 4
⊢ (((𝐾 ∈ Proset ∧
∀𝑥 ∈ (𝒫
𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ∃𝑦 ∈ 𝐵 (𝑎 ≤ 𝑦 ∧ 𝑏 ≤ 𝑦)) |
41 | 40 | ralrimivva 3103 |
. . 3
⊢ ((𝐾 ∈ Proset ∧
∀𝑥 ∈ (𝒫
𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) → ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 (𝑎 ≤ 𝑦 ∧ 𝑏 ≤ 𝑦)) |
42 | 8, 9 | isdrs 17653 |
. . 3
⊢ (𝐾 ∈ Dirset ↔ (𝐾 ∈ Proset ∧ 𝐵 ≠ ∅ ∧
∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 (𝑎 ≤ 𝑦 ∧ 𝑏 ≤ 𝑦))) |
43 | 14, 24, 41, 42 | syl3anbrc 1344 |
. 2
⊢ ((𝐾 ∈ Proset ∧
∀𝑥 ∈ (𝒫
𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) → 𝐾 ∈ Dirset) |
44 | 13, 43 | impbii 212 |
1
⊢ (𝐾 ∈ Dirset ↔ (𝐾 ∈ Proset ∧
∀𝑥 ∈ (𝒫
𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦)) |