Theorem rankdmr1

Description: A rank is a member of the cumulative hierarchy of sets. (Contributed by Mario Carneiro, 17-Nov-2014)

	Ref	Expression
Assertion	rankdmr1	⊢ ( rank ‘ 𝐴 ) ∈ dom 𝑅1

Proof

Step	Hyp	Ref	Expression
1		rankidb	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
2		elfvdm	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) → suc ( rank ‘ 𝐴 ) ∈ dom 𝑅1 )
3	1 2	syl	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → suc ( rank ‘ 𝐴 ) ∈ dom 𝑅1 )
4		r1dmlim	⊢ Lim dom 𝑅1
5		limsuc	⊢ ( Lim dom 𝑅1 → ( ( rank ‘ 𝐴 ) ∈ dom 𝑅1 ↔ suc ( rank ‘ 𝐴 ) ∈ dom 𝑅1 ) )
6	4 5	ax-mp	⊢ ( ( rank ‘ 𝐴 ) ∈ dom 𝑅1 ↔ suc ( rank ‘ 𝐴 ) ∈ dom 𝑅1 )
7	3 6	sylibr	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝐴 ) ∈ dom 𝑅1 )
8		rankvaln	⊢ ( ¬ 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝐴 ) = ∅ )
9		limomss	⊢ ( Lim dom 𝑅1 → ω ⊆ dom 𝑅1 )
10	4 9	ax-mp	⊢ ω ⊆ dom 𝑅1
11		peano1	⊢ ∅ ∈ ω
12	10 11	sselii	⊢ ∅ ∈ dom 𝑅1
13	8 12	eqeltrdi	⊢ ( ¬ 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝐴 ) ∈ dom 𝑅1 )
14	7 13	pm2.61i	⊢ ( rank ‘ 𝐴 ) ∈ dom 𝑅1