Metamath Proof Explorer

Theorem rankr1ag

Description: A version of rankr1a that is suitable without assuming Regularity or Replacement. (Contributed by Mario Carneiro, 3-Jun-2013) (Revised by Mario Carneiro, 17-Nov-2014)

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

Proof

Step Hyp Ref Expression
1 rankr1ai 
 |-  ( A e. ( R1 ` B ) -> ( rank ` A ) e. B )
2 r1funlim 
 |-  ( Fun R1 /\ Lim dom R1 )
3 2 simpri 
 |-  Lim dom R1
4 limord 
 |-  ( Lim dom R1 -> Ord dom R1 )
5 3 4 ax-mp 
 |-  Ord dom R1
6 ordelord 
 |-  ( ( Ord dom R1 /\ B e. dom R1 ) -> Ord B )
7 5 6 mpan 
 |-  ( B e. dom R1 -> Ord B )
8 7 adantl 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> Ord B )
9 ordsucss 
 |-  ( Ord B -> ( ( rank ` A ) e. B -> suc ( rank ` A ) C_ B ) )
10 8 9 syl 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( ( rank ` A ) e. B -> suc ( rank ` A ) C_ B ) )
11 rankidb 
 |-  ( A e. U. ( R1 " On ) -> A e. ( R1 ` suc ( rank ` A ) ) )
12 elfvdm 
 |-  ( A e. ( R1 ` suc ( rank ` A ) ) -> suc ( rank ` A ) e. dom R1 )
13 11 12 syl 
 |-  ( A e. U. ( R1 " On ) -> suc ( rank ` A ) e. dom R1 )
14 r1ord3g 
 |-  ( ( suc ( rank ` A ) e. dom R1 /\ B e. dom R1 ) -> ( suc ( rank ` A ) C_ B -> ( R1 ` suc ( rank ` A ) ) C_ ( R1 ` B ) ) )
15 13 14 sylan 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( suc ( rank ` A ) C_ B -> ( R1 ` suc ( rank ` A ) ) C_ ( R1 ` B ) ) )
16 11 adantr 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> A e. ( R1 ` suc ( rank ` A ) ) )
17 ssel 
 |-  ( ( R1 ` suc ( rank ` A ) ) C_ ( R1 ` B ) -> ( A e. ( R1 ` suc ( rank ` A ) ) -> A e. ( R1 ` B ) ) )
18 16 17 syl5com 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( ( R1 ` suc ( rank ` A ) ) C_ ( R1 ` B ) -> A e. ( R1 ` B ) ) )
19 10 15 18 3syld 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( ( rank ` A ) e. B -> A e. ( R1 ` B ) ) )
20 1 19 impbid2 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( A e. ( R1 ` B ) <-> ( rank ` A ) e. B ) )