Metamath Proof Explorer


Theorem en0OLD

Description: Obsolete version of en0 as of 23-Sep-2024. (Contributed by NM, 27-May-1998) Avoid ax-pow . (Revised by BTernaryTau, 31-Jul-2024) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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