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

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