Proof of Theorem dfsucon
Step | Hyp | Ref
| Expression |
1 | | 3ancomb 1095 |
. . . 4
⊢ ((Ord
𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅) ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ ¬ Lim 𝐴)) |
2 | | df-3an 1085 |
. . . 4
⊢ ((Ord
𝐴 ∧ 𝐴 ≠ ∅ ∧ ¬ Lim 𝐴) ↔ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) ∧ ¬ Lim 𝐴)) |
3 | | df-ne 3017 |
. . . . . . . . 9
⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅) |
4 | 3 | anbi2i 624 |
. . . . . . . 8
⊢ ((Ord
𝐴 ∧ 𝐴 ≠ ∅) ↔ (Ord 𝐴 ∧ ¬ 𝐴 = ∅)) |
5 | 4 | imbi1i 352 |
. . . . . . 7
⊢ (((Ord
𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥) ↔ ((Ord 𝐴 ∧ ¬ 𝐴 = ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥)) |
6 | | pm5.6 998 |
. . . . . . 7
⊢ (((Ord
𝐴 ∧ ¬ 𝐴 = ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥) ↔ (Ord 𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥))) |
7 | | iman 404 |
. . . . . . 7
⊢ ((Ord
𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)) ↔ ¬ (Ord 𝐴 ∧ ¬ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥))) |
8 | 5, 6, 7 | 3bitrri 300 |
. . . . . 6
⊢ (¬
(Ord 𝐴 ∧ ¬ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)) ↔ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥)) |
9 | | dflim3 7562 |
. . . . . 6
⊢ (Lim
𝐴 ↔ (Ord 𝐴 ∧ ¬ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥))) |
10 | 8, 9 | xchnxbir 335 |
. . . . 5
⊢ (¬
Lim 𝐴 ↔ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥)) |
11 | 10 | anbi2i 624 |
. . . 4
⊢ (((Ord
𝐴 ∧ 𝐴 ≠ ∅) ∧ ¬ Lim 𝐴) ↔ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) ∧ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥))) |
12 | 1, 2, 11 | 3bitri 299 |
. . 3
⊢ ((Ord
𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅) ↔ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) ∧ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥))) |
13 | | pm3.35 801 |
. . 3
⊢ (((Ord
𝐴 ∧ 𝐴 ≠ ∅) ∧ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥)) → ∃𝑥 ∈ On 𝐴 = suc 𝑥) |
14 | 12, 13 | sylbi 219 |
. 2
⊢ ((Ord
𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥) |
15 | | eloni 6201 |
. . . . . 6
⊢ (𝑥 ∈ On → Ord 𝑥) |
16 | | ordsuc 7529 |
. . . . . 6
⊢ (Ord
𝑥 ↔ Ord suc 𝑥) |
17 | 15, 16 | sylib 220 |
. . . . 5
⊢ (𝑥 ∈ On → Ord suc 𝑥) |
18 | | nlimsucg 7557 |
. . . . 5
⊢ (𝑥 ∈ On → ¬ Lim suc
𝑥) |
19 | | nsuceq0 6271 |
. . . . . 6
⊢ suc 𝑥 ≠ ∅ |
20 | 19 | a1i 11 |
. . . . 5
⊢ (𝑥 ∈ On → suc 𝑥 ≠ ∅) |
21 | 17, 18, 20 | 3jca 1124 |
. . . 4
⊢ (𝑥 ∈ On → (Ord suc 𝑥 ∧ ¬ Lim suc 𝑥 ∧ suc 𝑥 ≠ ∅)) |
22 | | ordeq 6198 |
. . . . 5
⊢ (𝐴 = suc 𝑥 → (Ord 𝐴 ↔ Ord suc 𝑥)) |
23 | | limeq 6203 |
. . . . . 6
⊢ (𝐴 = suc 𝑥 → (Lim 𝐴 ↔ Lim suc 𝑥)) |
24 | 23 | notbid 320 |
. . . . 5
⊢ (𝐴 = suc 𝑥 → (¬ Lim 𝐴 ↔ ¬ Lim suc 𝑥)) |
25 | | neeq1 3078 |
. . . . 5
⊢ (𝐴 = suc 𝑥 → (𝐴 ≠ ∅ ↔ suc 𝑥 ≠ ∅)) |
26 | 22, 24, 25 | 3anbi123d 1432 |
. . . 4
⊢ (𝐴 = suc 𝑥 → ((Ord 𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅) ↔ (Ord suc 𝑥 ∧ ¬ Lim suc 𝑥 ∧ suc 𝑥 ≠ ∅))) |
27 | 21, 26 | syl5ibrcom 249 |
. . 3
⊢ (𝑥 ∈ On → (𝐴 = suc 𝑥 → (Ord 𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅))) |
28 | 27 | rexlimiv 3280 |
. 2
⊢
(∃𝑥 ∈ On
𝐴 = suc 𝑥 → (Ord 𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅)) |
29 | 14, 28 | impbii 211 |
1
⊢ ((Ord
𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅) ↔ ∃𝑥 ∈ On 𝐴 = suc 𝑥) |