Metamath Proof Explorer

Theorem lubprop

Description: Properties of greatest lower bound of a poset. (Contributed by NM, 22-Oct-2011) (Revised by NM, 7-Sep-2018)

Ref Expression
Hypotheses lubprop.b ⊢B=BaseK
lubprop.l ⊢≤˙=≤K
lubprop.u ⊢U=lub⁡K
lubprop.k ⊢φ→K∈V
lubprop.s ⊢φ→S∈dom⁡U
Assertion lubprop ⊢φ→∀y∈Sy≤˙U⁡S∧∀z∈B∀y∈Sy≤˙z→U⁡S≤˙z

Proof

Step Hyp Ref Expression
1 lubprop.b ⊢B=BaseK
2 lubprop.l ⊢≤˙=≤K
3 lubprop.u ⊢U=lub⁡K
4 lubprop.k ⊢φ→K∈V
5 lubprop.s ⊢φ→S∈dom⁡U
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 4 5 lubelss ⊢φ→S⊆B
8 1 2 3 6 4 7 lubval ⊢φ→U⁡S=ιx∈B|∀y∈Sy≤˙x∧∀z∈B∀y∈Sy≤˙z→x≤˙z
9 8 eqcomd ⊢φ→ιx∈B|∀y∈Sy≤˙x∧∀z∈B∀y∈Sy≤˙z→x≤˙z=U⁡S
10 1 3 4 5 lubcl ⊢φ→U⁡S∈B
11 1 2 3 6 4 5 lubeu ⊢φ→∃!x∈B∀y∈Sy≤˙x∧∀z∈B∀y∈Sy≤˙z→x≤˙z
12 breq2 ⊢x=U⁡S→y≤˙x↔y≤˙U⁡S
13 12 ralbidv ⊢x=U⁡S→∀y∈Sy≤˙x↔∀y∈Sy≤˙U⁡S
14 breq1 ⊢x=U⁡S→x≤˙z↔U⁡S≤˙z
15 14 imbi2d ⊢x=U⁡S→∀y∈Sy≤˙z→x≤˙z↔∀y∈Sy≤˙z→U⁡S≤˙z
16 15 ralbidv ⊢x=U⁡S→∀z∈B∀y∈Sy≤˙z→x≤˙z↔∀z∈B∀y∈Sy≤˙z→U⁡S≤˙z
17 13 16 anbi12d ⊢x=U⁡S→∀y∈Sy≤˙x∧∀z∈B∀y∈Sy≤˙z→x≤˙z↔∀y∈Sy≤˙U⁡S∧∀z∈B∀y∈Sy≤˙z→U⁡S≤˙z
18 17 riota2 ⊢U⁡S∈B∧∃!x∈B∀y∈Sy≤˙x∧∀z∈B∀y∈Sy≤˙z→x≤˙z→∀y∈Sy≤˙U⁡S∧∀z∈B∀y∈Sy≤˙z→U⁡S≤˙z↔ιx∈B|∀y∈Sy≤˙x∧∀z∈B∀y∈Sy≤˙z→x≤˙z=U⁡S
19 10 11 18 syl2anc ⊢φ→∀y∈Sy≤˙U⁡S∧∀z∈B∀y∈Sy≤˙z→U⁡S≤˙z↔ιx∈B|∀y∈Sy≤˙x∧∀z∈B∀y∈Sy≤˙z→x≤˙z=U⁡S
20 9 19 mpbird ⊢φ→∀y∈Sy≤˙U⁡S∧∀z∈B∀y∈Sy≤˙z→U⁡S≤˙z