wunr1om

Description: A weak universe is infinite, because it contains all the finite levels of the cumulative hierarchy. (Contributed by Mario Carneiro, 2-Jan-2017)

		Ref	Expression
	Hypothesis	wun0.1	$⊢ φ \to U \in WUni$
	Assertion	wunr1om	$⊢ φ \to R_{1} [ω] \subseteq U$

Proof

Step	Hyp	Ref	Expression
1		wun0.1	$⊢ φ \to U \in WUni$
2		fveq2	$⊢ x = \emptyset \to R_{1} (x) = R_{1} (\emptyset)$
3	2	eleq1d	$⊢ x = \emptyset \to (R_{1} (x) \in U \leftrightarrow R_{1} (\emptyset) \in U)$
4		fveq2	$⊢ x = y \to R_{1} (x) = R_{1} (y)$
5	4	eleq1d	$⊢ x = y \to (R_{1} (x) \in U \leftrightarrow R_{1} (y) \in U)$
6		fveq2	$⊢ x = suc y \to R_{1} (x) = R_{1} (suc y)$
7	6	eleq1d	$⊢ x = suc y \to (R_{1} (x) \in U \leftrightarrow R_{1} (suc y) \in U)$
8		r10	$⊢ R_{1} (\emptyset) = \emptyset$
9	1	wun0	$⊢ φ \to \emptyset \in U$
10	8 9	eqeltrid	$⊢ φ \to R_{1} (\emptyset) \in U$
11	1	adantr	$⊢ (φ \land R_{1} (y) \in U) \to U \in WUni$
12		simpr	$⊢ (φ \land R_{1} (y) \in U) \to R_{1} (y) \in U$
13	11 12	wunpw	$⊢ (φ \land R_{1} (y) \in U) \to 𝒫 R_{1} (y) \in U$
14		nnon	$⊢ y \in ω \to y \in On$
15		r1suc	$⊢ y \in On \to R_{1} (suc y) = 𝒫 R_{1} (y)$
16	14 15	syl	$⊢ y \in ω \to R_{1} (suc y) = 𝒫 R_{1} (y)$
17	16	eleq1d	$⊢ y \in ω \to (R_{1} (suc y) \in U \leftrightarrow 𝒫 R_{1} (y) \in U)$
18	13 17	imbitrrid	$⊢ y \in ω \to ((φ \land R_{1} (y) \in U) \to R_{1} (suc y) \in U)$
19	18	expd	$⊢ y \in ω \to (φ \to (R_{1} (y) \in U \to R_{1} (suc y) \in U))$
20	3 5 7 10 19	finds2	$⊢ x \in ω \to (φ \to R_{1} (x) \in U)$
21		eleq1	$⊢ R_{1} (x) = y \to (R_{1} (x) \in U \leftrightarrow y \in U)$
22	21	imbi2d	$⊢ R_{1} (x) = y \to ((φ \to R_{1} (x) \in U) \leftrightarrow (φ \to y \in U))$
23	20 22	syl5ibcom	$⊢ x \in ω \to (R_{1} (x) = y \to (φ \to y \in U))$
24	23	rexlimiv	$⊢ \exists x \in ω R_{1} (x) = y \to (φ \to y \in U)$
25		r1fnon	$⊢ R_{1} Fn On$
26		fnfun	$⊢ R_{1} Fn On \to Fun R_{1}$
27	25 26	ax-mp	$⊢ Fun R_{1}$
28		fvelima	$⊢ (Fun R_{1} \land y \in R_{1} [ω]) \to \exists x \in ω R_{1} (x) = y$
29	27 28	mpan	$⊢ y \in R_{1} [ω] \to \exists x \in ω R_{1} (x) = y$
30	24 29	syl11	$⊢ φ \to (y \in R_{1} [ω] \to y \in U)$
31	30	ssrdv	$⊢ φ \to R_{1} [ω] \subseteq U$

Metamath Proof Explorer

Theorem wunr1om

Proof