Metamath Proof Explorer

Theorem dfsucon

Description: A is called a successor ordinal if it is not a limit ordinal and not the empty set. (Contributed by RP, 11-Nov-2023)

Ref Expression
Assertion dfsucon ( ( Ord 𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅ ) ↔ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 )

Proof

Step Hyp Ref Expression
1 3ancomb ⊢ ( ( Ord 𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅ ) ↔ ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ ¬ Lim 𝐴 ) )
2 df-3an ⊢ ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ ¬ Lim 𝐴 ) ↔ ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ) ∧ ¬ Lim 𝐴 ) )
3 df-ne ⊢ ( 𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅ )
4 3 anbi2i ⊢ ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ) ↔ ( Ord 𝐴 ∧ ¬ 𝐴 = ∅ ) )
5 4 imbi1i ⊢ ( ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ↔ ( ( Ord 𝐴 ∧ ¬ 𝐴 = ∅ ) → ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) )
6 pm5.6 ⊢ ( ( ( Ord 𝐴 ∧ ¬ 𝐴 = ∅ ) → ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ↔ ( Ord 𝐴 → ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ) )
7 iman ⊢ ( ( Ord 𝐴 → ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ) ↔ ¬ ( Ord 𝐴 ∧ ¬ ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ) )
8 5 6 7 3bitrri ⊢ ( ¬ ( Ord 𝐴 ∧ ¬ ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ) ↔ ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) )
9 dflim3 ⊢ ( Lim 𝐴 ↔ ( Ord 𝐴 ∧ ¬ ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ) )
10 8 9 xchnxbir ⊢ ( ¬ Lim 𝐴 ↔ ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) )
11 10 anbi2i ⊢ ( ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ) ∧ ¬ Lim 𝐴 ) ↔ ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ) ∧ ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ) )
12 1 2 11 3bitri ⊢ ( ( Ord 𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅ ) ↔ ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ) ∧ ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ) )
13 pm3.35 ⊢ ( ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ) ∧ ( ( Ord 𝐴 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 ) ) → ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 )
14 12 13 sylbi ⊢ ( ( Ord 𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 )
15 eloni ⊢ ( 𝑥 ∈ On → Ord 𝑥 )
16 ordsuc ⊢ ( Ord 𝑥 ↔ Ord suc 𝑥 )
17 15 16 sylib ⊢ ( 𝑥 ∈ On → Ord suc 𝑥 )
18 nlimsucg ⊢ ( 𝑥 ∈ On → ¬ Lim suc 𝑥 )
19 nsuceq0 ⊢ suc 𝑥 ≠ ∅
20 19 a1i ⊢ ( 𝑥 ∈ On → suc 𝑥 ≠ ∅ )
21 17 18 20 3jca ⊢ ( 𝑥 ∈ On → ( Ord suc 𝑥 ∧ ¬ Lim suc 𝑥 ∧ suc 𝑥 ≠ ∅ ) )
22 ordeq ⊢ ( 𝐴 = suc 𝑥 → ( Ord 𝐴 ↔ Ord suc 𝑥 ) )
23 limeq ⊢ ( 𝐴 = suc 𝑥 → ( Lim 𝐴 ↔ Lim suc 𝑥 ) )
24 23 notbid ⊢ ( 𝐴 = suc 𝑥 → ( ¬ Lim 𝐴 ↔ ¬ Lim suc 𝑥 ) )
25 neeq1 ⊢ ( 𝐴 = suc 𝑥 → ( 𝐴 ≠ ∅ ↔ suc 𝑥 ≠ ∅ ) )
26 22 24 25 3anbi123d ⊢ ( 𝐴 = suc 𝑥 → ( ( Ord 𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅ ) ↔ ( Ord suc 𝑥 ∧ ¬ Lim suc 𝑥 ∧ suc 𝑥 ≠ ∅ ) ) )
27 21 26 syl5ibrcom ⊢ ( 𝑥 ∈ On → ( 𝐴 = suc 𝑥 → ( Ord 𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅ ) ) )
28 27 rexlimiv ⊢ ( ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 → ( Ord 𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅ ) )
29 14 28 impbii ⊢ ( ( Ord 𝐴 ∧ ¬ Lim 𝐴 ∧ 𝐴 ≠ ∅ ) ↔ ∃ 𝑥 ∈ On 𝐴 = suc 𝑥 )