Theorem dfacfin7

Description: Axiom of Choice equivalent: the VII-finite sets are the same as I-finite sets. (Contributed by Mario Carneiro, 18-May-2015)

	Ref	Expression
Assertion	dfacfin7	$$⊢\mathrm{CHOICE}\leftrightarrow {\mathrm{Fin}}^{\mathrm{VII}}=\mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		ssequn2	$$⊢\mathrm{V}\setminus \mathrm{dom}\mathrm{card}\subseteq \mathrm{Fin}\leftrightarrow \mathrm{Fin}\cup \left(\mathrm{V}\setminus \mathrm{dom}\mathrm{card}\right)=\mathrm{Fin}$$
2		dfac10	$$⊢\mathrm{CHOICE}\leftrightarrow \mathrm{dom}\mathrm{card}=\mathrm{V}$$
3		finnum	$$⊢x\in \mathrm{Fin}\to x\in \mathrm{dom}\mathrm{card}$$
4	3	ssriv	$$⊢\mathrm{Fin}\subseteq \mathrm{dom}\mathrm{card}$$
5		ssequn2	$$⊢\mathrm{Fin}\subseteq \mathrm{dom}\mathrm{card}\leftrightarrow \mathrm{dom}\mathrm{card}\cup \mathrm{Fin}=\mathrm{dom}\mathrm{card}$$
6	4 5	mpbi	$$⊢\mathrm{dom}\mathrm{card}\cup \mathrm{Fin}=\mathrm{dom}\mathrm{card}$$
7	6	eqeq1i	$$⊢\mathrm{dom}\mathrm{card}\cup \mathrm{Fin}=\mathrm{V}\leftrightarrow \mathrm{dom}\mathrm{card}=\mathrm{V}$$
8	2 7	bitr4i	$$⊢\mathrm{CHOICE}\leftrightarrow \mathrm{dom}\mathrm{card}\cup \mathrm{Fin}=\mathrm{V}$$
9		ssv	$$⊢\mathrm{dom}\mathrm{card}\cup \mathrm{Fin}\subseteq \mathrm{V}$$
10		eqss	$$⊢\mathrm{dom}\mathrm{card}\cup \mathrm{Fin}=\mathrm{V}\leftrightarrow \left(\mathrm{dom}\mathrm{card}\cup \mathrm{Fin}\subseteq \mathrm{V}\wedge \mathrm{V}\subseteq \mathrm{dom}\mathrm{card}\cup \mathrm{Fin}\right)$$
11	9 10	mpbiran	$$⊢\mathrm{dom}\mathrm{card}\cup \mathrm{Fin}=\mathrm{V}\leftrightarrow \mathrm{V}\subseteq \mathrm{dom}\mathrm{card}\cup \mathrm{Fin}$$
12		ssundif	$$⊢\mathrm{V}\subseteq \mathrm{dom}\mathrm{card}\cup \mathrm{Fin}\leftrightarrow \mathrm{V}\setminus \mathrm{dom}\mathrm{card}\subseteq \mathrm{Fin}$$
13	8 11 12	3bitri	$$⊢\mathrm{CHOICE}\leftrightarrow \mathrm{V}\setminus \mathrm{dom}\mathrm{card}\subseteq \mathrm{Fin}$$
14		dffin7-2	$$⊢{\mathrm{Fin}}^{\mathrm{VII}}=\mathrm{Fin}\cup \left(\mathrm{V}\setminus \mathrm{dom}\mathrm{card}\right)$$
15	14	eqeq1i	$$⊢{\mathrm{Fin}}^{\mathrm{VII}}=\mathrm{Fin}\leftrightarrow \mathrm{Fin}\cup \left(\mathrm{V}\setminus \mathrm{dom}\mathrm{card}\right)=\mathrm{Fin}$$
16	1 13 15	3bitr4i	$$⊢\mathrm{CHOICE}\leftrightarrow {\mathrm{Fin}}^{\mathrm{VII}}=\mathrm{Fin}$$