Theorem bj-restn0

Description: An elementwise intersection on a nonempty family is nonempty. (Contributed by BJ, 27-Apr-2021)

	Ref	Expression
Assertion	bj-restn0	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( 𝑋 ≠ ∅ → ( 𝑋 ↾t 𝐴 ) ≠ ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		n0	⊢ ( 𝑋 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝑋 )
2		vex	⊢ 𝑦 ∈ V
3	2	inex1	⊢ ( 𝑦 ∩ 𝐴 ) ∈ V
4	3	isseti	⊢ ∃ 𝑥 𝑥 = ( 𝑦 ∩ 𝐴 )
5	4	jctr	⊢ ( 𝑦 ∈ 𝑋 → ( 𝑦 ∈ 𝑋 ∧ ∃ 𝑥 𝑥 = ( 𝑦 ∩ 𝐴 ) ) )
6	5	eximi	⊢ ( ∃ 𝑦 𝑦 ∈ 𝑋 → ∃ 𝑦 ( 𝑦 ∈ 𝑋 ∧ ∃ 𝑥 𝑥 = ( 𝑦 ∩ 𝐴 ) ) )
7		df-rex	⊢ ( ∃ 𝑦 ∈ 𝑋 ∃ 𝑥 𝑥 = ( 𝑦 ∩ 𝐴 ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑋 ∧ ∃ 𝑥 𝑥 = ( 𝑦 ∩ 𝐴 ) ) )
8	6 7	sylibr	⊢ ( ∃ 𝑦 𝑦 ∈ 𝑋 → ∃ 𝑦 ∈ 𝑋 ∃ 𝑥 𝑥 = ( 𝑦 ∩ 𝐴 ) )
9		rexcom4	⊢ ( ∃ 𝑦 ∈ 𝑋 ∃ 𝑥 𝑥 = ( 𝑦 ∩ 𝐴 ) ↔ ∃ 𝑥 ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 ∩ 𝐴 ) )
10	8 9	sylib	⊢ ( ∃ 𝑦 𝑦 ∈ 𝑋 → ∃ 𝑥 ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 ∩ 𝐴 ) )
11	10	a1i	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( ∃ 𝑦 𝑦 ∈ 𝑋 → ∃ 𝑥 ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 ∩ 𝐴 ) ) )
12	1 11	syl5bi	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( 𝑋 ≠ ∅ → ∃ 𝑥 ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 ∩ 𝐴 ) ) )
13		elrest	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( 𝑥 ∈ ( 𝑋 ↾t 𝐴 ) ↔ ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 ∩ 𝐴 ) ) )
14	13	biimprd	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 ∩ 𝐴 ) → 𝑥 ∈ ( 𝑋 ↾t 𝐴 ) ) )
15	14	eximdv	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( ∃ 𝑥 ∃ 𝑦 ∈ 𝑋 𝑥 = ( 𝑦 ∩ 𝐴 ) → ∃ 𝑥 𝑥 ∈ ( 𝑋 ↾t 𝐴 ) ) )
16	12 15	syld	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( 𝑋 ≠ ∅ → ∃ 𝑥 𝑥 ∈ ( 𝑋 ↾t 𝐴 ) ) )
17		n0	⊢ ( ( 𝑋 ↾t 𝐴 ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝑋 ↾t 𝐴 ) )
18	16 17	syl6ibr	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( 𝑋 ≠ ∅ → ( 𝑋 ↾t 𝐴 ) ≠ ∅ ) )