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 e. V /\ A e. W ) -> ( X =/= (/) -> ( X |`t A ) =/= (/) ) )

Proof

Step	Hyp	Ref	Expression
1		n0	|- ( X =/= (/) <-> E. y y e. X )
2		vex	|- y e. _V
3	2	inex1	|- ( y i^i A ) e. _V
4	3	isseti	|- E. x x = ( y i^i A )
5	4	jctr	|- ( y e. X -> ( y e. X /\ E. x x = ( y i^i A ) ) )
6	5	eximi	|- ( E. y y e. X -> E. y ( y e. X /\ E. x x = ( y i^i A ) ) )
7		df-rex	|- ( E. y e. X E. x x = ( y i^i A ) <-> E. y ( y e. X /\ E. x x = ( y i^i A ) ) )
8	6 7	sylibr	|- ( E. y y e. X -> E. y e. X E. x x = ( y i^i A ) )
9		rexcom4	|- ( E. y e. X E. x x = ( y i^i A ) <-> E. x E. y e. X x = ( y i^i A ) )
10	8 9	sylib	|- ( E. y y e. X -> E. x E. y e. X x = ( y i^i A ) )
11	10	a1i	|- ( ( X e. V /\ A e. W ) -> ( E. y y e. X -> E. x E. y e. X x = ( y i^i A ) ) )
12	1 11	biimtrid	|- ( ( X e. V /\ A e. W ) -> ( X =/= (/) -> E. x E. y e. X x = ( y i^i A ) ) )
13		elrest	|- ( ( X e. V /\ A e. W ) -> ( x e. ( X |`t A ) <-> E. y e. X x = ( y i^i A ) ) )
14	13	biimprd	|- ( ( X e. V /\ A e. W ) -> ( E. y e. X x = ( y i^i A ) -> x e. ( X |`t A ) ) )
15	14	eximdv	|- ( ( X e. V /\ A e. W ) -> ( E. x E. y e. X x = ( y i^i A ) -> E. x x e. ( X |`t A ) ) )
16	12 15	syld	|- ( ( X e. V /\ A e. W ) -> ( X =/= (/) -> E. x x e. ( X |`t A ) ) )
17		n0	|- ( ( X |`t A ) =/= (/) <-> E. x x e. ( X |`t A ) )
18	16 17	imbitrrdi	|- ( ( X e. V /\ A e. W ) -> ( X =/= (/) -> ( X |`t A ) =/= (/) ) )