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 AV
Assertion rankbnd2 BOnxArankxBrankAsucB

Proof

Step Hyp Ref Expression
1 rankr1b.1 AV
2 rankuni rankA=rankA
3 1 rankuni2 rankA=xArankx
4 2 3 eqtr3i rankA=xArankx
5 4 sseq1i rankABxArankxB
6 iunss xArankxBxArankxB
7 5 6 bitr2i xArankxBrankAB
8 rankon rankAOn
9 8 onssi rankAOn
10 eloni BOnOrdB
11 ordunisssuc rankAOnOrdBrankABrankAsucB
12 9 10 11 sylancr BOnrankABrankAsucB
13 7 12 bitrid BOnxArankxBrankAsucB