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 = Base K
lubprop.l ⊢ ≤ ˙ = ≤ K
lubprop.u ⊢ U = lub ⁡ K
lubprop.k ⊢ φ → K ∈ V
lubprop.s ⊢ φ → S ∈ dom ⁡ U
Assertion lubprop ⊢ φ → ∀ y ∈ S y ≤ ˙ U ⁡ S ∧ ∀ z ∈ B ∀ y ∈ S y ≤ ˙ z → U ⁡ S ≤ ˙ z

Proof

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