Theorem ttac

Description: Tarski's theorem about choice: infxpidm is equivalent to ax-ac . (Contributed by Stefan O'Rear, 4-Nov-2014) (Proof shortened by Stefan O'Rear, 10-Jul-2015)

	Ref	Expression
Assertion	ttac	$$⊢\mathrm{CHOICE}\leftrightarrow \forall c\left(\mathrm{\omega }\preccurlyeq c\to \left(c\times c\right)\approx c\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfac10	$$⊢\mathrm{CHOICE}\leftrightarrow \mathrm{dom}\mathrm{card}=\mathrm{V}$$
2		vex	$$⊢c\in \mathrm{V}$$
3		eleq2	$$⊢\mathrm{dom}\mathrm{card}=\mathrm{V}\to \left(c\in \mathrm{dom}\mathrm{card}\leftrightarrow c\in \mathrm{V}\right)$$
4	2 3	mpbiri	$$⊢\mathrm{dom}\mathrm{card}=\mathrm{V}\to c\in \mathrm{dom}\mathrm{card}$$
5		infxpidm2	$$⊢\left(c\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq c\right)\to \left(c\times c\right)\approx c$$
6	5	ex	$$⊢c\in \mathrm{dom}\mathrm{card}\to \left(\mathrm{\omega }\preccurlyeq c\to \left(c\times c\right)\approx c\right)$$
7	4 6	syl	$$⊢\mathrm{dom}\mathrm{card}=\mathrm{V}\to \left(\mathrm{\omega }\preccurlyeq c\to \left(c\times c\right)\approx c\right)$$
8	7	alrimiv	$$⊢\mathrm{dom}\mathrm{card}=\mathrm{V}\to \forall c\left(\mathrm{\omega }\preccurlyeq c\to \left(c\times c\right)\approx c\right)$$
9		finnum	$$⊢a\in \mathrm{Fin}\to a\in \mathrm{dom}\mathrm{card}$$
10	9	adantl	$$⊢\left(\forall c\left(\mathrm{\omega }\preccurlyeq c\to \left(c\times c\right)\approx c\right)\wedge a\in \mathrm{Fin}\right)\to a\in \mathrm{dom}\mathrm{card}$$
11		harcl	$$⊢\mathrm{har}\left(a\right)\in \mathrm{On}$$
12		onenon	$$⊢\mathrm{har}\left(a\right)\in \mathrm{On}\to \mathrm{har}\left(a\right)\in \mathrm{dom}\mathrm{card}$$
13	11 12	ax-mp	$$⊢\mathrm{har}\left(a\right)\in \mathrm{dom}\mathrm{card}$$
14		fvex	$$⊢\mathrm{har}\left(a\right)\in \mathrm{V}$$
15		vex	$$⊢a\in \mathrm{V}$$
16	14 15	unex	$$⊢\mathrm{har}\left(a\right)\cup a\in \mathrm{V}$$
17		harinf	$$⊢\left(a\in \mathrm{V}\wedge \neg a\in \mathrm{Fin}\right)\to \mathrm{\omega }\subseteq \mathrm{har}\left(a\right)$$
18	15 17	mpan	$$⊢\neg a\in \mathrm{Fin}\to \mathrm{\omega }\subseteq \mathrm{har}\left(a\right)$$
19		ssun1	$$⊢\mathrm{har}\left(a\right)\subseteq \mathrm{har}\left(a\right)\cup a$$
20	18 19	sstrdi	$$⊢\neg a\in \mathrm{Fin}\to \mathrm{\omega }\subseteq \mathrm{har}\left(a\right)\cup a$$
21		ssdomg	$$⊢\mathrm{har}\left(a\right)\cup a\in \mathrm{V}\to \left(\mathrm{\omega }\subseteq \mathrm{har}\left(a\right)\cup a\to \mathrm{\omega }\preccurlyeq \left(\mathrm{har}\left(a\right)\cup a\right)\right)$$
22	16 20 21	mpsyl	$$⊢\neg a\in \mathrm{Fin}\to \mathrm{\omega }\preccurlyeq \left(\mathrm{har}\left(a\right)\cup a\right)$$
23		breq2	$$⊢c=\mathrm{har}\left(a\right)\cup a\to \left(\mathrm{\omega }\preccurlyeq c\leftrightarrow \mathrm{\omega }\preccurlyeq \left(\mathrm{har}\left(a\right)\cup a\right)\right)$$
24		xpeq12	$$⊢\left(c=\mathrm{har}\left(a\right)\cup a\wedge c=\mathrm{har}\left(a\right)\cup a\right)\to c\times c=\left(\mathrm{har}\left(a\right)\cup a\right)\times \left(\mathrm{har}\left(a\right)\cup a\right)$$
25	24	anidms	$$⊢c=\mathrm{har}\left(a\right)\cup a\to c\times c=\left(\mathrm{har}\left(a\right)\cup a\right)\times \left(\mathrm{har}\left(a\right)\cup a\right)$$
26		id	$$⊢c=\mathrm{har}\left(a\right)\cup a\to c=\mathrm{har}\left(a\right)\cup a$$
27	25 26	breq12d	$$⊢c=\mathrm{har}\left(a\right)\cup a\to \left(\left(c\times c\right)\approx c\leftrightarrow \left(\left(\mathrm{har}\left(a\right)\cup a\right)\times \left(\mathrm{har}\left(a\right)\cup a\right)\right)\approx \left(\mathrm{har}\left(a\right)\cup a\right)\right)$$
28	23 27	imbi12d	$$⊢c=\mathrm{har}\left(a\right)\cup a\to \left(\left(\mathrm{\omega }\preccurlyeq c\to \left(c\times c\right)\approx c\right)\leftrightarrow \left(\mathrm{\omega }\preccurlyeq \left(\mathrm{har}\left(a\right)\cup a\right)\to \left(\left(\mathrm{har}\left(a\right)\cup a\right)\times \left(\mathrm{har}\left(a\right)\cup a\right)\right)\approx \left(\mathrm{har}\left(a\right)\cup a\right)\right)\right)$$
29	16 28	spcv	$$⊢\forall c\left(\mathrm{\omega }\preccurlyeq c\to \left(c\times c\right)\approx c\right)\to \left(\mathrm{\omega }\preccurlyeq \left(\mathrm{har}\left(a\right)\cup a\right)\to \left(\left(\mathrm{har}\left(a\right)\cup a\right)\times \left(\mathrm{har}\left(a\right)\cup a\right)\right)\approx \left(\mathrm{har}\left(a\right)\cup a\right)\right)$$
30	22 29	syl5	$$⊢\forall c\left(\mathrm{\omega }\preccurlyeq c\to \left(c\times c\right)\approx c\right)\to \left(\neg a\in \mathrm{Fin}\to \left(\left(\mathrm{har}\left(a\right)\cup a\right)\times \left(\mathrm{har}\left(a\right)\cup a\right)\right)\approx \left(\mathrm{har}\left(a\right)\cup a\right)\right)$$
31	30	imp	$$⊢\left(\forall c\left(\mathrm{\omega }\preccurlyeq c\to \left(c\times c\right)\approx c\right)\wedge \neg a\in \mathrm{Fin}\right)\to \left(\left(\mathrm{har}\left(a\right)\cup a\right)\times \left(\mathrm{har}\left(a\right)\cup a\right)\right)\approx \left(\mathrm{har}\left(a\right)\cup a\right)$$
32		harndom	$$⊢\neg \mathrm{har}\left(a\right)\preccurlyeq a$$
33		ssdomg	$$⊢\mathrm{har}\left(a\right)\cup a\in \mathrm{V}\to \left(\mathrm{har}\left(a\right)\subseteq \mathrm{har}\left(a\right)\cup a\to \mathrm{har}\left(a\right)\preccurlyeq \left(\mathrm{har}\left(a\right)\cup a\right)\right)$$
34	16 19 33	mp2	$$⊢\mathrm{har}\left(a\right)\preccurlyeq \left(\mathrm{har}\left(a\right)\cup a\right)$$
35		domtr	$$⊢\left(\mathrm{har}\left(a\right)\preccurlyeq \left(\mathrm{har}\left(a\right)\cup a\right)\wedge \left(\mathrm{har}\left(a\right)\cup a\right)\preccurlyeq a\right)\to \mathrm{har}\left(a\right)\preccurlyeq a$$
36	34 35	mpan	$$⊢\left(\mathrm{har}\left(a\right)\cup a\right)\preccurlyeq a\to \mathrm{har}\left(a\right)\preccurlyeq a$$
37	32 36	mto	$$⊢\neg \left(\mathrm{har}\left(a\right)\cup a\right)\preccurlyeq a$$
38		unxpwdom2	$$⊢\left(\left(\mathrm{har}\left(a\right)\cup a\right)\times \left(\mathrm{har}\left(a\right)\cup a\right)\right)\approx \left(\mathrm{har}\left(a\right)\cup a\right)\to \left(\left(\mathrm{har}\left(a\right)\cup a\right){\preccurlyeq }^{*}\mathrm{har}\left(a\right)\vee \left(\mathrm{har}\left(a\right)\cup a\right)\preccurlyeq a\right)$$
39		orel2	$$⊢\neg \left(\mathrm{har}\left(a\right)\cup a\right)\preccurlyeq a\to \left(\left(\left(\mathrm{har}\left(a\right)\cup a\right){\preccurlyeq }^{*}\mathrm{har}\left(a\right)\vee \left(\mathrm{har}\left(a\right)\cup a\right)\preccurlyeq a\right)\to \left(\mathrm{har}\left(a\right)\cup a\right){\preccurlyeq }^{*}\mathrm{har}\left(a\right)\right)$$
40	37 38 39	mpsyl	$$⊢\left(\left(\mathrm{har}\left(a\right)\cup a\right)\times \left(\mathrm{har}\left(a\right)\cup a\right)\right)\approx \left(\mathrm{har}\left(a\right)\cup a\right)\to \left(\mathrm{har}\left(a\right)\cup a\right){\preccurlyeq }^{*}\mathrm{har}\left(a\right)$$
41	31 40	syl	$$⊢\left(\forall c\left(\mathrm{\omega }\preccurlyeq c\to \left(c\times c\right)\approx c\right)\wedge \neg a\in \mathrm{Fin}\right)\to \left(\mathrm{har}\left(a\right)\cup a\right){\preccurlyeq }^{*}\mathrm{har}\left(a\right)$$
42		wdomnumr	$$⊢\mathrm{har}\left(a\right)\in \mathrm{dom}\mathrm{card}\to \left(\left(\mathrm{har}\left(a\right)\cup a\right){\preccurlyeq }^{*}\mathrm{har}\left(a\right)\leftrightarrow \left(\mathrm{har}\left(a\right)\cup a\right)\preccurlyeq \mathrm{har}\left(a\right)\right)$$
43	13 42	ax-mp	$$⊢\left(\mathrm{har}\left(a\right)\cup a\right){\preccurlyeq }^{*}\mathrm{har}\left(a\right)\leftrightarrow \left(\mathrm{har}\left(a\right)\cup a\right)\preccurlyeq \mathrm{har}\left(a\right)$$
44	41 43	sylib	$$⊢\left(\forall c\left(\mathrm{\omega }\preccurlyeq c\to \left(c\times c\right)\approx c\right)\wedge \neg a\in \mathrm{Fin}\right)\to \left(\mathrm{har}\left(a\right)\cup a\right)\preccurlyeq \mathrm{har}\left(a\right)$$
45		numdom	$$⊢\left(\mathrm{har}\left(a\right)\in \mathrm{dom}\mathrm{card}\wedge \left(\mathrm{har}\left(a\right)\cup a\right)\preccurlyeq \mathrm{har}\left(a\right)\right)\to \mathrm{har}\left(a\right)\cup a\in \mathrm{dom}\mathrm{card}$$
46	13 44 45	sylancr	$$⊢\left(\forall c\left(\mathrm{\omega }\preccurlyeq c\to \left(c\times c\right)\approx c\right)\wedge \neg a\in \mathrm{Fin}\right)\to \mathrm{har}\left(a\right)\cup a\in \mathrm{dom}\mathrm{card}$$
47		ssun2	$$⊢a\subseteq \mathrm{har}\left(a\right)\cup a$$
48		ssnum	$$⊢\left(\mathrm{har}\left(a\right)\cup a\in \mathrm{dom}\mathrm{card}\wedge a\subseteq \mathrm{har}\left(a\right)\cup a\right)\to a\in \mathrm{dom}\mathrm{card}$$
49	46 47 48	sylancl	$$⊢\left(\forall c\left(\mathrm{\omega }\preccurlyeq c\to \left(c\times c\right)\approx c\right)\wedge \neg a\in \mathrm{Fin}\right)\to a\in \mathrm{dom}\mathrm{card}$$
50	10 49	pm2.61dan	$$⊢\forall c\left(\mathrm{\omega }\preccurlyeq c\to \left(c\times c\right)\approx c\right)\to a\in \mathrm{dom}\mathrm{card}$$
51	50	alrimiv	$$⊢\forall c\left(\mathrm{\omega }\preccurlyeq c\to \left(c\times c\right)\approx c\right)\to \forall aa\in \mathrm{dom}\mathrm{card}$$
52		eqv	$$⊢\mathrm{dom}\mathrm{card}=\mathrm{V}\leftrightarrow \forall aa\in \mathrm{dom}\mathrm{card}$$
53	51 52	sylibr	$$⊢\forall c\left(\mathrm{\omega }\preccurlyeq c\to \left(c\times c\right)\approx c\right)\to \mathrm{dom}\mathrm{card}=\mathrm{V}$$
54	8 53	impbii	$$⊢\mathrm{dom}\mathrm{card}=\mathrm{V}\leftrightarrow \forall c\left(\mathrm{\omega }\preccurlyeq c\to \left(c\times c\right)\approx c\right)$$
55	1 54	bitri	$$⊢\mathrm{CHOICE}\leftrightarrow \forall c\left(\mathrm{\omega }\preccurlyeq c\to \left(c\times c\right)\approx c\right)$$