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

Metamath Proof Explorer

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 “ ω ) ⊆ 𝑈 )