Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . . . . 6
⊢ (𝑓 = 𝐾 → (Base‘𝑓) = (Base‘𝐾)) |
2 | | isdrs.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐾) |
3 | 1, 2 | syl6eqr 2662 |
. . . . 5
⊢ (𝑓 = 𝐾 → (Base‘𝑓) = 𝐵) |
4 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑓 = 𝐾 → (le‘𝑓) = (le‘𝐾)) |
5 | | isdrs.l |
. . . . . . 7
⊢ ≤ =
(le‘𝐾) |
6 | 4, 5 | syl6eqr 2662 |
. . . . . 6
⊢ (𝑓 = 𝐾 → (le‘𝑓) = ≤ ) |
7 | 6 | sbceq1d 3407 |
. . . . 5
⊢ (𝑓 = 𝐾 → ([(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧)) ↔ [ ≤ / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧)))) |
8 | 3, 7 | sbceqbid 3409 |
. . . 4
⊢ (𝑓 = 𝐾 → ([(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧)) ↔ [𝐵 / 𝑏][ ≤ / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧)))) |
9 | | fvex 6113 |
. . . . . 6
⊢
(Base‘𝐾)
∈ V |
10 | 2, 9 | eqeltri 2684 |
. . . . 5
⊢ 𝐵 ∈ V |
11 | | fvex 6113 |
. . . . . 6
⊢
(le‘𝐾) ∈
V |
12 | 5, 11 | eqeltri 2684 |
. . . . 5
⊢ ≤ ∈
V |
13 | | neeq1 2844 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → (𝑏 ≠ ∅ ↔ 𝐵 ≠ ∅)) |
14 | 13 | adantr 480 |
. . . . . 6
⊢ ((𝑏 = 𝐵 ∧ 𝑟 = ≤ ) → (𝑏 ≠ ∅ ↔ 𝐵 ≠ ∅)) |
15 | | rexeq 3116 |
. . . . . . . . 9
⊢ (𝑏 = 𝐵 → (∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧) ↔ ∃𝑧 ∈ 𝐵 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))) |
16 | 15 | raleqbi1dv 3123 |
. . . . . . . 8
⊢ (𝑏 = 𝐵 → (∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧) ↔ ∀𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))) |
17 | 16 | raleqbi1dv 3123 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))) |
18 | | breq 4585 |
. . . . . . . . . 10
⊢ (𝑟 = ≤ → (𝑥𝑟𝑧 ↔ 𝑥 ≤ 𝑧)) |
19 | | breq 4585 |
. . . . . . . . . 10
⊢ (𝑟 = ≤ → (𝑦𝑟𝑧 ↔ 𝑦 ≤ 𝑧)) |
20 | 18, 19 | anbi12d 743 |
. . . . . . . . 9
⊢ (𝑟 = ≤ → ((𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧) ↔ (𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧))) |
21 | 20 | rexbidv 3034 |
. . . . . . . 8
⊢ (𝑟 = ≤ → (∃𝑧 ∈ 𝐵 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧) ↔ ∃𝑧 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧))) |
22 | 21 | 2ralbidv 2972 |
. . . . . . 7
⊢ (𝑟 = ≤ → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧))) |
23 | 17, 22 | sylan9bb 732 |
. . . . . 6
⊢ ((𝑏 = 𝐵 ∧ 𝑟 = ≤ ) → (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧))) |
24 | 14, 23 | anbi12d 743 |
. . . . 5
⊢ ((𝑏 = 𝐵 ∧ 𝑟 = ≤ ) → ((𝑏 ≠ ∅ ∧
∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧)) ↔ (𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧)))) |
25 | 10, 12, 24 | sbc2ie 3472 |
. . . 4
⊢
([𝐵 / 𝑏][ ≤ / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧)) ↔ (𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧))) |
26 | 8, 25 | syl6bb 275 |
. . 3
⊢ (𝑓 = 𝐾 → ([(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧)) ↔ (𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧)))) |
27 | | df-drs 16752 |
. . 3
⊢ Dirset =
{𝑓 ∈ Preset ∣
[(Base‘𝑓) /
𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 (𝑥𝑟𝑧 ∧ 𝑦𝑟𝑧))} |
28 | 26, 27 | elrab2 3333 |
. 2
⊢ (𝐾 ∈ Dirset ↔ (𝐾 ∈ Preset ∧ (𝐵 ≠ ∅ ∧
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧)))) |
29 | | 3anass 1035 |
. 2
⊢ ((𝐾 ∈ Preset ∧ 𝐵 ≠ ∅ ∧
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧)) ↔ (𝐾 ∈ Preset ∧ (𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧)))) |
30 | 28, 29 | bitr4i 266 |
1
⊢ (𝐾 ∈ Dirset ↔ (𝐾 ∈ Preset ∧ 𝐵 ≠ ∅ ∧
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (𝑥 ≤ 𝑧 ∧ 𝑦 ≤ 𝑧))) |