Theorem isfin5

Description: Definition of a V-finite set. (Contributed by Stefan O'Rear, 16-May-2015)

	Ref	Expression
Assertion	isfin5	$$⊢A\in {\mathrm{Fin}}^{\mathrm{V}}\leftrightarrow \left(A=\varnothing \vee A\prec \left(A\mathrm{\bigsqcup ︀}A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-fin5	$$⊢{\mathrm{Fin}}^{\mathrm{V}}=\left\{x|\left(x=\varnothing \vee x\prec \left(x\mathrm{\bigsqcup ︀}x\right)\right)\right\}$$
2	1	eleq2i	$$⊢A\in {\mathrm{Fin}}^{\mathrm{V}}\leftrightarrow A\in \left\{x|\left(x=\varnothing \vee x\prec \left(x\mathrm{\bigsqcup ︀}x\right)\right)\right\}$$
3		id	$$⊢A=\varnothing \to A=\varnothing$$
4		0ex	$$⊢\varnothing \in \mathrm{V}$$
5	3 4	eqeltrdi	$$⊢A=\varnothing \to A\in \mathrm{V}$$
6		relsdom	$$⊢\mathrm{Rel}\prec$$
7	6	brrelex1i	$$⊢A\prec \left(A\mathrm{\bigsqcup ︀}A\right)\to A\in \mathrm{V}$$
8	5 7	jaoi	$$⊢\left(A=\varnothing \vee A\prec \left(A\mathrm{\bigsqcup ︀}A\right)\right)\to A\in \mathrm{V}$$
9		eqeq1	$$⊢x=A\to \left(x=\varnothing \leftrightarrow A=\varnothing \right)$$
10		id	$$⊢x=A\to x=A$$
11		djueq12	$$⊢\left(x=A\wedge x=A\right)\to \left(x\mathrm{\bigsqcup ︀}x\right)=\left(A\mathrm{\bigsqcup ︀}A\right)$$
12	11	anidms	$$⊢x=A\to \left(x\mathrm{\bigsqcup ︀}x\right)=\left(A\mathrm{\bigsqcup ︀}A\right)$$
13	10 12	breq12d	$$⊢x=A\to \left(x\prec \left(x\mathrm{\bigsqcup ︀}x\right)\leftrightarrow A\prec \left(A\mathrm{\bigsqcup ︀}A\right)\right)$$
14	9 13	orbi12d	$$⊢x=A\to \left(\left(x=\varnothing \vee x\prec \left(x\mathrm{\bigsqcup ︀}x\right)\right)\leftrightarrow \left(A=\varnothing \vee A\prec \left(A\mathrm{\bigsqcup ︀}A\right)\right)\right)$$
15	8 14	elab3	$$⊢A\in \left\{x|\left(x=\varnothing \vee x\prec \left(x\mathrm{\bigsqcup ︀}x\right)\right)\right\}\leftrightarrow \left(A=\varnothing \vee A\prec \left(A\mathrm{\bigsqcup ︀}A\right)\right)$$
16	2 15	bitri	$$⊢A\in {\mathrm{Fin}}^{\mathrm{V}}\leftrightarrow \left(A=\varnothing \vee A\prec \left(A\mathrm{\bigsqcup ︀}A\right)\right)$$