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 )