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

Metamath Proof Explorer

Theorem topclat

Description: A topology is a complete lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024)

Ref Expression
Hypothesis topclat.i 
|- I = ( toInc ` J )
Assertion topclat 
|- ( J e. Top -> I e. CLat )

Proof

Step Hyp Ref Expression
1 topclat.i 
 |-  I = ( toInc ` J )
2 1 ipobas 
 |-  ( J e. Top -> J = ( Base ` I ) )
3 eqidd 
 |-  ( J e. Top -> ( lub ` I ) = ( lub ` I ) )
4 eqidd 
 |-  ( J e. Top -> ( glb ` I ) = ( glb ` I ) )
5 1 ipopos 
 |-  I e. Poset
6 5 a1i 
 |-  ( J e. Top -> I e. Poset )
7 uniopn 
 |-  ( ( J e. Top /\ x C_ J ) -> U. x e. J )
8 simpl 
 |-  ( ( J e. Top /\ x C_ J ) -> J e. Top )
9 simpr 
 |-  ( ( J e. Top /\ x C_ J ) -> x C_ J )
10 eqidd 
 |-  ( ( J e. Top /\ x C_ J ) -> ( lub ` I ) = ( lub ` I ) )
11 intmin 
 |-  ( U. x e. J -> |^| { y e. J | U. x C_ y } = U. x )
12 11 eqcomd 
 |-  ( U. x e. J -> U. x = |^| { y e. J | U. x C_ y } )
13 7 12 syl 
 |-  ( ( J e. Top /\ x C_ J ) -> U. x = |^| { y e. J | U. x C_ y } )
14 1 8 9 10 13 ipolubdm 
 |-  ( ( J e. Top /\ x C_ J ) -> ( x e. dom ( lub ` I ) <-> U. x e. J ) )
15 7 14 mpbird 
 |-  ( ( J e. Top /\ x C_ J ) -> x e. dom ( lub ` I ) )
16 ssrab2 
 |-  { y e. J | y C_ |^| x } C_ J
17 uniopn 
 |-  ( ( J e. Top /\ { y e. J | y C_ |^| x } C_ J ) -> U. { y e. J | y C_ |^| x } e. J )
18 8 16 17 sylancl 
 |-  ( ( J e. Top /\ x C_ J ) -> U. { y e. J | y C_ |^| x } e. J )
19 eqidd 
 |-  ( ( J e. Top /\ x C_ J ) -> ( glb ` I ) = ( glb ` I ) )
20 eqidd 
 |-  ( ( J e. Top /\ x C_ J ) -> U. { y e. J | y C_ |^| x } = U. { y e. J | y C_ |^| x } )
21 1 8 9 19 20 ipoglbdm 
 |-  ( ( J e. Top /\ x C_ J ) -> ( x e. dom ( glb ` I ) <-> U. { y e. J | y C_ |^| x } e. J ) )
22 18 21 mpbird 
 |-  ( ( J e. Top /\ x C_ J ) -> x e. dom ( glb ` I ) )
23 2 3 4 6 15 22 isclatd 
 |-  ( J e. Top -> I e. CLat )