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 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇 ) → ( 𝑈 ‘ 𝑆 ) ≤ ( 𝑈 ‘ 𝑇 ) )