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 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 ω dom R1
5 3 4 ax-mp ω dom R1
6 peano1 ω
7 5 6 sselii dom R1
8 rankonid dom R1 rank =
9 7 8 mpbi rank =
10 1 9 eqtrdi A = rank A =
11 eqimss rank A = rank A
12 11 adantl A R1 On rank A = rank A
13 simpl A R1 On rank A = A R1 On
14 rankr1bg A R1 On dom R1 A R1 rank A
15 13 7 14 sylancl A R1 On rank A = A R1 rank A
16 12 15 mpbird A R1 On rank A = A R1
17 r10 R1 =
18 16 17 sseqtrdi A R1 On rank A = A
19 ss0 A A =
20 18 19 syl A R1 On rank A = A =
21 20 ex A R1 On rank A = A =
22 10 21 impbid2 A R1 On A = rank A =