Metamath Proof Explorer


Theorem lubval

Description: Value of the least upper 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. (Contributed by NM, 12-Sep-2011) (Revised by NM, 9-Sep-2018)

Ref Expression
Hypotheses lubval.b B = Base K
lubval.l ˙ = K
lubval.u U = lub K
lubval.p ψ y S y ˙ x z B y S y ˙ z x ˙ z
lubval.k φ K V
lubval.s φ S B
Assertion lubval φ U S = ι x B | ψ

Proof

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