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\in \mathrm{TopOn}\left(B\right)$$
Assertion	toponrestid	$$⊢A=A{\upharpoonright }_{𝑡}B$$

Proof

Step	Hyp	Ref	Expression
1		toponrestid.t	$$⊢A\in \mathrm{TopOn}\left(B\right)$$
2	1	toponunii	$$⊢B=\bigcup A$$
3	2	restid	$$⊢A\in \mathrm{TopOn}\left(B\right)\to A{\upharpoonright }_{𝑡}B=A$$
4	1 3	ax-mp	$$⊢A{\upharpoonright }_{𝑡}B=A$$
5	4	eqcomi	$$⊢A=A{\upharpoonright }_{𝑡}B$$