Theorem clatlem

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

	Ref	Expression
Hypotheses	clatlem.b	|- B = ( Base ` K )
	clatlem.u	|- U = ( lub ` K )
	clatlem.g	|- G = ( glb ` K )
Assertion	clatlem	|- ( ( K e. CLat /\ S C_ B ) -> ( ( U ` S ) e. B /\ ( G ` S ) e. B ) )

Proof

Step	Hyp	Ref	Expression
1		clatlem.b	|- B = ( Base ` K )
2		clatlem.u	|- U = ( lub ` K )
3		clatlem.g	|- G = ( glb ` K )
4		simpl	|- ( ( K e. CLat /\ S C_ B ) -> K e. CLat )
5	1	fvexi	|- B e. _V
6	5	elpw2	|- ( S e. ~P B <-> S C_ B )
7	6	bilanri	|- ( ( K e. CLat /\ S C_ B ) -> S e. ~P B )
8	1 2 3	isclat	|- ( K e. CLat <-> ( K e. Poset /\ ( dom U = ~P B /\ dom G = ~P B ) ) )
9	8	birani	|- ( ( K e. CLat /\ S C_ B ) -> ( K e. Poset /\ ( dom U = ~P B /\ dom G = ~P B ) ) )
10	9	simprld	|- ( ( K e. CLat /\ S C_ B ) -> dom U = ~P B )
11	7 10	eleqtrrd	|- ( ( K e. CLat /\ S C_ B ) -> S e. dom U )
12	1 2 4 11	lubcl	|- ( ( K e. CLat /\ S C_ B ) -> ( U ` S ) e. B )
13	9	simprrd	|- ( ( K e. CLat /\ S C_ B ) -> dom G = ~P B )
14	7 13	eleqtrrd	|- ( ( K e. CLat /\ S C_ B ) -> S e. dom G )
15	1 3 4 14	glbcl	|- ( ( K e. CLat /\ S C_ B ) -> ( G ` S ) e. B )
16	12 15	jca	|- ( ( K e. CLat /\ S C_ B ) -> ( ( U ` S ) e. B /\ ( G ` S ) e. B ) )