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

Metamath Proof Explorer

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 ) = (/)