Metamath Proof Explorer


Theorem ord1eln01

Description: An ordinal that is not 0 or 1 contains 1. (Contributed by BTernaryTau, 1-Dec-2024)

Ref Expression
Assertion ord1eln01 ( Ord 𝐴 → ( 1o𝐴 ↔ ( 𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ) ) )

Proof

Step Hyp Ref Expression
1 ne0i ( 1o𝐴𝐴 ≠ ∅ )
2 1on 1o ∈ On
3 2 onirri ¬ 1o ∈ 1o
4 eleq2 ( 𝐴 = 1o → ( 1o𝐴 ↔ 1o ∈ 1o ) )
5 3 4 mtbiri ( 𝐴 = 1o → ¬ 1o𝐴 )
6 5 necon2ai ( 1o𝐴𝐴 ≠ 1o )
7 1 6 jca ( 1o𝐴 → ( 𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ) )
8 el1o ( 𝐴 ∈ 1o𝐴 = ∅ )
9 8 biimpi ( 𝐴 ∈ 1o𝐴 = ∅ )
10 9 necon3ai ( 𝐴 ≠ ∅ → ¬ 𝐴 ∈ 1o )
11 nesym ( 𝐴 ≠ 1o ↔ ¬ 1o = 𝐴 )
12 11 biimpi ( 𝐴 ≠ 1o → ¬ 1o = 𝐴 )
13 10 12 anim12ci ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ) → ( ¬ 1o = 𝐴 ∧ ¬ 𝐴 ∈ 1o ) )
14 pm4.56 ( ( ¬ 1o = 𝐴 ∧ ¬ 𝐴 ∈ 1o ) ↔ ¬ ( 1o = 𝐴𝐴 ∈ 1o ) )
15 13 14 sylib ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ) → ¬ ( 1o = 𝐴𝐴 ∈ 1o ) )
16 2 onordi Ord 1o
17 ordtri2 ( ( Ord 1o ∧ Ord 𝐴 ) → ( 1o𝐴 ↔ ¬ ( 1o = 𝐴𝐴 ∈ 1o ) ) )
18 16 17 mpan ( Ord 𝐴 → ( 1o𝐴 ↔ ¬ ( 1o = 𝐴𝐴 ∈ 1o ) ) )
19 15 18 imbitrrid ( Ord 𝐴 → ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ) → 1o𝐴 ) )
20 7 19 impbid2 ( Ord 𝐴 → ( 1o𝐴 ↔ ( 𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ) ) )