Theorem ord1eln01

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

	Ref	Expression
Assertion	ord1eln01	⊢ ( Ord 𝐴 → ( 1o ∈ 𝐴 ↔ ( 𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ) ) )

Proof

Step	Hyp	Ref	Expression
1		ne0i	⊢ ( 1o ∈ 𝐴 → 𝐴 ≠ ∅ )
2		1on	⊢ 1o ∈ On
3	2	onirri	⊢ ¬ 1o ∈ 1o
4		eleq2	⊢ ( 𝐴 = 1o → ( 1o ∈ 𝐴 ↔ 1o ∈ 1o ) )
5	3 4	mtbiri	⊢ ( 𝐴 = 1o → ¬ 1o ∈ 𝐴 )
6	5	necon2ai	⊢ ( 1o ∈ 𝐴 → 𝐴 ≠ 1o )
7	1 6	jca	⊢ ( 1o ∈ 𝐴 → ( 𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ) )
8		el1o	⊢ ( 𝐴 ∈ 1o ↔ 𝐴 = ∅ )
9	8	biimpi	⊢ ( 𝐴 ∈ 1o → 𝐴 = ∅ )
10	9	necon3ai	⊢ ( 𝐴 ≠ ∅ → ¬ 𝐴 ∈ 1o )
11		nesym	⊢ ( 𝐴 ≠ 1o ↔ ¬ 1o = 𝐴 )
12	11	biimpi	⊢ ( 𝐴 ≠ 1o → ¬ 1o = 𝐴 )
13	10 12	anim12ci	⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ) → ( ¬ 1o = 𝐴 ∧ ¬ 𝐴 ∈ 1o ) )
14		pm4.56	⊢ ( ( ¬ 1o = 𝐴 ∧ ¬ 𝐴 ∈ 1o ) ↔ ¬ ( 1o = 𝐴 ∨ 𝐴 ∈ 1o ) )
15	13 14	sylib	⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ) → ¬ ( 1o = 𝐴 ∨ 𝐴 ∈ 1o ) )
16	2	onordi	⊢ Ord 1o
17		ordtri2	⊢ ( ( Ord 1o ∧ Ord 𝐴 ) → ( 1o ∈ 𝐴 ↔ ¬ ( 1o = 𝐴 ∨ 𝐴 ∈ 1o ) ) )
18	16 17	mpan	⊢ ( Ord 𝐴 → ( 1o ∈ 𝐴 ↔ ¬ ( 1o = 𝐴 ∨ 𝐴 ∈ 1o ) ) )
19	15 18	imbitrrid	⊢ ( Ord 𝐴 → ( ( 𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ) → 1o ∈ 𝐴 ) )
20	7 19	impbid2	⊢ ( Ord 𝐴 → ( 1o ∈ 𝐴 ↔ ( 𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ) ) )