Theorem isfin6

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

	Ref	Expression
Assertion	isfin6	$$⊢A\in {\mathrm{Fin}}^{\mathrm{VI}}\leftrightarrow \left(A\prec 2_{𝑜}\vee A\prec \left(A\times A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-fin6	$$⊢{\mathrm{Fin}}^{\mathrm{VI}}=\left\{x|\left(x\prec 2_{𝑜}\vee x\prec \left(x\times x\right)\right)\right\}$$
2	1	eleq2i	$$⊢A\in {\mathrm{Fin}}^{\mathrm{VI}}\leftrightarrow A\in \left\{x|\left(x\prec 2_{𝑜}\vee x\prec \left(x\times x\right)\right)\right\}$$
3		relsdom	$$⊢\mathrm{Rel}\prec$$
4	3	brrelex1i	$$⊢A\prec 2_{𝑜}\to A\in \mathrm{V}$$
5	3	brrelex1i	$$⊢A\prec \left(A\times A\right)\to A\in \mathrm{V}$$
6	4 5	jaoi	$$⊢\left(A\prec 2_{𝑜}\vee A\prec \left(A\times A\right)\right)\to A\in \mathrm{V}$$
7		breq1	$$⊢x=A\to \left(x\prec 2_{𝑜}\leftrightarrow A\prec 2_{𝑜}\right)$$
8		id	$$⊢x=A\to x=A$$
9	8	sqxpeqd	$$⊢x=A\to x\times x=A\times A$$
10	8 9	breq12d	$$⊢x=A\to \left(x\prec \left(x\times x\right)\leftrightarrow A\prec \left(A\times A\right)\right)$$
11	7 10	orbi12d	$$⊢x=A\to \left(\left(x\prec 2_{𝑜}\vee x\prec \left(x\times x\right)\right)\leftrightarrow \left(A\prec 2_{𝑜}\vee A\prec \left(A\times A\right)\right)\right)$$
12	6 11	elab3	$$⊢A\in \left\{x|\left(x\prec 2_{𝑜}\vee x\prec \left(x\times x\right)\right)\right\}\leftrightarrow \left(A\prec 2_{𝑜}\vee A\prec \left(A\times A\right)\right)$$
13	2 12	bitri	$$⊢A\in {\mathrm{Fin}}^{\mathrm{VI}}\leftrightarrow \left(A\prec 2_{𝑜}\vee A\prec \left(A\times A\right)\right)$$