Metamath Proof Explorer

Theorem ensucne0OLD

Description: A class equinumerous to a successor is never empty. (Contributed by RP, 11-Nov-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ensucne0OLD 
|- ( A ~~ suc B -> A =/= (/) )

Proof

Step Hyp Ref Expression
1 encv 
 |-  ( A ~~ suc B -> ( A e. _V /\ suc B e. _V ) )
2 1 simprd 
 |-  ( A ~~ suc B -> suc B e. _V )
3 en0 
 |-  ( A ~~ (/) <-> A = (/) )
4 3 biimpri 
 |-  ( A = (/) -> A ~~ (/) )
5 4 a1i 
 |-  ( suc B e. _V -> ( A = (/) -> A ~~ (/) ) )
6 nsuceq0 
 |-  suc B =/= (/)
7 0sdomg 
 |-  ( suc B e. _V -> ( (/) ~< suc B <-> suc B =/= (/) ) )
8 6 7 mpbiri 
 |-  ( suc B e. _V -> (/) ~< suc B )
9 5 8 jctird 
 |-  ( suc B e. _V -> ( A = (/) -> ( A ~~ (/) /\ (/) ~< suc B ) ) )
10 ensdomtr 
 |-  ( ( A ~~ (/) /\ (/) ~< suc B ) -> A ~< suc B )
11 sdomnen 
 |-  ( A ~< suc B -> -. A ~~ suc B )
12 10 11 syl 
 |-  ( ( A ~~ (/) /\ (/) ~< suc B ) -> -. A ~~ suc B )
13 9 12 syl6 
 |-  ( suc B e. _V -> ( A = (/) -> -. A ~~ suc B ) )
14 13 necon2ad 
 |-  ( suc B e. _V -> ( A ~~ suc B -> A =/= (/) ) )
15 2 14 mpcom 
 |-  ( A ~~ suc B -> A =/= (/) )