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		inex2g	$$⊢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}$$
6	4 5	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}$$
7		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)$$
8		cardon	$$⊢\mathrm{card}\left(A\right)\in \mathrm{On}$$
9	8	onordi	$$⊢\mathrm{Ord}\mathrm{card}\left(A\right)$$
10		ordwe	$$⊢\mathrm{Ord}\mathrm{card}\left(A\right)\to \mathrm{E}\mathrm{We}\mathrm{card}\left(A\right)$$
11	9 10	ax-mp	$$⊢\mathrm{E}\mathrm{We}\mathrm{card}\left(A\right)$$
12		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\}$$
13	12	f1owe	$$⊢f^{-1}:A\underset{1-1\; onto}{⟶}\mathrm{card}\left(A\right)\to \left(\left\{⟨z,w⟩|f^{-1}\left(z\right)\mathrm{E}{f}^{-1}\left(w\right)\right\}\mathrm{We}A\leftrightarrow \mathrm{E}\mathrm{We}\mathrm{card}\left(A\right)\right)$$
14	11 13	mpbiri	$$⊢f^{-1}:A\underset{1-1\; onto}{⟶}\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$$
15	7 14	syl	$$⊢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$$
16		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$$
17	15 16	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$$
18		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)$$
19	18	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)$$
20	6 17 19	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)$$
21	20	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)$$
22	3 21	mpd	$$⊢A\in \mathrm{dom}\mathrm{card}\to \exists xx\mathrm{We}A$$