Metamath Proof Explorer

Theorem rankeq0b

Description: A set is empty iff its rank is empty. (Contributed by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion rankeq0b 
|- ( A e. U. ( R1 " On ) -> ( A = (/) <-> ( rank ` A ) = (/) ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( A = (/) -> ( rank ` A ) = ( rank ` (/) ) )
2 r1funlim 
 |-  ( Fun R1 /\ Lim dom R1 )
3 2 simpri 
 |-  Lim dom R1
4 limomss 
 |-  ( Lim dom R1 -> _om C_ dom R1 )
5 3 4 ax-mp 
 |-  _om C_ dom R1
6 peano1 
 |-  (/) e. _om
7 5 6 sselii 
 |-  (/) e. dom R1
8 rankonid 
 |-  ( (/) e. dom R1 <-> ( rank ` (/) ) = (/) )
9 7 8 mpbi 
 |-  ( rank ` (/) ) = (/)
10 1 9 eqtrdi 
 |-  ( A = (/) -> ( rank ` A ) = (/) )
11 eqimss 
 |-  ( ( rank ` A ) = (/) -> ( rank ` A ) C_ (/) )
12 11 adantl 
 |-  ( ( A e. U. ( R1 " On ) /\ ( rank ` A ) = (/) ) -> ( rank ` A ) C_ (/) )
13 simpl 
 |-  ( ( A e. U. ( R1 " On ) /\ ( rank ` A ) = (/) ) -> A e. U. ( R1 " On ) )
14 rankr1bg 
 |-  ( ( A e. U. ( R1 " On ) /\ (/) e. dom R1 ) -> ( A C_ ( R1 ` (/) ) <-> ( rank ` A ) C_ (/) ) )
15 13 7 14 sylancl 
 |-  ( ( A e. U. ( R1 " On ) /\ ( rank ` A ) = (/) ) -> ( A C_ ( R1 ` (/) ) <-> ( rank ` A ) C_ (/) ) )
16 12 15 mpbird 
 |-  ( ( A e. U. ( R1 " On ) /\ ( rank ` A ) = (/) ) -> A C_ ( R1 ` (/) ) )
17 r10 
 |-  ( R1 ` (/) ) = (/)
18 16 17 sseqtrdi 
 |-  ( ( A e. U. ( R1 " On ) /\ ( rank ` A ) = (/) ) -> A C_ (/) )
19 ss0 
 |-  ( A C_ (/) -> A = (/) )
20 18 19 syl 
 |-  ( ( A e. U. ( R1 " On ) /\ ( rank ` A ) = (/) ) -> A = (/) )
21 20 ex 
 |-  ( A e. U. ( R1 " On ) -> ( ( rank ` A ) = (/) -> A = (/) ) )
22 10 21 impbid2 
 |-  ( A e. U. ( R1 " On ) -> ( A = (/) <-> ( rank ` A ) = (/) ) )