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 e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( A C_ ( R1 ` B ) <-> ( rank ` A ) C_ 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 e. dom R1 <-> suc B e. dom R1 ) )
4 2 3 ax-mp 
 |-  ( B e. dom R1 <-> suc B e. dom R1 )
5 rankr1ag 
 |-  ( ( A e. U. ( R1 " On ) /\ suc B e. dom R1 ) -> ( A e. ( R1 ` suc B ) <-> ( rank ` A ) e. suc B ) )
6 4 5 sylan2b 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( A e. ( R1 ` suc B ) <-> ( rank ` A ) e. suc B ) )
7 r1sucg 
 |-  ( B e. dom R1 -> ( R1 ` suc B ) = ~P ( R1 ` B ) )
8 7 adantl 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( R1 ` suc B ) = ~P ( R1 ` B ) )
9 8 eleq2d 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( A e. ( R1 ` suc B ) <-> A e. ~P ( R1 ` B ) ) )
10 fvex 
 |-  ( R1 ` B ) e. _V
11 10 elpw2 
 |-  ( A e. ~P ( R1 ` B ) <-> A C_ ( R1 ` B ) )
12 9 11 bitr2di 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( A C_ ( R1 ` B ) <-> A e. ( R1 ` suc B ) ) )
13 rankon 
 |-  ( rank ` A ) e. On
14 limord 
 |-  ( Lim dom R1 -> Ord dom R1 )
15 2 14 ax-mp 
 |-  Ord dom R1
16 ordelon 
 |-  ( ( Ord dom R1 /\ B e. dom R1 ) -> B e. On )
17 15 16 mpan 
 |-  ( B e. dom R1 -> B e. On )
18 17 adantl 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> B e. On )
19 onsssuc 
 |-  ( ( ( rank ` A ) e. On /\ B e. On ) -> ( ( rank ` A ) C_ B <-> ( rank ` A ) e. suc B ) )
20 13 18 19 sylancr 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( ( rank ` A ) C_ B <-> ( rank ` A ) e. suc B ) )
21 6 12 20 3bitr4d 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( A C_ ( R1 ` B ) <-> ( rank ` A ) C_ B ) )