Theorem finorwe

Description: If the Axiom of Infinity is denied, every total order is a well-order. The notion of a well-order cannot be usefully expressed without the Axiom of Infinity due to the inability to quantify over proper classes. (Contributed by ML, 5-Oct-2023)

	Ref	Expression
Assertion	finorwe	$$⊢\neg \mathrm{\omega }\in \mathrm{V}\to \left(\underset{\dot{}}{<}\mathrm{Or}A\to \underset{\dot{}}{<}\mathrm{We}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(\neg \mathrm{\omega }\in \mathrm{V}\wedge \underset{\dot{}}{<}\mathrm{Or}A\right)\to \neg \mathrm{\omega }\in \mathrm{V}$$
2		soss	$$⊢x\subseteq A\to \left(\underset{\dot{}}{<}\mathrm{Or}A\to \underset{\dot{}}{<}\mathrm{Or}x\right)$$
3	2	com12	$$⊢\underset{\dot{}}{<}\mathrm{Or}A\to \left(x\subseteq A\to \underset{\dot{}}{<}\mathrm{Or}x\right)$$
4	3	adantl	$$⊢\left(\neg \mathrm{\omega }\in \mathrm{V}\wedge \underset{\dot{}}{<}\mathrm{Or}A\right)\to \left(x\subseteq A\to \underset{\dot{}}{<}\mathrm{Or}x\right)$$
5		vex	$$⊢x\in \mathrm{V}$$
6		fineqv	$$⊢\neg \mathrm{\omega }\in \mathrm{V}\leftrightarrow \mathrm{Fin}=\mathrm{V}$$
7	6	biimpi	$$⊢\neg \mathrm{\omega }\in \mathrm{V}\to \mathrm{Fin}=\mathrm{V}$$
8	5 7	eleqtrrid	$$⊢\neg \mathrm{\omega }\in \mathrm{V}\to x\in \mathrm{Fin}$$
9		wofi	$$⊢\left(\underset{\dot{}}{<}\mathrm{Or}x\wedge x\in \mathrm{Fin}\right)\to \underset{\dot{}}{<}\mathrm{We}x$$
10	9	ancoms	$$⊢\left(x\in \mathrm{Fin}\wedge \underset{\dot{}}{<}\mathrm{Or}x\right)\to \underset{\dot{}}{<}\mathrm{We}x$$
11	8 10	sylan	$$⊢\left(\neg \mathrm{\omega }\in \mathrm{V}\wedge \underset{\dot{}}{<}\mathrm{Or}x\right)\to \underset{\dot{}}{<}\mathrm{We}x$$
12	1 4 11	syl6an	$$⊢\left(\neg \mathrm{\omega }\in \mathrm{V}\wedge \underset{\dot{}}{<}\mathrm{Or}A\right)\to \left(x\subseteq A\to \underset{\dot{}}{<}\mathrm{We}x\right)$$
13		ssid	$$⊢x\subseteq x$$
14		wereu	$$⊢\left(\underset{\dot{}}{<}\mathrm{We}x\wedge \left(x\in \mathrm{V}\wedge x\subseteq x\wedge x\ne \varnothing \right)\right)\to \exists !y\in x\forall z\in x\neg z\underset{\dot{}}{<}y$$
15		reurex	$$⊢\exists !y\in x\forall z\in x\neg z\underset{\dot{}}{<}y\to \exists y\in x\forall z\in x\neg z\underset{\dot{}}{<}y$$
16	14 15	syl	$$⊢\left(\underset{\dot{}}{<}\mathrm{We}x\wedge \left(x\in \mathrm{V}\wedge x\subseteq x\wedge x\ne \varnothing \right)\right)\to \exists y\in x\forall z\in x\neg z\underset{\dot{}}{<}y$$
17	5 16	mp3anr1	$$⊢\left(\underset{\dot{}}{<}\mathrm{We}x\wedge \left(x\subseteq x\wedge x\ne \varnothing \right)\right)\to \exists y\in x\forall z\in x\neg z\underset{\dot{}}{<}y$$
18	13 17	mpanr1	$$⊢\left(\underset{\dot{}}{<}\mathrm{We}x\wedge x\ne \varnothing \right)\to \exists y\in x\forall z\in x\neg z\underset{\dot{}}{<}y$$
19	18	ex	$$⊢\underset{\dot{}}{<}\mathrm{We}x\to \left(x\ne \varnothing \to \exists y\in x\forall z\in x\neg z\underset{\dot{}}{<}y\right)$$
20	12 19	syl6	$$⊢\left(\neg \mathrm{\omega }\in \mathrm{V}\wedge \underset{\dot{}}{<}\mathrm{Or}A\right)\to \left(x\subseteq A\to \left(x\ne \varnothing \to \exists y\in x\forall z\in x\neg z\underset{\dot{}}{<}y\right)\right)$$
21	20	impd	$$⊢\left(\neg \mathrm{\omega }\in \mathrm{V}\wedge \underset{\dot{}}{<}\mathrm{Or}A\right)\to \left(\left(x\subseteq A\wedge x\ne \varnothing \right)\to \exists y\in x\forall z\in x\neg z\underset{\dot{}}{<}y\right)$$
22	21	alrimiv	$$⊢\left(\neg \mathrm{\omega }\in \mathrm{V}\wedge \underset{\dot{}}{<}\mathrm{Or}A\right)\to \forall x\left(\left(x\subseteq A\wedge x\ne \varnothing \right)\to \exists y\in x\forall z\in x\neg z\underset{\dot{}}{<}y\right)$$
23		df-fr	$$⊢\underset{\dot{}}{<}\mathrm{Fr}A\leftrightarrow \forall x\left(\left(x\subseteq A\wedge x\ne \varnothing \right)\to \exists y\in x\forall z\in x\neg z\underset{\dot{}}{<}y\right)$$
24	22 23	sylibr	$$⊢\left(\neg \mathrm{\omega }\in \mathrm{V}\wedge \underset{\dot{}}{<}\mathrm{Or}A\right)\to \underset{\dot{}}{<}\mathrm{Fr}A$$
25		simpr	$$⊢\left(\neg \mathrm{\omega }\in \mathrm{V}\wedge \underset{\dot{}}{<}\mathrm{Or}A\right)\to \underset{\dot{}}{<}\mathrm{Or}A$$
26		df-we	$$⊢\underset{\dot{}}{<}\mathrm{We}A\leftrightarrow \left(\underset{\dot{}}{<}\mathrm{Fr}A\wedge \underset{\dot{}}{<}\mathrm{Or}A\right)$$
27	24 25 26	sylanbrc	$$⊢\left(\neg \mathrm{\omega }\in \mathrm{V}\wedge \underset{\dot{}}{<}\mathrm{Or}A\right)\to \underset{\dot{}}{<}\mathrm{We}A$$
28	27	ex	$$⊢\neg \mathrm{\omega }\in \mathrm{V}\to \left(\underset{\dot{}}{<}\mathrm{Or}A\to \underset{\dot{}}{<}\mathrm{We}A\right)$$