Proof of Theorem dfsucon
Step | Hyp | Ref
| Expression |
1 | | 3ancomb 1096 |
. . . 4
⊢ ((Ord
𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅) ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ ¬ Lim 𝐴)) |
2 | | df-3an 1086 |
. . . 4
⊢ ((Ord
𝐴 ∧ 𝐴 ≠ ∅ ∧ ¬ Lim 𝐴) ↔ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) ∧ ¬ Lim 𝐴)) |
3 | | df-ne 2988 |
. . . . . . . . 9
⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅) |
4 | 3 | anbi2i 625 |
. . . . . . . 8
⊢ ((Ord
𝐴 ∧ 𝐴 ≠ ∅) ↔ (Ord 𝐴 ∧ ¬ 𝐴 = ∅)) |
5 | 4 | imbi1i 353 |
. . . . . . 7
⊢ (((Ord
𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥) ↔ ((Ord 𝐴 ∧ ¬ 𝐴 = ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥)) |
6 | | pm5.6 999 |
. . . . . . 7
⊢ (((Ord
𝐴 ∧ ¬ 𝐴 = ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥) ↔ (Ord 𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥))) |
7 | | iman 405 |
. . . . . . 7
⊢ ((Ord
𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)) ↔ ¬ (Ord 𝐴 ∧ ¬ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥))) |
8 | 5, 6, 7 | 3bitrri 301 |
. . . . . 6
⊢ (¬
(Ord 𝐴 ∧ ¬ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)) ↔ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥)) |
9 | | dflim3 7542 |
. . . . . 6
⊢ (Lim
𝐴 ↔ (Ord 𝐴 ∧ ¬ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥))) |
10 | 8, 9 | xchnxbir 336 |
. . . . 5
⊢ (¬
Lim 𝐴 ↔ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥)) |
11 | 10 | anbi2i 625 |
. . . 4
⊢ (((Ord
𝐴 ∧ 𝐴 ≠ ∅) ∧ ¬ Lim 𝐴) ↔ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) ∧ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥))) |
12 | 1, 2, 11 | 3bitri 300 |
. . 3
⊢ ((Ord
𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅) ↔ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) ∧ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥))) |
13 | | pm3.35 802 |
. . 3
⊢ (((Ord
𝐴 ∧ 𝐴 ≠ ∅) ∧ ((Ord 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥)) → ∃𝑥 ∈ On 𝐴 = suc 𝑥) |
14 | 12, 13 | sylbi 220 |
. 2
⊢ ((Ord
𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ On 𝐴 = suc 𝑥) |
15 | | eloni 6169 |
. . . . . 6
⊢ (𝑥 ∈ On → Ord 𝑥) |
16 | | ordsuc 7509 |
. . . . . 6
⊢ (Ord
𝑥 ↔ Ord suc 𝑥) |
17 | 15, 16 | sylib 221 |
. . . . 5
⊢ (𝑥 ∈ On → Ord suc 𝑥) |
18 | | nlimsucg 7537 |
. . . . 5
⊢ (𝑥 ∈ On → ¬ Lim suc
𝑥) |
19 | | nsuceq0 6239 |
. . . . . 6
⊢ suc 𝑥 ≠ ∅ |
20 | 19 | a1i 11 |
. . . . 5
⊢ (𝑥 ∈ On → suc 𝑥 ≠ ∅) |
21 | 17, 18, 20 | 3jca 1125 |
. . . 4
⊢ (𝑥 ∈ On → (Ord suc 𝑥 ∧ ¬ Lim suc 𝑥 ∧ suc 𝑥 ≠ ∅)) |
22 | | ordeq 6166 |
. . . . 5
⊢ (𝐴 = suc 𝑥 → (Ord 𝐴 ↔ Ord suc 𝑥)) |
23 | | limeq 6171 |
. . . . . 6
⊢ (𝐴 = suc 𝑥 → (Lim 𝐴 ↔ Lim suc 𝑥)) |
24 | 23 | notbid 321 |
. . . . 5
⊢ (𝐴 = suc 𝑥 → (¬ Lim 𝐴 ↔ ¬ Lim suc 𝑥)) |
25 | | neeq1 3049 |
. . . . 5
⊢ (𝐴 = suc 𝑥 → (𝐴 ≠ ∅ ↔ suc 𝑥 ≠ ∅)) |
26 | 22, 24, 25 | 3anbi123d 1433 |
. . . 4
⊢ (𝐴 = suc 𝑥 → ((Ord 𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅) ↔ (Ord suc 𝑥 ∧ ¬ Lim suc 𝑥 ∧ suc 𝑥 ≠ ∅))) |
27 | 21, 26 | syl5ibrcom 250 |
. . 3
⊢ (𝑥 ∈ On → (𝐴 = suc 𝑥 → (Ord 𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅))) |
28 | 27 | rexlimiv 3239 |
. 2
⊢
(∃𝑥 ∈ On
𝐴 = suc 𝑥 → (Ord 𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅)) |
29 | 14, 28 | impbii 212 |
1
⊢ ((Ord
𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅) ↔ ∃𝑥 ∈ On 𝐴 = suc 𝑥) |