Step | Hyp | Ref
| Expression |
1 | | onelon 6098 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ On ∧ 𝑦 ∈ 𝑧) → 𝑦 ∈ On) |
2 | | vex 3443 |
. . . . . . . . . . . . . 14
⊢ 𝑧 ∈ V |
3 | | onelss 6115 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ On → (𝑦 ∈ 𝑧 → 𝑦 ⊆ 𝑧)) |
4 | 3 | imp 407 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ On ∧ 𝑦 ∈ 𝑧) → 𝑦 ⊆ 𝑧) |
5 | | ssdomg 8410 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ V → (𝑦 ⊆ 𝑧 → 𝑦 ≼ 𝑧)) |
6 | 2, 4, 5 | mpsyl 68 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ On ∧ 𝑦 ∈ 𝑧) → 𝑦 ≼ 𝑧) |
7 | 1, 6 | jca 512 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ On ∧ 𝑦 ∈ 𝑧) → (𝑦 ∈ On ∧ 𝑦 ≼ 𝑧)) |
8 | | domsdomtr 8506 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ≼ 𝑧 ∧ 𝑧 ≺ 𝐴) → 𝑦 ≺ 𝐴) |
9 | 8 | anim2i 616 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ On ∧ (𝑦 ≼ 𝑧 ∧ 𝑧 ≺ 𝐴)) → (𝑦 ∈ On ∧ 𝑦 ≺ 𝐴)) |
10 | 9 | anassrs 468 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ On ∧ 𝑦 ≼ 𝑧) ∧ 𝑧 ≺ 𝐴) → (𝑦 ∈ On ∧ 𝑦 ≺ 𝐴)) |
11 | 7, 10 | sylan 580 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ On ∧ 𝑦 ∈ 𝑧) ∧ 𝑧 ≺ 𝐴) → (𝑦 ∈ On ∧ 𝑦 ≺ 𝐴)) |
12 | 11 | exp31 420 |
. . . . . . . . . 10
⊢ (𝑧 ∈ On → (𝑦 ∈ 𝑧 → (𝑧 ≺ 𝐴 → (𝑦 ∈ On ∧ 𝑦 ≺ 𝐴)))) |
13 | 12 | com12 32 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝑧 → (𝑧 ∈ On → (𝑧 ≺ 𝐴 → (𝑦 ∈ On ∧ 𝑦 ≺ 𝐴)))) |
14 | 13 | impd 411 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝑧 → ((𝑧 ∈ On ∧ 𝑧 ≺ 𝐴) → (𝑦 ∈ On ∧ 𝑦 ≺ 𝐴))) |
15 | | breq1 4971 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (𝑥 ≺ 𝐴 ↔ 𝑧 ≺ 𝐴)) |
16 | 15 | elrab 3621 |
. . . . . . . 8
⊢ (𝑧 ∈ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ↔ (𝑧 ∈ On ∧ 𝑧 ≺ 𝐴)) |
17 | | breq1 4971 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥 ≺ 𝐴 ↔ 𝑦 ≺ 𝐴)) |
18 | 17 | elrab 3621 |
. . . . . . . 8
⊢ (𝑦 ∈ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ↔ (𝑦 ∈ On ∧ 𝑦 ≺ 𝐴)) |
19 | 14, 16, 18 | 3imtr4g 297 |
. . . . . . 7
⊢ (𝑦 ∈ 𝑧 → (𝑧 ∈ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} → 𝑦 ∈ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴})) |
20 | 19 | imp 407 |
. . . . . 6
⊢ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴}) → 𝑦 ∈ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴}) |
21 | 20 | gen2 1782 |
. . . . 5
⊢
∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴}) → 𝑦 ∈ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴}) |
22 | | dftr2 5072 |
. . . . 5
⊢ (Tr
{𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ↔ ∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴}) → 𝑦 ∈ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴})) |
23 | 21, 22 | mpbir 232 |
. . . 4
⊢ Tr {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} |
24 | | ssrab2 3983 |
. . . 4
⊢ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ⊆ On |
25 | | ordon 7361 |
. . . 4
⊢ Ord
On |
26 | | trssord 6090 |
. . . 4
⊢ ((Tr
{𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ∧ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ⊆ On ∧ Ord On) → Ord {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴}) |
27 | 23, 24, 25, 26 | mp3an 1453 |
. . 3
⊢ Ord
{𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} |
28 | | hartogs 8861 |
. . . 4
⊢ (𝐴 ∈ V → {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ On) |
29 | | sdomdom 8392 |
. . . . . . 7
⊢ (𝑥 ≺ 𝐴 → 𝑥 ≼ 𝐴) |
30 | 29 | a1i 11 |
. . . . . 6
⊢ (𝑥 ∈ On → (𝑥 ≺ 𝐴 → 𝑥 ≼ 𝐴)) |
31 | 30 | ss2rabi 3980 |
. . . . 5
⊢ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ⊆ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} |
32 | | ssexg 5125 |
. . . . 5
⊢ (({𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ⊆ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∧ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ On) → {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ∈ V) |
33 | 31, 32 | mpan 686 |
. . . 4
⊢ ({𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ On → {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ∈ V) |
34 | | elong 6081 |
. . . 4
⊢ ({𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ∈ V → ({𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ∈ On ↔ Ord {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴})) |
35 | 28, 33, 34 | 3syl 18 |
. . 3
⊢ (𝐴 ∈ V → ({𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ∈ On ↔ Ord {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴})) |
36 | 27, 35 | mpbiri 259 |
. 2
⊢ (𝐴 ∈ V → {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ∈ On) |
37 | | 0elon 6126 |
. . . 4
⊢ ∅
∈ On |
38 | | eleq1 2872 |
. . . 4
⊢ ({𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} = ∅ → ({𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ∈ On ↔ ∅ ∈
On)) |
39 | 37, 38 | mpbiri 259 |
. . 3
⊢ ({𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} = ∅ → {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ∈ On) |
40 | | df-ne 2987 |
. . . . 5
⊢ ({𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ≠ ∅ ↔ ¬ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} = ∅) |
41 | | rabn0 4265 |
. . . . 5
⊢ ({𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ≠ ∅ ↔ ∃𝑥 ∈ On 𝑥 ≺ 𝐴) |
42 | 40, 41 | bitr3i 278 |
. . . 4
⊢ (¬
{𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} = ∅ ↔ ∃𝑥 ∈ On 𝑥 ≺ 𝐴) |
43 | | relsdom 8371 |
. . . . . 6
⊢ Rel
≺ |
44 | 43 | brrelex2i 5502 |
. . . . 5
⊢ (𝑥 ≺ 𝐴 → 𝐴 ∈ V) |
45 | 44 | rexlimivw 3247 |
. . . 4
⊢
(∃𝑥 ∈ On
𝑥 ≺ 𝐴 → 𝐴 ∈ V) |
46 | 42, 45 | sylbi 218 |
. . 3
⊢ (¬
{𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} = ∅ → 𝐴 ∈ V) |
47 | 39, 46 | nsyl4 161 |
. 2
⊢ (¬
𝐴 ∈ V → {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ∈ On) |
48 | 36, 47 | pm2.61i 183 |
1
⊢ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ∈ On |