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 φ K Poset
lubsscl.t φ T S
glbsscl.g G = glb K
glbsscl.s φ S dom G
glbsscl.x φ G S T
Assertion glbsscl φ T dom G G T = G S

Proof

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