Step | Hyp | Ref
| Expression |
1 | | drsprs 16936 |
. . 3
⊢ (𝐾 ∈ Dirset → 𝐾 ∈ Preset
) |
2 | | simpl 473 |
. . . . 5
⊢ ((𝐾 ∈ Dirset ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → 𝐾 ∈ Dirset) |
3 | | inss1 3833 |
. . . . . . . 8
⊢
(𝒫 𝐵 ∩
Fin) ⊆ 𝒫 𝐵 |
4 | 3 | sseli 3599 |
. . . . . . 7
⊢ (𝑥 ∈ (𝒫 𝐵 ∩ Fin) → 𝑥 ∈ 𝒫 𝐵) |
5 | 4 | elpwid 4170 |
. . . . . 6
⊢ (𝑥 ∈ (𝒫 𝐵 ∩ Fin) → 𝑥 ⊆ 𝐵) |
6 | 5 | adantl 482 |
. . . . 5
⊢ ((𝐾 ∈ Dirset ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑥 ⊆ 𝐵) |
7 | | inss2 3834 |
. . . . . . 7
⊢
(𝒫 𝐵 ∩
Fin) ⊆ Fin |
8 | 7 | sseli 3599 |
. . . . . 6
⊢ (𝑥 ∈ (𝒫 𝐵 ∩ Fin) → 𝑥 ∈ Fin) |
9 | 8 | adantl 482 |
. . . . 5
⊢ ((𝐾 ∈ Dirset ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → 𝑥 ∈ Fin) |
10 | | drsbn0.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐾) |
11 | | drsdirfi.l |
. . . . . 6
⊢ ≤ =
(le‘𝐾) |
12 | 10, 11 | drsdirfi 16938 |
. . . . 5
⊢ ((𝐾 ∈ Dirset ∧ 𝑥 ⊆ 𝐵 ∧ 𝑥 ∈ Fin) → ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) |
13 | 2, 6, 9, 12 | syl3anc 1326 |
. . . 4
⊢ ((𝐾 ∈ Dirset ∧ 𝑥 ∈ (𝒫 𝐵 ∩ Fin)) → ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) |
14 | 13 | ralrimiva 2966 |
. . 3
⊢ (𝐾 ∈ Dirset →
∀𝑥 ∈ (𝒫
𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) |
15 | 1, 14 | jca 554 |
. 2
⊢ (𝐾 ∈ Dirset → (𝐾 ∈ Preset ∧
∀𝑥 ∈ (𝒫
𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦)) |
16 | | simpl 473 |
. . 3
⊢ ((𝐾 ∈ Preset ∧
∀𝑥 ∈ (𝒫
𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) → 𝐾 ∈ Preset ) |
17 | | 0elpw 4834 |
. . . . . . 7
⊢ ∅
∈ 𝒫 𝐵 |
18 | | 0fin 8188 |
. . . . . . 7
⊢ ∅
∈ Fin |
19 | | elin 3796 |
. . . . . . 7
⊢ (∅
∈ (𝒫 𝐵 ∩
Fin) ↔ (∅ ∈ 𝒫 𝐵 ∧ ∅ ∈ Fin)) |
20 | 17, 18, 19 | mpbir2an 955 |
. . . . . 6
⊢ ∅
∈ (𝒫 𝐵 ∩
Fin) |
21 | | raleq 3138 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 ↔ ∀𝑧 ∈ ∅ 𝑧 ≤ 𝑦)) |
22 | 21 | rexbidv 3052 |
. . . . . . 7
⊢ (𝑥 = ∅ → (∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 ↔ ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ ∅ 𝑧 ≤ 𝑦)) |
23 | 22 | rspcv 3305 |
. . . . . 6
⊢ (∅
∈ (𝒫 𝐵 ∩
Fin) → (∀𝑥
∈ (𝒫 𝐵 ∩
Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 → ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ ∅ 𝑧 ≤ 𝑦)) |
24 | 20, 23 | ax-mp 5 |
. . . . 5
⊢
(∀𝑥 ∈
(𝒫 𝐵 ∩
Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 → ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ ∅ 𝑧 ≤ 𝑦) |
25 | | rexn0 4074 |
. . . . 5
⊢
(∃𝑦 ∈
𝐵 ∀𝑧 ∈ ∅ 𝑧 ≤ 𝑦 → 𝐵 ≠ ∅) |
26 | 24, 25 | syl 17 |
. . . 4
⊢
(∀𝑥 ∈
(𝒫 𝐵 ∩
Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 → 𝐵 ≠ ∅) |
27 | 26 | adantl 482 |
. . 3
⊢ ((𝐾 ∈ Preset ∧
∀𝑥 ∈ (𝒫
𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) → 𝐵 ≠ ∅) |
28 | | prelpwi 4915 |
. . . . . . . 8
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → {𝑎, 𝑏} ∈ 𝒫 𝐵) |
29 | | prfi 8235 |
. . . . . . . . 9
⊢ {𝑎, 𝑏} ∈ Fin |
30 | 29 | a1i 11 |
. . . . . . . 8
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → {𝑎, 𝑏} ∈ Fin) |
31 | 28, 30 | elind 3798 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → {𝑎, 𝑏} ∈ (𝒫 𝐵 ∩ Fin)) |
32 | 31 | adantl 482 |
. . . . . 6
⊢ (((𝐾 ∈ Preset ∧
∀𝑥 ∈ (𝒫
𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → {𝑎, 𝑏} ∈ (𝒫 𝐵 ∩ Fin)) |
33 | | simplr 792 |
. . . . . 6
⊢ (((𝐾 ∈ Preset ∧
∀𝑥 ∈ (𝒫
𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ∀𝑥 ∈ (𝒫 𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) |
34 | | raleq 3138 |
. . . . . . . 8
⊢ (𝑥 = {𝑎, 𝑏} → (∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 ↔ ∀𝑧 ∈ {𝑎, 𝑏}𝑧 ≤ 𝑦)) |
35 | 34 | rexbidv 3052 |
. . . . . . 7
⊢ (𝑥 = {𝑎, 𝑏} → (∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦 ↔ ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ {𝑎, 𝑏}𝑧 ≤ 𝑦)) |
36 | 35 | rspcva 3307 |
. . . . . 6
⊢ (({𝑎, 𝑏} ∈ (𝒫 𝐵 ∩ Fin) ∧ ∀𝑥 ∈ (𝒫 𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) → ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ {𝑎, 𝑏}𝑧 ≤ 𝑦) |
37 | 32, 33, 36 | syl2anc 693 |
. . . . 5
⊢ (((𝐾 ∈ Preset ∧
∀𝑥 ∈ (𝒫
𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ {𝑎, 𝑏}𝑧 ≤ 𝑦) |
38 | | vex 3203 |
. . . . . . 7
⊢ 𝑎 ∈ V |
39 | | vex 3203 |
. . . . . . 7
⊢ 𝑏 ∈ V |
40 | | breq1 4656 |
. . . . . . 7
⊢ (𝑧 = 𝑎 → (𝑧 ≤ 𝑦 ↔ 𝑎 ≤ 𝑦)) |
41 | | breq1 4656 |
. . . . . . 7
⊢ (𝑧 = 𝑏 → (𝑧 ≤ 𝑦 ↔ 𝑏 ≤ 𝑦)) |
42 | 38, 39, 40, 41 | ralpr 4238 |
. . . . . 6
⊢
(∀𝑧 ∈
{𝑎, 𝑏}𝑧 ≤ 𝑦 ↔ (𝑎 ≤ 𝑦 ∧ 𝑏 ≤ 𝑦)) |
43 | 42 | rexbii 3041 |
. . . . 5
⊢
(∃𝑦 ∈
𝐵 ∀𝑧 ∈ {𝑎, 𝑏}𝑧 ≤ 𝑦 ↔ ∃𝑦 ∈ 𝐵 (𝑎 ≤ 𝑦 ∧ 𝑏 ≤ 𝑦)) |
44 | 37, 43 | sylib 208 |
. . . 4
⊢ (((𝐾 ∈ Preset ∧
∀𝑥 ∈ (𝒫
𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ∃𝑦 ∈ 𝐵 (𝑎 ≤ 𝑦 ∧ 𝑏 ≤ 𝑦)) |
45 | 44 | ralrimivva 2971 |
. . 3
⊢ ((𝐾 ∈ Preset ∧
∀𝑥 ∈ (𝒫
𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) → ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 (𝑎 ≤ 𝑦 ∧ 𝑏 ≤ 𝑦)) |
46 | 10, 11 | isdrs 16934 |
. . 3
⊢ (𝐾 ∈ Dirset ↔ (𝐾 ∈ Preset ∧ 𝐵 ≠ ∅ ∧
∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 (𝑎 ≤ 𝑦 ∧ 𝑏 ≤ 𝑦))) |
47 | 16, 27, 45, 46 | syl3anbrc 1246 |
. 2
⊢ ((𝐾 ∈ Preset ∧
∀𝑥 ∈ (𝒫
𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦) → 𝐾 ∈ Dirset) |
48 | 15, 47 | impbii 199 |
1
⊢ (𝐾 ∈ Dirset ↔ (𝐾 ∈ Preset ∧
∀𝑥 ∈ (𝒫
𝐵 ∩ Fin)∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑥 𝑧 ≤ 𝑦)) |