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 ⊢ ∅ ∈ 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 ‘ ∅ ) = ∅