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