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