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 | |- ( A e. V -> ( A = (/) <-> ( fi ` A ) = (/) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fveq2 | |- ( A = (/) -> ( fi ` A ) = ( fi ` (/) ) ) |
|
2 | fi0 | |- ( fi ` (/) ) = (/) |
|
3 | 1 2 | eqtrdi | |- ( A = (/) -> ( fi ` A ) = (/) ) |
4 | ssfii | |- ( A e. V -> A C_ ( fi ` A ) ) |
|
5 | sseq0 | |- ( ( A C_ ( fi ` A ) /\ ( fi ` A ) = (/) ) -> A = (/) ) |
|
6 | 4 5 | sylan | |- ( ( A e. V /\ ( fi ` A ) = (/) ) -> A = (/) ) |
7 | 6 | ex | |- ( A e. V -> ( ( fi ` A ) = (/) -> A = (/) ) ) |
8 | 3 7 | impbid2 | |- ( A e. V -> ( A = (/) <-> ( fi ` A ) = (/) ) ) |