Metamath Proof Explorer


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 φ A R1 R
Assertion r1rankcld φ rank A R1 R

Proof

Step Hyp Ref Expression
1 r1rankcld.1 φ A R1 R
2 onssr1 R dom R1 R R1 R
3 2 adantl φ R dom R1 R R1 R
4 rankr1ai A R1 R rank A R
5 1 4 syl φ rank A R
6 5 adantr φ R dom R1 rank A R
7 3 6 sseldd φ R dom R1 rank A R1 R
8 1 adantr φ ¬ R dom R1 A R1 R
9 noel ¬ A
10 9 a1i ¬ R dom R1 ¬ A
11 ndmfv ¬ R dom R1 R1 R =
12 10 11 neleqtrrd ¬ R dom R1 ¬ A R1 R
13 12 adantl φ ¬ R dom R1 ¬ A R1 R
14 8 13 pm2.21dd φ ¬ R dom R1 rank A R1 R
15 7 14 pm2.61dan φ rank A R1 R