Metamath Proof Explorer

Theorem lubeldm

Description: Member of the domain of the least upper bound function of a poset. (Contributed by NM, 7-Sep-2018)

Ref Expression
Hypotheses lubeldm.b ⊢B=BaseK
lubeldm.l ⊢≤˙=≤K
lubeldm.u ⊢U=lub⁡K
lubeldm.p ⊢ψ↔∀y∈Sy≤˙x∧∀z∈B∀y∈Sy≤˙z→x≤˙z
lubeldm.k ⊢φ→K∈V
Assertion lubeldm ⊢φ→S∈dom⁡U↔S⊆B∧∃!x∈Bψ

Proof

Step Hyp Ref Expression
1 lubeldm.b ⊢B=BaseK
2 lubeldm.l ⊢≤˙=≤K
3 lubeldm.u ⊢U=lub⁡K
4 lubeldm.p ⊢ψ↔∀y∈Sy≤˙x∧∀z∈B∀y∈Sy≤˙z→x≤˙z
5 lubeldm.k ⊢φ→K∈V
6 biid ⊢∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z↔∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z
7 1 2 3 6 5 lubdm ⊢φ→dom⁡U=s∈𝒫B|∃!x∈B∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z
8 7 eleq2d ⊢φ→S∈dom⁡U↔S∈s∈𝒫B|∃!x∈B∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z
9 raleq ⊢s=S→∀y∈sy≤˙x↔∀y∈Sy≤˙x
10 raleq ⊢s=S→∀y∈sy≤˙z↔∀y∈Sy≤˙z
11 10 imbi1d ⊢s=S→∀y∈sy≤˙z→x≤˙z↔∀y∈Sy≤˙z→x≤˙z
12 11 ralbidv ⊢s=S→∀z∈B∀y∈sy≤˙z→x≤˙z↔∀z∈B∀y∈Sy≤˙z→x≤˙z
13 9 12 anbi12d ⊢s=S→∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z↔∀y∈Sy≤˙x∧∀z∈B∀y∈Sy≤˙z→x≤˙z
14 13 reubidv ⊢s=S→∃!x∈B∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z↔∃!x∈B∀y∈Sy≤˙x∧∀z∈B∀y∈Sy≤˙z→x≤˙z
15 4 reubii ⊢∃!x∈Bψ↔∃!x∈B∀y∈Sy≤˙x∧∀z∈B∀y∈Sy≤˙z→x≤˙z
16 14 15 bitr4di ⊢s=S→∃!x∈B∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z↔∃!x∈Bψ
17 16 elrab ⊢S∈s∈𝒫B|∃!x∈B∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z↔S∈𝒫B∧∃!x∈Bψ
18 1 fvexi ⊢B∈V
19 18 elpw2 ⊢S∈𝒫B↔S⊆B
20 19 anbi1i ⊢S∈𝒫B∧∃!x∈Bψ↔S⊆B∧∃!x∈Bψ
21 17 20 bitri ⊢S∈s∈𝒫B|∃!x∈B∀y∈sy≤˙x∧∀z∈B∀y∈sy≤˙z→x≤˙z↔S⊆B∧∃!x∈Bψ
22 8 21 bitrdi ⊢φ→S∈dom⁡U↔S⊆B∧∃!x∈Bψ