This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem toplatlub

Description: Least upper bounds in a topology are realized by unions. (Contributed by Zhi Wang, 30-Sep-2024)

Ref Expression
Hypotheses topclat.i 
|- I = ( toInc ` J )
toplatlub.j 
|- ( ph -> J e. Top )
toplatlub.s 
|- ( ph -> S C_ J )
toplatlub.u 
|- U = ( lub ` I )
Assertion toplatlub 
|- ( ph -> ( U ` S ) = U. S )

Proof

Step Hyp Ref Expression
1 topclat.i 
 |-  I = ( toInc ` J )
2 toplatlub.j 
 |-  ( ph -> J e. Top )
3 toplatlub.s 
 |-  ( ph -> S C_ J )
4 toplatlub.u 
 |-  U = ( lub ` I )
5 4 a1i 
 |-  ( ph -> U = ( lub ` I ) )
6 uniopn 
 |-  ( ( J e. Top /\ S C_ J ) -> U. S e. J )
7 2 3 6 syl2anc 
 |-  ( ph -> U. S e. J )
8 intmin 
 |-  ( U. S e. J -> |^| { x e. J | U. S C_ x } = U. S )
9 8 eqcomd 
 |-  ( U. S e. J -> U. S = |^| { x e. J | U. S C_ x } )
10 7 9 syl 
 |-  ( ph -> U. S = |^| { x e. J | U. S C_ x } )
11 1 2 3 5 10 7 ipolub 
 |-  ( ph -> ( U ` S ) = U. S )