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

Metamath Proof Explorer

Theorem clatleglb

Description: Two ways of expressing "less than or equal to the greatest lower bound." (Contributed by NM, 5-Dec-2011)

Ref Expression
Hypotheses clatglb.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
clatglb.l ⊢ ≤ = ( le ‘ 𝐾 )
clatglb.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
Assertion clatleglb ( ( 𝐾 ∈ CLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑋 ≤ ( 𝐺 ‘ 𝑆 ) ↔ ∀ 𝑦 ∈ 𝑆 𝑋 ≤ 𝑦 ) )

Proof

Step Hyp Ref Expression
1 clatglb.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 clatglb.l ⊢ ≤ = ( le ‘ 𝐾 )
3 clatglb.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
4 1 2 3 clatglble ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑦 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑆 ) ≤ 𝑦 )
5 4 3expa ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑆 ) ≤ 𝑦 )
6 5 3adantl2 ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑆 ) ≤ 𝑦 )
7 simpl1 ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑆 ) → 𝐾 ∈ CLat )
8 clatl ⊢ ( 𝐾 ∈ CLat → 𝐾 ∈ Lat )
9 7 8 syl ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑆 ) → 𝐾 ∈ Lat )
10 simpl2 ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑆 ) → 𝑋 ∈ 𝐵 )
11 1 3 clatglbcl ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 )
12 11 3adant2 ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵 ) → ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 )
13 12 adantr ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 )
14 ssel ⊢ ( 𝑆 ⊆ 𝐵 → ( 𝑦 ∈ 𝑆 → 𝑦 ∈ 𝐵 ) )
15 14 3ad2ant3 ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑦 ∈ 𝑆 → 𝑦 ∈ 𝐵 ) )
16 15 imp ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ 𝐵 )
17 1 2 lattr ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑋 ≤ ( 𝐺 ‘ 𝑆 ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑦 ) → 𝑋 ≤ 𝑦 ) )
18 9 10 13 16 17 syl13anc ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑋 ≤ ( 𝐺 ‘ 𝑆 ) ∧ ( 𝐺 ‘ 𝑆 ) ≤ 𝑦 ) → 𝑋 ≤ 𝑦 ) )
19 6 18 mpan2d ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝑋 ≤ ( 𝐺 ‘ 𝑆 ) → 𝑋 ≤ 𝑦 ) )
20 19 ralrimdva ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑋 ≤ ( 𝐺 ‘ 𝑆 ) → ∀ 𝑦 ∈ 𝑆 𝑋 ≤ 𝑦 ) )
21 1 2 3 clatglb ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → ( ∀ 𝑦 ∈ 𝑆 ( 𝐺 ‘ 𝑆 ) ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ ( 𝐺 ‘ 𝑆 ) ) ) )
22 breq1 ⊢ ( 𝑧 = 𝑋 → ( 𝑧 ≤ 𝑦 ↔ 𝑋 ≤ 𝑦 ) )
23 22 ralbidv ⊢ ( 𝑧 = 𝑋 → ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 ↔ ∀ 𝑦 ∈ 𝑆 𝑋 ≤ 𝑦 ) )
24 breq1 ⊢ ( 𝑧 = 𝑋 → ( 𝑧 ≤ ( 𝐺 ‘ 𝑆 ) ↔ 𝑋 ≤ ( 𝐺 ‘ 𝑆 ) ) )
25 23 24 imbi12d ⊢ ( 𝑧 = 𝑋 → ( ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ ( 𝐺 ‘ 𝑆 ) ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑋 ≤ 𝑦 → 𝑋 ≤ ( 𝐺 ‘ 𝑆 ) ) ) )
26 25 rspccv ⊢ ( ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ ( 𝐺 ‘ 𝑆 ) ) → ( 𝑋 ∈ 𝐵 → ( ∀ 𝑦 ∈ 𝑆 𝑋 ≤ 𝑦 → 𝑋 ≤ ( 𝐺 ‘ 𝑆 ) ) ) )
27 21 26 simpl2im ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑋 ∈ 𝐵 → ( ∀ 𝑦 ∈ 𝑆 𝑋 ≤ 𝑦 → 𝑋 ≤ ( 𝐺 ‘ 𝑆 ) ) ) )
28 27 ex ⊢ ( 𝐾 ∈ CLat → ( 𝑆 ⊆ 𝐵 → ( 𝑋 ∈ 𝐵 → ( ∀ 𝑦 ∈ 𝑆 𝑋 ≤ 𝑦 → 𝑋 ≤ ( 𝐺 ‘ 𝑆 ) ) ) ) )
29 28 com23 ⊢ ( 𝐾 ∈ CLat → ( 𝑋 ∈ 𝐵 → ( 𝑆 ⊆ 𝐵 → ( ∀ 𝑦 ∈ 𝑆 𝑋 ≤ 𝑦 → 𝑋 ≤ ( 𝐺 ‘ 𝑆 ) ) ) ) )
30 29 3imp ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵 ) → ( ∀ 𝑦 ∈ 𝑆 𝑋 ≤ 𝑦 → 𝑋 ≤ ( 𝐺 ‘ 𝑆 ) ) )
31 20 30 impbid ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑋 ≤ ( 𝐺 ‘ 𝑆 ) ↔ ∀ 𝑦 ∈ 𝑆 𝑋 ≤ 𝑦 ) )