Metamath Proof Explorer

Theorem lubfval

Description: Value of the least upper bound function of a poset. (Contributed by NM, 12-Sep-2011) (Revised by NM, 6-Sep-2018)

Ref Expression
Hypotheses lubfval.b ⊢B=BaseK
lubfval.l ⊢≤˙=≤K
lubfval.u ⊢U=lub⁡K
lubfval.p ⊢ψ↔∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z
lubfval.k ⊢φ→K∈V
Assertion lubfval ⊢φ→U=s∈𝒫B⟼ιx∈B|ψ↾s|∃!x∈Bψ

Proof

Step Hyp Ref Expression
1 lubfval.b ⊢B=BaseK
2 lubfval.l ⊢≤˙=≤K
3 lubfval.u ⊢U=lub⁡K
4 lubfval.p ⊢ψ↔∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z
5 lubfval.k ⊢φ→K∈V
6 elex ⊢K∈V→K∈V
7 fveq2 ⊢p=K→Basep=BaseK
8 7 1 eqtr4di ⊢p=K→Basep=B
9 8 pweqd ⊢p=K→𝒫Basep=𝒫B
10 fveq2 ⊢p=K→≤p=≤K
11 10 2 eqtr4di ⊢p=K→≤p=≤˙
12 11 breqd ⊢p=K→y≤px↔y≤˙x
13 12 ralbidv ⊢p=K→∀y∈sy≤px↔∀y∈sy≤˙x
14 11 breqd ⊢p=K→y≤pz↔y≤˙z
15 14 ralbidv ⊢p=K→∀y∈sy≤pz↔∀y∈sy≤˙z
16 11 breqd ⊢p=K→x≤pz↔x≤˙z
17 15 16 imbi12d ⊢p=K→∀y∈sy≤pz→x≤pz↔∀y∈sy≤˙z→x≤˙z
18 8 17 raleqbidv ⊢p=K→∀z∈Basep∀y∈sy≤pz→x≤pz↔∀z∈B∀y∈sy≤˙z→x≤˙z
19 13 18 anbi12d ⊢p=K→∀y∈sy≤px∧∀z∈Basep∀y∈sy≤pz→x≤pz↔∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z
20 8 19 riotaeqbidv ⊢p=K→ιx∈Basep|∀y∈sy≤px∧∀z∈Basep∀y∈sy≤pz→x≤pz=ιx∈B|∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z
21 9 20 mpteq12dv ⊢p=K→s∈𝒫Basep⟼ιx∈Basep|∀y∈sy≤px∧∀z∈Basep∀y∈sy≤pz→x≤pz=s∈𝒫B⟼ιx∈B|∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z
22 19 reubidv ⊢p=K→∃!x∈Basep∀y∈sy≤px∧∀z∈Basep∀y∈sy≤pz→x≤pz↔∃!x∈Basep∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z
23 reueq1 ⊢Basep=B→∃!x∈Basep∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z↔∃!x∈B∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z
24 8 23 syl ⊢p=K→∃!x∈Basep∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z↔∃!x∈B∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z
25 22 24 bitrd ⊢p=K→∃!x∈Basep∀y∈sy≤px∧∀z∈Basep∀y∈sy≤pz→x≤pz↔∃!x∈B∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z
26 25 abbidv ⊢p=K→s|∃!x∈Basep∀y∈sy≤px∧∀z∈Basep∀y∈sy≤pz→x≤pz=s|∃!x∈B∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z
27 21 26 reseq12d ⊢p=K→s∈𝒫Basep⟼ιx∈Basep|∀y∈sy≤px∧∀z∈Basep∀y∈sy≤pz→x≤pz↾s|∃!x∈Basep∀y∈sy≤px∧∀z∈Basep∀y∈sy≤pz→x≤pz=s∈𝒫B⟼ιx∈B|∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z↾s|∃!x∈B∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z
28 df-lub ⊢lub=p∈V⟼s∈𝒫Basep⟼ιx∈Basep|∀y∈sy≤px∧∀z∈Basep∀y∈sy≤pz→x≤pz↾s|∃!x∈Basep∀y∈sy≤px∧∀z∈Basep∀y∈sy≤pz→x≤pz
29 1 fvexi ⊢B∈V
30 29 pwex ⊢𝒫B∈V
31 30 mptex ⊢s∈𝒫B⟼ιx∈B|∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z∈V
32 31 resex ⊢s∈𝒫B⟼ιx∈B|∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z↾s|∃!x∈B∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z∈V
33 27 28 32 fvmpt ⊢K∈V→lub⁡K=s∈𝒫B⟼ιx∈B|∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z↾s|∃!x∈B∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z
34 4 a1i ⊢x∈B→ψ↔∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z
35 34 riotabiia ⊢ιx∈B|ψ=ιx∈B|∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z
36 35 mpteq2i ⊢s∈𝒫B⟼ιx∈B|ψ=s∈𝒫B⟼ιx∈B|∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z
37 4 reubii ⊢∃!x∈Bψ↔∃!x∈B∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z
38 37 abbii ⊢s|∃!x∈Bψ=s|∃!x∈B∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z
39 36 38 reseq12i ⊢s∈𝒫B⟼ιx∈B|ψ↾s|∃!x∈Bψ=s∈𝒫B⟼ιx∈B|∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z↾s|∃!x∈B∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z
40 33 3 39 3eqtr4g ⊢K∈V→U=s∈𝒫B⟼ιx∈B|ψ↾s|∃!x∈Bψ
41 5 6 40 3syl ⊢φ→U=s∈𝒫B⟼ιx∈B|ψ↾s|∃!x∈Bψ