Metamath Proof Explorer

Theorem bj-restn0

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

		Ref	Expression
	Assertion	bj-restn0	$⊢ (X \in V \land A \in W) \to (X \neq \emptyset \to X ↾_{𝑡} A \neq \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		n0	$⊢ X \neq \emptyset \leftrightarrow \exists y y \in X$
2		vex	$⊢ y \in V$
3	2	inex1	$⊢ y \cap A \in V$
4	3	isseti	$⊢ \exists x x = y \cap A$
5	4	jctr	$⊢ y \in X \to (y \in X \land \exists x x = y \cap A)$
6	5	eximi	$⊢ \exists y y \in X \to \exists y (y \in X \land \exists x x = y \cap A)$
7		df-rex	$⊢ \exists y \in X \exists x x = y \cap A \leftrightarrow \exists y (y \in X \land \exists x x = y \cap A)$
8	6 7	sylibr	$⊢ \exists y y \in X \to \exists y \in X \exists x x = y \cap A$
9		rexcom4	$⊢ \exists y \in X \exists x x = y \cap A \leftrightarrow \exists x \exists y \in X x = y \cap A$
10	8 9	sylib	$⊢ \exists y y \in X \to \exists x \exists y \in X x = y \cap A$
11	10	a1i	$⊢ (X \in V \land A \in W) \to (\exists y y \in X \to \exists x \exists y \in X x = y \cap A)$
12	1 11	biimtrid	$⊢ (X \in V \land A \in W) \to (X \neq \emptyset \to \exists x \exists y \in X x = y \cap A)$
13		elrest	$⊢ (X \in V \land A \in W) \to (x \in (X ↾_{𝑡} A) \leftrightarrow \exists y \in X x = y \cap A)$
14	13	biimprd	$⊢ (X \in V \land A \in W) \to (\exists y \in X x = y \cap A \to x \in (X ↾_{𝑡} A))$
15	14	eximdv	$⊢ (X \in V \land A \in W) \to (\exists x \exists y \in X x = y \cap A \to \exists x x \in (X ↾_{𝑡} A))$
16	12 15	syld	$⊢ (X \in V \land A \in W) \to (X \neq \emptyset \to \exists x x \in (X ↾_{𝑡} A))$
17		n0	$⊢ X ↾_{𝑡} A \neq \emptyset \leftrightarrow \exists x x \in (X ↾_{𝑡} A)$
18	16 17	imbitrrdi	$⊢ (X \in V \land A \in W) \to (X \neq \emptyset \to X ↾_{𝑡} A \neq \emptyset)$