Detailed syntax breakdown of Definition df-lub
Step | Hyp | Ref
| Expression |
1 | | club 16942 |
. 2
class
lub |
2 | | vp |
. . 3
setvar 𝑝 |
3 | | cvv 3200 |
. . 3
class
V |
4 | | vs |
. . . . 5
setvar 𝑠 |
5 | 2 | cv 1482 |
. . . . . . 7
class 𝑝 |
6 | | cbs 15857 |
. . . . . . 7
class
Base |
7 | 5, 6 | cfv 5888 |
. . . . . 6
class
(Base‘𝑝) |
8 | 7 | cpw 4158 |
. . . . 5
class 𝒫
(Base‘𝑝) |
9 | | vy |
. . . . . . . . . 10
setvar 𝑦 |
10 | 9 | cv 1482 |
. . . . . . . . 9
class 𝑦 |
11 | | vx |
. . . . . . . . . 10
setvar 𝑥 |
12 | 11 | cv 1482 |
. . . . . . . . 9
class 𝑥 |
13 | | cple 15948 |
. . . . . . . . . 10
class
le |
14 | 5, 13 | cfv 5888 |
. . . . . . . . 9
class
(le‘𝑝) |
15 | 10, 12, 14 | wbr 4653 |
. . . . . . . 8
wff 𝑦(le‘𝑝)𝑥 |
16 | 4 | cv 1482 |
. . . . . . . 8
class 𝑠 |
17 | 15, 9, 16 | wral 2912 |
. . . . . . 7
wff
∀𝑦 ∈
𝑠 𝑦(le‘𝑝)𝑥 |
18 | | vz |
. . . . . . . . . . . 12
setvar 𝑧 |
19 | 18 | cv 1482 |
. . . . . . . . . . 11
class 𝑧 |
20 | 10, 19, 14 | wbr 4653 |
. . . . . . . . . 10
wff 𝑦(le‘𝑝)𝑧 |
21 | 20, 9, 16 | wral 2912 |
. . . . . . . . 9
wff
∀𝑦 ∈
𝑠 𝑦(le‘𝑝)𝑧 |
22 | 12, 19, 14 | wbr 4653 |
. . . . . . . . 9
wff 𝑥(le‘𝑝)𝑧 |
23 | 21, 22 | wi 4 |
. . . . . . . 8
wff
(∀𝑦 ∈
𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧) |
24 | 23, 18, 7 | wral 2912 |
. . . . . . 7
wff
∀𝑧 ∈
(Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧) |
25 | 17, 24 | wa 384 |
. . . . . 6
wff
(∀𝑦 ∈
𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧)) |
26 | 25, 11, 7 | crio 6610 |
. . . . 5
class
(℩𝑥
∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧))) |
27 | 4, 8, 26 | cmpt 4729 |
. . . 4
class (𝑠 ∈ 𝒫
(Base‘𝑝) ↦
(℩𝑥 ∈
(Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧)))) |
28 | 25, 11, 7 | wreu 2914 |
. . . . 5
wff
∃!𝑥 ∈
(Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧)) |
29 | 28, 4 | cab 2608 |
. . . 4
class {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧))} |
30 | 27, 29 | cres 5116 |
. . 3
class ((𝑠 ∈ 𝒫
(Base‘𝑝) ↦
(℩𝑥 ∈
(Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧)))) ↾ {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧))}) |
31 | 2, 3, 30 | cmpt 4729 |
. 2
class (𝑝 ∈ V ↦ ((𝑠 ∈ 𝒫
(Base‘𝑝) ↦
(℩𝑥 ∈
(Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧)))) ↾ {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧))})) |
32 | 1, 31 | wceq 1483 |
1
wff lub =
(𝑝 ∈ V ↦ ((𝑠 ∈ 𝒫
(Base‘𝑝) ↦
(℩𝑥 ∈
(Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧)))) ↾ {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧))})) |