Proof of Theorem lubeldm2d
Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . 3
⊢
(Base‘𝐾) =
(Base‘𝐾) |
2 | | eqid 2738 |
. . 3
⊢
(le‘𝐾) =
(le‘𝐾) |
3 | | eqid 2738 |
. . 3
⊢
(lub‘𝐾) =
(lub‘𝐾) |
4 | | biid 260 |
. . 3
⊢
((∀𝑦 ∈
𝑆 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑆 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧)) ↔ (∀𝑦 ∈ 𝑆 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑆 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧))) |
5 | | lubeldm2d.k |
. . 3
⊢ (𝜑 → 𝐾 ∈ Poset) |
6 | 1, 2, 3, 4, 5 | lubeldm2 46207 |
. 2
⊢ (𝜑 → (𝑆 ∈ dom (lub‘𝐾) ↔ (𝑆 ⊆ (Base‘𝐾) ∧ ∃𝑥 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑆 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑆 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧))))) |
7 | | lubeldm2d.u |
. . . 4
⊢ (𝜑 → 𝑈 = (lub‘𝐾)) |
8 | 7 | dmeqd 5809 |
. . 3
⊢ (𝜑 → dom 𝑈 = dom (lub‘𝐾)) |
9 | 8 | eleq2d 2824 |
. 2
⊢ (𝜑 → (𝑆 ∈ dom 𝑈 ↔ 𝑆 ∈ dom (lub‘𝐾))) |
10 | | lubeldm2d.b |
. . . 4
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) |
11 | 10 | sseq2d 3954 |
. . 3
⊢ (𝜑 → (𝑆 ⊆ 𝐵 ↔ 𝑆 ⊆ (Base‘𝐾))) |
12 | | lubeldm2d.p |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝜓 ↔ (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧)))) |
13 | | lubeldm2d.l |
. . . . . . . . . . 11
⊢ (𝜑 → ≤ = (le‘𝐾)) |
14 | 13 | breqd 5086 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ≤ 𝑥 ↔ 𝑦(le‘𝐾)𝑥)) |
15 | 14 | ralbidv 3119 |
. . . . . . . . 9
⊢ (𝜑 → (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ↔ ∀𝑦 ∈ 𝑆 𝑦(le‘𝐾)𝑥)) |
16 | 13 | breqd 5086 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑦 ≤ 𝑧 ↔ 𝑦(le‘𝐾)𝑧)) |
17 | 16 | ralbidv 3119 |
. . . . . . . . . . 11
⊢ (𝜑 → (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 ↔ ∀𝑦 ∈ 𝑆 𝑦(le‘𝐾)𝑧)) |
18 | 13 | breqd 5086 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ≤ 𝑧 ↔ 𝑥(le‘𝐾)𝑧)) |
19 | 17, 18 | imbi12d 345 |
. . . . . . . . . 10
⊢ (𝜑 → ((∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧) ↔ (∀𝑦 ∈ 𝑆 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧))) |
20 | 10, 19 | raleqbidv 3335 |
. . . . . . . . 9
⊢ (𝜑 → (∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧) ↔ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑆 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧))) |
21 | 15, 20 | anbi12d 631 |
. . . . . . . 8
⊢ (𝜑 → ((∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧)) ↔ (∀𝑦 ∈ 𝑆 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑆 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧)))) |
22 | 21 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀𝑧 ∈ 𝐵 (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧)) ↔ (∀𝑦 ∈ 𝑆 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑆 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧)))) |
23 | 12, 22 | bitrd 278 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝜓 ↔ (∀𝑦 ∈ 𝑆 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑆 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧)))) |
24 | 23 | pm5.32da 579 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ (∀𝑦 ∈ 𝑆 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑆 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧))))) |
25 | 10 | eleq2d 2824 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ (Base‘𝐾))) |
26 | 25 | anbi1d 630 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ (∀𝑦 ∈ 𝑆 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑆 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧))) ↔ (𝑥 ∈ (Base‘𝐾) ∧ (∀𝑦 ∈ 𝑆 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑆 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧))))) |
27 | 24, 26 | bitrd 278 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ 𝜓) ↔ (𝑥 ∈ (Base‘𝐾) ∧ (∀𝑦 ∈ 𝑆 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑆 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧))))) |
28 | 27 | rexbidv2 3223 |
. . 3
⊢ (𝜑 → (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑆 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑆 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧)))) |
29 | 11, 28 | anbi12d 631 |
. 2
⊢ (𝜑 → ((𝑆 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐵 𝜓) ↔ (𝑆 ⊆ (Base‘𝐾) ∧ ∃𝑥 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑆 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ 𝑆 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧))))) |
30 | 6, 9, 29 | 3bitr4d 311 |
1
⊢ (𝜑 → (𝑆 ∈ dom 𝑈 ↔ (𝑆 ⊆ 𝐵 ∧ ∃𝑥 ∈ 𝐵 𝜓))) |