Step | Hyp | Ref
| Expression |
1 | | 0ex 5301 |
. . . 4
⊢ ∅
∈ V |
2 | | eleq1 2817 |
. . . 4
⊢ (𝐴 = ∅ → (𝐴 ∈ V ↔ ∅ ∈
V)) |
3 | 1, 2 | mpbiri 258 |
. . 3
⊢ (𝐴 = ∅ → 𝐴 ∈ V) |
4 | | rabexg 5327 |
. . 3
⊢ (𝐴 ∈ V → {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ∈ V) |
5 | 3, 4 | syl 17 |
. 2
⊢ (𝐴 = ∅ → {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ∈ V) |
6 | | neq0 4341 |
. . 3
⊢ (¬
𝐴 = ∅ ↔
∃𝑦 𝑦 ∈ 𝐴) |
7 | | nfra1 3277 |
. . . . . 6
⊢
Ⅎ𝑦∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦) |
8 | | nfcv 2899 |
. . . . . 6
⊢
Ⅎ𝑦𝐴 |
9 | 7, 8 | nfrabw 3464 |
. . . . 5
⊢
Ⅎ𝑦{𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} |
10 | 9 | nfel1 2915 |
. . . 4
⊢
Ⅎ𝑦{𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ∈ V |
11 | | rsp 3240 |
. . . . . . . 8
⊢
(∀𝑦 ∈
𝐴 (rank‘𝑥) ⊆ (rank‘𝑦) → (𝑦 ∈ 𝐴 → (rank‘𝑥) ⊆ (rank‘𝑦))) |
12 | 11 | com12 32 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐴 → (∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦) → (rank‘𝑥) ⊆ (rank‘𝑦))) |
13 | 12 | adantr 480 |
. . . . . 6
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦) → (rank‘𝑥) ⊆ (rank‘𝑦))) |
14 | 13 | ss2rabdv 4069 |
. . . . 5
⊢ (𝑦 ∈ 𝐴 → {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ⊆ {𝑥 ∈ 𝐴 ∣ (rank‘𝑥) ⊆ (rank‘𝑦)}) |
15 | | rankon 9812 |
. . . . . . . 8
⊢
(rank‘𝑦)
∈ On |
16 | | fveq2 6891 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑤 → (rank‘𝑥) = (rank‘𝑤)) |
17 | 16 | sseq1d 4009 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑤 → ((rank‘𝑥) ⊆ (rank‘𝑦) ↔ (rank‘𝑤) ⊆ (rank‘𝑦))) |
18 | 17 | elrab 3681 |
. . . . . . . . . 10
⊢ (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (rank‘𝑥) ⊆ (rank‘𝑦)} ↔ (𝑤 ∈ 𝐴 ∧ (rank‘𝑤) ⊆ (rank‘𝑦))) |
19 | 18 | simprbi 496 |
. . . . . . . . 9
⊢ (𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (rank‘𝑥) ⊆ (rank‘𝑦)} → (rank‘𝑤) ⊆ (rank‘𝑦)) |
20 | 19 | rgen 3059 |
. . . . . . . 8
⊢
∀𝑤 ∈
{𝑥 ∈ 𝐴 ∣ (rank‘𝑥) ⊆ (rank‘𝑦)} (rank‘𝑤) ⊆ (rank‘𝑦) |
21 | | sseq2 4004 |
. . . . . . . . . 10
⊢ (𝑧 = (rank‘𝑦) → ((rank‘𝑤) ⊆ 𝑧 ↔ (rank‘𝑤) ⊆ (rank‘𝑦))) |
22 | 21 | ralbidv 3173 |
. . . . . . . . 9
⊢ (𝑧 = (rank‘𝑦) → (∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (rank‘𝑥) ⊆ (rank‘𝑦)} (rank‘𝑤) ⊆ 𝑧 ↔ ∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (rank‘𝑥) ⊆ (rank‘𝑦)} (rank‘𝑤) ⊆ (rank‘𝑦))) |
23 | 22 | rspcev 3608 |
. . . . . . . 8
⊢
(((rank‘𝑦)
∈ On ∧ ∀𝑤
∈ {𝑥 ∈ 𝐴 ∣ (rank‘𝑥) ⊆ (rank‘𝑦)} (rank‘𝑤) ⊆ (rank‘𝑦)) → ∃𝑧 ∈ On ∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (rank‘𝑥) ⊆ (rank‘𝑦)} (rank‘𝑤) ⊆ 𝑧) |
24 | 15, 20, 23 | mp2an 691 |
. . . . . . 7
⊢
∃𝑧 ∈ On
∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (rank‘𝑥) ⊆ (rank‘𝑦)} (rank‘𝑤) ⊆ 𝑧 |
25 | | bndrank 9858 |
. . . . . . 7
⊢
(∃𝑧 ∈ On
∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ (rank‘𝑥) ⊆ (rank‘𝑦)} (rank‘𝑤) ⊆ 𝑧 → {𝑥 ∈ 𝐴 ∣ (rank‘𝑥) ⊆ (rank‘𝑦)} ∈ V) |
26 | 24, 25 | ax-mp 5 |
. . . . . 6
⊢ {𝑥 ∈ 𝐴 ∣ (rank‘𝑥) ⊆ (rank‘𝑦)} ∈ V |
27 | 26 | ssex 5315 |
. . . . 5
⊢ ({𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ⊆ {𝑥 ∈ 𝐴 ∣ (rank‘𝑥) ⊆ (rank‘𝑦)} → {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ∈ V) |
28 | 14, 27 | syl 17 |
. . . 4
⊢ (𝑦 ∈ 𝐴 → {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ∈ V) |
29 | 10, 28 | exlimi 2206 |
. . 3
⊢
(∃𝑦 𝑦 ∈ 𝐴 → {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ∈ V) |
30 | 6, 29 | sylbi 216 |
. 2
⊢ (¬
𝐴 = ∅ → {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ∈ V) |
31 | 5, 30 | pm2.61i 182 |
1
⊢ {𝑥 ∈ 𝐴 ∣ ∀𝑦 ∈ 𝐴 (rank‘𝑥) ⊆ (rank‘𝑦)} ∈ V |