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

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