Theorem ord1eln01

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

	Ref	Expression
Assertion	ord1eln01	$$⊢\mathrm{Ord}A\to \left(1_{𝑜}\in A\leftrightarrow \left(A\ne \varnothing \wedge A\ne 1_{𝑜}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ne0i	$$⊢1_{𝑜}\in A\to A\ne \varnothing$$
2		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
3	2	onirri	$$⊢\neg 1_{𝑜}\in 1_{𝑜}$$
4		eleq2	$$⊢A=1_{𝑜}\to \left(1_{𝑜}\in A\leftrightarrow 1_{𝑜}\in 1_{𝑜}\right)$$
5	3 4	mtbiri	$$⊢A=1_{𝑜}\to \neg 1_{𝑜}\in A$$
6	5	necon2ai	$$⊢1_{𝑜}\in A\to A\ne 1_{𝑜}$$
7	1 6	jca	$$⊢1_{𝑜}\in A\to \left(A\ne \varnothing \wedge A\ne 1_{𝑜}\right)$$
8		el1o	$$⊢A\in 1_{𝑜}\leftrightarrow A=\varnothing$$
9	8	biimpi	$$⊢A\in 1_{𝑜}\to A=\varnothing$$
10	9	necon3ai	$$⊢A\ne \varnothing \to \neg A\in 1_{𝑜}$$
11		nesym	$$⊢A\ne 1_{𝑜}\leftrightarrow \neg 1_{𝑜}=A$$
12	11	biimpi	$$⊢A\ne 1_{𝑜}\to \neg 1_{𝑜}=A$$
13	10 12	anim12ci	$$⊢\left(A\ne \varnothing \wedge A\ne 1_{𝑜}\right)\to \left(\neg 1_{𝑜}=A\wedge \neg A\in 1_{𝑜}\right)$$
14		pm4.56	$$⊢\left(\neg 1_{𝑜}=A\wedge \neg A\in 1_{𝑜}\right)\leftrightarrow \neg \left(1_{𝑜}=A\vee A\in 1_{𝑜}\right)$$
15	13 14	sylib	$$⊢\left(A\ne \varnothing \wedge A\ne 1_{𝑜}\right)\to \neg \left(1_{𝑜}=A\vee A\in 1_{𝑜}\right)$$
16	2	onordi	$$⊢\mathrm{Ord}{1}_{𝑜}$$
17		ordtri2	$$⊢\left(\mathrm{Ord}{1}_{𝑜}\wedge \mathrm{Ord}A\right)\to \left(1_{𝑜}\in A\leftrightarrow \neg \left(1_{𝑜}=A\vee A\in 1_{𝑜}\right)\right)$$
18	16 17	mpan	$$⊢\mathrm{Ord}A\to \left(1_{𝑜}\in A\leftrightarrow \neg \left(1_{𝑜}=A\vee A\in 1_{𝑜}\right)\right)$$
19	15 18	imbitrrid	$$⊢\mathrm{Ord}A\to \left(\left(A\ne \varnothing \wedge A\ne 1_{𝑜}\right)\to 1_{𝑜}\in A\right)$$
20	7 19	impbid2	$$⊢\mathrm{Ord}A\to \left(1_{𝑜}\in A\leftrightarrow \left(A\ne \varnothing \wedge A\ne 1_{𝑜}\right)\right)$$