| Step | Hyp | Ref
| Expression |
| 1 | | onelon 6409 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ On ∧ 𝑦 ∈ 𝑧) → 𝑦 ∈ On) |
| 2 | | vex 3484 |
. . . . . . . . . . . . . 14
⊢ 𝑧 ∈ V |
| 3 | | onelss 6426 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ On → (𝑦 ∈ 𝑧 → 𝑦 ⊆ 𝑧)) |
| 4 | 3 | imp 406 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ On ∧ 𝑦 ∈ 𝑧) → 𝑦 ⊆ 𝑧) |
| 5 | | ssdomg 9040 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ V → (𝑦 ⊆ 𝑧 → 𝑦 ≼ 𝑧)) |
| 6 | 2, 4, 5 | mpsyl 68 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ On ∧ 𝑦 ∈ 𝑧) → 𝑦 ≼ 𝑧) |
| 7 | 1, 6 | jca 511 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ On ∧ 𝑦 ∈ 𝑧) → (𝑦 ∈ On ∧ 𝑦 ≼ 𝑧)) |
| 8 | | domsdomtr 9152 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ≼ 𝑧 ∧ 𝑧 ≺ 𝐴) → 𝑦 ≺ 𝐴) |
| 9 | 8 | anim2i 617 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ On ∧ (𝑦 ≼ 𝑧 ∧ 𝑧 ≺ 𝐴)) → (𝑦 ∈ On ∧ 𝑦 ≺ 𝐴)) |
| 10 | 9 | anassrs 467 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ On ∧ 𝑦 ≼ 𝑧) ∧ 𝑧 ≺ 𝐴) → (𝑦 ∈ On ∧ 𝑦 ≺ 𝐴)) |
| 11 | 7, 10 | sylan 580 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ On ∧ 𝑦 ∈ 𝑧) ∧ 𝑧 ≺ 𝐴) → (𝑦 ∈ On ∧ 𝑦 ≺ 𝐴)) |
| 12 | 11 | exp31 419 |
. . . . . . . . . 10
⊢ (𝑧 ∈ On → (𝑦 ∈ 𝑧 → (𝑧 ≺ 𝐴 → (𝑦 ∈ On ∧ 𝑦 ≺ 𝐴)))) |
| 13 | 12 | com12 32 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝑧 → (𝑧 ∈ On → (𝑧 ≺ 𝐴 → (𝑦 ∈ On ∧ 𝑦 ≺ 𝐴)))) |
| 14 | 13 | impd 410 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝑧 → ((𝑧 ∈ On ∧ 𝑧 ≺ 𝐴) → (𝑦 ∈ On ∧ 𝑦 ≺ 𝐴))) |
| 15 | | breq1 5146 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → (𝑥 ≺ 𝐴 ↔ 𝑧 ≺ 𝐴)) |
| 16 | 15 | elrab 3692 |
. . . . . . . 8
⊢ (𝑧 ∈ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ↔ (𝑧 ∈ On ∧ 𝑧 ≺ 𝐴)) |
| 17 | | breq1 5146 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥 ≺ 𝐴 ↔ 𝑦 ≺ 𝐴)) |
| 18 | 17 | elrab 3692 |
. . . . . . . 8
⊢ (𝑦 ∈ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ↔ (𝑦 ∈ On ∧ 𝑦 ≺ 𝐴)) |
| 19 | 14, 16, 18 | 3imtr4g 296 |
. . . . . . 7
⊢ (𝑦 ∈ 𝑧 → (𝑧 ∈ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} → 𝑦 ∈ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴})) |
| 20 | 19 | imp 406 |
. . . . . 6
⊢ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴}) → 𝑦 ∈ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴}) |
| 21 | 20 | gen2 1796 |
. . . . 5
⊢
∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴}) → 𝑦 ∈ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴}) |
| 22 | | dftr2 5261 |
. . . . 5
⊢ (Tr
{𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ↔ ∀𝑦∀𝑧((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴}) → 𝑦 ∈ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴})) |
| 23 | 21, 22 | mpbir 231 |
. . . 4
⊢ Tr {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} |
| 24 | | ssrab2 4080 |
. . . 4
⊢ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ⊆ On |
| 25 | | ordon 7797 |
. . . 4
⊢ Ord
On |
| 26 | | trssord 6401 |
. . . 4
⊢ ((Tr
{𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ∧ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ⊆ On ∧ Ord On) → Ord {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴}) |
| 27 | 23, 24, 25, 26 | mp3an 1463 |
. . 3
⊢ Ord
{𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} |
| 28 | | hartogs 9584 |
. . . 4
⊢ (𝐴 ∈ V → {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ On) |
| 29 | | sdomdom 9020 |
. . . . . . 7
⊢ (𝑥 ≺ 𝐴 → 𝑥 ≼ 𝐴) |
| 30 | 29 | a1i 11 |
. . . . . 6
⊢ (𝑥 ∈ On → (𝑥 ≺ 𝐴 → 𝑥 ≼ 𝐴)) |
| 31 | 30 | ss2rabi 4077 |
. . . . 5
⊢ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ⊆ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} |
| 32 | | ssexg 5323 |
. . . . 5
⊢ (({𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ⊆ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∧ {𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ On) → {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ∈ V) |
| 33 | 31, 32 | mpan 690 |
. . . 4
⊢ ({𝑥 ∈ On ∣ 𝑥 ≼ 𝐴} ∈ On → {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ∈ V) |
| 34 | | elong 6392 |
. . . 4
⊢ ({𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ∈ V → ({𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ∈ On ↔ Ord {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴})) |
| 35 | 28, 33, 34 | 3syl 18 |
. . 3
⊢ (𝐴 ∈ V → ({𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ∈ On ↔ Ord {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴})) |
| 36 | 27, 35 | mpbiri 258 |
. 2
⊢ (𝐴 ∈ V → {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ∈ On) |
| 37 | | 0elon 6438 |
. . . 4
⊢ ∅
∈ On |
| 38 | | eleq1 2829 |
. . . 4
⊢ ({𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} = ∅ → ({𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ∈ On ↔ ∅ ∈
On)) |
| 39 | 37, 38 | mpbiri 258 |
. . 3
⊢ ({𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} = ∅ → {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ∈ On) |
| 40 | | df-ne 2941 |
. . . . 5
⊢ ({𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ≠ ∅ ↔ ¬ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} = ∅) |
| 41 | | rabn0 4389 |
. . . . 5
⊢ ({𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ≠ ∅ ↔ ∃𝑥 ∈ On 𝑥 ≺ 𝐴) |
| 42 | 40, 41 | bitr3i 277 |
. . . 4
⊢ (¬
{𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} = ∅ ↔ ∃𝑥 ∈ On 𝑥 ≺ 𝐴) |
| 43 | | relsdom 8992 |
. . . . . 6
⊢ Rel
≺ |
| 44 | 43 | brrelex2i 5742 |
. . . . 5
⊢ (𝑥 ≺ 𝐴 → 𝐴 ∈ V) |
| 45 | 44 | rexlimivw 3151 |
. . . 4
⊢
(∃𝑥 ∈ On
𝑥 ≺ 𝐴 → 𝐴 ∈ V) |
| 46 | 42, 45 | sylbi 217 |
. . 3
⊢ (¬
{𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} = ∅ → 𝐴 ∈ V) |
| 47 | 39, 46 | nsyl4 158 |
. 2
⊢ (¬
𝐴 ∈ V → {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ∈ On) |
| 48 | 36, 47 | pm2.61i 182 |
1
⊢ {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴} ∈ On |