Step |
Hyp |
Ref |
Expression |
1 |
|
glbeldm.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
2 |
|
glbeldm.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
3 |
|
glbeldm.g |
⊢ 𝐺 = ( glb ‘ 𝐾 ) |
4 |
|
glbeldm.p |
⊢ ( 𝜓 ↔ ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) |
5 |
|
glbeldm.k |
⊢ ( 𝜑 → 𝐾 ∈ 𝑉 ) |
6 |
|
biid |
⊢ ( ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) |
7 |
1 2 3 6 5
|
glbdm |
⊢ ( 𝜑 → dom 𝐺 = { 𝑠 ∈ 𝒫 𝐵 ∣ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) } ) |
8 |
7
|
eleq2d |
⊢ ( 𝜑 → ( 𝑆 ∈ dom 𝐺 ↔ 𝑆 ∈ { 𝑠 ∈ 𝒫 𝐵 ∣ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) } ) ) |
9 |
|
raleq |
⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ↔ ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) ) |
10 |
|
raleq |
⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 ↔ ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 ) ) |
11 |
10
|
imbi1d |
⊢ ( 𝑠 = 𝑆 → ( ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) |
12 |
11
|
ralbidv |
⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ↔ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) |
13 |
9 12
|
anbi12d |
⊢ ( 𝑠 = 𝑆 → ( ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) ) |
14 |
13
|
reubidv |
⊢ ( 𝑠 = 𝑆 → ( ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ↔ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) ) |
15 |
4
|
reubii |
⊢ ( ∃! 𝑥 ∈ 𝐵 𝜓 ↔ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) |
16 |
14 15
|
bitr4di |
⊢ ( 𝑠 = 𝑆 → ( ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ↔ ∃! 𝑥 ∈ 𝐵 𝜓 ) ) |
17 |
16
|
elrab |
⊢ ( 𝑆 ∈ { 𝑠 ∈ 𝒫 𝐵 ∣ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) } ↔ ( 𝑆 ∈ 𝒫 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) ) |
18 |
1
|
fvexi |
⊢ 𝐵 ∈ V |
19 |
18
|
elpw2 |
⊢ ( 𝑆 ∈ 𝒫 𝐵 ↔ 𝑆 ⊆ 𝐵 ) |
20 |
19
|
anbi1i |
⊢ ( ( 𝑆 ∈ 𝒫 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) ↔ ( 𝑆 ⊆ 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) ) |
21 |
17 20
|
bitri |
⊢ ( 𝑆 ∈ { 𝑠 ∈ 𝒫 𝐵 ∣ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) } ↔ ( 𝑆 ⊆ 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) ) |
22 |
8 21
|
bitrdi |
⊢ ( 𝜑 → ( 𝑆 ∈ dom 𝐺 ↔ ( 𝑆 ⊆ 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) ) ) |