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