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	biimpri	⊢ ( 𝑆 ⊆ 𝐵 → 𝑆 ∈ 𝒫 𝐵 )
8	7	adantl	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → 𝑆 ∈ 𝒫 𝐵 )
9	1 2 3	isclat	⊢ ( 𝐾 ∈ CLat ↔ ( 𝐾 ∈ Poset ∧ ( dom 𝑈 = 𝒫 𝐵 ∧ dom 𝐺 = 𝒫 𝐵 ) ) )
10	9	biimpi	⊢ ( 𝐾 ∈ CLat → ( 𝐾 ∈ Poset ∧ ( dom 𝑈 = 𝒫 𝐵 ∧ dom 𝐺 = 𝒫 𝐵 ) ) )
11	10	adantr	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → ( 𝐾 ∈ Poset ∧ ( dom 𝑈 = 𝒫 𝐵 ∧ dom 𝐺 = 𝒫 𝐵 ) ) )
12	11	simprld	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → dom 𝑈 = 𝒫 𝐵 )
13	8 12	eleqtrrd	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → 𝑆 ∈ dom 𝑈 )
14	1 2 4 13	lubcl	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑈 ‘ 𝑆 ) ∈ 𝐵 )
15	11	simprrd	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → dom 𝐺 = 𝒫 𝐵 )
16	8 15	eleqtrrd	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → 𝑆 ∈ dom 𝐺 )
17	1 3 4 16	glbcl	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 )
18	14 17	jca	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → ( ( 𝑈 ‘ 𝑆 ) ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑆 ) ∈ 𝐵 ) )