Theorem 1ellim

Description: A limit ordinal contains 1. (Contributed by BTernaryTau, 1-Dec-2024)

	Ref	Expression
Assertion	1ellim	⊢ ( Lim 𝐴 → 1o ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		nlim0	⊢ ¬ Lim ∅
2		limeq	⊢ ( 𝐴 = ∅ → ( Lim 𝐴 ↔ Lim ∅ ) )
3	1 2	mtbiri	⊢ ( 𝐴 = ∅ → ¬ Lim 𝐴 )
4	3	necon2ai	⊢ ( Lim 𝐴 → 𝐴 ≠ ∅ )
5		nlim1	⊢ ¬ Lim 1o
6		limeq	⊢ ( 𝐴 = 1o → ( Lim 𝐴 ↔ Lim 1o ) )
7	5 6	mtbiri	⊢ ( 𝐴 = 1o → ¬ Lim 𝐴 )
8	7	necon2ai	⊢ ( Lim 𝐴 → 𝐴 ≠ 1o )
9		limord	⊢ ( Lim 𝐴 → Ord 𝐴 )
10		ord1eln01	⊢ ( Ord 𝐴 → ( 1o ∈ 𝐴 ↔ ( 𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ) ) )
11	9 10	syl	⊢ ( Lim 𝐴 → ( 1o ∈ 𝐴 ↔ ( 𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ) ) )
12	4 8 11	mpbir2and	⊢ ( Lim 𝐴 → 1o ∈ 𝐴 )