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