Metamath Proof Explorer

Theorem ipolubdm

Description: The domain of the LUB of the inclusion poset. (Contributed by Zhi Wang, 28-Sep-2024)

Ref Expression
Hypotheses ipolub.i 
|- I = ( toInc ` F )
ipolub.f 
|- ( ph -> F e. V )
ipolub.s 
|- ( ph -> S C_ F )
ipolub.u 
|- ( ph -> U = ( lub ` I ) )
ipolubdm.t 
|- ( ph -> T = |^| { x e. F | U. S C_ x } )
Assertion ipolubdm 
|- ( ph -> ( S e. dom U <-> 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 ipolub.u 
 |-  ( ph -> U = ( lub ` I ) )
5 ipolubdm.t 
 |-  ( ph -> T = |^| { x e. F | U. S C_ x } )
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 ipolublem 
 |-  ( ( ph /\ t e. F ) -> ( ( U. S C_ t /\ A. z e. F ( U. S C_ z -> t C_ z ) ) <-> ( A. y e. S y ( le ` I ) t /\ A. z e. F ( A. y e. S y ( le ` I ) z -> t ( le ` I ) z ) ) ) )
11 1 ipopos 
 |-  I e. Poset
12 11 a1i 
 |-  ( ph -> I e. Poset )
13 7 8 4 10 12 lubeldm2d 
 |-  ( ph -> ( S e. dom U <-> ( S C_ F /\ E. t e. F ( U. S C_ t /\ A. z e. F ( U. S C_ z -> t C_ z ) ) ) ) )
14 3 13 mpbirand 
 |-  ( ph -> ( S e. dom U <-> E. t e. F ( U. S C_ t /\ A. z e. F ( U. S C_ z -> t C_ z ) ) ) )
15 5 ad2antrr 
 |-  ( ( ( ph /\ t e. F ) /\ ( U. S C_ t /\ A. z e. F ( U. S C_ z -> t C_ z ) ) ) -> T = |^| { x e. F | U. S C_ x } )
16 intubeu 
 |-  ( t e. F -> ( ( U. S C_ t /\ A. z e. F ( U. S C_ z -> t C_ z ) ) <-> t = |^| { x e. F | U. S C_ x } ) )
17 16 biimpa 
 |-  ( ( t e. F /\ ( U. S C_ t /\ A. z e. F ( U. S C_ z -> t C_ z ) ) ) -> t = |^| { x e. F | U. S C_ x } )
18 17 adantll 
 |-  ( ( ( ph /\ t e. F ) /\ ( U. S C_ t /\ A. z e. F ( U. S C_ z -> t C_ z ) ) ) -> t = |^| { x e. F | U. S C_ x } )
19 15 18 eqtr4d 
 |-  ( ( ( ph /\ t e. F ) /\ ( U. S C_ t /\ A. z e. F ( U. S C_ z -> t C_ z ) ) ) -> T = t )
20 simplr 
 |-  ( ( ( ph /\ t e. F ) /\ ( U. S C_ t /\ A. z e. F ( U. S C_ z -> t C_ z ) ) ) -> t e. F )
21 19 20 eqeltrd 
 |-  ( ( ( ph /\ t e. F ) /\ ( U. S C_ t /\ A. z e. F ( U. S C_ z -> t C_ z ) ) ) -> T e. F )
22 21 ex 
 |-  ( ( ph /\ t e. F ) -> ( ( U. S C_ t /\ A. z e. F ( U. S C_ z -> t C_ z ) ) -> T e. F ) )
23 simpr 
 |-  ( ( ph /\ T e. F ) -> T e. F )
24 intubeu 
 |-  ( T e. F -> ( ( U. S C_ T /\ A. z e. F ( U. S C_ z -> T C_ z ) ) <-> T = |^| { x e. F | U. S C_ x } ) )
25 24 biimparc 
 |-  ( ( T = |^| { x e. F | U. S C_ x } /\ T e. F ) -> ( U. S C_ T /\ A. z e. F ( U. S C_ z -> T C_ z ) ) )
26 5 25 sylan 
 |-  ( ( ph /\ T e. F ) -> ( U. S C_ T /\ A. z e. F ( U. S C_ z -> T C_ z ) ) )
27 sseq2 
 |-  ( t = T -> ( U. S C_ t <-> U. S C_ T ) )
28 sseq1 
 |-  ( t = T -> ( t C_ z <-> T C_ z ) )
29 28 imbi2d 
 |-  ( t = T -> ( ( U. S C_ z -> t C_ z ) <-> ( U. S C_ z -> T C_ z ) ) )
30 29 ralbidv 
 |-  ( t = T -> ( A. z e. F ( U. S C_ z -> t C_ z ) <-> A. z e. F ( U. S C_ z -> T C_ z ) ) )
31 27 30 anbi12d 
 |-  ( t = T -> ( ( U. S C_ t /\ A. z e. F ( U. S C_ z -> t C_ z ) ) <-> ( U. S C_ T /\ A. z e. F ( U. S C_ z -> T C_ z ) ) ) )
32 22 23 26 31 rspceb2dv 
 |-  ( ph -> ( E. t e. F ( U. S C_ t /\ A. z e. F ( U. S C_ z -> t C_ z ) ) <-> T e. F ) )
33 14 32 bitrd 
 |-  ( ph -> ( S e. dom U <-> T e. F ) )