Metamath Proof Explorer


Theorem rankr1bg

Description: A relationship between rank and R1 . See rankr1ag for the membership version. (Contributed by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion rankr1bg A R1 On B dom R1 A R1 B rank A B

Proof

Step Hyp Ref Expression
1 r1funlim Fun R1 Lim dom R1
2 1 simpri Lim dom R1
3 limsuc Lim dom R1 B dom R1 suc B dom R1
4 2 3 ax-mp B dom R1 suc B dom R1
5 rankr1ag A R1 On suc B dom R1 A R1 suc B rank A suc B
6 4 5 sylan2b A R1 On B dom R1 A R1 suc B rank A suc B
7 r1sucg B dom R1 R1 suc B = 𝒫 R1 B
8 7 adantl A R1 On B dom R1 R1 suc B = 𝒫 R1 B
9 8 eleq2d A R1 On B dom R1 A R1 suc B A 𝒫 R1 B
10 fvex R1 B V
11 10 elpw2 A 𝒫 R1 B A R1 B
12 9 11 bitr2di A R1 On B dom R1 A R1 B A R1 suc B
13 rankon rank A On
14 limord Lim dom R1 Ord dom R1
15 2 14 ax-mp Ord dom R1
16 ordelon Ord dom R1 B dom R1 B On
17 15 16 mpan B dom R1 B On
18 17 adantl A R1 On B dom R1 B On
19 onsssuc rank A On B On rank A B rank A suc B
20 13 18 19 sylancr A R1 On B dom R1 rank A B rank A suc B
21 6 12 20 3bitr4d A R1 On B dom R1 A R1 B rank A B