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