Metamath Proof Explorer

Theorem ipoglbdm

Description: The domain of the GLB of the inclusion poset. (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 } )
Assertion ipoglbdm 
|- ( ph -> ( S e. dom G <-> T e. F ) )

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 1 ipobas 
 |-  ( F e. V -> F = ( Base ` I ) )
7 2 6 syl 
 |-  ( ph -> F = ( Base ` I ) )
8 eqidd 
 |-  ( ph -> ( le ` I ) = ( le ` I ) )
9 eqid 
 |-  ( le ` I ) = ( le ` I )
10 1 2 3 9 ipoglblem 
 |-  ( ( ph /\ w e. F ) -> ( ( w C_ |^| S /\ A. z e. F ( z C_ |^| S -> z C_ w ) ) <-> ( A. y e. S w ( le ` I ) y /\ A. z e. F ( A. y e. S z ( le ` I ) y -> z ( le ` I ) w ) ) ) )
11 1 ipopos 
 |-  I e. Poset
12 11 a1i 
 |-  ( ph -> I e. Poset )
13 7 8 4 10 12 glbeldm2d 
 |-  ( ph -> ( S e. dom G <-> ( S C_ F /\ E. w e. F ( w C_ |^| S /\ A. z e. F ( z C_ |^| S -> z C_ w ) ) ) ) )
14 3 13 mpbirand 
 |-  ( ph -> ( S e. dom G <-> E. w e. F ( w C_ |^| S /\ A. z e. F ( z C_ |^| S -> z C_ w ) ) ) )
15 5 ad2antrr 
 |-  ( ( ( ph /\ w e. F ) /\ ( w C_ |^| S /\ A. z e. F ( z C_ |^| S -> z C_ w ) ) ) -> T = U. { x e. F | x C_ |^| S } )
16 unilbeu 
 |-  ( w e. F -> ( ( w C_ |^| S /\ A. z e. F ( z C_ |^| S -> z C_ w ) ) <-> w = U. { x e. F | x C_ |^| S } ) )
17 16 biimpa 
 |-  ( ( w e. F /\ ( w C_ |^| S /\ A. z e. F ( z C_ |^| S -> z C_ w ) ) ) -> w = U. { x e. F | x C_ |^| S } )
18 17 adantll 
 |-  ( ( ( ph /\ w e. F ) /\ ( w C_ |^| S /\ A. z e. F ( z C_ |^| S -> z C_ w ) ) ) -> w = U. { x e. F | x C_ |^| S } )
19 15 18 eqtr4d 
 |-  ( ( ( ph /\ w e. F ) /\ ( w C_ |^| S /\ A. z e. F ( z C_ |^| S -> z C_ w ) ) ) -> T = w )
20 simplr 
 |-  ( ( ( ph /\ w e. F ) /\ ( w C_ |^| S /\ A. z e. F ( z C_ |^| S -> z C_ w ) ) ) -> w e. F )
21 19 20 eqeltrd 
 |-  ( ( ( ph /\ w e. F ) /\ ( w C_ |^| S /\ A. z e. F ( z C_ |^| S -> z C_ w ) ) ) -> T e. F )
22 21 ex 
 |-  ( ( ph /\ w e. F ) -> ( ( w C_ |^| S /\ A. z e. F ( z C_ |^| S -> z C_ w ) ) -> T e. F ) )
23 simpr 
 |-  ( ( ph /\ T e. F ) -> T e. F )
24 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 } ) )
25 24 biimparc 
 |-  ( ( T = U. { x e. F | x C_ |^| S } /\ T e. F ) -> ( T C_ |^| S /\ A. z e. F ( z C_ |^| S -> z C_ T ) ) )
26 5 25 sylan 
 |-  ( ( ph /\ T e. F ) -> ( T C_ |^| S /\ A. z e. F ( z C_ |^| S -> z C_ T ) ) )
27 sseq1 
 |-  ( w = T -> ( w C_ |^| S <-> T C_ |^| S ) )
28 sseq2 
 |-  ( w = T -> ( z C_ w <-> z C_ T ) )
29 28 imbi2d 
 |-  ( w = T -> ( ( z C_ |^| S -> z C_ w ) <-> ( z C_ |^| S -> z C_ T ) ) )
30 29 ralbidv 
 |-  ( w = T -> ( A. z e. F ( z C_ |^| S -> z C_ w ) <-> A. z e. F ( z C_ |^| S -> z C_ T ) ) )
31 27 30 anbi12d 
 |-  ( w = T -> ( ( w C_ |^| S /\ A. z e. F ( z C_ |^| S -> z C_ w ) ) <-> ( T C_ |^| S /\ A. z e. F ( z C_ |^| S -> z C_ T ) ) ) )
32 22 23 26 31 rspceb2dv 
 |-  ( ph -> ( E. w e. F ( w C_ |^| S /\ A. z e. F ( z C_ |^| S -> z C_ w ) ) <-> T e. F ) )
33 14 32 bitrd 
 |-  ( ph -> ( S e. dom G <-> T e. F ) )