Metamath Proof Explorer

Theorem glbsscl

Description: If a subset of S contains the GLB of S , then the two sets have the same GLB. (Contributed by Zhi Wang, 26-Sep-2024)

Ref Expression
Hypotheses lubsscl.k 
|- ( ph -> K e. Poset )
lubsscl.t 
|- ( ph -> T C_ S )
glbsscl.g 
|- G = ( glb ` K )
glbsscl.s 
|- ( ph -> S e. dom G )
glbsscl.x 
|- ( ph -> ( G ` S ) e. T )
Assertion glbsscl 
|- ( ph -> ( T e. dom G /\ ( G ` T ) = ( G ` S ) ) )

Proof

Step Hyp Ref Expression
1 lubsscl.k 
 |-  ( ph -> K e. Poset )
2 lubsscl.t 
 |-  ( ph -> T C_ S )
3 glbsscl.g 
 |-  G = ( glb ` K )
4 glbsscl.s 
 |-  ( ph -> S e. dom G )
5 glbsscl.x 
 |-  ( ph -> ( G ` S ) e. T )
6 eqid 
 |-  ( Base ` K ) = ( Base ` K )
7 eqid 
 |-  ( le ` K ) = ( le ` K )
8 6 7 3 1 4 glbelss 
 |-  ( ph -> S C_ ( Base ` K ) )
9 2 8 sstrd 
 |-  ( ph -> T C_ ( Base ` K ) )
10 9 5 sseldd 
 |-  ( ph -> ( G ` S ) e. ( Base ` K ) )
11 1 adantr 
 |-  ( ( ph /\ y e. T ) -> K e. Poset )
12 4 adantr 
 |-  ( ( ph /\ y e. T ) -> S e. dom G )
13 2 sselda 
 |-  ( ( ph /\ y e. T ) -> y e. S )
14 6 7 3 11 12 13 glble 
 |-  ( ( ph /\ y e. T ) -> ( G ` S ) ( le ` K ) y )
15 14 ralrimiva 
 |-  ( ph -> A. y e. T ( G ` S ) ( le ` K ) y )
16 breq2 
 |-  ( y = ( G ` S ) -> ( z ( le ` K ) y <-> z ( le ` K ) ( G ` S ) ) )
17 simp3 
 |-  ( ( ph /\ z e. ( Base ` K ) /\ A. y e. T z ( le ` K ) y ) -> A. y e. T z ( le ` K ) y )
18 5 3ad2ant1 
 |-  ( ( ph /\ z e. ( Base ` K ) /\ A. y e. T z ( le ` K ) y ) -> ( G ` S ) e. T )
19 16 17 18 rspcdva 
 |-  ( ( ph /\ z e. ( Base ` K ) /\ A. y e. T z ( le ` K ) y ) -> z ( le ` K ) ( G ` S ) )
20 19 3expia 
 |-  ( ( ph /\ z e. ( Base ` K ) ) -> ( A. y e. T z ( le ` K ) y -> z ( le ` K ) ( G ` S ) ) )
21 20 ralrimiva 
 |-  ( ph -> A. z e. ( Base ` K ) ( A. y e. T z ( le ` K ) y -> z ( le ` K ) ( G ` S ) ) )
22 breq1 
 |-  ( x = ( G ` S ) -> ( x ( le ` K ) y <-> ( G ` S ) ( le ` K ) y ) )
23 22 ralbidv 
 |-  ( x = ( G ` S ) -> ( A. y e. T x ( le ` K ) y <-> A. y e. T ( G ` S ) ( le ` K ) y ) )
24 breq2 
 |-  ( x = ( G ` S ) -> ( z ( le ` K ) x <-> z ( le ` K ) ( G ` S ) ) )
25 24 imbi2d 
 |-  ( x = ( G ` S ) -> ( ( A. y e. T z ( le ` K ) y -> z ( le ` K ) x ) <-> ( A. y e. T z ( le ` K ) y -> z ( le ` K ) ( G ` S ) ) ) )
26 25 ralbidv 
 |-  ( x = ( G ` S ) -> ( A. z e. ( Base ` K ) ( A. y e. T z ( le ` K ) y -> z ( le ` K ) x ) <-> A. z e. ( Base ` K ) ( A. y e. T z ( le ` K ) y -> z ( le ` K ) ( G ` S ) ) ) )
27 23 26 anbi12d 
 |-  ( x = ( G ` S ) -> ( ( A. y e. T x ( le ` K ) y /\ A. z e. ( Base ` K ) ( A. y e. T z ( le ` K ) y -> z ( le ` K ) x ) ) <-> ( A. y e. T ( G ` S ) ( le ` K ) y /\ A. z e. ( Base ` K ) ( A. y e. T z ( le ` K ) y -> z ( le ` K ) ( G ` S ) ) ) ) )
28 27 rspcev 
 |-  ( ( ( G ` S ) e. ( Base ` K ) /\ ( A. y e. T ( G ` S ) ( le ` K ) y /\ A. z e. ( Base ` K ) ( A. y e. T z ( le ` K ) y -> z ( le ` K ) ( G ` S ) ) ) ) -> E. x e. ( Base ` K ) ( A. y e. T x ( le ` K ) y /\ A. z e. ( Base ` K ) ( A. y e. T z ( le ` K ) y -> z ( le ` K ) x ) ) )
29 10 15 21 28 syl12anc 
 |-  ( ph -> E. x e. ( Base ` K ) ( A. y e. T x ( le ` K ) y /\ A. z e. ( Base ` K ) ( A. y e. T z ( le ` K ) y -> z ( le ` K ) x ) ) )
30 biid 
 |-  ( ( A. y e. T x ( le ` K ) y /\ A. z e. ( Base ` K ) ( A. y e. T z ( le ` K ) y -> z ( le ` K ) x ) ) <-> ( A. y e. T x ( le ` K ) y /\ A. z e. ( Base ` K ) ( A. y e. T z ( le ` K ) y -> z ( le ` K ) x ) ) )
31 6 7 3 30 1 glbeldm2 
 |-  ( ph -> ( T e. dom G <-> ( T C_ ( Base ` K ) /\ E. x e. ( Base ` K ) ( A. y e. T x ( le ` K ) y /\ A. z e. ( Base ` K ) ( A. y e. T z ( le ` K ) y -> z ( le ` K ) x ) ) ) ) )
32 9 29 31 mpbir2and 
 |-  ( ph -> T e. dom G )
33 eqidd 
 |-  ( ph -> ( Base ` K ) = ( Base ` K ) )
34 3 a1i 
 |-  ( ph -> G = ( glb ` K ) )
35 7 33 34 1 9 10 14 19 posglbdg 
 |-  ( ph -> ( G ` T ) = ( G ` S ) )
36 32 35 jca 
 |-  ( ph -> ( T e. dom G /\ ( G ` T ) = ( G ` S ) ) )