Metamath Proof Explorer

Theorem rankr1clem

Description: Lemma for rankr1c . (Contributed by NM, 6-Oct-2003) (Revised by Mario Carneiro, 17-Nov-2014)

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

Proof

Step Hyp Ref Expression
1 rankr1ag 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( A e. ( R1 ` B ) <-> ( rank ` A ) e. B ) )
2 1 notbid 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( -. A e. ( R1 ` B ) <-> -. ( rank ` A ) e. B ) )
3 r1funlim 
 |-  ( Fun R1 /\ Lim dom R1 )
4 3 simpri 
 |-  Lim dom R1
5 limord 
 |-  ( Lim dom R1 -> Ord dom R1 )
6 4 5 ax-mp 
 |-  Ord dom R1
7 ordelon 
 |-  ( ( Ord dom R1 /\ B e. dom R1 ) -> B e. On )
8 6 7 mpan 
 |-  ( B e. dom R1 -> B e. On )
9 8 adantl 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> B e. On )
10 rankon 
 |-  ( rank ` A ) e. On
11 ontri1 
 |-  ( ( B e. On /\ ( rank ` A ) e. On ) -> ( B C_ ( rank ` A ) <-> -. ( rank ` A ) e. B ) )
12 9 10 11 sylancl 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( B C_ ( rank ` A ) <-> -. ( rank ` A ) e. B ) )
13 2 12 bitr4d 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( -. A e. ( R1 ` B ) <-> B C_ ( rank ` A ) ) )