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 2 𝑜 A A A 1 𝑜 A 2 𝑜

Proof

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