Metamath Proof Explorer

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 ⊢ A ∈ On ∧ suc ⁡ A ∈ V → suc ⁡ A ∈ On

Proof

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