| Step | Hyp | Ref
| Expression |
| 1 | | nn0suc 7916 |
. . . 4
⊢ (𝐴 ∈ ω → (𝐴 = ∅ ∨ ∃𝑧 ∈ ω 𝐴 = suc 𝑧)) |
| 2 | | simp1 1137 |
. . . . . 6
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦) → 𝐴 ≠ ∅) |
| 3 | 2 | necon2bi 2971 |
. . . . 5
⊢ (𝐴 = ∅ → ¬ (𝐴 ≠ ∅ ∧ 𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦)) |
| 4 | | vex 3484 |
. . . . . . . . . . . 12
⊢ 𝑧 ∈ V |
| 5 | 4 | sucid 6466 |
. . . . . . . . . . 11
⊢ 𝑧 ∈ suc 𝑧 |
| 6 | | eleq2 2830 |
. . . . . . . . . . 11
⊢ (𝐴 = suc 𝑧 → (𝑧 ∈ 𝐴 ↔ 𝑧 ∈ suc 𝑧)) |
| 7 | 5, 6 | mpbiri 258 |
. . . . . . . . . 10
⊢ (𝐴 = suc 𝑧 → 𝑧 ∈ 𝐴) |
| 8 | 7 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ω ∧ 𝐴 = suc 𝑧) → 𝑧 ∈ 𝐴) |
| 9 | | breq1 5146 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝑥 ≺ 𝑦 ↔ 𝑧 ≺ 𝑦)) |
| 10 | 9 | rexbidv 3179 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ↔ ∃𝑦 ∈ 𝐴 𝑧 ≺ 𝑦)) |
| 11 | | breq2 5147 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑤 → (𝑧 ≺ 𝑦 ↔ 𝑧 ≺ 𝑤)) |
| 12 | 11 | cbvrexvw 3238 |
. . . . . . . . . . 11
⊢
(∃𝑦 ∈
𝐴 𝑧 ≺ 𝑦 ↔ ∃𝑤 ∈ 𝐴 𝑧 ≺ 𝑤) |
| 13 | 10, 12 | bitrdi 287 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ↔ ∃𝑤 ∈ 𝐴 𝑧 ≺ 𝑤)) |
| 14 | 13 | rspcv 3618 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 → ∃𝑤 ∈ 𝐴 𝑧 ≺ 𝑤)) |
| 15 | 8, 14 | syl 17 |
. . . . . . . 8
⊢ ((𝑧 ∈ ω ∧ 𝐴 = suc 𝑧) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 → ∃𝑤 ∈ 𝐴 𝑧 ≺ 𝑤)) |
| 16 | | eleq2 2830 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 = suc 𝑧 → (𝑤 ∈ 𝐴 ↔ 𝑤 ∈ suc 𝑧)) |
| 17 | 16 | biimpa 476 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 = suc 𝑧 ∧ 𝑤 ∈ 𝐴) → 𝑤 ∈ suc 𝑧) |
| 18 | 17 | 3ad2antl2 1187 |
. . . . . . . . . . . . 13
⊢ (((𝑧 ∈ ω ∧ 𝐴 = suc 𝑧 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦) ∧ 𝑤 ∈ 𝐴) → 𝑤 ∈ suc 𝑧) |
| 19 | | nnon 7893 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ ω → 𝑧 ∈ On) |
| 20 | | onsuc 7831 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ On → suc 𝑧 ∈ On) |
| 21 | 19, 20 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ ω → suc 𝑧 ∈ On) |
| 22 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 = suc 𝑧 → (𝐴 ∈ On ↔ suc 𝑧 ∈ On)) |
| 23 | 22 | biimparc 479 |
. . . . . . . . . . . . . . . . 17
⊢ ((suc
𝑧 ∈ On ∧ 𝐴 = suc 𝑧) → 𝐴 ∈ On) |
| 24 | 21, 23 | sylan 580 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ ω ∧ 𝐴 = suc 𝑧) → 𝐴 ∈ On) |
| 25 | 24 | 3adant3 1133 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ ω ∧ 𝐴 = suc 𝑧 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦) → 𝐴 ∈ On) |
| 26 | | onelon 6409 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ On ∧ 𝑤 ∈ 𝐴) → 𝑤 ∈ On) |
| 27 | 25, 26 | sylan 580 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 ∈ ω ∧ 𝐴 = suc 𝑧 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦) ∧ 𝑤 ∈ 𝐴) → 𝑤 ∈ On) |
| 28 | | simpl1 1192 |
. . . . . . . . . . . . . . 15
⊢ (((𝑧 ∈ ω ∧ 𝐴 = suc 𝑧 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦) ∧ 𝑤 ∈ 𝐴) → 𝑧 ∈ ω) |
| 29 | 28, 19 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 ∈ ω ∧ 𝐴 = suc 𝑧 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦) ∧ 𝑤 ∈ 𝐴) → 𝑧 ∈ On) |
| 30 | | onsssuc 6474 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ On ∧ 𝑧 ∈ On) → (𝑤 ⊆ 𝑧 ↔ 𝑤 ∈ suc 𝑧)) |
| 31 | 27, 29, 30 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝑧 ∈ ω ∧ 𝐴 = suc 𝑧 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦) ∧ 𝑤 ∈ 𝐴) → (𝑤 ⊆ 𝑧 ↔ 𝑤 ∈ suc 𝑧)) |
| 32 | 18, 31 | mpbird 257 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∈ ω ∧ 𝐴 = suc 𝑧 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦) ∧ 𝑤 ∈ 𝐴) → 𝑤 ⊆ 𝑧) |
| 33 | | ssdomg 9040 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ V → (𝑤 ⊆ 𝑧 → 𝑤 ≼ 𝑧)) |
| 34 | 4, 32, 33 | mpsyl 68 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ ω ∧ 𝐴 = suc 𝑧 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦) ∧ 𝑤 ∈ 𝐴) → 𝑤 ≼ 𝑧) |
| 35 | | domnsym 9139 |
. . . . . . . . . . 11
⊢ (𝑤 ≼ 𝑧 → ¬ 𝑧 ≺ 𝑤) |
| 36 | 34, 35 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ ω ∧ 𝐴 = suc 𝑧 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦) ∧ 𝑤 ∈ 𝐴) → ¬ 𝑧 ≺ 𝑤) |
| 37 | 36 | nrexdv 3149 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ω ∧ 𝐴 = suc 𝑧 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦) → ¬ ∃𝑤 ∈ 𝐴 𝑧 ≺ 𝑤) |
| 38 | 37 | 3expia 1122 |
. . . . . . . 8
⊢ ((𝑧 ∈ ω ∧ 𝐴 = suc 𝑧) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 → ¬ ∃𝑤 ∈ 𝐴 𝑧 ≺ 𝑤)) |
| 39 | 15, 38 | pm2.65d 196 |
. . . . . . 7
⊢ ((𝑧 ∈ ω ∧ 𝐴 = suc 𝑧) → ¬ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦) |
| 40 | 39 | intn3an3d 1483 |
. . . . . 6
⊢ ((𝑧 ∈ ω ∧ 𝐴 = suc 𝑧) → ¬ (𝐴 ≠ ∅ ∧ 𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦)) |
| 41 | 40 | rexlimiva 3147 |
. . . . 5
⊢
(∃𝑧 ∈
ω 𝐴 = suc 𝑧 → ¬ (𝐴 ≠ ∅ ∧ 𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦)) |
| 42 | 3, 41 | jaoi 858 |
. . . 4
⊢ ((𝐴 = ∅ ∨ ∃𝑧 ∈ ω 𝐴 = suc 𝑧) → ¬ (𝐴 ≠ ∅ ∧ 𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦)) |
| 43 | 1, 42 | syl 17 |
. . 3
⊢ (𝐴 ∈ ω → ¬
(𝐴 ≠ ∅ ∧ 𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦)) |
| 44 | 43 | con2i 139 |
. 2
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦) → ¬ 𝐴 ∈ ω) |
| 45 | | ordom 7897 |
. . 3
⊢ Ord
ω |
| 46 | | eloni 6394 |
. . . 4
⊢ (𝐴 ∈ On → Ord 𝐴) |
| 47 | 46 | 3ad2ant2 1135 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦) → Ord 𝐴) |
| 48 | | ordtri1 6417 |
. . 3
⊢ ((Ord
ω ∧ Ord 𝐴) →
(ω ⊆ 𝐴 ↔
¬ 𝐴 ∈
ω)) |
| 49 | 45, 47, 48 | sylancr 587 |
. 2
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦) → (ω ⊆ 𝐴 ↔ ¬ 𝐴 ∈ ω)) |
| 50 | 44, 49 | mpbird 257 |
1
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 𝑥 ≺ 𝑦) → ω ⊆ 𝐴) |