This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 sselid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ω ) → 𝑥 ∈ dom 𝑅1 )
15 onssr1 ⊢ ( 𝑥 ∈ dom 𝑅1 → 𝑥 ⊆ ( 𝑅1 ‘ 𝑥 ) )
16 14 15 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ω ) → 𝑥 ⊆ ( 𝑅1 ‘ 𝑥 ) )
17 2 12 16 wunss ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ω ) → 𝑥 ∈ 𝑈 )
18 17 ex ⊢ ( 𝜑 → ( 𝑥 ∈ ω → 𝑥 ∈ 𝑈 ) )
19 18 ssrdv ⊢ ( 𝜑 → ω ⊆ 𝑈 )