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 ) |