Description: Ordinal 1 is an ordinal number. (Contributed by NM, 29-Oct-1995) Avoid ax-un . (Revised by BTernaryTau, 30-Nov-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | 1on | ⊢ 1o ∈ On |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-1o | ⊢ 1o = suc ∅ | |
2 | 0elon | ⊢ ∅ ∈ On | |
3 | 1oex | ⊢ 1o ∈ V | |
4 | 1 3 | eqeltrri | ⊢ suc ∅ ∈ V |
5 | sucexeloni | ⊢ ( ( ∅ ∈ On ∧ suc ∅ ∈ V ) → suc ∅ ∈ On ) | |
6 | 2 4 5 | mp2an | ⊢ suc ∅ ∈ On |
7 | 1 6 | eqeltri | ⊢ 1o ∈ On |