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 𝐴 → ( 2o ∈ 𝐴 ↔ ( 𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ∧ 𝐴 ≠ 2o ) ) )

Proof

Step Hyp Ref Expression
1 ne0i ⊢ ( 2o ∈ 𝐴 → 𝐴 ≠ ∅ )
2 2on0 ⊢ 2o ≠ ∅
3 el1o ⊢ ( 2o ∈ 1o ↔ 2o = ∅ )
4 2 3 nemtbir ⊢ ¬ 2o ∈ 1o
5 eleq2 ⊢ ( 𝐴 = 1o → ( 2o ∈ 𝐴 ↔ 2o ∈ 1o ) )
6 4 5 mtbiri ⊢ ( 𝐴 = 1o → ¬ 2o ∈ 𝐴 )
7 6 necon2ai ⊢ ( 2o ∈ 𝐴 → 𝐴 ≠ 1o )
8 2on ⊢ 2o ∈ On
9 8 onirri ⊢ ¬ 2o ∈ 2o
10 eleq2 ⊢ ( 𝐴 = 2o → ( 2o ∈ 𝐴 ↔ 2o ∈ 2o ) )
11 9 10 mtbiri ⊢ ( 𝐴 = 2o → ¬ 2o ∈ 𝐴 )
12 11 necon2ai ⊢ ( 2o ∈ 𝐴 → 𝐴 ≠ 2o )
13 1 7 12 3jca ⊢ ( 2o ∈ 𝐴 → ( 𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ∧ 𝐴 ≠ 2o ) )
14 nesym ⊢ ( 𝐴 ≠ 2o ↔ ¬ 2o = 𝐴 )
15 14 biimpi ⊢ ( 𝐴 ≠ 2o → ¬ 2o = 𝐴 )
16 15 3ad2ant3 ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ∧ 𝐴 ≠ 2o ) → ¬ 2o = 𝐴 )
17 simp1 ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ∧ 𝐴 ≠ 2o ) → 𝐴 ≠ ∅ )
18 simp2 ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ∧ 𝐴 ≠ 2o ) → 𝐴 ≠ 1o )
19 17 18 nelprd ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ∧ 𝐴 ≠ 2o ) → ¬ 𝐴 ∈ { ∅ , 1o } )
20 df2o3 ⊢ 2o = { ∅ , 1o }
21 20 eleq2i ⊢ ( 𝐴 ∈ 2o ↔ 𝐴 ∈ { ∅ , 1o } )
22 19 21 sylnibr ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ∧ 𝐴 ≠ 2o ) → ¬ 𝐴 ∈ 2o )
23 16 22 jca ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ∧ 𝐴 ≠ 2o ) → ( ¬ 2o = 𝐴 ∧ ¬ 𝐴 ∈ 2o ) )
24 pm4.56 ⊢ ( ( ¬ 2o = 𝐴 ∧ ¬ 𝐴 ∈ 2o ) ↔ ¬ ( 2o = 𝐴 ∨ 𝐴 ∈ 2o ) )
25 23 24 sylib ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ∧ 𝐴 ≠ 2o ) → ¬ ( 2o = 𝐴 ∨ 𝐴 ∈ 2o ) )
26 8 onordi ⊢ Ord 2o
27 ordtri2 ⊢ ( ( Ord 2o ∧ Ord 𝐴 ) → ( 2o ∈ 𝐴 ↔ ¬ ( 2o = 𝐴 ∨ 𝐴 ∈ 2o ) ) )
28 26 27 mpan ⊢ ( Ord 𝐴 → ( 2o ∈ 𝐴 ↔ ¬ ( 2o = 𝐴 ∨ 𝐴 ∈ 2o ) ) )
29 25 28 imbitrrid ⊢ ( Ord 𝐴 → ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ∧ 𝐴 ≠ 2o ) → 2o ∈ 𝐴 ) )
30 13 29 impbid2 ⊢ ( Ord 𝐴 → ( 2o ∈ 𝐴 ↔ ( 𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ∧ 𝐴 ≠ 2o ) ) )