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