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		r1funlim	⊢ ( Fun 𝑅1 ∧ Lim dom 𝑅1 )
5	4	simpli	⊢ Fun 𝑅1
6	4	simpri	⊢ Lim dom 𝑅1
7		limomss	⊢ ( Lim dom 𝑅1 → ω ⊆ dom 𝑅1 )
8	6 7	ax-mp	⊢ ω ⊆ dom 𝑅1
9		funimass4	⊢ ( ( Fun 𝑅1 ∧ ω ⊆ dom 𝑅1 ) → ( ( 𝑅1 “ ω ) ⊆ 𝑈 ↔ ∀ 𝑥 ∈ ω ( 𝑅1 ‘ 𝑥 ) ∈ 𝑈 ) )
10	5 8 9	mp2an	⊢ ( ( 𝑅1 “ ω ) ⊆ 𝑈 ↔ ∀ 𝑥 ∈ ω ( 𝑅1 ‘ 𝑥 ) ∈ 𝑈 )
11	3 10	sylib	⊢ ( 𝜑 → ∀ 𝑥 ∈ ω ( 𝑅1 ‘ 𝑥 ) ∈ 𝑈 )
12	11	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ω ) → ( 𝑅1 ‘ 𝑥 ) ∈ 𝑈 )
13		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ω ) → 𝑥 ∈ ω )
14	8 13	sseldi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ω ) → 𝑥 ∈ dom 𝑅1 )
15		onssr1	⊢ ( 𝑥 ∈ dom 𝑅1 → 𝑥 ⊆ ( 𝑅1 ‘ 𝑥 ) )
16	14 15	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ω ) → 𝑥 ⊆ ( 𝑅1 ‘ 𝑥 ) )
17	2 12 16	wunss	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ω ) → 𝑥 ∈ 𝑈 )
18	17	ex	⊢ ( 𝜑 → ( 𝑥 ∈ ω → 𝑥 ∈ 𝑈 ) )
19	18	ssrdv	⊢ ( 𝜑 → ω ⊆ 𝑈 )