Theorem 2ellim

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

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

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		nlim2	⊢ ¬ Lim 2o
10		limeq	⊢ ( 𝐴 = 2o → ( Lim 𝐴 ↔ Lim 2o ) )
11	9 10	mtbiri	⊢ ( 𝐴 = 2o → ¬ Lim 𝐴 )
12	11	necon2ai	⊢ ( Lim 𝐴 → 𝐴 ≠ 2o )
13		limord	⊢ ( Lim 𝐴 → Ord 𝐴 )
14		ord2eln012	⊢ ( Ord 𝐴 → ( 2o ∈ 𝐴 ↔ ( 𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ∧ 𝐴 ≠ 2o ) ) )
15	13 14	syl	⊢ ( Lim 𝐴 → ( 2o ∈ 𝐴 ↔ ( 𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ∧ 𝐴 ≠ 2o ) ) )
16	4 8 12 15	mpbir3and	⊢ ( Lim 𝐴 → 2o ∈ 𝐴 )