Step | Hyp | Ref
| Expression |
1 | | df-scott 41527 |
. 2
⊢ Scott
{𝑥 ∣ 𝜑} = {𝑧 ∈ {𝑥 ∣ 𝜑} ∣ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)} |
2 | | df-rab 3070 |
. 2
⊢ {𝑧 ∈ {𝑥 ∣ 𝜑} ∣ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)} = {𝑧 ∣ (𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤))} |
3 | | abeq1 2870 |
. . 3
⊢ ({𝑧 ∣ (𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤))} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))} ↔ ∀𝑧((𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)) ↔ 𝑧 ∈ {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))})) |
4 | | nfsab1 2722 |
. . . . . 6
⊢
Ⅎ𝑥 𝑧 ∈ {𝑥 ∣ 𝜑} |
5 | | nfab1 2906 |
. . . . . . 7
⊢
Ⅎ𝑥{𝑥 ∣ 𝜑} |
6 | | nfv 1922 |
. . . . . . 7
⊢
Ⅎ𝑥(rank‘𝑧) ⊆ (rank‘𝑤) |
7 | 5, 6 | nfralw 3147 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤) |
8 | 4, 7 | nfan 1907 |
. . . . 5
⊢
Ⅎ𝑥(𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)) |
9 | | vex 3412 |
. . . . 5
⊢ 𝑧 ∈ V |
10 | | abid 2718 |
. . . . . . 7
⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) |
11 | | eleq1w 2820 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝑧 ∈ {𝑥 ∣ 𝜑})) |
12 | 10, 11 | bitr3id 288 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝑧 ∈ {𝑥 ∣ 𝜑})) |
13 | | df-clab 2715 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑) |
14 | | scottabf.1 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥𝜓 |
15 | | scottabf.2 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
16 | 14, 15 | sbiev 2313 |
. . . . . . . . . . . 12
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
17 | 13, 16 | bitr2i 279 |
. . . . . . . . . . 11
⊢ (𝜓 ↔ 𝑦 ∈ {𝑥 ∣ 𝜑}) |
18 | | eleq1w 2820 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑤 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝑤 ∈ {𝑥 ∣ 𝜑})) |
19 | 17, 18 | syl5bb 286 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑤 → (𝜓 ↔ 𝑤 ∈ {𝑥 ∣ 𝜑})) |
20 | 19 | adantl 485 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜓 ↔ 𝑤 ∈ {𝑥 ∣ 𝜑})) |
21 | | simpl 486 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝑥 = 𝑧) |
22 | 21 | fveq2d 6721 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (rank‘𝑥) = (rank‘𝑧)) |
23 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤) |
24 | 23 | fveq2d 6721 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (rank‘𝑦) = (rank‘𝑤)) |
25 | 22, 24 | sseq12d 3934 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((rank‘𝑥) ⊆ (rank‘𝑦) ↔ (rank‘𝑧) ⊆ (rank‘𝑤))) |
26 | 20, 25 | imbi12d 348 |
. . . . . . . 8
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ (𝑤 ∈ {𝑥 ∣ 𝜑} → (rank‘𝑧) ⊆ (rank‘𝑤)))) |
27 | 26 | cbvaldvaw 2046 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ ∀𝑤(𝑤 ∈ {𝑥 ∣ 𝜑} → (rank‘𝑧) ⊆ (rank‘𝑤)))) |
28 | | df-ral 3066 |
. . . . . . 7
⊢
(∀𝑤 ∈
{𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤) ↔ ∀𝑤(𝑤 ∈ {𝑥 ∣ 𝜑} → (rank‘𝑧) ⊆ (rank‘𝑤))) |
29 | 27, 28 | bitr4di 292 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)) ↔ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤))) |
30 | 12, 29 | anbi12d 634 |
. . . . 5
⊢ (𝑥 = 𝑧 → ((𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦))) ↔ (𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)))) |
31 | 8, 9, 30 | elabf 3584 |
. . . 4
⊢ (𝑧 ∈ {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))} ↔ (𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤))) |
32 | 31 | bicomi 227 |
. . 3
⊢ ((𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤)) ↔ 𝑧 ∈ {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))}) |
33 | 3, 32 | mpgbir 1807 |
. 2
⊢ {𝑧 ∣ (𝑧 ∈ {𝑥 ∣ 𝜑} ∧ ∀𝑤 ∈ {𝑥 ∣ 𝜑} (rank‘𝑧) ⊆ (rank‘𝑤))} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))} |
34 | 1, 2, 33 | 3eqtri 2769 |
1
⊢ Scott
{𝑥 ∣ 𝜑} = {𝑥 ∣ (𝜑 ∧ ∀𝑦(𝜓 → (rank‘𝑥) ⊆ (rank‘𝑦)))} |