Theorem weexenwe

Description: If a well-ordering of an infinite set exists, then a well-ordering equinumerous to the set exists. (Contributed by BTernaryTau, 31-Jul-2026)

	Ref	Expression
Assertion	weexenwe	$$⊢\left(\exists rr\mathrm{We}A\wedge \mathrm{\omega }\preccurlyeq A\right)\to \exists s\left(s\subseteq A\times A\wedge s\mathrm{We}A\wedge s\approx A\right)$$

Proof

Step	Hyp	Ref	Expression
1		ween	$$⊢A\in \mathrm{dom}\mathrm{card}\leftrightarrow \exists rr\mathrm{We}A$$
2		inss2	$$⊢r\cap \left(A\times A\right)\subseteq A\times A$$
3		weinxp	$$⊢r\mathrm{We}A\leftrightarrow \left(r\cap \left(A\times A\right)\right)\mathrm{We}A$$
4	3	biimpi	$$⊢r\mathrm{We}A\to \left(r\cap \left(A\times A\right)\right)\mathrm{We}A$$
5	4	3ad2ant3	$$⊢\left(A\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq A\wedge r\mathrm{We}A\right)\to \left(r\cap \left(A\times A\right)\right)\mathrm{We}A$$
6		reldom	$$⊢\mathrm{Rel}\preccurlyeq$$
7	6	brrelex2i	$$⊢\mathrm{\omega }\preccurlyeq A\to A\in \mathrm{V}$$
8	7 7	xpexd	$$⊢\mathrm{\omega }\preccurlyeq A\to A\times A\in \mathrm{V}$$
9		ssdomg	$$⊢A\times A\in \mathrm{V}\to \left(r\cap \left(A\times A\right)\subseteq A\times A\to \left(r\cap \left(A\times A\right)\right)\preccurlyeq \left(A\times A\right)\right)$$
10	8 2 9	mpisyl	$$⊢\mathrm{\omega }\preccurlyeq A\to \left(r\cap \left(A\times A\right)\right)\preccurlyeq \left(A\times A\right)$$
11		infxpidm2	$$⊢\left(A\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq A\right)\to \left(A\times A\right)\approx A$$
12		domentr	$$⊢\left(\left(r\cap \left(A\times A\right)\right)\preccurlyeq \left(A\times A\right)\wedge \left(A\times A\right)\approx A\right)\to \left(r\cap \left(A\times A\right)\right)\preccurlyeq A$$
13	10 11 12	syl2an2	$$⊢\left(A\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq A\right)\to \left(r\cap \left(A\times A\right)\right)\preccurlyeq A$$
14	13	3adant3	$$⊢\left(A\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq A\wedge r\mathrm{We}A\right)\to \left(r\cap \left(A\times A\right)\right)\preccurlyeq A$$
15		weso	$$⊢\left(r\cap \left(A\times A\right)\right)\mathrm{We}A\to \left(r\cap \left(A\times A\right)\right)\mathrm{Or}A$$
16	3 15	sylbi	$$⊢r\mathrm{We}A\to \left(r\cap \left(A\times A\right)\right)\mathrm{Or}A$$
17		vex	$$⊢r\in \mathrm{V}$$
18	17	inex1	$$⊢r\cap \left(A\times A\right)\in \mathrm{V}$$
19		soinfdom	$$⊢\left(\left(r\cap \left(A\times A\right)\right)\mathrm{Or}A\wedge r\cap \left(A\times A\right)\in \mathrm{V}\wedge \mathrm{\omega }\preccurlyeq A\right)\to A\preccurlyeq \left(r\cap \left(A\times A\right)\right)$$
20	18 19	mp3an2	$$⊢\left(\left(r\cap \left(A\times A\right)\right)\mathrm{Or}A\wedge \mathrm{\omega }\preccurlyeq A\right)\to A\preccurlyeq \left(r\cap \left(A\times A\right)\right)$$
21	16 20	sylan	$$⊢\left(r\mathrm{We}A\wedge \mathrm{\omega }\preccurlyeq A\right)\to A\preccurlyeq \left(r\cap \left(A\times A\right)\right)$$
22	21	ancoms	$$⊢\left(\mathrm{\omega }\preccurlyeq A\wedge r\mathrm{We}A\right)\to A\preccurlyeq \left(r\cap \left(A\times A\right)\right)$$
23	22	3adant1	$$⊢\left(A\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq A\wedge r\mathrm{We}A\right)\to A\preccurlyeq \left(r\cap \left(A\times A\right)\right)$$
24		sbth	$$⊢\left(\left(r\cap \left(A\times A\right)\right)\preccurlyeq A\wedge A\preccurlyeq \left(r\cap \left(A\times A\right)\right)\right)\to \left(r\cap \left(A\times A\right)\right)\approx A$$
25	14 23 24	syl2anc	$$⊢\left(A\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq A\wedge r\mathrm{We}A\right)\to \left(r\cap \left(A\times A\right)\right)\approx A$$
26		sseq1	$$⊢s=r\cap \left(A\times A\right)\to \left(s\subseteq A\times A\leftrightarrow r\cap \left(A\times A\right)\subseteq A\times A\right)$$
27		weeq1	$$⊢s=r\cap \left(A\times A\right)\to \left(s\mathrm{We}A\leftrightarrow \left(r\cap \left(A\times A\right)\right)\mathrm{We}A\right)$$
28		breq1	$$⊢s=r\cap \left(A\times A\right)\to \left(s\approx A\leftrightarrow \left(r\cap \left(A\times A\right)\right)\approx A\right)$$
29	26 27 28	3anbi123d	$$⊢s=r\cap \left(A\times A\right)\to \left(\left(s\subseteq A\times A\wedge s\mathrm{We}A\wedge s\approx A\right)\leftrightarrow \left(r\cap \left(A\times A\right)\subseteq A\times A\wedge \left(r\cap \left(A\times A\right)\right)\mathrm{We}A\wedge \left(r\cap \left(A\times A\right)\right)\approx A\right)\right)$$
30	18 29	spcev	$$⊢\left(r\cap \left(A\times A\right)\subseteq A\times A\wedge \left(r\cap \left(A\times A\right)\right)\mathrm{We}A\wedge \left(r\cap \left(A\times A\right)\right)\approx A\right)\to \exists s\left(s\subseteq A\times A\wedge s\mathrm{We}A\wedge s\approx A\right)$$
31	2 5 25 30	mp3an2i	$$⊢\left(A\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq A\wedge r\mathrm{We}A\right)\to \exists s\left(s\subseteq A\times A\wedge s\mathrm{We}A\wedge s\approx A\right)$$
32	31	3expia	$$⊢\left(A\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq A\right)\to \left(r\mathrm{We}A\to \exists s\left(s\subseteq A\times A\wedge s\mathrm{We}A\wedge s\approx A\right)\right)$$
33	32	exlimdv	$$⊢\left(A\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq A\right)\to \left(\exists rr\mathrm{We}A\to \exists s\left(s\subseteq A\times A\wedge s\mathrm{We}A\wedge s\approx A\right)\right)$$
34	1 33	sylanbr	$$⊢\left(\exists rr\mathrm{We}A\wedge \mathrm{\omega }\preccurlyeq A\right)\to \left(\exists rr\mathrm{We}A\to \exists s\left(s\subseteq A\times A\wedge s\mathrm{We}A\wedge s\approx A\right)\right)$$
35	34	adantrd	$$⊢\left(\exists rr\mathrm{We}A\wedge \mathrm{\omega }\preccurlyeq A\right)\to \left(\left(\exists rr\mathrm{We}A\wedge \mathrm{\omega }\preccurlyeq A\right)\to \exists s\left(s\subseteq A\times A\wedge s\mathrm{We}A\wedge s\approx A\right)\right)$$
36	35	pm2.43i	$$⊢\left(\exists rr\mathrm{We}A\wedge \mathrm{\omega }\preccurlyeq A\right)\to \exists s\left(s\subseteq A\times A\wedge s\mathrm{We}A\wedge s\approx A\right)$$