Theorem ord2eln012

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

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

Proof

Step	Hyp	Ref	Expression
1		ne0i	$$⊢2_{𝑜}\in A\to A\ne \varnothing$$
2		2on0	$$⊢2_{𝑜}\ne \varnothing$$
3		el1o	$$⊢2_{𝑜}\in 1_{𝑜}\leftrightarrow 2_{𝑜}=\varnothing$$
4	2 3	nemtbir	$$⊢\neg 2_{𝑜}\in 1_{𝑜}$$
5		eleq2	$$⊢A=1_{𝑜}\to \left(2_{𝑜}\in A\leftrightarrow 2_{𝑜}\in 1_{𝑜}\right)$$
6	4 5	mtbiri	$$⊢A=1_{𝑜}\to \neg 2_{𝑜}\in A$$
7	6	necon2ai	$$⊢2_{𝑜}\in A\to A\ne 1_{𝑜}$$
8		2on	$$⊢2_{𝑜}\in \mathrm{On}$$
9	8	onirri	$$⊢\neg 2_{𝑜}\in 2_{𝑜}$$
10		eleq2	$$⊢A=2_{𝑜}\to \left(2_{𝑜}\in A\leftrightarrow 2_{𝑜}\in 2_{𝑜}\right)$$
11	9 10	mtbiri	$$⊢A=2_{𝑜}\to \neg 2_{𝑜}\in A$$
12	11	necon2ai	$$⊢2_{𝑜}\in A\to A\ne 2_{𝑜}$$
13	1 7 12	3jca	$$⊢2_{𝑜}\in A\to \left(A\ne \varnothing \wedge A\ne 1_{𝑜}\wedge A\ne 2_{𝑜}\right)$$
14		nesym	$$⊢A\ne 2_{𝑜}\leftrightarrow \neg 2_{𝑜}=A$$
15	14	biimpi	$$⊢A\ne 2_{𝑜}\to \neg 2_{𝑜}=A$$
16	15	3ad2ant3	$$⊢\left(A\ne \varnothing \wedge A\ne 1_{𝑜}\wedge A\ne 2_{𝑜}\right)\to \neg 2_{𝑜}=A$$
17		simp1	$$⊢\left(A\ne \varnothing \wedge A\ne 1_{𝑜}\wedge A\ne 2_{𝑜}\right)\to A\ne \varnothing$$
18		simp2	$$⊢\left(A\ne \varnothing \wedge A\ne 1_{𝑜}\wedge A\ne 2_{𝑜}\right)\to A\ne 1_{𝑜}$$
19	17 18	nelprd	$$⊢\left(A\ne \varnothing \wedge A\ne 1_{𝑜}\wedge A\ne 2_{𝑜}\right)\to \neg A\in \left\{\varnothing ,1_{𝑜}\right\}$$
20		df2o3	$$⊢2_{𝑜}=\left\{\varnothing ,1_{𝑜}\right\}$$
21	20	eleq2i	$$⊢A\in 2_{𝑜}\leftrightarrow A\in \left\{\varnothing ,1_{𝑜}\right\}$$
22	19 21	sylnibr	$$⊢\left(A\ne \varnothing \wedge A\ne 1_{𝑜}\wedge A\ne 2_{𝑜}\right)\to \neg A\in 2_{𝑜}$$
23	16 22	jca	$$⊢\left(A\ne \varnothing \wedge A\ne 1_{𝑜}\wedge A\ne 2_{𝑜}\right)\to \left(\neg 2_{𝑜}=A\wedge \neg A\in 2_{𝑜}\right)$$
24		pm4.56	$$⊢\left(\neg 2_{𝑜}=A\wedge \neg A\in 2_{𝑜}\right)\leftrightarrow \neg \left(2_{𝑜}=A\vee A\in 2_{𝑜}\right)$$
25	23 24	sylib	$$⊢\left(A\ne \varnothing \wedge A\ne 1_{𝑜}\wedge A\ne 2_{𝑜}\right)\to \neg \left(2_{𝑜}=A\vee A\in 2_{𝑜}\right)$$
26	8	onordi	$$⊢\mathrm{Ord}{2}_{𝑜}$$
27		ordtri2	$$⊢\left(\mathrm{Ord}{2}_{𝑜}\wedge \mathrm{Ord}A\right)\to \left(2_{𝑜}\in A\leftrightarrow \neg \left(2_{𝑜}=A\vee A\in 2_{𝑜}\right)\right)$$
28	26 27	mpan	$$⊢\mathrm{Ord}A\to \left(2_{𝑜}\in A\leftrightarrow \neg \left(2_{𝑜}=A\vee A\in 2_{𝑜}\right)\right)$$
29	25 28	imbitrrid	$$⊢\mathrm{Ord}A\to \left(\left(A\ne \varnothing \wedge A\ne 1_{𝑜}\wedge A\ne 2_{𝑜}\right)\to 2_{𝑜}\in A\right)$$
30	13 29	impbid2	$$⊢\mathrm{Ord}A\to \left(2_{𝑜}\in A\leftrightarrow \left(A\ne \varnothing \wedge A\ne 1_{𝑜}\wedge A\ne 2_{𝑜}\right)\right)$$