Theorem 0rest

Description: Value of the structure restriction when the topology input is empty. (Contributed by Mario Carneiro, 13-Aug-2015)

	Ref	Expression
Assertion	0rest	|- ( (/) |`t A ) = (/)

Proof

Step	Hyp	Ref	Expression
1		0ex	|- (/) e. _V
2		restval	|- ( ( (/) e. _V /\ A e. _V ) -> ( (/) |`t A ) = ran ( x e. (/) |-> ( x i^i A ) ) )
3	1 2	mpan	|- ( A e. _V -> ( (/) |`t A ) = ran ( x e. (/) |-> ( x i^i A ) ) )
4		mpt0	|- ( x e. (/) |-> ( x i^i A ) ) = (/)
5	4	rneqi	|- ran ( x e. (/) |-> ( x i^i A ) ) = ran (/)
6		rn0	|- ran (/) = (/)
7	5 6	eqtri	|- ran ( x e. (/) |-> ( x i^i A ) ) = (/)
8	3 7	eqtrdi	|- ( A e. _V -> ( (/) |`t A ) = (/) )
9		relxp	|- Rel ( _V X. _V )
10		restfn	|- |`t Fn ( _V X. _V )
11	10	fndmi	|- dom |`t = ( _V X. _V )
12	11	releqi	|- ( Rel dom |`t <-> Rel ( _V X. _V ) )
13	9 12	mpbir	|- Rel dom |`t
14	13	ovprc2	|- ( -. A e. _V -> ( (/) |`t A ) = (/) )
15	8 14	pm2.61i	|- ( (/) |`t A ) = (/)