Theorem r1rankcld

Description: Any rank of the cumulative hierarchy is closed under the rank function. (Contributed by Rohan Ridenour, 11-Aug-2023)

	Ref	Expression
Hypothesis	r1rankcld.1	⊢ ( 𝜑 → 𝐴 ∈ ( 𝑅1 ‘ 𝑅 ) )
Assertion	r1rankcld	⊢ ( 𝜑 → ( rank ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		r1rankcld.1	⊢ ( 𝜑 → 𝐴 ∈ ( 𝑅1 ‘ 𝑅 ) )
2		onssr1	⊢ ( 𝑅 ∈ dom 𝑅1 → 𝑅 ⊆ ( 𝑅1 ‘ 𝑅 ) )
3	2	adantl	⊢ ( ( 𝜑 ∧ 𝑅 ∈ dom 𝑅1 ) → 𝑅 ⊆ ( 𝑅1 ‘ 𝑅 ) )
4		rankr1ai	⊢ ( 𝐴 ∈ ( 𝑅1 ‘ 𝑅 ) → ( rank ‘ 𝐴 ) ∈ 𝑅 )
5	1 4	syl	⊢ ( 𝜑 → ( rank ‘ 𝐴 ) ∈ 𝑅 )
6	5	adantr	⊢ ( ( 𝜑 ∧ 𝑅 ∈ dom 𝑅1 ) → ( rank ‘ 𝐴 ) ∈ 𝑅 )
7	3 6	sseldd	⊢ ( ( 𝜑 ∧ 𝑅 ∈ dom 𝑅1 ) → ( rank ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝑅 ) )
8	1	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ∈ dom 𝑅1 ) → 𝐴 ∈ ( 𝑅1 ‘ 𝑅 ) )
9		noel	⊢ ¬ 𝐴 ∈ ∅
10	9	a1i	⊢ ( ¬ 𝑅 ∈ dom 𝑅1 → ¬ 𝐴 ∈ ∅ )
11		ndmfv	⊢ ( ¬ 𝑅 ∈ dom 𝑅1 → ( 𝑅1 ‘ 𝑅 ) = ∅ )
12	10 11	neleqtrrd	⊢ ( ¬ 𝑅 ∈ dom 𝑅1 → ¬ 𝐴 ∈ ( 𝑅1 ‘ 𝑅 ) )
13	12	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ∈ dom 𝑅1 ) → ¬ 𝐴 ∈ ( 𝑅1 ‘ 𝑅 ) )
14	8 13	pm2.21dd	⊢ ( ( 𝜑 ∧ ¬ 𝑅 ∈ dom 𝑅1 ) → ( rank ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝑅 ) )
15	7 14	pm2.61dan	⊢ ( 𝜑 → ( rank ‘ 𝐴 ) ∈ ( 𝑅1 ‘ 𝑅 ) )