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 posglbd 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 
|- ( ph -> F e. V )
ipolub.s 
|- ( ph -> S C_ F )
ipoglb.g 
|- ( ph -> G = ( glb ` I ) )
ipoglbdm.t 
|- ( ph -> T = U. { x e. F | x C_ |^| S } )
ipoglb.t 
|- ( ph -> T e. F )
Assertion ipoglb 
|- ( ph -> ( G ` S ) = T )

Proof

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