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		r1dmlim	⊢ Lim dom 𝑅1
3		limomss	⊢ ( Lim dom 𝑅1 → ω ⊆ dom 𝑅1 )
4	2 3	ax-mp	⊢ ω ⊆ dom 𝑅1
5		peano1	⊢ ∅ ∈ ω
6	4 5	sselii	⊢ ∅ ∈ dom 𝑅1
7		rankonid	⊢ ( ∅ ∈ dom 𝑅1 ↔ ( rank ‘ ∅ ) = ∅ )
8	6 7	mpbi	⊢ ( rank ‘ ∅ ) = ∅
9	1 8	eqtrdi	⊢ ( 𝐴 = ∅ → ( rank ‘ 𝐴 ) = ∅ )
10		eqimss	⊢ ( ( rank ‘ 𝐴 ) = ∅ → ( rank ‘ 𝐴 ) ⊆ ∅ )
11	10	adantl	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝐴 ) = ∅ ) → ( rank ‘ 𝐴 ) ⊆ ∅ )
12		simpl	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝐴 ) = ∅ ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
13		rankr1bg	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ∅ ∈ dom 𝑅1 ) → ( 𝐴 ⊆ ( 𝑅1 ‘ ∅ ) ↔ ( rank ‘ 𝐴 ) ⊆ ∅ ) )
14	12 6 13	sylancl	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝐴 ) = ∅ ) → ( 𝐴 ⊆ ( 𝑅1 ‘ ∅ ) ↔ ( rank ‘ 𝐴 ) ⊆ ∅ ) )
15	11 14	mpbird	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝐴 ) = ∅ ) → 𝐴 ⊆ ( 𝑅1 ‘ ∅ ) )
16		r10	⊢ ( 𝑅1 ‘ ∅ ) = ∅
17	15 16	sseqtrdi	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝐴 ) = ∅ ) → 𝐴 ⊆ ∅ )
18		ss0	⊢ ( 𝐴 ⊆ ∅ → 𝐴 = ∅ )
19	17 18	syl	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ( rank ‘ 𝐴 ) = ∅ ) → 𝐴 = ∅ )
20	19	ex	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( ( rank ‘ 𝐴 ) = ∅ → 𝐴 = ∅ ) )
21	9 20	impbid2	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝐴 = ∅ ↔ ( rank ‘ 𝐴 ) = ∅ ) )