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 eqtrid 
 |-  ( ( 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 ) )