Metamath Proof Explorer

Theorem indisuni

Description: The base set of the indiscrete topology. (Contributed by Mario Carneiro, 14-Aug-2015)

Ref Expression
Assertion indisuni 
|- ( _I ` A ) = U. { (/) , A }

Proof

Step Hyp Ref Expression
1 indislem 
 |-  { (/) , ( _I ` A ) } = { (/) , A }
2 fvex 
 |-  ( _I ` A ) e. _V
3 indistopon 
 |-  ( ( _I ` A ) e. _V -> { (/) , ( _I ` A ) } e. ( TopOn ` ( _I ` A ) ) )
4 2 3 ax-mp 
 |-  { (/) , ( _I ` A ) } e. ( TopOn ` ( _I ` A ) )
5 1 4 eqeltrri 
 |-  { (/) , A } e. ( TopOn ` ( _I ` A ) )
6 5 toponunii 
 |-  ( _I ` A ) = U. { (/) , A }