r1fin

Description: The first _om stages of the cumulative hierarchy of sets are all finite. (Contributed by Mario Carneiro, 15-May-2013)

		Ref	Expression
	Assertion	r1fin	$⊢ A \in ω \to R_{1} (A) \in Fin$

Step	Hyp	Ref	Expression
1		fveq2	$⊢ n = \emptyset \to R_{1} (n) = R_{1} (\emptyset)$
2	1	eleq1d	$⊢ n = \emptyset \to (R_{1} (n) \in Fin \leftrightarrow R_{1} (\emptyset) \in Fin)$
3		fveq2	$⊢ n = m \to R_{1} (n) = R_{1} (m)$
4	3	eleq1d	$⊢ n = m \to (R_{1} (n) \in Fin \leftrightarrow R_{1} (m) \in Fin)$
5		fveq2	$⊢ n = suc m \to R_{1} (n) = R_{1} (suc m)$
6	5	eleq1d	$⊢ n = suc m \to (R_{1} (n) \in Fin \leftrightarrow R_{1} (suc m) \in Fin)$
7		fveq2	$⊢ n = A \to R_{1} (n) = R_{1} (A)$
8	7	eleq1d	$⊢ n = A \to (R_{1} (n) \in Fin \leftrightarrow R_{1} (A) \in Fin)$
9		r10	$⊢ R_{1} (\emptyset) = \emptyset$
10		0fi	$⊢ \emptyset \in Fin$
11	9 10	eqeltri	$⊢ R_{1} (\emptyset) \in Fin$
12		pwfi	$⊢ R_{1} (m) \in Fin \leftrightarrow 𝒫 R_{1} (m) \in Fin$
13		r1dmlim	$⊢ Lim dom R_{1}$
14		limomss	$⊢ Lim dom R_{1} \to ω \subseteq dom R_{1}$
15	13 14	ax-mp	$⊢ ω \subseteq dom R_{1}$
16	15	sseli	$⊢ m \in ω \to m \in dom R_{1}$
17		r1sucg	$⊢ m \in dom R_{1} \to R_{1} (suc m) = 𝒫 R_{1} (m)$
18	16 17	syl	$⊢ m \in ω \to R_{1} (suc m) = 𝒫 R_{1} (m)$
19	18	eleq1d	$⊢ m \in ω \to (R_{1} (suc m) \in Fin \leftrightarrow 𝒫 R_{1} (m) \in Fin)$
20	12 19	bitr4id	$⊢ m \in ω \to (R_{1} (m) \in Fin \leftrightarrow R_{1} (suc m) \in Fin)$
21	20	biimpd	$⊢ m \in ω \to (R_{1} (m) \in Fin \to R_{1} (suc m) \in Fin)$
22	2 4 6 8 11 21	finds	$⊢ A \in ω \to R_{1} (A) \in Fin$

Metamath Proof Explorer