Theorem rankdmr1

Description: A rank is a member of the cumulative hierarchy. (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		r1funlim	⊢ ( Fun 𝑅1 ∧ Lim dom 𝑅1 )
5	4	simpri	⊢ Lim dom 𝑅1
6		limsuc	⊢ ( Lim dom 𝑅1 → ( ( rank ‘ 𝐴 ) ∈ dom 𝑅1 ↔ suc ( rank ‘ 𝐴 ) ∈ dom 𝑅1 ) )
7	5 6	ax-mp	⊢ ( ( rank ‘ 𝐴 ) ∈ dom 𝑅1 ↔ suc ( rank ‘ 𝐴 ) ∈ dom 𝑅1 )
8	3 7	sylibr	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝐴 ) ∈ dom 𝑅1 )
9		rankvaln	⊢ ( ¬ 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝐴 ) = ∅ )
10		limomss	⊢ ( Lim dom 𝑅1 → ω ⊆ dom 𝑅1 )
11	5 10	ax-mp	⊢ ω ⊆ dom 𝑅1
12		peano1	⊢ ∅ ∈ ω
13	11 12	sselii	⊢ ∅ ∈ dom 𝑅1
14	9 13	eqeltrdi	⊢ ( ¬ 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝐴 ) ∈ dom 𝑅1 )
15	8 14	pm2.61i	⊢ ( rank ‘ 𝐴 ) ∈ dom 𝑅1