isfin6

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

		Ref	Expression
	Assertion	isfin6	$⊢ A \in {Fin}^{VI} \leftrightarrow (A ≺ 2_{𝑜} \lor A ≺ (A \times A))$

Step	Hyp	Ref	Expression
1		df-fin6	$⊢ {Fin}^{VI} = \{x \| (x ≺ 2_{𝑜} \lor x ≺ (x \times x))\}$
2	1	eleq2i	$⊢ A \in {Fin}^{VI} \leftrightarrow A \in \{x \| (x ≺ 2_{𝑜} \lor x ≺ (x \times x))\}$
3		relsdom	$⊢ Rel ≺$
4	3	brrelex1i	$⊢ A ≺ 2_{𝑜} \to A \in V$
5	3	brrelex1i	$⊢ A ≺ (A \times A) \to A \in V$
6	4 5	jaoi	$⊢ (A ≺ 2_{𝑜} \lor A ≺ (A \times A)) \to A \in V$
7		breq1	$⊢ x = A \to (x ≺ 2_{𝑜} \leftrightarrow A ≺ 2_{𝑜})$
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 (x ≺ (x \times x) \leftrightarrow A ≺ (A \times A))$
11	7 10	orbi12d	$⊢ x = A \to ((x ≺ 2_{𝑜} \lor x ≺ (x \times x)) \leftrightarrow (A ≺ 2_{𝑜} \lor A ≺ (A \times A)))$
12	6 11	elab3	$⊢ A \in \{x \| (x ≺ 2_{𝑜} \lor x ≺ (x \times x))\} \leftrightarrow (A ≺ 2_{𝑜} \lor A ≺ (A \times A))$
13	2 12	bitri	$⊢ A \in {Fin}^{VI} \leftrightarrow (A ≺ 2_{𝑜} \lor A ≺ (A \times A))$

Metamath Proof Explorer