Theorem 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	⊢ ( 𝜑 → 𝑈 ∈ WUni )
Assertion	wunr1om	⊢ ( 𝜑 → ( 𝑅1 “ ω ) ⊆ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		wun0.1	⊢ ( 𝜑 → 𝑈 ∈ WUni )
2		fveq2	⊢ ( 𝑥 = ∅ → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ ∅ ) )
3	2	eleq1d	⊢ ( 𝑥 = ∅ → ( ( 𝑅1 ‘ 𝑥 ) ∈ 𝑈 ↔ ( 𝑅1 ‘ ∅ ) ∈ 𝑈 ) )
4		fveq2	⊢ ( 𝑥 = 𝑦 → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) )
5	4	eleq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑅1 ‘ 𝑥 ) ∈ 𝑈 ↔ ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) )
6		fveq2	⊢ ( 𝑥 = suc 𝑦 → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ suc 𝑦 ) )
7	6	eleq1d	⊢ ( 𝑥 = suc 𝑦 → ( ( 𝑅1 ‘ 𝑥 ) ∈ 𝑈 ↔ ( 𝑅1 ‘ suc 𝑦 ) ∈ 𝑈 ) )
8		r10	⊢ ( 𝑅1 ‘ ∅ ) = ∅
9	1	wun0	⊢ ( 𝜑 → ∅ ∈ 𝑈 )
10	8 9	eqeltrid	⊢ ( 𝜑 → ( 𝑅1 ‘ ∅ ) ∈ 𝑈 )
11	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) → 𝑈 ∈ WUni )
12		simpr	⊢ ( ( 𝜑 ∧ ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) → ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 )
13	11 12	wunpw	⊢ ( ( 𝜑 ∧ ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) → 𝒫 ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 )
14		nnon	⊢ ( 𝑦 ∈ ω → 𝑦 ∈ On )
15		r1suc	⊢ ( 𝑦 ∈ On → ( 𝑅1 ‘ suc 𝑦 ) = 𝒫 ( 𝑅1 ‘ 𝑦 ) )
16	14 15	syl	⊢ ( 𝑦 ∈ ω → ( 𝑅1 ‘ suc 𝑦 ) = 𝒫 ( 𝑅1 ‘ 𝑦 ) )
17	16	eleq1d	⊢ ( 𝑦 ∈ ω → ( ( 𝑅1 ‘ suc 𝑦 ) ∈ 𝑈 ↔ 𝒫 ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) )
18	13 17	imbitrrid	⊢ ( 𝑦 ∈ ω → ( ( 𝜑 ∧ ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 ) → ( 𝑅1 ‘ suc 𝑦 ) ∈ 𝑈 ) )
19	18	expd	⊢ ( 𝑦 ∈ ω → ( 𝜑 → ( ( 𝑅1 ‘ 𝑦 ) ∈ 𝑈 → ( 𝑅1 ‘ suc 𝑦 ) ∈ 𝑈 ) ) )
20	3 5 7 10 19	finds2	⊢ ( 𝑥 ∈ ω → ( 𝜑 → ( 𝑅1 ‘ 𝑥 ) ∈ 𝑈 ) )
21		eleq1	⊢ ( ( 𝑅1 ‘ 𝑥 ) = 𝑦 → ( ( 𝑅1 ‘ 𝑥 ) ∈ 𝑈 ↔ 𝑦 ∈ 𝑈 ) )
22	21	imbi2d	⊢ ( ( 𝑅1 ‘ 𝑥 ) = 𝑦 → ( ( 𝜑 → ( 𝑅1 ‘ 𝑥 ) ∈ 𝑈 ) ↔ ( 𝜑 → 𝑦 ∈ 𝑈 ) ) )
23	20 22	syl5ibcom	⊢ ( 𝑥 ∈ ω → ( ( 𝑅1 ‘ 𝑥 ) = 𝑦 → ( 𝜑 → 𝑦 ∈ 𝑈 ) ) )
24	23	rexlimiv	⊢ ( ∃ 𝑥 ∈ ω ( 𝑅1 ‘ 𝑥 ) = 𝑦 → ( 𝜑 → 𝑦 ∈ 𝑈 ) )
25		r1fnon	⊢ 𝑅1 Fn On
26		fnfun	⊢ ( 𝑅1 Fn On → Fun 𝑅1 )
27	25 26	ax-mp	⊢ Fun 𝑅1
28		fvelima	⊢ ( ( Fun 𝑅1 ∧ 𝑦 ∈ ( 𝑅1 “ ω ) ) → ∃ 𝑥 ∈ ω ( 𝑅1 ‘ 𝑥 ) = 𝑦 )
29	27 28	mpan	⊢ ( 𝑦 ∈ ( 𝑅1 “ ω ) → ∃ 𝑥 ∈ ω ( 𝑅1 ‘ 𝑥 ) = 𝑦 )
30	24 29	syl11	⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑅1 “ ω ) → 𝑦 ∈ 𝑈 ) )
31	30	ssrdv	⊢ ( 𝜑 → ( 𝑅1 “ ω ) ⊆ 𝑈 )