Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . 3
⊢
(Base‘𝐾) =
(Base‘𝐾) |
2 | | eqid 2737 |
. . 3
⊢
(le‘𝐾) =
(le‘𝐾) |
3 | | lub0.u |
. . 3
⊢ 1 =
(lub‘𝐾) |
4 | | biid 264 |
. . 3
⊢
((∀𝑦 ∈
∅ 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ ∅ 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧)) ↔ (∀𝑦 ∈ ∅ 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ ∅ 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧))) |
5 | | id 22 |
. . 3
⊢ (𝐾 ∈ OP → 𝐾 ∈ OP) |
6 | | 0ss 4311 |
. . . 4
⊢ ∅
⊆ (Base‘𝐾) |
7 | 6 | a1i 11 |
. . 3
⊢ (𝐾 ∈ OP → ∅
⊆ (Base‘𝐾)) |
8 | 1, 2, 3, 4, 5, 7 | lubval 17862 |
. 2
⊢ (𝐾 ∈ OP → ( 1
‘∅) = (℩𝑥 ∈ (Base‘𝐾)(∀𝑦 ∈ ∅ 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ ∅ 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧)))) |
9 | | lub0.z |
. . . 4
⊢ 0 =
(0.‘𝐾) |
10 | 1, 9 | op0cl 36935 |
. . 3
⊢ (𝐾 ∈ OP → 0 ∈
(Base‘𝐾)) |
11 | | ral0 4424 |
. . . . . . 7
⊢
∀𝑦 ∈
∅ 𝑦(le‘𝐾)𝑧 |
12 | 11 | a1bi 366 |
. . . . . 6
⊢ (𝑥(le‘𝐾)𝑧 ↔ (∀𝑦 ∈ ∅ 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧)) |
13 | 12 | ralbii 3088 |
. . . . 5
⊢
(∀𝑧 ∈
(Base‘𝐾)𝑥(le‘𝐾)𝑧 ↔ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ ∅ 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧)) |
14 | | ral0 4424 |
. . . . . 6
⊢
∀𝑦 ∈
∅ 𝑦(le‘𝐾)𝑥 |
15 | 14 | biantrur 534 |
. . . . 5
⊢
(∀𝑧 ∈
(Base‘𝐾)(∀𝑦 ∈ ∅ 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧) ↔ (∀𝑦 ∈ ∅ 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ ∅ 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧))) |
16 | 13, 15 | bitri 278 |
. . . 4
⊢
(∀𝑧 ∈
(Base‘𝐾)𝑥(le‘𝐾)𝑧 ↔ (∀𝑦 ∈ ∅ 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ ∅ 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧))) |
17 | 10 | adantr 484 |
. . . . . . 7
⊢ ((𝐾 ∈ OP ∧ 𝑥 ∈ (Base‘𝐾)) → 0 ∈ (Base‘𝐾)) |
18 | | breq2 5057 |
. . . . . . . 8
⊢ (𝑧 = 0 → (𝑥(le‘𝐾)𝑧 ↔ 𝑥(le‘𝐾) 0 )) |
19 | 18 | rspcv 3532 |
. . . . . . 7
⊢ ( 0 ∈
(Base‘𝐾) →
(∀𝑧 ∈
(Base‘𝐾)𝑥(le‘𝐾)𝑧 → 𝑥(le‘𝐾) 0 )) |
20 | 17, 19 | syl 17 |
. . . . . 6
⊢ ((𝐾 ∈ OP ∧ 𝑥 ∈ (Base‘𝐾)) → (∀𝑧 ∈ (Base‘𝐾)𝑥(le‘𝐾)𝑧 → 𝑥(le‘𝐾) 0 )) |
21 | 1, 2, 9 | ople0 36938 |
. . . . . 6
⊢ ((𝐾 ∈ OP ∧ 𝑥 ∈ (Base‘𝐾)) → (𝑥(le‘𝐾) 0 ↔ 𝑥 = 0 )) |
22 | 20, 21 | sylibd 242 |
. . . . 5
⊢ ((𝐾 ∈ OP ∧ 𝑥 ∈ (Base‘𝐾)) → (∀𝑧 ∈ (Base‘𝐾)𝑥(le‘𝐾)𝑧 → 𝑥 = 0 )) |
23 | 1, 2, 9 | op0le 36937 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ OP ∧ 𝑧 ∈ (Base‘𝐾)) → 0 (le‘𝐾)𝑧) |
24 | 23 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝐾 ∈ OP ∧ 𝑥 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) → 0 (le‘𝐾)𝑧) |
25 | 24 | ex 416 |
. . . . . . . 8
⊢ ((𝐾 ∈ OP ∧ 𝑥 ∈ (Base‘𝐾)) → (𝑧 ∈ (Base‘𝐾) → 0 (le‘𝐾)𝑧)) |
26 | | breq1 5056 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (𝑥(le‘𝐾)𝑧 ↔ 0 (le‘𝐾)𝑧)) |
27 | 26 | biimprcd 253 |
. . . . . . . 8
⊢ ( 0
(le‘𝐾)𝑧 → (𝑥 = 0 → 𝑥(le‘𝐾)𝑧)) |
28 | 25, 27 | syl6 35 |
. . . . . . 7
⊢ ((𝐾 ∈ OP ∧ 𝑥 ∈ (Base‘𝐾)) → (𝑧 ∈ (Base‘𝐾) → (𝑥 = 0 → 𝑥(le‘𝐾)𝑧))) |
29 | 28 | com23 86 |
. . . . . 6
⊢ ((𝐾 ∈ OP ∧ 𝑥 ∈ (Base‘𝐾)) → (𝑥 = 0 → (𝑧 ∈ (Base‘𝐾) → 𝑥(le‘𝐾)𝑧))) |
30 | 29 | ralrimdv 3109 |
. . . . 5
⊢ ((𝐾 ∈ OP ∧ 𝑥 ∈ (Base‘𝐾)) → (𝑥 = 0 → ∀𝑧 ∈ (Base‘𝐾)𝑥(le‘𝐾)𝑧)) |
31 | 22, 30 | impbid 215 |
. . . 4
⊢ ((𝐾 ∈ OP ∧ 𝑥 ∈ (Base‘𝐾)) → (∀𝑧 ∈ (Base‘𝐾)𝑥(le‘𝐾)𝑧 ↔ 𝑥 = 0 )) |
32 | 16, 31 | bitr3id 288 |
. . 3
⊢ ((𝐾 ∈ OP ∧ 𝑥 ∈ (Base‘𝐾)) → ((∀𝑦 ∈ ∅ 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ ∅ 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧)) ↔ 𝑥 = 0 )) |
33 | 10, 32 | riota5 7200 |
. 2
⊢ (𝐾 ∈ OP →
(℩𝑥 ∈
(Base‘𝐾)(∀𝑦 ∈ ∅ 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ ∅ 𝑦(le‘𝐾)𝑧 → 𝑥(le‘𝐾)𝑧))) = 0 ) |
34 | 8, 33 | eqtrd 2777 |
1
⊢ (𝐾 ∈ OP → ( 1
‘∅) = 0 ) |