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

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 ⊢ 𝐴 ∈ ( TopOn ‘ 𝐵 )
Assertion toponrestid 𝐴 = ( 𝐴 ↾t 𝐵 )

Proof

Step Hyp Ref Expression
1 toponrestid.t ⊢ 𝐴 ∈ ( TopOn ‘ 𝐵 )
2 1 toponunii ⊢ 𝐵 = ∪ 𝐴
3 2 restid ⊢ ( 𝐴 ∈ ( TopOn ‘ 𝐵 ) → ( 𝐴 ↾t 𝐵 ) = 𝐴 )
4 1 3 ax-mp ⊢ ( 𝐴 ↾t 𝐵 ) = 𝐴
5 4 eqcomi ⊢ 𝐴 = ( 𝐴 ↾t 𝐵 )