Theorem bj-rest10

Description: An elementwise intersection on a nonempty family by the empty set is the singleton on the empty set. TODO: this generalizes rest0 and could replace it. (Contributed by BJ, 27-Apr-2021)

	Ref	Expression
Assertion	bj-rest10	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 ≠ ∅ → ( 𝑋 ↾t ∅ ) = { ∅ } ) )

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2		elrest	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∅ ∈ V ) → ( 𝑥 ∈ ( 𝑋 ↾t ∅ ) ↔ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 ∩ ∅ ) ) )
3	1 2	mpan2	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑥 ∈ ( 𝑋 ↾t ∅ ) ↔ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 ∩ ∅ ) ) )
4		in0	⊢ ( 𝑦 ∩ ∅ ) = ∅
5	4	eqeq2i	⊢ ( 𝑥 = ( 𝑦 ∩ ∅ ) ↔ 𝑥 = ∅ )
6	5	rexbii	⊢ ( ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 ∩ ∅ ) ↔ ∃ 𝑦 ∈ 𝑋 𝑥 = ∅ )
7		df-rex	⊢ ( ∃ 𝑦 ∈ 𝑋 𝑥 = ∅ ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑋 ∧ 𝑥 = ∅ ) )
8		19.41v	⊢ ( ∃ 𝑦 ( 𝑦 ∈ 𝑋 ∧ 𝑥 = ∅ ) ↔ ( ∃ 𝑦 𝑦 ∈ 𝑋 ∧ 𝑥 = ∅ ) )
9		n0	⊢ ( 𝑋 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝑋 )
10	9	bicomi	⊢ ( ∃ 𝑦 𝑦 ∈ 𝑋 ↔ 𝑋 ≠ ∅ )
11	10	anbi1i	⊢ ( ( ∃ 𝑦 𝑦 ∈ 𝑋 ∧ 𝑥 = ∅ ) ↔ ( 𝑋 ≠ ∅ ∧ 𝑥 = ∅ ) )
12	8 11	bitri	⊢ ( ∃ 𝑦 ( 𝑦 ∈ 𝑋 ∧ 𝑥 = ∅ ) ↔ ( 𝑋 ≠ ∅ ∧ 𝑥 = ∅ ) )
13	7 12	bitri	⊢ ( ∃ 𝑦 ∈ 𝑋 𝑥 = ∅ ↔ ( 𝑋 ≠ ∅ ∧ 𝑥 = ∅ ) )
14	6 13	bitri	⊢ ( ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 ∩ ∅ ) ↔ ( 𝑋 ≠ ∅ ∧ 𝑥 = ∅ ) )
15	14	baib	⊢ ( 𝑋 ≠ ∅ → ( ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 ∩ ∅ ) ↔ 𝑥 = ∅ ) )
16	3 15	sylan9bb	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ ∅ ) → ( 𝑥 ∈ ( 𝑋 ↾t ∅ ) ↔ 𝑥 = ∅ ) )
17		velsn	⊢ ( 𝑥 ∈ { ∅ } ↔ 𝑥 = ∅ )
18	16 17	bitr4di	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ ∅ ) → ( 𝑥 ∈ ( 𝑋 ↾t ∅ ) ↔ 𝑥 ∈ { ∅ } ) )
19	18	eqrdv	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ ∅ ) → ( 𝑋 ↾t ∅ ) = { ∅ } )
20	19	ex	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 ≠ ∅ → ( 𝑋 ↾t ∅ ) = { ∅ } ) )