Metamath Proof Explorer


Theorem ensn1OLD

Description: Obsolete version of ensn1 as of 23-Sep-2024. (Contributed by NM, 4-Nov-2002) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis ensn1OLD.1
|- A e. _V
Assertion ensn1OLD
|- { A } ~~ 1o

Proof

Step Hyp Ref Expression
1 ensn1OLD.1
 |-  A e. _V
2 snex
 |-  { <. A , (/) >. } e. _V
3 f1oeq1
 |-  ( f = { <. A , (/) >. } -> ( f : { A } -1-1-onto-> { (/) } <-> { <. A , (/) >. } : { A } -1-1-onto-> { (/) } ) )
4 0ex
 |-  (/) e. _V
5 1 4 f1osn
 |-  { <. A , (/) >. } : { A } -1-1-onto-> { (/) }
6 2 3 5 ceqsexv2d
 |-  E. f f : { A } -1-1-onto-> { (/) }
7 bren
 |-  ( { A } ~~ { (/) } <-> E. f f : { A } -1-1-onto-> { (/) } )
8 6 7 mpbir
 |-  { A } ~~ { (/) }
9 df1o2
 |-  1o = { (/) }
10 8 9 breqtrri
 |-  { A } ~~ 1o