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 ⊢ ∅ ↾ 𝑡 A = ∅

Proof

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