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 A -> ( 1o e. A <-> ( A =/= (/) /\ A =/= 1o ) ) )

Proof

Step Hyp Ref Expression
1 ne0i
 |-  ( 1o e. A -> A =/= (/) )
2 1on
 |-  1o e. On
3 2 onirri
 |-  -. 1o e. 1o
4 eleq2
 |-  ( A = 1o -> ( 1o e. A <-> 1o e. 1o ) )
5 3 4 mtbiri
 |-  ( A = 1o -> -. 1o e. A )
6 5 necon2ai
 |-  ( 1o e. A -> A =/= 1o )
7 1 6 jca
 |-  ( 1o e. A -> ( A =/= (/) /\ A =/= 1o ) )
8 el1o
 |-  ( A e. 1o <-> A = (/) )
9 8 biimpi
 |-  ( A e. 1o -> A = (/) )
10 9 necon3ai
 |-  ( A =/= (/) -> -. A e. 1o )
11 nesym
 |-  ( A =/= 1o <-> -. 1o = A )
12 11 biimpi
 |-  ( A =/= 1o -> -. 1o = A )
13 10 12 anim12ci
 |-  ( ( A =/= (/) /\ A =/= 1o ) -> ( -. 1o = A /\ -. A e. 1o ) )
14 pm4.56
 |-  ( ( -. 1o = A /\ -. A e. 1o ) <-> -. ( 1o = A \/ A e. 1o ) )
15 13 14 sylib
 |-  ( ( A =/= (/) /\ A =/= 1o ) -> -. ( 1o = A \/ A e. 1o ) )
16 2 onordi
 |-  Ord 1o
17 ordtri2
 |-  ( ( Ord 1o /\ Ord A ) -> ( 1o e. A <-> -. ( 1o = A \/ A e. 1o ) ) )
18 16 17 mpan
 |-  ( Ord A -> ( 1o e. A <-> -. ( 1o = A \/ A e. 1o ) ) )
19 15 18 imbitrrid
 |-  ( Ord A -> ( ( A =/= (/) /\ A =/= 1o ) -> 1o e. A ) )
20 7 19 impbid2
 |-  ( Ord A -> ( 1o e. A <-> ( A =/= (/) /\ A =/= 1o ) ) )