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 ` (/) ) = (/)