Metamath Proof Explorer


Theorem glbval

Description: Value of the greatest lower bound function of a poset. Out-of-domain arguments (those not satisfying S e. dom U ) are allowed for convenience, evaluating to the empty set on both sides of the equality. (Contributed by NM, 12-Sep-2011) (Revised by NM, 9-Sep-2018)

Ref Expression
Hypotheses glbval.b B = Base K
glbval.l ˙ = K
glbval.g G = glb K
glbval.p ψ y S x ˙ y z B y S z ˙ y z ˙ x
glbva.k φ K V
glbval.ss φ S B
Assertion glbval φ G S = ι x B | ψ

Proof

Step Hyp Ref Expression
1 glbval.b B = Base K
2 glbval.l ˙ = K
3 glbval.g G = glb K
4 glbval.p ψ y S x ˙ y z B y S z ˙ y z ˙ x
5 glbva.k φ K V
6 glbval.ss φ S B
7 biid y s x ˙ y z B y s z ˙ y z ˙ x y s x ˙ y z B y s z ˙ y z ˙ x
8 5 adantr φ S dom G K V
9 1 2 3 7 8 glbfval φ S dom G G = s 𝒫 B ι x B | y s x ˙ y z B y s z ˙ y z ˙ x s | ∃! x B y s x ˙ y z B y s z ˙ y z ˙ x
10 9 fveq1d φ S dom G G S = s 𝒫 B ι x B | y s x ˙ y z B y s z ˙ y z ˙ x s | ∃! x B y s x ˙ y z B y s z ˙ y z ˙ x S
11 simpr φ S dom G S dom G
12 1 2 3 4 8 11 glbeu φ S dom G ∃! x B ψ
13 raleq s = S y s x ˙ y y S x ˙ y
14 raleq s = S y s z ˙ y y S z ˙ y
15 14 imbi1d s = S y s z ˙ y z ˙ x y S z ˙ y z ˙ x
16 15 ralbidv s = S z B y s z ˙ y z ˙ x z B y S z ˙ y z ˙ x
17 13 16 anbi12d s = S y s x ˙ y z B y s z ˙ y z ˙ x y S x ˙ y z B y S z ˙ y z ˙ x
18 17 4 bitr4di s = S y s x ˙ y z B y s z ˙ y z ˙ x ψ
19 18 reubidv s = S ∃! x B y s x ˙ y z B y s z ˙ y z ˙ x ∃! x B ψ
20 11 12 19 elabd φ S dom G S s | ∃! x B y s x ˙ y z B y s z ˙ y z ˙ x
21 20 fvresd φ S dom G s 𝒫 B ι x B | y s x ˙ y z B y s z ˙ y z ˙ x s | ∃! x B y s x ˙ y z B y s z ˙ y z ˙ x S = s 𝒫 B ι x B | y s x ˙ y z B y s z ˙ y z ˙ x S
22 6 adantr φ S dom G S B
23 1 fvexi B V
24 23 elpw2 S 𝒫 B S B
25 22 24 sylibr φ S dom G S 𝒫 B
26 18 riotabidv s = S ι x B | y s x ˙ y z B y s z ˙ y z ˙ x = ι x B | ψ
27 eqid s 𝒫 B ι x B | y s x ˙ y z B y s z ˙ y z ˙ x = s 𝒫 B ι x B | y s x ˙ y z B y s z ˙ y z ˙ x
28 riotaex ι x B | ψ V
29 26 27 28 fvmpt S 𝒫 B s 𝒫 B ι x B | y s x ˙ y z B y s z ˙ y z ˙ x S = ι x B | ψ
30 25 29 syl φ S dom G s 𝒫 B ι x B | y s x ˙ y z B y s z ˙ y z ˙ x S = ι x B | ψ
31 10 21 30 3eqtrd φ S dom G G S = ι x B | ψ
32 ndmfv ¬ S dom G G S =
33 32 adantl φ ¬ S dom G G S =
34 1 2 3 4 5 glbeldm φ S dom G S B ∃! x B ψ
35 34 biimprd φ S B ∃! x B ψ S dom G
36 6 35 mpand φ ∃! x B ψ S dom G
37 36 con3dimp φ ¬ S dom G ¬ ∃! x B ψ
38 riotaund ¬ ∃! x B ψ ι x B | ψ =
39 37 38 syl φ ¬ S dom G ι x B | ψ =
40 33 39 eqtr4d φ ¬ S dom G G S = ι x B | ψ
41 31 40 pm2.61dan φ G S = ι x B | ψ