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 ⊢ ∅ ∈ V
2 fival ⊢ ∅ ∈ V → fi ⁡ ∅ = y | ∃ x ∈ 𝒫 ∅ ∩ Fin y = ⋂ x
3 1 2 ax-mp ⊢ fi ⁡ ∅ = y | ∃ x ∈ 𝒫 ∅ ∩ Fin y = ⋂ x
4 vprc ⊢ ¬ V ∈ V
5 id ⊢ y = ⋂ x → y = ⋂ x
6 elinel1 ⊢ x ∈ 𝒫 ∅ ∩ Fin → x ∈ 𝒫 ∅
7 elpwi ⊢ x ∈ 𝒫 ∅ → x ⊆ ∅
8 ss0 ⊢ x ⊆ ∅ → x = ∅
9 6 7 8 3syl ⊢ x ∈ 𝒫 ∅ ∩ Fin → x = ∅
10 9 inteqd ⊢ x ∈ 𝒫 ∅ ∩ Fin → ⋂ x = ⋂ ∅
11 int0 ⊢ ⋂ ∅ = V
12 10 11 syl6eq ⊢ x ∈ 𝒫 ∅ ∩ Fin → ⋂ x = V
13 5 12 sylan9eqr ⊢ x ∈ 𝒫 ∅ ∩ Fin ∧ y = ⋂ x → y = V
14 13 rexlimiva ⊢ ∃ x ∈ 𝒫 ∅ ∩ Fin y = ⋂ x → y = V
15 vex ⊢ y ∈ V
16 14 15 eqeltrrdi ⊢ ∃ x ∈ 𝒫 ∅ ∩ Fin y = ⋂ x → V ∈ V
17 4 16 mto ⊢ ¬ ∃ x ∈ 𝒫 ∅ ∩ Fin y = ⋂ x
18 17 abf ⊢ y | ∃ x ∈ 𝒫 ∅ ∩ Fin y = ⋂ x = ∅
19 3 18 eqtri ⊢ fi ⁡ ∅ = ∅