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	biimpri	|- ( S C_ B -> S e. ~P B )
8	7	adantl	|- ( ( K e. CLat /\ S C_ B ) -> S e. ~P B )
9	1 2 3	isclat	|- ( K e. CLat <-> ( K e. Poset /\ ( dom U = ~P B /\ dom G = ~P B ) ) )
10	9	biimpi	|- ( K e. CLat -> ( K e. Poset /\ ( dom U = ~P B /\ dom G = ~P B ) ) )
11	10	adantr	|- ( ( K e. CLat /\ S C_ B ) -> ( K e. Poset /\ ( dom U = ~P B /\ dom G = ~P B ) ) )
12	11	simprld	|- ( ( K e. CLat /\ S C_ B ) -> dom U = ~P B )
13	8 12	eleqtrrd	|- ( ( K e. CLat /\ S C_ B ) -> S e. dom U )
14	1 2 4 13	lubcl	|- ( ( K e. CLat /\ S C_ B ) -> ( U ` S ) e. B )
15	11	simprrd	|- ( ( K e. CLat /\ S C_ B ) -> dom G = ~P B )
16	8 15	eleqtrrd	|- ( ( K e. CLat /\ S C_ B ) -> S e. dom G )
17	1 3 4 16	glbcl	|- ( ( K e. CLat /\ S C_ B ) -> ( G ` S ) e. B )
18	14 17	jca	|- ( ( K e. CLat /\ S C_ B ) -> ( ( U ` S ) e. B /\ ( G ` S ) e. B ) )