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 r1dmlim 
 |-  Lim dom R1
4 limord 
 |-  ( Lim dom R1 -> Ord dom R1 )
5 3 4 ax-mp 
 |-  Ord dom R1
6 ordelon 
 |-  ( ( Ord dom R1 /\ B e. dom R1 ) -> B e. On )
7 5 6 mpan 
 |-  ( B e. dom R1 -> B e. On )
8 7 adantl 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> B e. On )
9 rankon 
 |-  ( rank ` A ) e. On
10 ontri1 
 |-  ( ( B e. On /\ ( rank ` A ) e. On ) -> ( B C_ ( rank ` A ) <-> -. ( rank ` A ) e. B ) )
11 8 9 10 sylancl 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( B C_ ( rank ` A ) <-> -. ( rank ` A ) e. B ) )
12 2 11 bitr4d 
 |-  ( ( A e. U. ( R1 " On ) /\ B e. dom R1 ) -> ( -. A e. ( R1 ` B ) <-> B C_ ( rank ` A ) ) )