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

Metamath Proof Explorer

Theorem ord2eln012

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

Ref Expression
Assertion ord2eln012 
|- ( Ord A -> ( 2o e. A <-> ( A =/= (/) /\ A =/= 1o /\ A =/= 2o ) ) )

Proof

Step Hyp Ref Expression
1 ne0i 
 |-  ( 2o e. A -> A =/= (/) )
2 2on0 
 |-  2o =/= (/)
3 el1o 
 |-  ( 2o e. 1o <-> 2o = (/) )
4 2 3 nemtbir 
 |-  -. 2o e. 1o
5 eleq2 
 |-  ( A = 1o -> ( 2o e. A <-> 2o e. 1o ) )
6 4 5 mtbiri 
 |-  ( A = 1o -> -. 2o e. A )
7 6 necon2ai 
 |-  ( 2o e. A -> A =/= 1o )
8 2on 
 |-  2o e. On
9 8 onirri 
 |-  -. 2o e. 2o
10 eleq2 
 |-  ( A = 2o -> ( 2o e. A <-> 2o e. 2o ) )
11 9 10 mtbiri 
 |-  ( A = 2o -> -. 2o e. A )
12 11 necon2ai 
 |-  ( 2o e. A -> A =/= 2o )
13 1 7 12 3jca 
 |-  ( 2o e. A -> ( A =/= (/) /\ A =/= 1o /\ A =/= 2o ) )
14 nesym 
 |-  ( A =/= 2o <-> -. 2o = A )
15 14 biimpi 
 |-  ( A =/= 2o -> -. 2o = A )
16 15 3ad2ant3 
 |-  ( ( A =/= (/) /\ A =/= 1o /\ A =/= 2o ) -> -. 2o = A )
17 simp1 
 |-  ( ( A =/= (/) /\ A =/= 1o /\ A =/= 2o ) -> A =/= (/) )
18 simp2 
 |-  ( ( A =/= (/) /\ A =/= 1o /\ A =/= 2o ) -> A =/= 1o )
19 17 18 nelprd 
 |-  ( ( A =/= (/) /\ A =/= 1o /\ A =/= 2o ) -> -. A e. { (/) , 1o } )
20 df2o3 
 |-  2o = { (/) , 1o }
21 20 eleq2i 
 |-  ( A e. 2o <-> A e. { (/) , 1o } )
22 19 21 sylnibr 
 |-  ( ( A =/= (/) /\ A =/= 1o /\ A =/= 2o ) -> -. A e. 2o )
23 16 22 jca 
 |-  ( ( A =/= (/) /\ A =/= 1o /\ A =/= 2o ) -> ( -. 2o = A /\ -. A e. 2o ) )
24 pm4.56 
 |-  ( ( -. 2o = A /\ -. A e. 2o ) <-> -. ( 2o = A \/ A e. 2o ) )
25 23 24 sylib 
 |-  ( ( A =/= (/) /\ A =/= 1o /\ A =/= 2o ) -> -. ( 2o = A \/ A e. 2o ) )
26 8 onordi 
 |-  Ord 2o
27 ordtri2 
 |-  ( ( Ord 2o /\ Ord A ) -> ( 2o e. A <-> -. ( 2o = A \/ A e. 2o ) ) )
28 26 27 mpan 
 |-  ( Ord A -> ( 2o e. A <-> -. ( 2o = A \/ A e. 2o ) ) )
29 25 28 imbitrrid 
 |-  ( Ord A -> ( ( A =/= (/) /\ A =/= 1o /\ A =/= 2o ) -> 2o e. A ) )
30 13 29 impbid2 
 |-  ( Ord A -> ( 2o e. A <-> ( A =/= (/) /\ A =/= 1o /\ A =/= 2o ) ) )