Theorem nlim1

Description: 1 is not a limit ordinal. (Contributed by BTernaryTau, 1-Dec-2024)

	Ref	Expression
Assertion	nlim1	⊢ ¬ Lim 1o

Proof

Step	Hyp	Ref	Expression
1		1n0	⊢ 1o ≠ ∅
2		0ex	⊢ ∅ ∈ V
3	2	unisn	⊢ ∪ { ∅ } = ∅
4	1 3	neeqtrri	⊢ 1o ≠ ∪ { ∅ }
5		df1o2	⊢ 1o = { ∅ }
6	5	unieqi	⊢ ∪ 1o = ∪ { ∅ }
7	4 6	neeqtrri	⊢ 1o ≠ ∪ 1o
8	7	neii	⊢ ¬ 1o = ∪ 1o
9		simp3	⊢ ( ( Ord 1o ∧ 1o ≠ ∅ ∧ 1o = ∪ 1o ) → 1o = ∪ 1o )
10	8 9	mto	⊢ ¬ ( Ord 1o ∧ 1o ≠ ∅ ∧ 1o = ∪ 1o )
11		df-lim	⊢ ( Lim 1o ↔ ( Ord 1o ∧ 1o ≠ ∅ ∧ 1o = ∪ 1o ) )
12	10 11	mtbir	⊢ ¬ Lim 1o