This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem glbprop

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

Ref Expression
Hypotheses glbprop.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
glbprop.l ⊢ ≤ = ( le ‘ 𝐾 )
glbprop.u ⊢ 𝑈 = ( glb ‘ 𝐾 )
glbprop.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
glbprop.s ⊢ ( 𝜑 → 𝑆 ∈ dom 𝑈 )
Assertion glbprop ( 𝜑 → ( ∀ 𝑦 ∈ 𝑆 ( 𝑈 ‘ 𝑆 ) ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ ( 𝑈 ‘ 𝑆 ) ) ) )

Proof

Step Hyp Ref Expression
1 glbprop.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 glbprop.l ⊢ ≤ = ( le ‘ 𝐾 )
3 glbprop.u ⊢ 𝑈 = ( glb ‘ 𝐾 )
4 glbprop.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
5 glbprop.s ⊢ ( 𝜑 → 𝑆 ∈ dom 𝑈 )
6 biid ⊢ ( ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) )
7 1 2 3 4 5 glbelss ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
8 1 2 3 6 4 7 glbval ⊢ ( 𝜑 → ( 𝑈 ‘ 𝑆 ) = ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) )
9 8 eqcomd ⊢ ( 𝜑 → ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) = ( 𝑈 ‘ 𝑆 ) )
10 1 3 4 5 glbcl ⊢ ( 𝜑 → ( 𝑈 ‘ 𝑆 ) ∈ 𝐵 )
11 1 2 3 6 4 5 glbeu ⊢ ( 𝜑 → ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) )
12 breq1 ⊢ ( 𝑥 = ( 𝑈 ‘ 𝑆 ) → ( 𝑥 ≤ 𝑦 ↔ ( 𝑈 ‘ 𝑆 ) ≤ 𝑦 ) )
13 12 ralbidv ⊢ ( 𝑥 = ( 𝑈 ‘ 𝑆 ) → ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ↔ ∀ 𝑦 ∈ 𝑆 ( 𝑈 ‘ 𝑆 ) ≤ 𝑦 ) )
14 breq2 ⊢ ( 𝑥 = ( 𝑈 ‘ 𝑆 ) → ( 𝑧 ≤ 𝑥 ↔ 𝑧 ≤ ( 𝑈 ‘ 𝑆 ) ) )
15 14 imbi2d ⊢ ( 𝑥 = ( 𝑈 ‘ 𝑆 ) → ( ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ ( 𝑈 ‘ 𝑆 ) ) ) )
16 15 ralbidv ⊢ ( 𝑥 = ( 𝑈 ‘ 𝑆 ) → ( ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ↔ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ ( 𝑈 ‘ 𝑆 ) ) ) )
17 13 16 anbi12d ⊢ ( 𝑥 = ( 𝑈 ‘ 𝑆 ) → ( ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ 𝑆 ( 𝑈 ‘ 𝑆 ) ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ ( 𝑈 ‘ 𝑆 ) ) ) ) )
18 17 riota2 ⊢ ( ( ( 𝑈 ‘ 𝑆 ) ∈ 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) → ( ( ∀ 𝑦 ∈ 𝑆 ( 𝑈 ‘ 𝑆 ) ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ ( 𝑈 ‘ 𝑆 ) ) ) ↔ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) = ( 𝑈 ‘ 𝑆 ) ) )
19 10 11 18 syl2anc ⊢ ( 𝜑 → ( ( ∀ 𝑦 ∈ 𝑆 ( 𝑈 ‘ 𝑆 ) ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ ( 𝑈 ‘ 𝑆 ) ) ) ↔ ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) = ( 𝑈 ‘ 𝑆 ) ) )
20 9 19 mpbird ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝑆 ( 𝑈 ‘ 𝑆 ) ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ ( 𝑈 ‘ 𝑆 ) ) ) )