Theorem ac10ct

Description: A proof of the well-ordering theorem weth , an Axiom of Choice equivalent, restricted to sets dominated by some ordinal (in particular finite sets and countable sets), proven in ZF without AC. (Contributed by Mario Carneiro, 5-Jan-2013)

	Ref	Expression
Assertion	ac10ct	$$⊢\exists y\in \mathrm{On}A\preccurlyeq y\to \exists xx\mathrm{We}A$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢y\in \mathrm{V}$$
2	1	brdom	$$⊢A\preccurlyeq y\leftrightarrow \exists ff:A\underset{1-1}{⟶}y$$
3		onss	$$⊢y\in \mathrm{On}\to y\subseteq \mathrm{On}$$
4	3	a1i	$$⊢f:A\underset{1-1}{⟶}y\to \left(y\in \mathrm{On}\to y\subseteq \mathrm{On}\right)$$
5		epweon	$$⊢\mathrm{E}\mathrm{We}\mathrm{On}$$
6		wess	$$⊢y\subseteq \mathrm{On}\to \left(\mathrm{E}\mathrm{We}\mathrm{On}\to \mathrm{E}\mathrm{We}y\right)$$
7	4 5 6	syl6mpi	$$⊢f:A\underset{1-1}{⟶}y\to \left(y\in \mathrm{On}\to \mathrm{E}\mathrm{We}y\right)$$
8	7	adantl	$$⊢\left(A\preccurlyeq y\wedge f:A\underset{1-1}{⟶}y\right)\to \left(y\in \mathrm{On}\to \mathrm{E}\mathrm{We}y\right)$$
9		eqid	$$⊢\left\{⟨w,z⟩|f\left(w\right)\mathrm{E}f\left(z\right)\right\}=\left\{⟨w,z⟩|f\left(w\right)\mathrm{E}f\left(z\right)\right\}$$
10	9	f1we	$$⊢f:A\underset{1-1}{⟶}y\to \left(\mathrm{E}\mathrm{We}y\to \left\{⟨w,z⟩|f\left(w\right)\mathrm{E}f\left(z\right)\right\}\mathrm{We}A\right)$$
11		weinxp	$$⊢\left\{⟨w,z⟩|f\left(w\right)\mathrm{E}f\left(z\right)\right\}\mathrm{We}A\leftrightarrow \left(\left\{⟨w,z⟩|f\left(w\right)\mathrm{E}f\left(z\right)\right\}\cap \left(A\times A\right)\right)\mathrm{We}A$$
12		reldom	$$⊢\mathrm{Rel}\preccurlyeq$$
13	12	brrelex1i	$$⊢A\preccurlyeq y\to A\in \mathrm{V}$$
14		sqxpexg	$$⊢A\in \mathrm{V}\to A\times A\in \mathrm{V}$$
15		inex2g	$$⊢A\times A\in \mathrm{V}\to \left\{⟨w,z⟩|f\left(w\right)\mathrm{E}f\left(z\right)\right\}\cap \left(A\times A\right)\in \mathrm{V}$$
16		weeq1	$$⊢x=\left\{⟨w,z⟩|f\left(w\right)\mathrm{E}f\left(z\right)\right\}\cap \left(A\times A\right)\to \left(x\mathrm{We}A\leftrightarrow \left(\left\{⟨w,z⟩|f\left(w\right)\mathrm{E}f\left(z\right)\right\}\cap \left(A\times A\right)\right)\mathrm{We}A\right)$$
17	16	spcegv	$$⊢\left\{⟨w,z⟩|f\left(w\right)\mathrm{E}f\left(z\right)\right\}\cap \left(A\times A\right)\in \mathrm{V}\to \left(\left(\left\{⟨w,z⟩|f\left(w\right)\mathrm{E}f\left(z\right)\right\}\cap \left(A\times A\right)\right)\mathrm{We}A\to \exists xx\mathrm{We}A\right)$$
18	13 14 15 17	4syl	$$⊢A\preccurlyeq y\to \left(\left(\left\{⟨w,z⟩|f\left(w\right)\mathrm{E}f\left(z\right)\right\}\cap \left(A\times A\right)\right)\mathrm{We}A\to \exists xx\mathrm{We}A\right)$$
19	11 18	biimtrid	$$⊢A\preccurlyeq y\to \left(\left\{⟨w,z⟩|f\left(w\right)\mathrm{E}f\left(z\right)\right\}\mathrm{We}A\to \exists xx\mathrm{We}A\right)$$
20	10 19	sylan9r	$$⊢\left(A\preccurlyeq y\wedge f:A\underset{1-1}{⟶}y\right)\to \left(\mathrm{E}\mathrm{We}y\to \exists xx\mathrm{We}A\right)$$
21	8 20	syld	$$⊢\left(A\preccurlyeq y\wedge f:A\underset{1-1}{⟶}y\right)\to \left(y\in \mathrm{On}\to \exists xx\mathrm{We}A\right)$$
22	21	impancom	$$⊢\left(A\preccurlyeq y\wedge y\in \mathrm{On}\right)\to \left(f:A\underset{1-1}{⟶}y\to \exists xx\mathrm{We}A\right)$$
23	22	exlimdv	$$⊢\left(A\preccurlyeq y\wedge y\in \mathrm{On}\right)\to \left(\exists ff:A\underset{1-1}{⟶}y\to \exists xx\mathrm{We}A\right)$$
24	2 23	biimtrid	$$⊢\left(A\preccurlyeq y\wedge y\in \mathrm{On}\right)\to \left(A\preccurlyeq y\to \exists xx\mathrm{We}A\right)$$
25	24	ex	$$⊢A\preccurlyeq y\to \left(y\in \mathrm{On}\to \left(A\preccurlyeq y\to \exists xx\mathrm{We}A\right)\right)$$
26	25	pm2.43b	$$⊢y\in \mathrm{On}\to \left(A\preccurlyeq y\to \exists xx\mathrm{We}A\right)$$
27	26	rexlimiv	$$⊢\exists y\in \mathrm{On}A\preccurlyeq y\to \exists xx\mathrm{We}A$$