Step |
Hyp |
Ref |
Expression |
0 |
|
club |
⊢ lub |
1 |
|
vp |
⊢ 𝑝 |
2 |
|
cvv |
⊢ V |
3 |
|
vs |
⊢ 𝑠 |
4 |
|
cbs |
⊢ Base |
5 |
1
|
cv |
⊢ 𝑝 |
6 |
5 4
|
cfv |
⊢ ( Base ‘ 𝑝 ) |
7 |
6
|
cpw |
⊢ 𝒫 ( Base ‘ 𝑝 ) |
8 |
|
vx |
⊢ 𝑥 |
9 |
|
vy |
⊢ 𝑦 |
10 |
3
|
cv |
⊢ 𝑠 |
11 |
9
|
cv |
⊢ 𝑦 |
12 |
|
cple |
⊢ le |
13 |
5 12
|
cfv |
⊢ ( le ‘ 𝑝 ) |
14 |
8
|
cv |
⊢ 𝑥 |
15 |
11 14 13
|
wbr |
⊢ 𝑦 ( le ‘ 𝑝 ) 𝑥 |
16 |
15 9 10
|
wral |
⊢ ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 |
17 |
|
vz |
⊢ 𝑧 |
18 |
17
|
cv |
⊢ 𝑧 |
19 |
11 18 13
|
wbr |
⊢ 𝑦 ( le ‘ 𝑝 ) 𝑧 |
20 |
19 9 10
|
wral |
⊢ ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧 |
21 |
14 18 13
|
wbr |
⊢ 𝑥 ( le ‘ 𝑝 ) 𝑧 |
22 |
20 21
|
wi |
⊢ ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧 → 𝑥 ( le ‘ 𝑝 ) 𝑧 ) |
23 |
22 17 6
|
wral |
⊢ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧 → 𝑥 ( le ‘ 𝑝 ) 𝑧 ) |
24 |
16 23
|
wa |
⊢ ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧 → 𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) |
25 |
24 8 6
|
crio |
⊢ ( ℩ 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧 → 𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) ) |
26 |
3 7 25
|
cmpt |
⊢ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑝 ) ↦ ( ℩ 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧 → 𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) ) ) |
27 |
24 8 6
|
wreu |
⊢ ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧 → 𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) |
28 |
27 3
|
cab |
⊢ { 𝑠 ∣ ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧 → 𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) } |
29 |
26 28
|
cres |
⊢ ( ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑝 ) ↦ ( ℩ 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧 → 𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧 → 𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) } ) |
30 |
1 2 29
|
cmpt |
⊢ ( 𝑝 ∈ V ↦ ( ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑝 ) ↦ ( ℩ 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧 → 𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧 → 𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) } ) ) |
31 |
0 30
|
wceq |
⊢ lub = ( 𝑝 ∈ V ↦ ( ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑝 ) ↦ ( ℩ 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧 → 𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧 → 𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) } ) ) |