This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem en0

Description: The empty set is equinumerous only to itself. Exercise 1 of TakeutiZaring p. 88. (Contributed by NM, 27-May-1998) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 23-Sep-2024)

Ref Expression
Assertion en0 
|- ( A ~~ (/) <-> A = (/) )

Proof

Step Hyp Ref Expression
1 encv 
 |-  ( A ~~ (/) -> ( A e. _V /\ (/) e. _V ) )
2 breng 
 |-  ( ( A e. _V /\ (/) e. _V ) -> ( A ~~ (/) <-> E. f f : A -1-1-onto-> (/) ) )
3 1 2 syl 
 |-  ( A ~~ (/) -> ( A ~~ (/) <-> E. f f : A -1-1-onto-> (/) ) )
4 3 ibi 
 |-  ( A ~~ (/) -> E. f f : A -1-1-onto-> (/) )
5 f1ocnv 
 |-  ( f : A -1-1-onto-> (/) -> `' f : (/) -1-1-onto-> A )
6 f1o00 
 |-  ( `' f : (/) -1-1-onto-> A <-> ( `' f = (/) /\ A = (/) ) )
7 6 simprbi 
 |-  ( `' f : (/) -1-1-onto-> A -> A = (/) )
8 5 7 syl 
 |-  ( f : A -1-1-onto-> (/) -> A = (/) )
9 8 exlimiv 
 |-  ( E. f f : A -1-1-onto-> (/) -> A = (/) )
10 4 9 syl 
 |-  ( A ~~ (/) -> A = (/) )
11 0ex 
 |-  (/) e. _V
12 f1oeq1 
 |-  ( f = (/) -> ( f : (/) -1-1-onto-> (/) <-> (/) : (/) -1-1-onto-> (/) ) )
13 f1o0 
 |-  (/) : (/) -1-1-onto-> (/)
14 11 12 13 ceqsexv2d 
 |-  E. f f : (/) -1-1-onto-> (/)
15 breng 
 |-  ( ( (/) e. _V /\ (/) e. _V ) -> ( (/) ~~ (/) <-> E. f f : (/) -1-1-onto-> (/) ) )
16 11 11 15 mp2an 
 |-  ( (/) ~~ (/) <-> E. f f : (/) -1-1-onto-> (/) )
17 14 16 mpbir 
 |-  (/) ~~ (/)
18 breq1 
 |-  ( A = (/) -> ( A ~~ (/) <-> (/) ~~ (/) ) )
19 17 18 mpbiri 
 |-  ( A = (/) -> A ~~ (/) )
20 10 19 impbii 
 |-  ( A ~~ (/) <-> A = (/) )