Step |
Hyp |
Ref |
Expression |
1 |
|
lubprop.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
2 |
|
lubprop.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
3 |
|
lubprop.u |
⊢ 𝑈 = ( lub ‘ 𝐾 ) |
4 |
|
lubprop.k |
⊢ ( 𝜑 → 𝐾 ∈ 𝑉 ) |
5 |
|
lubprop.s |
⊢ ( 𝜑 → 𝑆 ∈ dom 𝑈 ) |
6 |
|
biid |
⊢ ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) |
7 |
1 2 3 4 5
|
lubelss |
⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 ) |
8 |
1 2 3 6 4 7
|
lubval |
⊢ ( 𝜑 → ( 𝑈 ‘ 𝑆 ) = ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) ) |
9 |
8
|
eqcomd |
⊢ ( 𝜑 → ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) = ( 𝑈 ‘ 𝑆 ) ) |
10 |
1 3 4 5
|
lubcl |
⊢ ( 𝜑 → ( 𝑈 ‘ 𝑆 ) ∈ 𝐵 ) |
11 |
1 2 3 6 4 5
|
lubeu |
⊢ ( 𝜑 → ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) |
12 |
|
breq2 |
⊢ ( 𝑥 = ( 𝑈 ‘ 𝑆 ) → ( 𝑦 ≤ 𝑥 ↔ 𝑦 ≤ ( 𝑈 ‘ 𝑆 ) ) ) |
13 |
12
|
ralbidv |
⊢ ( 𝑥 = ( 𝑈 ‘ 𝑆 ) → ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ↔ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ ( 𝑈 ‘ 𝑆 ) ) ) |
14 |
|
breq1 |
⊢ ( 𝑥 = ( 𝑈 ‘ 𝑆 ) → ( 𝑥 ≤ 𝑧 ↔ ( 𝑈 ‘ 𝑆 ) ≤ 𝑧 ) ) |
15 |
14
|
imbi2d |
⊢ ( 𝑥 = ( 𝑈 ‘ 𝑆 ) → ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → ( 𝑈 ‘ 𝑆 ) ≤ 𝑧 ) ) ) |
16 |
15
|
ralbidv |
⊢ ( 𝑥 = ( 𝑈 ‘ 𝑆 ) → ( ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ↔ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → ( 𝑈 ‘ 𝑆 ) ≤ 𝑧 ) ) ) |
17 |
13 16
|
anbi12d |
⊢ ( 𝑥 = ( 𝑈 ‘ 𝑆 ) → ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ ( 𝑈 ‘ 𝑆 ) ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → ( 𝑈 ‘ 𝑆 ) ≤ 𝑧 ) ) ) ) |
18 |
17
|
riota2 |
⊢ ( ( ( 𝑈 ‘ 𝑆 ) ∈ 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) → ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ ( 𝑈 ‘ 𝑆 ) ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → ( 𝑈 ‘ 𝑆 ) ≤ 𝑧 ) ) ↔ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) = ( 𝑈 ‘ 𝑆 ) ) ) |
19 |
10 11 18
|
syl2anc |
⊢ ( 𝜑 → ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ ( 𝑈 ‘ 𝑆 ) ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → ( 𝑈 ‘ 𝑆 ) ≤ 𝑧 ) ) ↔ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) = ( 𝑈 ‘ 𝑆 ) ) ) |
20 |
9 19
|
mpbird |
⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ ( 𝑈 ‘ 𝑆 ) ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → ( 𝑈 ‘ 𝑆 ) ≤ 𝑧 ) ) ) |