Theorem dfac8b

Description: The well-ordering theorem: every numerable set is well-orderable. (Contributed by Mario Carneiro, 5-Jan-2013) (Revised by Mario Carneiro, 29-Apr-2015)

	Ref	Expression
Assertion	dfac8b	$$⊢A\in \mathrm{dom}\mathrm{card}\to \exists xx\mathrm{We}A$$

Proof

Step	Hyp	Ref	Expression
1		cardid2	$$⊢A\in \mathrm{dom}\mathrm{card}\to \mathrm{card}\left(A\right)\approx A$$
2		bren	$$⊢\mathrm{card}\left(A\right)\approx A\leftrightarrow \exists ff:\mathrm{card}\left(A\right)\underset{1-1\; onto}{⟶}A$$
3	1 2	sylib	$$⊢A\in \mathrm{dom}\mathrm{card}\to \exists ff:\mathrm{card}\left(A\right)\underset{1-1\; onto}{⟶}A$$
4		sqxpexg	$$⊢A\in \mathrm{dom}\mathrm{card}\to A\times A\in \mathrm{V}$$
5		incom	$$⊢\left\{⟨z,w⟩|f^{-1}\left(z\right)\mathrm{E}{f}^{-1}\left(w\right)\right\}\cap \left(A\times A\right)=\left(A\times A\right)\cap \left\{⟨z,w⟩|f^{-1}\left(z\right)\mathrm{E}{f}^{-1}\left(w\right)\right\}$$
6		inex1g	$$⊢A\times A\in \mathrm{V}\to \left(A\times A\right)\cap \left\{⟨z,w⟩|f^{-1}\left(z\right)\mathrm{E}{f}^{-1}\left(w\right)\right\}\in \mathrm{V}$$
7	5 6	eqeltrid	$$⊢A\times A\in \mathrm{V}\to \left\{⟨z,w⟩|f^{-1}\left(z\right)\mathrm{E}{f}^{-1}\left(w\right)\right\}\cap \left(A\times A\right)\in \mathrm{V}$$
8	4 7	syl	$$⊢A\in \mathrm{dom}\mathrm{card}\to \left\{⟨z,w⟩|f^{-1}\left(z\right)\mathrm{E}{f}^{-1}\left(w\right)\right\}\cap \left(A\times A\right)\in \mathrm{V}$$
9		f1ocnv	$$⊢f:\mathrm{card}\left(A\right)\underset{1-1\; onto}{⟶}A\to f^{-1}:A\underset{1-1\; onto}{⟶}\mathrm{card}\left(A\right)$$
10		cardon	$$⊢\mathrm{card}\left(A\right)\in \mathrm{On}$$
11	10	onordi	$$⊢\mathrm{Ord}\mathrm{card}\left(A\right)$$
12		ordwe	$$⊢\mathrm{Ord}\mathrm{card}\left(A\right)\to \mathrm{E}\mathrm{We}\mathrm{card}\left(A\right)$$
13	11 12	ax-mp	$$⊢\mathrm{E}\mathrm{We}\mathrm{card}\left(A\right)$$
14		eqid	$$⊢\left\{⟨z,w⟩|f^{-1}\left(z\right)\mathrm{E}{f}^{-1}\left(w\right)\right\}=\left\{⟨z,w⟩|f^{-1}\left(z\right)\mathrm{E}{f}^{-1}\left(w\right)\right\}$$
15	14	f1owe	$$⊢f^{-1}:A\underset{1-1\; onto}{⟶}\mathrm{card}\left(A\right)\to \left(\mathrm{E}\mathrm{We}\mathrm{card}\left(A\right)\to \left\{⟨z,w⟩|f^{-1}\left(z\right)\mathrm{E}{f}^{-1}\left(w\right)\right\}\mathrm{We}A\right)$$
16	9 13 15	mpisyl	$$⊢f:\mathrm{card}\left(A\right)\underset{1-1\; onto}{⟶}A\to \left\{⟨z,w⟩|f^{-1}\left(z\right)\mathrm{E}{f}^{-1}\left(w\right)\right\}\mathrm{We}A$$
17		weinxp	$$⊢\left\{⟨z,w⟩|f^{-1}\left(z\right)\mathrm{E}{f}^{-1}\left(w\right)\right\}\mathrm{We}A\leftrightarrow \left(\left\{⟨z,w⟩|f^{-1}\left(z\right)\mathrm{E}{f}^{-1}\left(w\right)\right\}\cap \left(A\times A\right)\right)\mathrm{We}A$$
18	16 17	sylib	$$⊢f:\mathrm{card}\left(A\right)\underset{1-1\; onto}{⟶}A\to \left(\left\{⟨z,w⟩|f^{-1}\left(z\right)\mathrm{E}{f}^{-1}\left(w\right)\right\}\cap \left(A\times A\right)\right)\mathrm{We}A$$
19		weeq1	$$⊢x=\left\{⟨z,w⟩|f^{-1}\left(z\right)\mathrm{E}{f}^{-1}\left(w\right)\right\}\cap \left(A\times A\right)\to \left(x\mathrm{We}A\leftrightarrow \left(\left\{⟨z,w⟩|f^{-1}\left(z\right)\mathrm{E}{f}^{-1}\left(w\right)\right\}\cap \left(A\times A\right)\right)\mathrm{We}A\right)$$
20	19	spcegv	$$⊢\left\{⟨z,w⟩|f^{-1}\left(z\right)\mathrm{E}{f}^{-1}\left(w\right)\right\}\cap \left(A\times A\right)\in \mathrm{V}\to \left(\left(\left\{⟨z,w⟩|f^{-1}\left(z\right)\mathrm{E}{f}^{-1}\left(w\right)\right\}\cap \left(A\times A\right)\right)\mathrm{We}A\to \exists xx\mathrm{We}A\right)$$
21	8 18 20	syl2im	$$⊢A\in \mathrm{dom}\mathrm{card}\to \left(f:\mathrm{card}\left(A\right)\underset{1-1\; onto}{⟶}A\to \exists xx\mathrm{We}A\right)$$
22	21	exlimdv	$$⊢A\in \mathrm{dom}\mathrm{card}\to \left(\exists ff:\mathrm{card}\left(A\right)\underset{1-1\; onto}{⟶}A\to \exists xx\mathrm{We}A\right)$$
23	3 22	mpd	$$⊢A\in \mathrm{dom}\mathrm{card}\to \exists xx\mathrm{We}A$$