Metamath Proof Explorer

Theorem wunex3

Description: Construct a weak universe from a given set. This version of wunex has a simpler proof, but requires the axiom of regularity. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypothesis wunex3.u ⊢ 𝑈 = ( 𝑅1 ‘ ( ( rank ‘ 𝐴 ) +o ω ) )
Assertion wunex3 ( 𝐴 ∈ 𝑉 → ( 𝑈 ∈ WUni ∧ 𝐴 ⊆ 𝑈 ) )

Proof

Step Hyp Ref Expression
1 wunex3.u ⊢ 𝑈 = ( 𝑅1 ‘ ( ( rank ‘ 𝐴 ) +o ω ) )
2 r1rankid ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
3 rankon ⊢ ( rank ‘ 𝐴 ) ∈ On
4 omelon ⊢ ω ∈ On
5 oacl ⊢ ( ( ( rank ‘ 𝐴 ) ∈ On ∧ ω ∈ On ) → ( ( rank ‘ 𝐴 ) +o ω ) ∈ On )
6 3 4 5 mp2an ⊢ ( ( rank ‘ 𝐴 ) +o ω ) ∈ On
7 peano1 ⊢ ∅ ∈ ω
8 oaord1 ⊢ ( ( ( rank ‘ 𝐴 ) ∈ On ∧ ω ∈ On ) → ( ∅ ∈ ω ↔ ( rank ‘ 𝐴 ) ∈ ( ( rank ‘ 𝐴 ) +o ω ) ) )
9 3 4 8 mp2an ⊢ ( ∅ ∈ ω ↔ ( rank ‘ 𝐴 ) ∈ ( ( rank ‘ 𝐴 ) +o ω ) )
10 7 9 mpbi ⊢ ( rank ‘ 𝐴 ) ∈ ( ( rank ‘ 𝐴 ) +o ω )
11 r1ord2 ⊢ ( ( ( rank ‘ 𝐴 ) +o ω ) ∈ On → ( ( rank ‘ 𝐴 ) ∈ ( ( rank ‘ 𝐴 ) +o ω ) → ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ⊆ ( 𝑅1 ‘ ( ( rank ‘ 𝐴 ) +o ω ) ) ) )
12 6 10 11 mp2 ⊢ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ⊆ ( 𝑅1 ‘ ( ( rank ‘ 𝐴 ) +o ω ) )
13 12 1 sseqtrri ⊢ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ⊆ 𝑈
14 2 13 sstrdi ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ⊆ 𝑈 )
15 limom ⊢ Lim ω
16 4 15 pm3.2i ⊢ ( ω ∈ On ∧ Lim ω )
17 oalimcl ⊢ ( ( ( rank ‘ 𝐴 ) ∈ On ∧ ( ω ∈ On ∧ Lim ω ) ) → Lim ( ( rank ‘ 𝐴 ) +o ω ) )
18 3 16 17 mp2an ⊢ Lim ( ( rank ‘ 𝐴 ) +o ω )
19 r1limwun ⊢ ( ( ( ( rank ‘ 𝐴 ) +o ω ) ∈ On ∧ Lim ( ( rank ‘ 𝐴 ) +o ω ) ) → ( 𝑅1 ‘ ( ( rank ‘ 𝐴 ) +o ω ) ) ∈ WUni )
20 6 18 19 mp2an ⊢ ( 𝑅1 ‘ ( ( rank ‘ 𝐴 ) +o ω ) ) ∈ WUni
21 1 20 eqeltri ⊢ 𝑈 ∈ WUni
22 14 21 jctil ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑈 ∈ WUni ∧ 𝐴 ⊆ 𝑈 ) )