Metamath Proof Explorer


Theorem fieq0

Description: A set is empty iff the class of all the finite intersections of that set is empty. (Contributed by FL, 27-Apr-2008) (Revised by Mario Carneiro, 24-Nov-2013)

Ref Expression
Assertion fieq0 ( 𝐴𝑉 → ( 𝐴 = ∅ ↔ ( fi ‘ 𝐴 ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 fveq2 ( 𝐴 = ∅ → ( fi ‘ 𝐴 ) = ( fi ‘ ∅ ) )
2 fi0 ( fi ‘ ∅ ) = ∅
3 1 2 eqtrdi ( 𝐴 = ∅ → ( fi ‘ 𝐴 ) = ∅ )
4 ssfii ( 𝐴𝑉𝐴 ⊆ ( fi ‘ 𝐴 ) )
5 sseq0 ( ( 𝐴 ⊆ ( fi ‘ 𝐴 ) ∧ ( fi ‘ 𝐴 ) = ∅ ) → 𝐴 = ∅ )
6 4 5 sylan ( ( 𝐴𝑉 ∧ ( fi ‘ 𝐴 ) = ∅ ) → 𝐴 = ∅ )
7 6 ex ( 𝐴𝑉 → ( ( fi ‘ 𝐴 ) = ∅ → 𝐴 = ∅ ) )
8 3 7 impbid2 ( 𝐴𝑉 → ( 𝐴 = ∅ ↔ ( fi ‘ 𝐴 ) = ∅ ) )