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

Metamath Proof Explorer

Theorem lubss

Description: Subset law for least upper bounds. ( chsupss analog.) (Contributed by NM, 20-Oct-2011)

Ref Expression
Hypotheses lublem.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
lublem.l ⊢ ≤ = ( le ‘ 𝐾 )
lublem.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
Assertion lubss ( ( 𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇 ) → ( 𝑈 ‘ 𝑆 ) ≤ ( 𝑈 ‘ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 lublem.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lublem.l ⊢ ≤ = ( le ‘ 𝐾 )
3 lublem.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
4 simp1 ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇 ) → 𝐾 ∈ CLat )
5 sstr2 ⊢ ( 𝑆 ⊆ 𝑇 → ( 𝑇 ⊆ 𝐵 → 𝑆 ⊆ 𝐵 ) )
6 5 impcom ⊢ ( ( 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇 ) → 𝑆 ⊆ 𝐵 )
7 6 3adant1 ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇 ) → 𝑆 ⊆ 𝐵 )
8 1 3 clatlubcl ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ) → ( 𝑈 ‘ 𝑇 ) ∈ 𝐵 )
9 8 3adant3 ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇 ) → ( 𝑈 ‘ 𝑇 ) ∈ 𝐵 )
10 4 7 9 3jca ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇 ) → ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ ( 𝑈 ‘ 𝑇 ) ∈ 𝐵 ) )
11 simpl1 ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇 ) ∧ 𝑦 ∈ 𝑆 ) → 𝐾 ∈ CLat )
12 simpl2 ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇 ) ∧ 𝑦 ∈ 𝑆 ) → 𝑇 ⊆ 𝐵 )
13 ssel2 ⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ 𝑇 )
14 13 3ad2antl3 ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇 ) ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ 𝑇 )
15 1 2 3 lubub ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑦 ∈ 𝑇 ) → 𝑦 ≤ ( 𝑈 ‘ 𝑇 ) )
16 11 12 14 15 syl3anc ⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇 ) ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ≤ ( 𝑈 ‘ 𝑇 ) )
17 16 ralrimiva ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇 ) → ∀ 𝑦 ∈ 𝑆 𝑦 ≤ ( 𝑈 ‘ 𝑇 ) )
18 1 2 3 lubl ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ ( 𝑈 ‘ 𝑇 ) ∈ 𝐵 ) → ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ ( 𝑈 ‘ 𝑇 ) → ( 𝑈 ‘ 𝑆 ) ≤ ( 𝑈 ‘ 𝑇 ) ) )
19 10 17 18 sylc ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇 ) → ( 𝑈 ‘ 𝑆 ) ≤ ( 𝑈 ‘ 𝑇 ) )