Metamath Proof Explorer


Theorem ipoglb

Description: The GLB of the inclusion poset. (hypotheses "ipolub.s" and "ipoglb.t" could be eliminated with S e. dom G .) Could be significantly shortened if posglbdg is in quantified form. mrelatglb could potentially be shortened using this. See mrelatglbALT . (Contributed by Zhi Wang, 29-Sep-2024)

Ref Expression
Hypotheses ipolub.i I = toInc F
ipolub.f φ F V
ipolub.s φ S F
ipoglb.g φ G = glb I
ipoglbdm.t φ T = x F | x S
ipoglb.t φ T F
Assertion ipoglb φ G S = T

Proof

Step Hyp Ref Expression
1 ipolub.i I = toInc F
2 ipolub.f φ F V
3 ipolub.s φ S F
4 ipoglb.g φ G = glb I
5 ipoglbdm.t φ T = x F | x S
6 ipoglb.t φ T F
7 eqid I = I
8 1 ipobas F V F = Base I
9 2 8 syl φ F = Base I
10 1 ipopos I Poset
11 10 a1i φ I Poset
12 breq2 y = v T I y T I v
13 unilbeu T F T S z F z S z T T = x F | x S
14 13 biimpar T F T = x F | x S T S z F z S z T
15 6 5 14 syl2anc φ T S z F z S z T
16 1 2 3 7 ipoglblem φ T F T S z F z S z T y S T I y z F y S z I y z I T
17 6 16 mpdan φ T S z F z S z T y S T I y z F y S z I y z I T
18 15 17 mpbid φ y S T I y z F y S z I y z I T
19 18 simpld φ y S T I y
20 19 adantr φ v S y S T I y
21 simpr φ v S v S
22 12 20 21 rspcdva φ v S T I v
23 breq1 z = w z I y w I y
24 23 ralbidv z = w y S z I y y S w I y
25 breq2 y = v w I y w I v
26 25 cbvralvw y S w I y v S w I v
27 24 26 bitrdi z = w y S z I y v S w I v
28 breq1 z = w z I T w I T
29 27 28 imbi12d z = w y S z I y z I T v S w I v w I T
30 18 simprd φ z F y S z I y z I T
31 30 adantr φ w F z F y S z I y z I T
32 simpr φ w F w F
33 29 31 32 rspcdva φ w F v S w I v w I T
34 33 3impia φ w F v S w I v w I T
35 7 9 4 11 3 6 22 34 posglbdg φ G S = T