# 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 ${⊢}\mathrm{fi}\left(\varnothing \right)=\varnothing$

### Proof

Step Hyp Ref Expression
1 0ex ${⊢}\varnothing \in \mathrm{V}$
2 fival ${⊢}\varnothing \in \mathrm{V}\to \mathrm{fi}\left(\varnothing \right)=\left\{{y}|\exists {x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{y}=\bigcap {x}\right\}$
3 1 2 ax-mp ${⊢}\mathrm{fi}\left(\varnothing \right)=\left\{{y}|\exists {x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{y}=\bigcap {x}\right\}$
4 vprc ${⊢}¬\mathrm{V}\in \mathrm{V}$
5 id ${⊢}{y}=\bigcap {x}\to {y}=\bigcap {x}$
6 elinel1 ${⊢}{x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\to {x}\in 𝒫\varnothing$
7 elpwi ${⊢}{x}\in 𝒫\varnothing \to {x}\subseteq \varnothing$
8 ss0 ${⊢}{x}\subseteq \varnothing \to {x}=\varnothing$
9 6 7 8 3syl ${⊢}{x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\to {x}=\varnothing$
10 9 inteqd ${⊢}{x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\to \bigcap {x}=\bigcap \varnothing$
11 int0 ${⊢}\bigcap \varnothing =\mathrm{V}$
12 10 11 syl6eq ${⊢}{x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\to \bigcap {x}=\mathrm{V}$
13 5 12 sylan9eqr ${⊢}\left({x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\wedge {y}=\bigcap {x}\right)\to {y}=\mathrm{V}$
14 13 rexlimiva ${⊢}\exists {x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{y}=\bigcap {x}\to {y}=\mathrm{V}$
15 vex ${⊢}{y}\in \mathrm{V}$
16 14 15 syl6eqelr ${⊢}\exists {x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{y}=\bigcap {x}\to \mathrm{V}\in \mathrm{V}$
17 4 16 mto ${⊢}¬\exists {x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{y}=\bigcap {x}$
18 17 abf ${⊢}\left\{{y}|\exists {x}\in \left(𝒫\varnothing \cap \mathrm{Fin}\right)\phantom{\rule{.4em}{0ex}}{y}=\bigcap {x}\right\}=\varnothing$
19 3 18 eqtri ${⊢}\mathrm{fi}\left(\varnothing \right)=\varnothing$