This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝐴 ) = ∅ ) )