Metamath Proof Explorer

Theorem glbeldm

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

Ref Expression
Hypotheses glbeldm.b ⊢B=BaseK
glbeldm.l ⊢≤˙=≤K
glbeldm.g ⊢G=glb⁡K
glbeldm.p ⊢ψ↔∀y∈Sx≤˙y∧∀z∈B∀y∈Sz≤˙y→z≤˙x
glbeldm.k ⊢φ→K∈V
Assertion glbeldm ⊢φ→S∈dom⁡G↔S⊆B∧∃!x∈Bψ

Proof

Step Hyp Ref Expression
1 glbeldm.b ⊢B=BaseK
2 glbeldm.l ⊢≤˙=≤K
3 glbeldm.g ⊢G=glb⁡K
4 glbeldm.p ⊢ψ↔∀y∈Sx≤˙y∧∀z∈B∀y∈Sz≤˙y→z≤˙x
5 glbeldm.k ⊢φ→K∈V
6 biid ⊢∀y∈sx≤˙y∧∀z∈B∀y∈sz≤˙y→z≤˙x↔∀y∈sx≤˙y∧∀z∈B∀y∈sz≤˙y→z≤˙x
7 1 2 3 6 5 glbdm ⊢φ→dom⁡G=s∈𝒫B|∃!x∈B∀y∈sx≤˙y∧∀z∈B∀y∈sz≤˙y→z≤˙x
8 7 eleq2d ⊢φ→S∈dom⁡G↔S∈s∈𝒫B|∃!x∈B∀y∈sx≤˙y∧∀z∈B∀y∈sz≤˙y→z≤˙x
9 raleq ⊢s=S→∀y∈sx≤˙y↔∀y∈Sx≤˙y
10 raleq ⊢s=S→∀y∈sz≤˙y↔∀y∈Sz≤˙y
11 10 imbi1d ⊢s=S→∀y∈sz≤˙y→z≤˙x↔∀y∈Sz≤˙y→z≤˙x
12 11 ralbidv ⊢s=S→∀z∈B∀y∈sz≤˙y→z≤˙x↔∀z∈B∀y∈Sz≤˙y→z≤˙x
13 9 12 anbi12d ⊢s=S→∀y∈sx≤˙y∧∀z∈B∀y∈sz≤˙y→z≤˙x↔∀y∈Sx≤˙y∧∀z∈B∀y∈Sz≤˙y→z≤˙x
14 13 reubidv ⊢s=S→∃!x∈B∀y∈sx≤˙y∧∀z∈B∀y∈sz≤˙y→z≤˙x↔∃!x∈B∀y∈Sx≤˙y∧∀z∈B∀y∈Sz≤˙y→z≤˙x
15 4 reubii ⊢∃!x∈Bψ↔∃!x∈B∀y∈Sx≤˙y∧∀z∈B∀y∈Sz≤˙y→z≤˙x
16 14 15 bitr4di ⊢s=S→∃!x∈B∀y∈sx≤˙y∧∀z∈B∀y∈sz≤˙y→z≤˙x↔∃!x∈Bψ
17 16 elrab ⊢S∈s∈𝒫B|∃!x∈B∀y∈sx≤˙y∧∀z∈B∀y∈sz≤˙y→z≤˙x↔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∈sx≤˙y∧∀z∈B∀y∈sz≤˙y→z≤˙x↔S⊆B∧∃!x∈Bψ
22 8 21 bitrdi ⊢φ→S∈dom⁡G↔S⊆B∧∃!x∈Bψ