Metamath Proof Explorer


Theorem toponrestid

Description: Given a topology on a set, restricting it to that same set has no effect. (Contributed by Jim Kingdon, 6-Jul-2022)

Ref Expression
Hypothesis toponrestid.t
|- A e. ( TopOn ` B )
Assertion toponrestid
|- A = ( A |`t B )

Proof

Step Hyp Ref Expression
1 toponrestid.t
 |-  A e. ( TopOn ` B )
2 1 toponunii
 |-  B = U. A
3 2 restid
 |-  ( A e. ( TopOn ` B ) -> ( A |`t B ) = A )
4 1 3 ax-mp
 |-  ( A |`t B ) = A
5 4 eqcomi
 |-  A = ( A |`t B )