This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∈ 𝐴 )