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 ( ∃ 𝑥 ∈ On ∀ 𝑦𝐴 ( rank ‘ 𝑦 ) ⊆ 𝑥𝐴 ∈ V )

Proof

Step Hyp Ref Expression
1 rankon ( rank ‘ 𝑦 ) ∈ On
2 1 onordi Ord ( rank ‘ 𝑦 )
3 eloni ( 𝑥 ∈ On → Ord 𝑥 )
4 ordsucsssuc ( ( Ord ( rank ‘ 𝑦 ) ∧ Ord 𝑥 ) → ( ( rank ‘ 𝑦 ) ⊆ 𝑥 ↔ suc ( rank ‘ 𝑦 ) ⊆ suc 𝑥 ) )
5 2 3 4 sylancr ( 𝑥 ∈ On → ( ( rank ‘ 𝑦 ) ⊆ 𝑥 ↔ suc ( rank ‘ 𝑦 ) ⊆ suc 𝑥 ) )
6 1 onsuci suc ( rank ‘ 𝑦 ) ∈ On
7 suceloni ( 𝑥 ∈ On → suc 𝑥 ∈ On )
8 r1ord3 ( ( suc ( rank ‘ 𝑦 ) ∈ On ∧ suc 𝑥 ∈ On ) → ( suc ( rank ‘ 𝑦 ) ⊆ suc 𝑥 → ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ⊆ ( 𝑅1 ‘ suc 𝑥 ) ) )
9 6 7 8 sylancr ( 𝑥 ∈ On → ( suc ( rank ‘ 𝑦 ) ⊆ suc 𝑥 → ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ⊆ ( 𝑅1 ‘ suc 𝑥 ) ) )
10 5 9 sylbid ( 𝑥 ∈ On → ( ( rank ‘ 𝑦 ) ⊆ 𝑥 → ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ⊆ ( 𝑅1 ‘ suc 𝑥 ) ) )
11 vex 𝑦 ∈ V
12 11 rankid 𝑦 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) )
13 ssel ( ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) ⊆ ( 𝑅1 ‘ suc 𝑥 ) → ( 𝑦 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑦 ) ) → 𝑦 ∈ ( 𝑅1 ‘ suc 𝑥 ) ) )
14 10 12 13 syl6mpi ( 𝑥 ∈ On → ( ( rank ‘ 𝑦 ) ⊆ 𝑥𝑦 ∈ ( 𝑅1 ‘ suc 𝑥 ) ) )
15 14 ralimdv ( 𝑥 ∈ On → ( ∀ 𝑦𝐴 ( rank ‘ 𝑦 ) ⊆ 𝑥 → ∀ 𝑦𝐴 𝑦 ∈ ( 𝑅1 ‘ suc 𝑥 ) ) )
16 dfss3 ( 𝐴 ⊆ ( 𝑅1 ‘ suc 𝑥 ) ↔ ∀ 𝑦𝐴 𝑦 ∈ ( 𝑅1 ‘ suc 𝑥 ) )
17 fvex ( 𝑅1 ‘ suc 𝑥 ) ∈ V
18 17 ssex ( 𝐴 ⊆ ( 𝑅1 ‘ suc 𝑥 ) → 𝐴 ∈ V )
19 16 18 sylbir ( ∀ 𝑦𝐴 𝑦 ∈ ( 𝑅1 ‘ suc 𝑥 ) → 𝐴 ∈ V )
20 15 19 syl6 ( 𝑥 ∈ On → ( ∀ 𝑦𝐴 ( rank ‘ 𝑦 ) ⊆ 𝑥𝐴 ∈ V ) )
21 20 rexlimiv ( ∃ 𝑥 ∈ On ∀ 𝑦𝐴 ( rank ‘ 𝑦 ) ⊆ 𝑥𝐴 ∈ V )