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=toIncF
ipolub.f φFV
ipolub.s φSF
ipoglb.g φG=glbI
ipoglbdm.t φT=xF|xS
ipoglb.t φTF
Assertion ipoglb φGS=T

Proof

Step Hyp Ref Expression
1 ipolub.i I=toIncF
2 ipolub.f φFV
3 ipolub.s φSF
4 ipoglb.g φG=glbI
5 ipoglbdm.t φT=xF|xS
6 ipoglb.t φTF
7 eqid I=I
8 1 ipobas FVF=BaseI
9 2 8 syl φF=BaseI
10 1 ipopos IPoset
11 10 a1i φIPoset
12 breq2 y=vTIyTIv
13 unilbeu TFTSzFzSzTT=xF|xS
14 13 biimpar TFT=xF|xSTSzFzSzT
15 6 5 14 syl2anc φTSzFzSzT
16 1 2 3 7 ipoglblem φTFTSzFzSzTySTIyzFySzIyzIT
17 6 16 mpdan φTSzFzSzTySTIyzFySzIyzIT
18 15 17 mpbid φySTIyzFySzIyzIT
19 18 simpld φySTIy
20 19 adantr φvSySTIy
21 simpr φvSvS
22 12 20 21 rspcdva φvSTIv
23 breq1 z=wzIywIy
24 23 ralbidv z=wySzIyySwIy
25 breq2 y=vwIywIv
26 25 cbvralvw ySwIyvSwIv
27 24 26 bitrdi z=wySzIyvSwIv
28 breq1 z=wzITwIT
29 27 28 imbi12d z=wySzIyzITvSwIvwIT
30 18 simprd φzFySzIyzIT
31 30 adantr φwFzFySzIyzIT
32 simpr φwFwF
33 29 31 32 rspcdva φwFvSwIvwIT
34 33 3impia φwFvSwIvwIT
35 7 9 4 11 3 6 22 34 posglbdg φGS=T