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

Metamath Proof Explorer

Theorem isglbd

Description: Properties that determine the greatest lower bound of a complete lattice. (Contributed by Mario Carneiro, 19-Mar-2014)

Ref Expression
Hypotheses isglbd.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
isglbd.l ⊢ ≤ = ( le ‘ 𝐾 )
isglbd.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
isglbd.1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝐻 ≤ 𝑦 )
isglbd.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) → 𝑥 ≤ 𝐻 )
isglbd.3 ⊢ ( 𝜑 → 𝐾 ∈ CLat )
isglbd.4 ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
isglbd.5 ⊢ ( 𝜑 → 𝐻 ∈ 𝐵 )
Assertion isglbd ( 𝜑 → ( 𝐺 ‘ 𝑆 ) = 𝐻 )

Proof

Step Hyp Ref Expression
1 isglbd.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 isglbd.l ⊢ ≤ = ( le ‘ 𝐾 )
3 isglbd.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
4 isglbd.1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝐻 ≤ 𝑦 )
5 isglbd.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ) → 𝑥 ≤ 𝐻 )
6 isglbd.3 ⊢ ( 𝜑 → 𝐾 ∈ CLat )
7 isglbd.4 ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
8 isglbd.5 ⊢ ( 𝜑 → 𝐻 ∈ 𝐵 )
9 biid ⊢ ( ( ∀ 𝑦 ∈ 𝑆 ℎ ≤ 𝑦 ∧ ∀ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑥 ≤ ℎ ) ) ↔ ( ∀ 𝑦 ∈ 𝑆 ℎ ≤ 𝑦 ∧ ∀ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑥 ≤ ℎ ) ) )
10 1 2 3 9 6 7 glbval ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑆 ) = ( ℩ ℎ ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 ℎ ≤ 𝑦 ∧ ∀ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑥 ≤ ℎ ) ) ) )
11 4 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑆 𝐻 ≤ 𝑦 )
12 5 3exp ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 → ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑥 ≤ 𝐻 ) ) )
13 12 ralrimiv ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑥 ≤ 𝐻 ) )
14 1 3 clatglbcl2 ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → 𝑆 ∈ dom 𝐺 )
15 6 7 14 syl2anc ⊢ ( 𝜑 → 𝑆 ∈ dom 𝐺 )
16 1 2 3 9 6 15 glbeu ⊢ ( 𝜑 → ∃! ℎ ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 ℎ ≤ 𝑦 ∧ ∀ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑥 ≤ ℎ ) ) )
17 breq1 ⊢ ( ℎ = 𝐻 → ( ℎ ≤ 𝑦 ↔ 𝐻 ≤ 𝑦 ) )
18 17 ralbidv ⊢ ( ℎ = 𝐻 → ( ∀ 𝑦 ∈ 𝑆 ℎ ≤ 𝑦 ↔ ∀ 𝑦 ∈ 𝑆 𝐻 ≤ 𝑦 ) )
19 breq2 ⊢ ( ℎ = 𝐻 → ( 𝑥 ≤ ℎ ↔ 𝑥 ≤ 𝐻 ) )
20 19 imbi2d ⊢ ( ℎ = 𝐻 → ( ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑥 ≤ ℎ ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑥 ≤ 𝐻 ) ) )
21 20 ralbidv ⊢ ( ℎ = 𝐻 → ( ∀ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑥 ≤ ℎ ) ↔ ∀ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑥 ≤ 𝐻 ) ) )
22 18 21 anbi12d ⊢ ( ℎ = 𝐻 → ( ( ∀ 𝑦 ∈ 𝑆 ℎ ≤ 𝑦 ∧ ∀ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑥 ≤ ℎ ) ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝐻 ≤ 𝑦 ∧ ∀ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑥 ≤ 𝐻 ) ) ) )
23 22 riota2 ⊢ ( ( 𝐻 ∈ 𝐵 ∧ ∃! ℎ ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 ℎ ≤ 𝑦 ∧ ∀ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑥 ≤ ℎ ) ) ) → ( ( ∀ 𝑦 ∈ 𝑆 𝐻 ≤ 𝑦 ∧ ∀ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑥 ≤ 𝐻 ) ) ↔ ( ℩ ℎ ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 ℎ ≤ 𝑦 ∧ ∀ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑥 ≤ ℎ ) ) ) = 𝐻 ) )
24 8 16 23 syl2anc ⊢ ( 𝜑 → ( ( ∀ 𝑦 ∈ 𝑆 𝐻 ≤ 𝑦 ∧ ∀ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑥 ≤ 𝐻 ) ) ↔ ( ℩ ℎ ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 ℎ ≤ 𝑦 ∧ ∀ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑥 ≤ ℎ ) ) ) = 𝐻 ) )
25 11 13 24 mpbi2and ⊢ ( 𝜑 → ( ℩ ℎ ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 ℎ ≤ 𝑦 ∧ ∀ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 → 𝑥 ≤ ℎ ) ) ) = 𝐻 )
26 10 25 eqtrd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑆 ) = 𝐻 )