Metamath Proof Explorer

Theorem rankr1c

Description: A relationship between the rank function and the cumulative hierarchy of sets function R1 . Proposition 9.15(2) of TakeutiZaring p. 79. (Contributed by Mario Carneiro, 22-Mar-2013) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion rankr1c 
|- ( A e. U. ( R1 " On ) -> ( B = ( rank ` A ) <-> ( -. A e. ( R1 ` B ) /\ A e. ( R1 ` suc B ) ) ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( B = ( rank ` A ) -> B = ( rank ` A ) )
2 rankdmr1 
 |-  ( rank ` A ) e. dom R1
3 1 2 eqeltrdi 
 |-  ( B = ( rank ` A ) -> B e. dom R1 )
4 3 a1i 
 |-  ( A e. U. ( R1 " On ) -> ( B = ( rank ` A ) -> B e. dom R1 ) )
5 elfvdm 
 |-  ( A e. ( R1 ` suc B ) -> suc B e. dom R1 )
6 r1funlim 
 |-  ( Fun R1 /\ Lim dom R1 )
7 6 simpri 
 |-  Lim dom R1
8 limsuc 
 |-  ( Lim dom R1 -> ( B e. dom R1 <-> suc B e. dom R1 ) )
9 7 8 ax-mp 
 |-  ( B e. dom R1 <-> suc B e. dom R1 )
10 5 9 sylibr 
 |-  ( A e. ( R1 ` suc B ) -> B e. dom R1 )
11 10 adantl 
 |-  ( ( -. A e. ( R1 ` B ) /\ A e. ( R1 ` suc B ) ) -> B e. dom R1 )
12 11 a1i 
 |-  ( A e. U. ( R1 " On ) -> ( ( -. A e. ( R1 ` B ) /\ A e. ( R1 ` suc B ) ) -> B e. dom R1 ) )
13 eqss 
 |-  ( B = ( rank ` A ) <-> ( B C_ ( rank ` A ) /\ ( rank ` A ) C_ B ) )
14 rankr1clem 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( -. A e. ( R1 ` B ) <-> B C_ ( rank ` A ) ) )
15 rankr1ag 
 |-  ( ( A e. U. ( R1 " On ) /\ suc B e. dom R1 ) -> ( A e. ( R1 ` suc B ) <-> ( rank ` A ) e. suc B ) )
16 9 15 sylan2b 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( A e. ( R1 ` suc B ) <-> ( rank ` A ) e. suc B ) )
17 rankon 
 |-  ( rank ` A ) e. On
18 limord 
 |-  ( Lim dom R1 -> Ord dom R1 )
19 7 18 ax-mp 
 |-  Ord dom R1
20 ordelon 
 |-  ( ( Ord dom R1 /\ B e. dom R1 ) -> B e. On )
21 19 20 mpan 
 |-  ( B e. dom R1 -> B e. On )
22 21 adantl 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> B e. On )
23 onsssuc 
 |-  ( ( ( rank ` A ) e. On /\ B e. On ) -> ( ( rank ` A ) C_ B <-> ( rank ` A ) e. suc B ) )
24 17 22 23 sylancr 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( ( rank ` A ) C_ B <-> ( rank ` A ) e. suc B ) )
25 16 24 bitr4d 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( A e. ( R1 ` suc B ) <-> ( rank ` A ) C_ B ) )
26 14 25 anbi12d 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( ( -. A e. ( R1 ` B ) /\ A e. ( R1 ` suc B ) ) <-> ( B C_ ( rank ` A ) /\ ( rank ` A ) C_ B ) ) )
27 13 26 bitr4id 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( B = ( rank ` A ) <-> ( -. A e. ( R1 ` B ) /\ A e. ( R1 ` suc B ) ) ) )
28 27 ex 
 |-  ( A e. U. ( R1 " On ) -> ( B e. dom R1 -> ( B = ( rank ` A ) <-> ( -. A e. ( R1 ` B ) /\ A e. ( R1 ` suc B ) ) ) ) )
29 4 12 28 pm5.21ndd 
 |-  ( A e. U. ( R1 " On ) -> ( B = ( rank ` A ) <-> ( -. A e. ( R1 ` B ) /\ A e. ( R1 ` suc B ) ) ) )