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 ${⊢}{U}={R}_{1}\left(\mathrm{rank}\left({A}\right){+}_{𝑜}\mathrm{\omega }\right)$
Assertion wunex3 ${⊢}{A}\in {V}\to \left({U}\in \mathrm{WUni}\wedge {A}\subseteq {U}\right)$

Proof

Step Hyp Ref Expression
1 wunex3.u ${⊢}{U}={R}_{1}\left(\mathrm{rank}\left({A}\right){+}_{𝑜}\mathrm{\omega }\right)$
2 r1rankid ${⊢}{A}\in {V}\to {A}\subseteq {R}_{1}\left(\mathrm{rank}\left({A}\right)\right)$
3 rankon ${⊢}\mathrm{rank}\left({A}\right)\in \mathrm{On}$
4 omelon ${⊢}\mathrm{\omega }\in \mathrm{On}$
5 oacl ${⊢}\left(\mathrm{rank}\left({A}\right)\in \mathrm{On}\wedge \mathrm{\omega }\in \mathrm{On}\right)\to \mathrm{rank}\left({A}\right){+}_{𝑜}\mathrm{\omega }\in \mathrm{On}$
6 3 4 5 mp2an ${⊢}\mathrm{rank}\left({A}\right){+}_{𝑜}\mathrm{\omega }\in \mathrm{On}$
7 peano1 ${⊢}\varnothing \in \mathrm{\omega }$
8 oaord1 ${⊢}\left(\mathrm{rank}\left({A}\right)\in \mathrm{On}\wedge \mathrm{\omega }\in \mathrm{On}\right)\to \left(\varnothing \in \mathrm{\omega }↔\mathrm{rank}\left({A}\right)\in \left(\mathrm{rank}\left({A}\right){+}_{𝑜}\mathrm{\omega }\right)\right)$
9 3 4 8 mp2an ${⊢}\varnothing \in \mathrm{\omega }↔\mathrm{rank}\left({A}\right)\in \left(\mathrm{rank}\left({A}\right){+}_{𝑜}\mathrm{\omega }\right)$
10 7 9 mpbi ${⊢}\mathrm{rank}\left({A}\right)\in \left(\mathrm{rank}\left({A}\right){+}_{𝑜}\mathrm{\omega }\right)$
11 r1ord2 ${⊢}\mathrm{rank}\left({A}\right){+}_{𝑜}\mathrm{\omega }\in \mathrm{On}\to \left(\mathrm{rank}\left({A}\right)\in \left(\mathrm{rank}\left({A}\right){+}_{𝑜}\mathrm{\omega }\right)\to {R}_{1}\left(\mathrm{rank}\left({A}\right)\right)\subseteq {R}_{1}\left(\mathrm{rank}\left({A}\right){+}_{𝑜}\mathrm{\omega }\right)\right)$
12 6 10 11 mp2 ${⊢}{R}_{1}\left(\mathrm{rank}\left({A}\right)\right)\subseteq {R}_{1}\left(\mathrm{rank}\left({A}\right){+}_{𝑜}\mathrm{\omega }\right)$
13 12 1 sseqtrri ${⊢}{R}_{1}\left(\mathrm{rank}\left({A}\right)\right)\subseteq {U}$
14 2 13 sstrdi ${⊢}{A}\in {V}\to {A}\subseteq {U}$
15 limom ${⊢}\mathrm{Lim}\mathrm{\omega }$
16 4 15 pm3.2i ${⊢}\left(\mathrm{\omega }\in \mathrm{On}\wedge \mathrm{Lim}\mathrm{\omega }\right)$
17 oalimcl ${⊢}\left(\mathrm{rank}\left({A}\right)\in \mathrm{On}\wedge \left(\mathrm{\omega }\in \mathrm{On}\wedge \mathrm{Lim}\mathrm{\omega }\right)\right)\to \mathrm{Lim}\left(\mathrm{rank}\left({A}\right){+}_{𝑜}\mathrm{\omega }\right)$
18 3 16 17 mp2an ${⊢}\mathrm{Lim}\left(\mathrm{rank}\left({A}\right){+}_{𝑜}\mathrm{\omega }\right)$
19 r1limwun ${⊢}\left(\mathrm{rank}\left({A}\right){+}_{𝑜}\mathrm{\omega }\in \mathrm{On}\wedge \mathrm{Lim}\left(\mathrm{rank}\left({A}\right){+}_{𝑜}\mathrm{\omega }\right)\right)\to {R}_{1}\left(\mathrm{rank}\left({A}\right){+}_{𝑜}\mathrm{\omega }\right)\in \mathrm{WUni}$
20 6 18 19 mp2an ${⊢}{R}_{1}\left(\mathrm{rank}\left({A}\right){+}_{𝑜}\mathrm{\omega }\right)\in \mathrm{WUni}$
21 1 20 eqeltri ${⊢}{U}\in \mathrm{WUni}$
22 14 21 jctil ${⊢}{A}\in {V}\to \left({U}\in \mathrm{WUni}\wedge {A}\subseteq {U}\right)$