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