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 𝐴 ) = ∅

Proof

Step Hyp Ref Expression
1 0ex ∅ ∈ V
2 restval ( ( ∅ ∈ V ∧ 𝐴 ∈ V ) → ( ∅ ↾t 𝐴 ) = ran ( 𝑥 ∈ ∅ ↦ ( 𝑥𝐴 ) ) )
3 1 2 mpan ( 𝐴 ∈ V → ( ∅ ↾t 𝐴 ) = ran ( 𝑥 ∈ ∅ ↦ ( 𝑥𝐴 ) ) )
4 mpt0 ( 𝑥 ∈ ∅ ↦ ( 𝑥𝐴 ) ) = ∅
5 4 rneqi ran ( 𝑥 ∈ ∅ ↦ ( 𝑥𝐴 ) ) = ran ∅
6 rn0 ran ∅ = ∅
7 5 6 eqtri ran ( 𝑥 ∈ ∅ ↦ ( 𝑥𝐴 ) ) = ∅
8 3 7 eqtrdi ( 𝐴 ∈ V → ( ∅ ↾t 𝐴 ) = ∅ )
9 relxp Rel ( V × V )
10 restfn t Fn ( V × V )
11 10 fndmi dom ↾t = ( V × V )
12 11 releqi ( Rel dom ↾t ↔ Rel ( V × V ) )
13 9 12 mpbir Rel dom ↾t
14 13 ovprc2 ( ¬ 𝐴 ∈ V → ( ∅ ↾t 𝐴 ) = ∅ )
15 8 14 pm2.61i ( ∅ ↾t 𝐴 ) = ∅