Proof of Theorem dfsucon
| Step | Hyp | Ref
| Expression |
| 1 | | 3ancomb 1099 |
. . . 4
⊢ ((Ord
𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅) ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ ¬ Lim 𝐴)) |
| 2 | | df-3an 1089 |
. . . 4
⊢ ((Ord
𝐴 ∧ 𝐴 ≠ ∅ ∧ ¬ Lim 𝐴) ↔ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) ∧ ¬ Lim 𝐴)) |
| 3 | | df-ne 2941 |
. . . . . . . . 9
⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅) |
| 4 | 3 | anbi2i 623 |
. . . . . . . 8
⊢ ((Ord
𝐴 ∧ 𝐴 ≠ ∅) ↔ (Ord 𝐴 ∧ ¬ 𝐴 = ∅)) |
| 5 | 4 | imbi1i 349 |
. . . . . . 7
⊢ (((Ord
𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥) ↔ ((Ord 𝐴 ∧ ¬ 𝐴 = ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥)) |
| 6 | | pm5.6 1004 |
. . . . . . 7
⊢ (((Ord
𝐴 ∧ ¬ 𝐴 = ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥) ↔ (Ord 𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥))) |
| 7 | | iman 401 |
. . . . . . 7
⊢ ((Ord
𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)) ↔ ¬ (Ord 𝐴 ∧ ¬ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥))) |
| 8 | 5, 6, 7 | 3bitrri 298 |
. . . . . 6
⊢ (¬
(Ord 𝐴 ∧ ¬ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)) ↔ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥)) |
| 9 | | dflim3 7868 |
. . . . . 6
⊢ (Lim
𝐴 ↔ (Ord 𝐴 ∧ ¬ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥))) |
| 10 | 8, 9 | xchnxbir 333 |
. . . . 5
⊢ (¬
Lim 𝐴 ↔ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥)) |
| 11 | 10 | anbi2i 623 |
. . . 4
⊢ (((Ord
𝐴 ∧ 𝐴 ≠ ∅) ∧ ¬ Lim 𝐴) ↔ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) ∧ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥))) |
| 12 | 1, 2, 11 | 3bitri 297 |
. . 3
⊢ ((Ord
𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅) ↔ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) ∧ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥))) |
| 13 | | pm3.35 803 |
. . 3
⊢ (((Ord
𝐴 ∧ 𝐴 ≠ ∅) ∧ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥)) → ∃𝑥 ∈ On 𝐴 = suc 𝑥) |
| 14 | 12, 13 | sylbi 217 |
. 2
⊢ ((Ord
𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥) |
| 15 | | eloni 6394 |
. . . . . 6
⊢ (𝑥 ∈ On → Ord 𝑥) |
| 16 | | ordsuc 7833 |
. . . . . 6
⊢ (Ord
𝑥 ↔ Ord suc 𝑥) |
| 17 | 15, 16 | sylib 218 |
. . . . 5
⊢ (𝑥 ∈ On → Ord suc 𝑥) |
| 18 | | nlimsuc 43454 |
. . . . 5
⊢ (𝑥 ∈ On → ¬ Lim suc
𝑥) |
| 19 | | nsuceq0 6467 |
. . . . . 6
⊢ suc 𝑥 ≠ ∅ |
| 20 | 19 | a1i 11 |
. . . . 5
⊢ (𝑥 ∈ On → suc 𝑥 ≠ ∅) |
| 21 | 17, 18, 20 | 3jca 1129 |
. . . 4
⊢ (𝑥 ∈ On → (Ord suc 𝑥 ∧ ¬ Lim suc 𝑥 ∧ suc 𝑥 ≠ ∅)) |
| 22 | | ordeq 6391 |
. . . . 5
⊢ (𝐴 = suc 𝑥 → (Ord 𝐴 ↔ Ord suc 𝑥)) |
| 23 | | limeq 6396 |
. . . . . 6
⊢ (𝐴 = suc 𝑥 → (Lim 𝐴 ↔ Lim suc 𝑥)) |
| 24 | 23 | notbid 318 |
. . . . 5
⊢ (𝐴 = suc 𝑥 → (¬ Lim 𝐴 ↔ ¬ Lim suc 𝑥)) |
| 25 | | neeq1 3003 |
. . . . 5
⊢ (𝐴 = suc 𝑥 → (𝐴 ≠ ∅ ↔ suc 𝑥 ≠ ∅)) |
| 26 | 22, 24, 25 | 3anbi123d 1438 |
. . . 4
⊢ (𝐴 = suc 𝑥 → ((Ord 𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅) ↔ (Ord suc 𝑥 ∧ ¬ Lim suc 𝑥 ∧ suc 𝑥 ≠ ∅))) |
| 27 | 21, 26 | syl5ibrcom 247 |
. . 3
⊢ (𝑥 ∈ On → (𝐴 = suc 𝑥 → (Ord 𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅))) |
| 28 | 27 | rexlimiv 3148 |
. 2
⊢
(∃𝑥 ∈ On
𝐴 = suc 𝑥 → (Ord 𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅)) |
| 29 | 14, 28 | impbii 209 |
1
⊢ ((Ord
𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅) ↔ ∃𝑥 ∈ On 𝐴 = suc 𝑥) |