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 ‘ ∅ ) = { 𝑦 ∣ ∃ 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) 𝑦 = 𝑥 } )
3 1 2 ax-mp ( fi ‘ ∅ ) = { 𝑦 ∣ ∃ 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) 𝑦 = 𝑥 }
4 vprc ¬ V ∈ V
5 id ( 𝑦 = 𝑥𝑦 = 𝑥 )
6 elinel1 ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) → 𝑥 ∈ 𝒫 ∅ )
7 elpwi ( 𝑥 ∈ 𝒫 ∅ → 𝑥 ⊆ ∅ )
8 ss0 ( 𝑥 ⊆ ∅ → 𝑥 = ∅ )
9 6 7 8 3syl ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) → 𝑥 = ∅ )
10 9 inteqd ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) → 𝑥 = ∅ )
11 int0 ∅ = V
12 10 11 eqtrdi ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) → 𝑥 = V )
13 5 12 sylan9eqr ( ( 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) ∧ 𝑦 = 𝑥 ) → 𝑦 = V )
14 13 rexlimiva ( ∃ 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) 𝑦 = 𝑥𝑦 = V )
15 vex 𝑦 ∈ V
16 14 15 eqeltrrdi ( ∃ 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) 𝑦 = 𝑥 → V ∈ V )
17 4 16 mto ¬ ∃ 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) 𝑦 = 𝑥
18 17 abf { 𝑦 ∣ ∃ 𝑥 ∈ ( 𝒫 ∅ ∩ Fin ) 𝑦 = 𝑥 } = ∅
19 3 18 eqtri ( fi ‘ ∅ ) = ∅