Theorem wunom

Description: A weak universe contains all the finite ordinals, and hence is infinite. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypothesis	wun0.1	⊢ ( 𝜑 → 𝑈 ∈ WUni )
Assertion	wunom	⊢ ( 𝜑 → ω ⊆ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		wun0.1	⊢ ( 𝜑 → 𝑈 ∈ WUni )
2	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ω ) → 𝑈 ∈ WUni )
3	1	wunr1om	⊢ ( 𝜑 → ( 𝑅1 “ ω ) ⊆ 𝑈 )
4		r1fun	⊢ Fun 𝑅1
5		r1dmlim	⊢ Lim dom 𝑅1
6		limomss	⊢ ( Lim dom 𝑅1 → ω ⊆ dom 𝑅1 )
7	5 6	ax-mp	⊢ ω ⊆ dom 𝑅1
8		funimass4	⊢ ( ( Fun 𝑅1 ∧ ω ⊆ dom 𝑅1 ) → ( ( 𝑅1 “ ω ) ⊆ 𝑈 ↔ ∀ 𝑥 ∈ ω ( 𝑅1 ‘ 𝑥 ) ∈ 𝑈 ) )
9	4 7 8	mp2an	⊢ ( ( 𝑅1 “ ω ) ⊆ 𝑈 ↔ ∀ 𝑥 ∈ ω ( 𝑅1 ‘ 𝑥 ) ∈ 𝑈 )
10	3 9	sylib	⊢ ( 𝜑 → ∀ 𝑥 ∈ ω ( 𝑅1 ‘ 𝑥 ) ∈ 𝑈 )
11	10	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ω ) → ( 𝑅1 ‘ 𝑥 ) ∈ 𝑈 )
12		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ω ) → 𝑥 ∈ ω )
13	7 12	sselid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ω ) → 𝑥 ∈ dom 𝑅1 )
14		onssr1	⊢ ( 𝑥 ∈ dom 𝑅1 → 𝑥 ⊆ ( 𝑅1 ‘ 𝑥 ) )
15	13 14	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ω ) → 𝑥 ⊆ ( 𝑅1 ‘ 𝑥 ) )
16	2 11 15	wunss	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ω ) → 𝑥 ∈ 𝑈 )
17	16	ex	⊢ ( 𝜑 → ( 𝑥 ∈ ω → 𝑥 ∈ 𝑈 ) )
18	17	ssrdv	⊢ ( 𝜑 → ω ⊆ 𝑈 )