Theorem clatglbss

Description: Subset law for greatest lower bound. (Contributed by Mario Carneiro, 16-Apr-2014)

	Ref	Expression
Hypotheses	clatglb.b	|- B = ( Base ` K )
	clatglb.l	|- .<_ = ( le ` K )
	clatglb.g	|- G = ( glb ` K )
Assertion	clatglbss	|- ( ( K e. CLat /\ T C_ B /\ S C_ T ) -> ( G ` T ) .<_ ( G ` S ) )

Proof

Step	Hyp	Ref	Expression
1		clatglb.b	|- B = ( Base ` K )
2		clatglb.l	|- .<_ = ( le ` K )
3		clatglb.g	|- G = ( glb ` K )
4		simpl1	|- ( ( ( K e. CLat /\ T C_ B /\ S C_ T ) /\ y e. S ) -> K e. CLat )
5		simpl2	|- ( ( ( K e. CLat /\ T C_ B /\ S C_ T ) /\ y e. S ) -> T C_ B )
6		simp3	|- ( ( K e. CLat /\ T C_ B /\ S C_ T ) -> S C_ T )
7	6	sselda	|- ( ( ( K e. CLat /\ T C_ B /\ S C_ T ) /\ y e. S ) -> y e. T )
8	1 2 3	clatglble	|- ( ( K e. CLat /\ T C_ B /\ y e. T ) -> ( G ` T ) .<_ y )
9	4 5 7 8	syl3anc	|- ( ( ( K e. CLat /\ T C_ B /\ S C_ T ) /\ y e. S ) -> ( G ` T ) .<_ y )
10	9	ralrimiva	|- ( ( K e. CLat /\ T C_ B /\ S C_ T ) -> A. y e. S ( G ` T ) .<_ y )
11		simp1	|- ( ( K e. CLat /\ T C_ B /\ S C_ T ) -> K e. CLat )
12	1 3	clatglbcl	|- ( ( K e. CLat /\ T C_ B ) -> ( G ` T ) e. B )
13	12	3adant3	|- ( ( K e. CLat /\ T C_ B /\ S C_ T ) -> ( G ` T ) e. B )
14		sstr	|- ( ( S C_ T /\ T C_ B ) -> S C_ B )
15	14	ancoms	|- ( ( T C_ B /\ S C_ T ) -> S C_ B )
16	15	3adant1	|- ( ( K e. CLat /\ T C_ B /\ S C_ T ) -> S C_ B )
17	1 2 3	clatleglb	|- ( ( K e. CLat /\ ( G ` T ) e. B /\ S C_ B ) -> ( ( G ` T ) .<_ ( G ` S ) <-> A. y e. S ( G ` T ) .<_ y ) )
18	11 13 16 17	syl3anc	|- ( ( K e. CLat /\ T C_ B /\ S C_ T ) -> ( ( G ` T ) .<_ ( G ` S ) <-> A. y e. S ( G ` T ) .<_ y ) )
19	10 18	mpbird	|- ( ( K e. CLat /\ T C_ B /\ S C_ T ) -> ( G ` T ) .<_ ( G ` S ) )