This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Union Ordinals (continued) sucexeloni
Description: If the successor of an ordinal number exists, it is an ordinal number.
This variation of onsuc does not require ax-un . (Contributed by BTernaryTau , 30-Nov-2024) (Proof shortened by BJ , 11-Jan-2025)
Ref
Expression
Assertion
sucexeloni ⊢ ( ( 𝐴 ∈ On ∧ suc 𝐴 ∈ 𝑉 ) → suc 𝐴 ∈ On )
Proof
Step
Hyp
Ref
Expression
1
eloni ⊢ ( 𝐴 ∈ On → Ord 𝐴 )
2
ordsuci ⊢ ( Ord 𝐴 → Ord suc 𝐴 )
3
1 2
syl ⊢ ( 𝐴 ∈ On → Ord suc 𝐴 )
4
elex ⊢ ( suc 𝐴 ∈ 𝑉 → suc 𝐴 ∈ V )
5
elong ⊢ ( suc 𝐴 ∈ V → ( suc 𝐴 ∈ On ↔ Ord suc 𝐴 ) )
6
5
biimparc ⊢ ( ( Ord suc 𝐴 ∧ suc 𝐴 ∈ V ) → suc 𝐴 ∈ On )
7
3 4 6
syl2an ⊢ ( ( 𝐴 ∈ On ∧ suc 𝐴 ∈ 𝑉 ) → suc 𝐴 ∈ On )