Metamath Proof Explorer


Theorem bndrank

Description: Any class whose elements have bounded rank is a set. Proposition 9.19 of TakeutiZaring p. 80. (Contributed by NM, 13-Oct-2003)

Ref Expression
Assertion bndrank xOnyArankyxAV

Proof

Step Hyp Ref Expression
1 rankon rankyOn
2 1 onordi Ordranky
3 eloni xOnOrdx
4 ordsucsssuc OrdrankyOrdxrankyxsucrankysucx
5 2 3 4 sylancr xOnrankyxsucrankysucx
6 1 onsuci sucrankyOn
7 onsuc xOnsucxOn
8 r1ord3 sucrankyOnsucxOnsucrankysucxR1sucrankyR1sucx
9 6 7 8 sylancr xOnsucrankysucxR1sucrankyR1sucx
10 5 9 sylbid xOnrankyxR1sucrankyR1sucx
11 vex yV
12 11 rankid yR1sucranky
13 ssel R1sucrankyR1sucxyR1sucrankyyR1sucx
14 10 12 13 syl6mpi xOnrankyxyR1sucx
15 14 ralimdv xOnyArankyxyAyR1sucx
16 dfss3 AR1sucxyAyR1sucx
17 fvex R1sucxV
18 17 ssex AR1sucxAV
19 16 18 sylbir yAyR1sucxAV
20 15 19 syl6 xOnyArankyxAV
21 20 rexlimiv xOnyArankyxAV