Theorem isfin5-2

Description: Alternate definition of V-finite which emphasizes the idempotent behavior of V-infinite sets. (Contributed by Stefan O'Rear, 30-Oct-2014) (Revised by Mario Carneiro, 17-May-2015)

	Ref	Expression
Assertion	isfin5-2	$$⊢A\in V\to \left(A\in {\mathrm{Fin}}^{\mathrm{V}}\leftrightarrow \neg \left(A\ne \varnothing \wedge A\approx \left(A\mathrm{\bigsqcup ︀}A\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		nne	$$⊢\neg A\ne \varnothing \leftrightarrow A=\varnothing$$
2	1	bicomi	$$⊢A=\varnothing \leftrightarrow \neg A\ne \varnothing$$
3	2	a1i	$$⊢A\in V\to \left(A=\varnothing \leftrightarrow \neg A\ne \varnothing \right)$$
4		djudoml	$$⊢\left(A\in V\wedge A\in V\right)\to A\preccurlyeq \left(A\mathrm{\bigsqcup ︀}A\right)$$
5	4	anidms	$$⊢A\in V\to A\preccurlyeq \left(A\mathrm{\bigsqcup ︀}A\right)$$
6		brsdom	$$⊢A\prec \left(A\mathrm{\bigsqcup ︀}A\right)\leftrightarrow \left(A\preccurlyeq \left(A\mathrm{\bigsqcup ︀}A\right)\wedge \neg A\approx \left(A\mathrm{\bigsqcup ︀}A\right)\right)$$
7	6	baib	$$⊢A\preccurlyeq \left(A\mathrm{\bigsqcup ︀}A\right)\to \left(A\prec \left(A\mathrm{\bigsqcup ︀}A\right)\leftrightarrow \neg A\approx \left(A\mathrm{\bigsqcup ︀}A\right)\right)$$
8	5 7	syl	$$⊢A\in V\to \left(A\prec \left(A\mathrm{\bigsqcup ︀}A\right)\leftrightarrow \neg A\approx \left(A\mathrm{\bigsqcup ︀}A\right)\right)$$
9	3 8	orbi12d	$$⊢A\in V\to \left(\left(A=\varnothing \vee A\prec \left(A\mathrm{\bigsqcup ︀}A\right)\right)\leftrightarrow \left(\neg A\ne \varnothing \vee \neg A\approx \left(A\mathrm{\bigsqcup ︀}A\right)\right)\right)$$
10		isfin5	$$⊢A\in {\mathrm{Fin}}^{\mathrm{V}}\leftrightarrow \left(A=\varnothing \vee A\prec \left(A\mathrm{\bigsqcup ︀}A\right)\right)$$
11		ianor	$$⊢\neg \left(A\ne \varnothing \wedge A\approx \left(A\mathrm{\bigsqcup ︀}A\right)\right)\leftrightarrow \left(\neg A\ne \varnothing \vee \neg A\approx \left(A\mathrm{\bigsqcup ︀}A\right)\right)$$
12	9 10 11	3bitr4g	$$⊢A\in V\to \left(A\in {\mathrm{Fin}}^{\mathrm{V}}\leftrightarrow \neg \left(A\ne \varnothing \wedge A\approx \left(A\mathrm{\bigsqcup ︀}A\right)\right)\right)$$