Step |
Hyp |
Ref |
Expression |
1 |
|
lubfval.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
2 |
|
lubfval.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
3 |
|
lubfval.u |
⊢ 𝑈 = ( lub ‘ 𝐾 ) |
4 |
|
lubfval.p |
⊢ ( 𝜓 ↔ ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) |
5 |
|
lubfval.k |
⊢ ( 𝜑 → 𝐾 ∈ 𝑉 ) |
6 |
|
elex |
⊢ ( 𝐾 ∈ 𝑉 → 𝐾 ∈ V ) |
7 |
|
fveq2 |
⊢ ( 𝑝 = 𝐾 → ( Base ‘ 𝑝 ) = ( Base ‘ 𝐾 ) ) |
8 |
7 1
|
eqtr4di |
⊢ ( 𝑝 = 𝐾 → ( Base ‘ 𝑝 ) = 𝐵 ) |
9 |
8
|
pweqd |
⊢ ( 𝑝 = 𝐾 → 𝒫 ( Base ‘ 𝑝 ) = 𝒫 𝐵 ) |
10 |
|
fveq2 |
⊢ ( 𝑝 = 𝐾 → ( le ‘ 𝑝 ) = ( le ‘ 𝐾 ) ) |
11 |
10 2
|
eqtr4di |
⊢ ( 𝑝 = 𝐾 → ( le ‘ 𝑝 ) = ≤ ) |
12 |
11
|
breqd |
⊢ ( 𝑝 = 𝐾 → ( 𝑦 ( le ‘ 𝑝 ) 𝑥 ↔ 𝑦 ≤ 𝑥 ) ) |
13 |
12
|
ralbidv |
⊢ ( 𝑝 = 𝐾 → ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ↔ ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ) ) |
14 |
11
|
breqd |
⊢ ( 𝑝 = 𝐾 → ( 𝑦 ( le ‘ 𝑝 ) 𝑧 ↔ 𝑦 ≤ 𝑧 ) ) |
15 |
14
|
ralbidv |
⊢ ( 𝑝 = 𝐾 → ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧 ↔ ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 ) ) |
16 |
11
|
breqd |
⊢ ( 𝑝 = 𝐾 → ( 𝑥 ( le ‘ 𝑝 ) 𝑧 ↔ 𝑥 ≤ 𝑧 ) ) |
17 |
15 16
|
imbi12d |
⊢ ( 𝑝 = 𝐾 → ( ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧 → 𝑥 ( le ‘ 𝑝 ) 𝑧 ) ↔ ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) |
18 |
8 17
|
raleqbidv |
⊢ ( 𝑝 = 𝐾 → ( ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧 → 𝑥 ( le ‘ 𝑝 ) 𝑧 ) ↔ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) |
19 |
13 18
|
anbi12d |
⊢ ( 𝑝 = 𝐾 → ( ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧 → 𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) ) |
20 |
8 19
|
riotaeqbidv |
⊢ ( 𝑝 = 𝐾 → ( ℩ 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧 → 𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) ) = ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) ) |
21 |
9 20
|
mpteq12dv |
⊢ ( 𝑝 = 𝐾 → ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑝 ) ↦ ( ℩ 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧 → 𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) ) ) = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) ) ) |
22 |
19
|
reubidv |
⊢ ( 𝑝 = 𝐾 → ( ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧 → 𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) ↔ ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) ) |
23 |
|
reueq1 |
⊢ ( ( Base ‘ 𝑝 ) = 𝐵 → ( ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ↔ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) ) |
24 |
8 23
|
syl |
⊢ ( 𝑝 = 𝐾 → ( ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ↔ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) ) |
25 |
22 24
|
bitrd |
⊢ ( 𝑝 = 𝐾 → ( ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧 → 𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) ↔ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) ) |
26 |
25
|
abbidv |
⊢ ( 𝑝 = 𝐾 → { 𝑠 ∣ ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧 → 𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) } = { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) } ) |
27 |
21 26
|
reseq12d |
⊢ ( 𝑝 = 𝐾 → ( ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑝 ) ↦ ( ℩ 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧 → 𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧 → 𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) } ) = ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) } ) ) |
28 |
|
df-lub |
⊢ lub = ( 𝑝 ∈ V ↦ ( ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑝 ) ↦ ( ℩ 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧 → 𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝑝 ) ( ∀ 𝑦 ∈ 𝑠 𝑦 ( le ‘ 𝑝 ) 𝑧 → 𝑥 ( le ‘ 𝑝 ) 𝑧 ) ) } ) ) |
29 |
1
|
fvexi |
⊢ 𝐵 ∈ V |
30 |
29
|
pwex |
⊢ 𝒫 𝐵 ∈ V |
31 |
30
|
mptex |
⊢ ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) ) ∈ V |
32 |
31
|
resex |
⊢ ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) } ) ∈ V |
33 |
27 28 32
|
fvmpt |
⊢ ( 𝐾 ∈ V → ( lub ‘ 𝐾 ) = ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) } ) ) |
34 |
4
|
a1i |
⊢ ( 𝑥 ∈ 𝐵 → ( 𝜓 ↔ ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) ) |
35 |
34
|
riotabiia |
⊢ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) = ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) |
36 |
35
|
mpteq2i |
⊢ ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) ) = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) ) |
37 |
4
|
reubii |
⊢ ( ∃! 𝑥 ∈ 𝐵 𝜓 ↔ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) |
38 |
37
|
abbii |
⊢ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 𝜓 } = { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) } |
39 |
36 38
|
reseq12i |
⊢ ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 𝜓 } ) = ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) } ) |
40 |
33 3 39
|
3eqtr4g |
⊢ ( 𝐾 ∈ V → 𝑈 = ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 𝜓 } ) ) |
41 |
5 6 40
|
3syl |
⊢ ( 𝜑 → 𝑈 = ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 𝜓 } ) ) |