Metamath Proof Explorer

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 
|- ( X e. V -> ( X =/= (/) -> ( X |`t (/) ) = { (/) } ) )

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 elrest 
 |-  ( ( X e. V /\ (/) e. _V ) -> ( x e. ( X |`t (/) ) <-> E. y e. X x = ( y i^i (/) ) ) )
3 1 2 mpan2 
 |-  ( X e. V -> ( x e. ( X |`t (/) ) <-> E. y e. X x = ( y i^i (/) ) ) )
4 in0 
 |-  ( y i^i (/) ) = (/)
5 4 eqeq2i 
 |-  ( x = ( y i^i (/) ) <-> x = (/) )
6 5 rexbii 
 |-  ( E. y e. X x = ( y i^i (/) ) <-> E. y e. X x = (/) )
7 df-rex 
 |-  ( E. y e. X x = (/) <-> E. y ( y e. X /\ x = (/) ) )
8 19.41v 
 |-  ( E. y ( y e. X /\ x = (/) ) <-> ( E. y y e. X /\ x = (/) ) )
9 n0 
 |-  ( X =/= (/) <-> E. y y e. X )
10 9 bicomi 
 |-  ( E. y y e. X <-> X =/= (/) )
11 10 anbi1i 
 |-  ( ( E. y y e. X /\ x = (/) ) <-> ( X =/= (/) /\ x = (/) ) )
12 8 11 bitri 
 |-  ( E. y ( y e. X /\ x = (/) ) <-> ( X =/= (/) /\ x = (/) ) )
13 7 12 bitri 
 |-  ( E. y e. X x = (/) <-> ( X =/= (/) /\ x = (/) ) )
14 6 13 bitri 
 |-  ( E. y e. X x = ( y i^i (/) ) <-> ( X =/= (/) /\ x = (/) ) )
15 14 baib 
 |-  ( X =/= (/) -> ( E. y e. X x = ( y i^i (/) ) <-> x = (/) ) )
16 3 15 sylan9bb 
 |-  ( ( X e. V /\ X =/= (/) ) -> ( x e. ( X |`t (/) ) <-> x = (/) ) )
17 velsn 
 |-  ( x e. { (/) } <-> x = (/) )
18 16 17 bitr4di 
 |-  ( ( X e. V /\ X =/= (/) ) -> ( x e. ( X |`t (/) ) <-> x e. { (/) } ) )
19 18 eqrdv 
 |-  ( ( X e. V /\ X =/= (/) ) -> ( X |`t (/) ) = { (/) } )
20 19 ex 
 |-  ( X e. V -> ( X =/= (/) -> ( X |`t (/) ) = { (/) } ) )