Theorem clatlem

Description: Lemma for properties of a complete lattice. (Contributed by NM, 14-Sep-2011)

	Ref	Expression
Hypotheses	clatlem.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	clatlem.u	⊢ 𝑈 = ( lub ‘ 𝐾 )
	clatlem.g	⊢ 𝐺 = ( glb ‘ 𝐾 )
Assertion	clatlem	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → ( ( 𝑈 ‘ 𝑆 ) ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		clatlem.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		clatlem.u	⊢ 𝑈 = ( lub ‘ 𝐾 )
3		clatlem.g	⊢ 𝐺 = ( glb ‘ 𝐾 )
4		simpl	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → 𝐾 ∈ CLat )
5	1	fvexi	⊢ 𝐵 ∈ V
6	5	elpw2	⊢ ( 𝑆 ∈ 𝒫 𝐵 ↔ 𝑆 ⊆ 𝐵 )
7	6	bilanri	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → 𝑆 ∈ 𝒫 𝐵 )
8	1 2 3	isclat	⊢ ( 𝐾 ∈ CLat ↔ ( 𝐾 ∈ Poset ∧ ( dom 𝑈 = 𝒫 𝐵 ∧ dom 𝐺 = 𝒫 𝐵 ) ) )
9	8	birani	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → ( 𝐾 ∈ Poset ∧ ( dom 𝑈 = 𝒫 𝐵 ∧ dom 𝐺 = 𝒫 𝐵 ) ) )
10	9	simprld	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → dom 𝑈 = 𝒫 𝐵 )
11	7 10	eleqtrrd	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → 𝑆 ∈ dom 𝑈 )
12	1 2 4 11	lubcl	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑈 ‘ 𝑆 ) ∈ 𝐵 )
13	9	simprrd	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → dom 𝐺 = 𝒫 𝐵 )
14	7 13	eleqtrrd	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → 𝑆 ∈ dom 𝐺 )
15	1 3 4 14	glbcl	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 )
16	12 15	jca	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → ( ( 𝑈 ‘ 𝑆 ) ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 ) )