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 ( 𝐴 ( 𝑅1 “ On ) → ( 𝐴 = ∅ ↔ ( rank ‘ 𝐴 ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 fveq2 ( 𝐴 = ∅ → ( rank ‘ 𝐴 ) = ( rank ‘ ∅ ) )
2 r1funlim ( Fun 𝑅1 ∧ Lim dom 𝑅1 )
3 2 simpri Lim dom 𝑅1
4 limomss ( Lim dom 𝑅1 → ω ⊆ dom 𝑅1 )
5 3 4 ax-mp ω ⊆ dom 𝑅1
6 peano1 ∅ ∈ ω
7 5 6 sselii ∅ ∈ dom 𝑅1
8 rankonid ( ∅ ∈ dom 𝑅1 ↔ ( rank ‘ ∅ ) = ∅ )
9 7 8 mpbi ( rank ‘ ∅ ) = ∅
10 1 9 eqtrdi ( 𝐴 = ∅ → ( rank ‘ 𝐴 ) = ∅ )
11 eqimss ( ( rank ‘ 𝐴 ) = ∅ → ( rank ‘ 𝐴 ) ⊆ ∅ )
12 11 adantl ( ( 𝐴 ( 𝑅1 “ On ) ∧ ( rank ‘ 𝐴 ) = ∅ ) → ( rank ‘ 𝐴 ) ⊆ ∅ )
13 simpl ( ( 𝐴 ( 𝑅1 “ On ) ∧ ( rank ‘ 𝐴 ) = ∅ ) → 𝐴 ( 𝑅1 “ On ) )
14 rankr1bg ( ( 𝐴 ( 𝑅1 “ On ) ∧ ∅ ∈ dom 𝑅1 ) → ( 𝐴 ⊆ ( 𝑅1 ‘ ∅ ) ↔ ( rank ‘ 𝐴 ) ⊆ ∅ ) )
15 13 7 14 sylancl ( ( 𝐴 ( 𝑅1 “ On ) ∧ ( rank ‘ 𝐴 ) = ∅ ) → ( 𝐴 ⊆ ( 𝑅1 ‘ ∅ ) ↔ ( rank ‘ 𝐴 ) ⊆ ∅ ) )
16 12 15 mpbird ( ( 𝐴 ( 𝑅1 “ On ) ∧ ( rank ‘ 𝐴 ) = ∅ ) → 𝐴 ⊆ ( 𝑅1 ‘ ∅ ) )
17 r10 ( 𝑅1 ‘ ∅ ) = ∅
18 16 17 sseqtrdi ( ( 𝐴 ( 𝑅1 “ On ) ∧ ( rank ‘ 𝐴 ) = ∅ ) → 𝐴 ⊆ ∅ )
19 ss0 ( 𝐴 ⊆ ∅ → 𝐴 = ∅ )
20 18 19 syl ( ( 𝐴 ( 𝑅1 “ On ) ∧ ( rank ‘ 𝐴 ) = ∅ ) → 𝐴 = ∅ )
21 20 ex ( 𝐴 ( 𝑅1 “ On ) → ( ( rank ‘ 𝐴 ) = ∅ → 𝐴 = ∅ ) )
22 10 21 impbid2 ( 𝐴 ( 𝑅1 “ On ) → ( 𝐴 = ∅ ↔ ( rank ‘ 𝐴 ) = ∅ ) )