This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fi0

Description: The set of finite intersections of the empty set. (Contributed by Mario Carneiro, 30-Aug-2015)

Ref Expression
Assertion fi0 
|- ( fi ` (/) ) = (/)

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 fival 
 |-  ( (/) e. _V -> ( fi ` (/) ) = { y | E. x e. ( ~P (/) i^i Fin ) y = |^| x } )
3 1 2 ax-mp 
 |-  ( fi ` (/) ) = { y | E. x e. ( ~P (/) i^i Fin ) y = |^| x }
4 vprc 
 |-  -. _V e. _V
5 id 
 |-  ( y = |^| x -> y = |^| x )
6 elinel1 
 |-  ( x e. ( ~P (/) i^i Fin ) -> x e. ~P (/) )
7 elpwi 
 |-  ( x e. ~P (/) -> x C_ (/) )
8 ss0 
 |-  ( x C_ (/) -> x = (/) )
9 6 7 8 3syl 
 |-  ( x e. ( ~P (/) i^i Fin ) -> x = (/) )
10 9 inteqd 
 |-  ( x e. ( ~P (/) i^i Fin ) -> |^| x = |^| (/) )
11 int0 
 |-  |^| (/) = _V
12 10 11 eqtrdi 
 |-  ( x e. ( ~P (/) i^i Fin ) -> |^| x = _V )
13 5 12 sylan9eqr 
 |-  ( ( x e. ( ~P (/) i^i Fin ) /\ y = |^| x ) -> y = _V )
14 13 rexlimiva 
 |-  ( E. x e. ( ~P (/) i^i Fin ) y = |^| x -> y = _V )
15 vex 
 |-  y e. _V
16 14 15 eqeltrrdi 
 |-  ( E. x e. ( ~P (/) i^i Fin ) y = |^| x -> _V e. _V )
17 4 16 mto 
 |-  -. E. x e. ( ~P (/) i^i Fin ) y = |^| x
18 17 abf 
 |-  { y | E. x e. ( ~P (/) i^i Fin ) y = |^| x } = (/)
19 3 18 eqtri 
 |-  ( fi ` (/) ) = (/)