Metamath Proof Explorer


Theorem tgidm

Description: The topology generator function is idempotent. (Contributed by NM, 18-Jul-2006) (Revised by Mario Carneiro, 2-Sep-2015)

Ref Expression
Assertion tgidm
|- ( B e. V -> ( topGen ` ( topGen ` B ) ) = ( topGen ` B ) )

Proof

Step Hyp Ref Expression
1 fvex
 |-  ( topGen ` B ) e. _V
2 eltg3
 |-  ( ( topGen ` B ) e. _V -> ( x e. ( topGen ` ( topGen ` B ) ) <-> E. y ( y C_ ( topGen ` B ) /\ x = U. y ) ) )
3 1 2 ax-mp
 |-  ( x e. ( topGen ` ( topGen ` B ) ) <-> E. y ( y C_ ( topGen ` B ) /\ x = U. y ) )
4 uniiun
 |-  U. y = U_ z e. y z
5 simpr
 |-  ( ( B e. V /\ y C_ ( topGen ` B ) ) -> y C_ ( topGen ` B ) )
6 5 sselda
 |-  ( ( ( B e. V /\ y C_ ( topGen ` B ) ) /\ z e. y ) -> z e. ( topGen ` B ) )
7 eltg4i
 |-  ( z e. ( topGen ` B ) -> z = U. ( B i^i ~P z ) )
8 6 7 syl
 |-  ( ( ( B e. V /\ y C_ ( topGen ` B ) ) /\ z e. y ) -> z = U. ( B i^i ~P z ) )
9 8 iuneq2dv
 |-  ( ( B e. V /\ y C_ ( topGen ` B ) ) -> U_ z e. y z = U_ z e. y U. ( B i^i ~P z ) )
10 4 9 syl5eq
 |-  ( ( B e. V /\ y C_ ( topGen ` B ) ) -> U. y = U_ z e. y U. ( B i^i ~P z ) )
11 iuncom4
 |-  U_ z e. y U. ( B i^i ~P z ) = U. U_ z e. y ( B i^i ~P z )
12 10 11 eqtrdi
 |-  ( ( B e. V /\ y C_ ( topGen ` B ) ) -> U. y = U. U_ z e. y ( B i^i ~P z ) )
13 inss1
 |-  ( B i^i ~P z ) C_ B
14 13 rgenw
 |-  A. z e. y ( B i^i ~P z ) C_ B
15 iunss
 |-  ( U_ z e. y ( B i^i ~P z ) C_ B <-> A. z e. y ( B i^i ~P z ) C_ B )
16 14 15 mpbir
 |-  U_ z e. y ( B i^i ~P z ) C_ B
17 16 a1i
 |-  ( y C_ ( topGen ` B ) -> U_ z e. y ( B i^i ~P z ) C_ B )
18 eltg3i
 |-  ( ( B e. V /\ U_ z e. y ( B i^i ~P z ) C_ B ) -> U. U_ z e. y ( B i^i ~P z ) e. ( topGen ` B ) )
19 17 18 sylan2
 |-  ( ( B e. V /\ y C_ ( topGen ` B ) ) -> U. U_ z e. y ( B i^i ~P z ) e. ( topGen ` B ) )
20 12 19 eqeltrd
 |-  ( ( B e. V /\ y C_ ( topGen ` B ) ) -> U. y e. ( topGen ` B ) )
21 eleq1
 |-  ( x = U. y -> ( x e. ( topGen ` B ) <-> U. y e. ( topGen ` B ) ) )
22 20 21 syl5ibrcom
 |-  ( ( B e. V /\ y C_ ( topGen ` B ) ) -> ( x = U. y -> x e. ( topGen ` B ) ) )
23 22 expimpd
 |-  ( B e. V -> ( ( y C_ ( topGen ` B ) /\ x = U. y ) -> x e. ( topGen ` B ) ) )
24 23 exlimdv
 |-  ( B e. V -> ( E. y ( y C_ ( topGen ` B ) /\ x = U. y ) -> x e. ( topGen ` B ) ) )
25 3 24 syl5bi
 |-  ( B e. V -> ( x e. ( topGen ` ( topGen ` B ) ) -> x e. ( topGen ` B ) ) )
26 25 ssrdv
 |-  ( B e. V -> ( topGen ` ( topGen ` B ) ) C_ ( topGen ` B ) )
27 bastg
 |-  ( B e. V -> B C_ ( topGen ` B ) )
28 tgss
 |-  ( ( ( topGen ` B ) e. _V /\ B C_ ( topGen ` B ) ) -> ( topGen ` B ) C_ ( topGen ` ( topGen ` B ) ) )
29 1 27 28 sylancr
 |-  ( B e. V -> ( topGen ` B ) C_ ( topGen ` ( topGen ` B ) ) )
30 26 29 eqssd
 |-  ( B e. V -> ( topGen ` ( topGen ` B ) ) = ( topGen ` B ) )