Proof of Theorem dfsucon
Step | Hyp | Ref
| Expression |
1 | | 3ancomb 1097 |
. . . 4
⊢ ((Ord
𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅) ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ ¬ Lim 𝐴)) |
2 | | df-3an 1087 |
. . . 4
⊢ ((Ord
𝐴 ∧ 𝐴 ≠ ∅ ∧ ¬ Lim 𝐴) ↔ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) ∧ ¬ Lim 𝐴)) |
3 | | df-ne 2945 |
. . . . . . . . 9
⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅) |
4 | 3 | anbi2i 622 |
. . . . . . . 8
⊢ ((Ord
𝐴 ∧ 𝐴 ≠ ∅) ↔ (Ord 𝐴 ∧ ¬ 𝐴 = ∅)) |
5 | 4 | imbi1i 349 |
. . . . . . 7
⊢ (((Ord
𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥) ↔ ((Ord 𝐴 ∧ ¬ 𝐴 = ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥)) |
6 | | pm5.6 998 |
. . . . . . 7
⊢ (((Ord
𝐴 ∧ ¬ 𝐴 = ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥) ↔ (Ord 𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥))) |
7 | | iman 401 |
. . . . . . 7
⊢ ((Ord
𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)) ↔ ¬ (Ord 𝐴 ∧ ¬ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥))) |
8 | 5, 6, 7 | 3bitrri 297 |
. . . . . 6
⊢ (¬
(Ord 𝐴 ∧ ¬ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)) ↔ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥)) |
9 | | dflim3 7682 |
. . . . . 6
⊢ (Lim
𝐴 ↔ (Ord 𝐴 ∧ ¬ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥))) |
10 | 8, 9 | xchnxbir 332 |
. . . . 5
⊢ (¬
Lim 𝐴 ↔ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥)) |
11 | 10 | anbi2i 622 |
. . . 4
⊢ (((Ord
𝐴 ∧ 𝐴 ≠ ∅) ∧ ¬ Lim 𝐴) ↔ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) ∧ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥))) |
12 | 1, 2, 11 | 3bitri 296 |
. . 3
⊢ ((Ord
𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅) ↔ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) ∧ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥))) |
13 | | pm3.35 799 |
. . 3
⊢ (((Ord
𝐴 ∧ 𝐴 ≠ ∅) ∧ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥)) → ∃𝑥 ∈ On 𝐴 = suc 𝑥) |
14 | 12, 13 | sylbi 216 |
. 2
⊢ ((Ord
𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥) |
15 | | eloni 6273 |
. . . . . 6
⊢ (𝑥 ∈ On → Ord 𝑥) |
16 | | ordsuc 7649 |
. . . . . 6
⊢ (Ord
𝑥 ↔ Ord suc 𝑥) |
17 | 15, 16 | sylib 217 |
. . . . 5
⊢ (𝑥 ∈ On → Ord suc 𝑥) |
18 | | nlimsucg 7677 |
. . . . 5
⊢ (𝑥 ∈ On → ¬ Lim suc
𝑥) |
19 | | nsuceq0 6343 |
. . . . . 6
⊢ suc 𝑥 ≠ ∅ |
20 | 19 | a1i 11 |
. . . . 5
⊢ (𝑥 ∈ On → suc 𝑥 ≠ ∅) |
21 | 17, 18, 20 | 3jca 1126 |
. . . 4
⊢ (𝑥 ∈ On → (Ord suc 𝑥 ∧ ¬ Lim suc 𝑥 ∧ suc 𝑥 ≠ ∅)) |
22 | | ordeq 6270 |
. . . . 5
⊢ (𝐴 = suc 𝑥 → (Ord 𝐴 ↔ Ord suc 𝑥)) |
23 | | limeq 6275 |
. . . . . 6
⊢ (𝐴 = suc 𝑥 → (Lim 𝐴 ↔ Lim suc 𝑥)) |
24 | 23 | notbid 317 |
. . . . 5
⊢ (𝐴 = suc 𝑥 → (¬ Lim 𝐴 ↔ ¬ Lim suc 𝑥)) |
25 | | neeq1 3007 |
. . . . 5
⊢ (𝐴 = suc 𝑥 → (𝐴 ≠ ∅ ↔ suc 𝑥 ≠ ∅)) |
26 | 22, 24, 25 | 3anbi123d 1434 |
. . . 4
⊢ (𝐴 = suc 𝑥 → ((Ord 𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅) ↔ (Ord suc 𝑥 ∧ ¬ Lim suc 𝑥 ∧ suc 𝑥 ≠ ∅))) |
27 | 21, 26 | syl5ibrcom 246 |
. . 3
⊢ (𝑥 ∈ On → (𝐴 = suc 𝑥 → (Ord 𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅))) |
28 | 27 | rexlimiv 3210 |
. 2
⊢
(∃𝑥 ∈ On
𝐴 = suc 𝑥 → (Ord 𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅)) |
29 | 14, 28 | impbii 208 |
1
⊢ ((Ord
𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅) ↔ ∃𝑥 ∈ On 𝐴 = suc 𝑥) |