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