r1fin

Description: The first _om levels of the cumulative hierarchy 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		0fin	$⊢ \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		r1funlim	$⊢ (Fun R_{1} \land Lim dom R_{1})$
14	13	simpri	$⊢ Lim dom R_{1}$
15		limomss	$⊢ Lim dom R_{1} \to ω \subseteq dom R_{1}$
16	14 15	ax-mp	$⊢ ω \subseteq dom R_{1}$
17	16	sseli	$⊢ m \in ω \to m \in dom R_{1}$
18		r1sucg	$⊢ m \in dom R_{1} \to R_{1} (suc m) = 𝒫 R_{1} (m)$
19	17 18	syl	$⊢ m \in ω \to R_{1} (suc m) = 𝒫 R_{1} (m)$
20	19	eleq1d	$⊢ m \in ω \to (R_{1} (suc m) \in Fin \leftrightarrow 𝒫 R_{1} (m) \in Fin)$
21	12 20	bitr4id	$⊢ m \in ω \to (R_{1} (m) \in Fin \leftrightarrow R_{1} (suc m) \in Fin)$
22	21	biimpd	$⊢ m \in ω \to (R_{1} (m) \in Fin \to R_{1} (suc m) \in Fin)$
23	2 4 6 8 11 22	finds	$⊢ A \in ω \to R_{1} (A) \in Fin$

Metamath Proof Explorer