Metamath Proof Explorer

Theorem rankbnd2

Description: The rank of a set is bounded by the successor of a bound for its members. (Contributed by NM, 15-Sep-2006)

Ref Expression
Hypothesis rankr1b.1 
|- A e. _V
Assertion rankbnd2 
|- ( B e. On -> ( A. x e. A ( rank ` x ) C_ B <-> ( rank ` A ) C_ suc B ) )

Proof

Step Hyp Ref Expression
1 rankr1b.1 
 |-  A e. _V
2 rankuni 
 |-  ( rank ` U. A ) = U. ( rank ` A )
3 1 rankuni2 
 |-  ( rank ` U. A ) = U_ x e. A ( rank ` x )
4 2 3 eqtr3i 
 |-  U. ( rank ` A ) = U_ x e. A ( rank ` x )
5 4 sseq1i 
 |-  ( U. ( rank ` A ) C_ B <-> U_ x e. A ( rank ` x ) C_ B )
6 iunss 
 |-  ( U_ x e. A ( rank ` x ) C_ B <-> A. x e. A ( rank ` x ) C_ B )
7 5 6 bitr2i 
 |-  ( A. x e. A ( rank ` x ) C_ B <-> U. ( rank ` A ) C_ B )
8 rankon 
 |-  ( rank ` A ) e. On
9 8 onssi 
 |-  ( rank ` A ) C_ On
10 eloni 
 |-  ( B e. On -> Ord B )
11 ordunisssuc 
 |-  ( ( ( rank ` A ) C_ On /\ Ord B ) -> ( U. ( rank ` A ) C_ B <-> ( rank ` A ) C_ suc B ) )
12 9 10 11 sylancr 
 |-  ( B e. On -> ( U. ( rank ` A ) C_ B <-> ( rank ` A ) C_ suc B ) )
13 7 12 bitrid 
 |-  ( B e. On -> ( A. x e. A ( rank ` x ) C_ B <-> ( rank ` A ) C_ suc B ) )