Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . 3
⊢
(Base‘𝐾) =
(Base‘𝐾) |
2 | | eqid 2738 |
. . 3
⊢
(le‘𝐾) =
(le‘𝐾) |
3 | | glb0.g |
. . 3
⊢ 𝐺 = (glb‘𝐾) |
4 | | biid 260 |
. . 3
⊢
((∀𝑦 ∈
∅ 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ ∅ 𝑧(le‘𝐾)𝑦 → 𝑧(le‘𝐾)𝑥)) ↔ (∀𝑦 ∈ ∅ 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ ∅ 𝑧(le‘𝐾)𝑦 → 𝑧(le‘𝐾)𝑥))) |
5 | | id 22 |
. . 3
⊢ (𝐾 ∈ OP → 𝐾 ∈ OP) |
6 | | 0ss 4327 |
. . . 4
⊢ ∅
⊆ (Base‘𝐾) |
7 | 6 | a1i 11 |
. . 3
⊢ (𝐾 ∈ OP → ∅
⊆ (Base‘𝐾)) |
8 | 1, 2, 3, 4, 5, 7 | glbval 18002 |
. 2
⊢ (𝐾 ∈ OP → (𝐺‘∅) =
(℩𝑥 ∈
(Base‘𝐾)(∀𝑦 ∈ ∅ 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ ∅ 𝑧(le‘𝐾)𝑦 → 𝑧(le‘𝐾)𝑥)))) |
9 | | glb0.u |
. . . 4
⊢ 1 =
(1.‘𝐾) |
10 | 1, 9 | op1cl 37126 |
. . 3
⊢ (𝐾 ∈ OP → 1 ∈
(Base‘𝐾)) |
11 | | ral0 4440 |
. . . . . . 7
⊢
∀𝑦 ∈
∅ 𝑧(le‘𝐾)𝑦 |
12 | 11 | a1bi 362 |
. . . . . 6
⊢ (𝑧(le‘𝐾)𝑥 ↔ (∀𝑦 ∈ ∅ 𝑧(le‘𝐾)𝑦 → 𝑧(le‘𝐾)𝑥)) |
13 | 12 | ralbii 3090 |
. . . . 5
⊢
(∀𝑧 ∈
(Base‘𝐾)𝑧(le‘𝐾)𝑥 ↔ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ ∅ 𝑧(le‘𝐾)𝑦 → 𝑧(le‘𝐾)𝑥)) |
14 | | ral0 4440 |
. . . . . 6
⊢
∀𝑦 ∈
∅ 𝑥(le‘𝐾)𝑦 |
15 | 14 | biantrur 530 |
. . . . 5
⊢
(∀𝑧 ∈
(Base‘𝐾)(∀𝑦 ∈ ∅ 𝑧(le‘𝐾)𝑦 → 𝑧(le‘𝐾)𝑥) ↔ (∀𝑦 ∈ ∅ 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ ∅ 𝑧(le‘𝐾)𝑦 → 𝑧(le‘𝐾)𝑥))) |
16 | 13, 15 | bitri 274 |
. . . 4
⊢
(∀𝑧 ∈
(Base‘𝐾)𝑧(le‘𝐾)𝑥 ↔ (∀𝑦 ∈ ∅ 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ ∅ 𝑧(le‘𝐾)𝑦 → 𝑧(le‘𝐾)𝑥))) |
17 | 10 | adantr 480 |
. . . . . . 7
⊢ ((𝐾 ∈ OP ∧ 𝑥 ∈ (Base‘𝐾)) → 1 ∈ (Base‘𝐾)) |
18 | | breq1 5073 |
. . . . . . . 8
⊢ (𝑧 = 1 → (𝑧(le‘𝐾)𝑥 ↔ 1 (le‘𝐾)𝑥)) |
19 | 18 | rspcv 3547 |
. . . . . . 7
⊢ ( 1 ∈
(Base‘𝐾) →
(∀𝑧 ∈
(Base‘𝐾)𝑧(le‘𝐾)𝑥 → 1 (le‘𝐾)𝑥)) |
20 | 17, 19 | syl 17 |
. . . . . 6
⊢ ((𝐾 ∈ OP ∧ 𝑥 ∈ (Base‘𝐾)) → (∀𝑧 ∈ (Base‘𝐾)𝑧(le‘𝐾)𝑥 → 1 (le‘𝐾)𝑥)) |
21 | 1, 2, 9 | op1le 37133 |
. . . . . 6
⊢ ((𝐾 ∈ OP ∧ 𝑥 ∈ (Base‘𝐾)) → ( 1 (le‘𝐾)𝑥 ↔ 𝑥 = 1 )) |
22 | 20, 21 | sylibd 238 |
. . . . 5
⊢ ((𝐾 ∈ OP ∧ 𝑥 ∈ (Base‘𝐾)) → (∀𝑧 ∈ (Base‘𝐾)𝑧(le‘𝐾)𝑥 → 𝑥 = 1 )) |
23 | 1, 2, 9 | ople1 37132 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ OP ∧ 𝑧 ∈ (Base‘𝐾)) → 𝑧(le‘𝐾) 1 ) |
24 | 23 | adantlr 711 |
. . . . . . . . 9
⊢ (((𝐾 ∈ OP ∧ 𝑥 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) → 𝑧(le‘𝐾) 1 ) |
25 | 24 | ex 412 |
. . . . . . . 8
⊢ ((𝐾 ∈ OP ∧ 𝑥 ∈ (Base‘𝐾)) → (𝑧 ∈ (Base‘𝐾) → 𝑧(le‘𝐾) 1 )) |
26 | | breq2 5074 |
. . . . . . . . 9
⊢ (𝑥 = 1 → (𝑧(le‘𝐾)𝑥 ↔ 𝑧(le‘𝐾) 1 )) |
27 | 26 | biimprcd 249 |
. . . . . . . 8
⊢ (𝑧(le‘𝐾) 1 → (𝑥 = 1 → 𝑧(le‘𝐾)𝑥)) |
28 | 25, 27 | syl6 35 |
. . . . . . 7
⊢ ((𝐾 ∈ OP ∧ 𝑥 ∈ (Base‘𝐾)) → (𝑧 ∈ (Base‘𝐾) → (𝑥 = 1 → 𝑧(le‘𝐾)𝑥))) |
29 | 28 | com23 86 |
. . . . . 6
⊢ ((𝐾 ∈ OP ∧ 𝑥 ∈ (Base‘𝐾)) → (𝑥 = 1 → (𝑧 ∈ (Base‘𝐾) → 𝑧(le‘𝐾)𝑥))) |
30 | 29 | ralrimdv 3111 |
. . . . 5
⊢ ((𝐾 ∈ OP ∧ 𝑥 ∈ (Base‘𝐾)) → (𝑥 = 1 → ∀𝑧 ∈ (Base‘𝐾)𝑧(le‘𝐾)𝑥)) |
31 | 22, 30 | impbid 211 |
. . . 4
⊢ ((𝐾 ∈ OP ∧ 𝑥 ∈ (Base‘𝐾)) → (∀𝑧 ∈ (Base‘𝐾)𝑧(le‘𝐾)𝑥 ↔ 𝑥 = 1 )) |
32 | 16, 31 | bitr3id 284 |
. . 3
⊢ ((𝐾 ∈ OP ∧ 𝑥 ∈ (Base‘𝐾)) → ((∀𝑦 ∈ ∅ 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ ∅ 𝑧(le‘𝐾)𝑦 → 𝑧(le‘𝐾)𝑥)) ↔ 𝑥 = 1 )) |
33 | 10, 32 | riota5 7242 |
. 2
⊢ (𝐾 ∈ OP →
(℩𝑥 ∈
(Base‘𝐾)(∀𝑦 ∈ ∅ 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ ∅ 𝑧(le‘𝐾)𝑦 → 𝑧(le‘𝐾)𝑥))) = 1 ) |
34 | 8, 33 | eqtrd 2778 |
1
⊢ (𝐾 ∈ OP → (𝐺‘∅) = 1
) |