Theorem sucexeloni

Description: If the successor of an ordinal number exists, it is an ordinal number. This variation of suceloni does not require ax-un . (Contributed by BTernaryTau, 30-Nov-2024)

	Ref	Expression
Assertion	sucexeloni	⊢ ( ( 𝐴 ∈ On ∧ suc 𝐴 ∈ 𝑉 ) → suc 𝐴 ∈ On )

Proof

Step	Hyp	Ref	Expression
1		onelss	⊢ ( 𝐴 ∈ On → ( 𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴 ) )
2		velsn	⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )
3		eqimss	⊢ ( 𝑥 = 𝐴 → 𝑥 ⊆ 𝐴 )
4	2 3	sylbi	⊢ ( 𝑥 ∈ { 𝐴 } → 𝑥 ⊆ 𝐴 )
5	4	a1i	⊢ ( 𝐴 ∈ On → ( 𝑥 ∈ { 𝐴 } → 𝑥 ⊆ 𝐴 ) )
6	1 5	orim12d	⊢ ( 𝐴 ∈ On → ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ { 𝐴 } ) → ( 𝑥 ⊆ 𝐴 ∨ 𝑥 ⊆ 𝐴 ) ) )
7		df-suc	⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } )
8	7	eleq2i	⊢ ( 𝑥 ∈ suc 𝐴 ↔ 𝑥 ∈ ( 𝐴 ∪ { 𝐴 } ) )
9		elun	⊢ ( 𝑥 ∈ ( 𝐴 ∪ { 𝐴 } ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ { 𝐴 } ) )
10	8 9	bitr2i	⊢ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ { 𝐴 } ) ↔ 𝑥 ∈ suc 𝐴 )
11		oridm	⊢ ( ( 𝑥 ⊆ 𝐴 ∨ 𝑥 ⊆ 𝐴 ) ↔ 𝑥 ⊆ 𝐴 )
12	6 10 11	3imtr3g	⊢ ( 𝐴 ∈ On → ( 𝑥 ∈ suc 𝐴 → 𝑥 ⊆ 𝐴 ) )
13		sssucid	⊢ 𝐴 ⊆ suc 𝐴
14		sstr2	⊢ ( 𝑥 ⊆ 𝐴 → ( 𝐴 ⊆ suc 𝐴 → 𝑥 ⊆ suc 𝐴 ) )
15	12 13 14	syl6mpi	⊢ ( 𝐴 ∈ On → ( 𝑥 ∈ suc 𝐴 → 𝑥 ⊆ suc 𝐴 ) )
16	15	ralrimiv	⊢ ( 𝐴 ∈ On → ∀ 𝑥 ∈ suc 𝐴 𝑥 ⊆ suc 𝐴 )
17		dftr3	⊢ ( Tr suc 𝐴 ↔ ∀ 𝑥 ∈ suc 𝐴 𝑥 ⊆ suc 𝐴 )
18	16 17	sylibr	⊢ ( 𝐴 ∈ On → Tr suc 𝐴 )
19		onss	⊢ ( 𝐴 ∈ On → 𝐴 ⊆ On )
20		snssi	⊢ ( 𝐴 ∈ On → { 𝐴 } ⊆ On )
21	19 20	unssd	⊢ ( 𝐴 ∈ On → ( 𝐴 ∪ { 𝐴 } ) ⊆ On )
22	7 21	eqsstrid	⊢ ( 𝐴 ∈ On → suc 𝐴 ⊆ On )
23		ordon	⊢ Ord On
24		trssord	⊢ ( ( Tr suc 𝐴 ∧ suc 𝐴 ⊆ On ∧ Ord On ) → Ord suc 𝐴 )
25	24	3exp	⊢ ( Tr suc 𝐴 → ( suc 𝐴 ⊆ On → ( Ord On → Ord suc 𝐴 ) ) )
26	23 25	mpii	⊢ ( Tr suc 𝐴 → ( suc 𝐴 ⊆ On → Ord suc 𝐴 ) )
27	18 22 26	sylc	⊢ ( 𝐴 ∈ On → Ord suc 𝐴 )
28	27	adantr	⊢ ( ( 𝐴 ∈ On ∧ suc 𝐴 ∈ 𝑉 ) → Ord suc 𝐴 )
29		elong	⊢ ( suc 𝐴 ∈ 𝑉 → ( suc 𝐴 ∈ On ↔ Ord suc 𝐴 ) )
30	29	adantl	⊢ ( ( 𝐴 ∈ On ∧ suc 𝐴 ∈ 𝑉 ) → ( suc 𝐴 ∈ On ↔ Ord suc 𝐴 ) )
31	28 30	mpbird	⊢ ( ( 𝐴 ∈ On ∧ suc 𝐴 ∈ 𝑉 ) → suc 𝐴 ∈ On )