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} (rank (A) +_{𝑜} ω)$
	Assertion	wunex3	$⊢ A \in V \to (U \in WUni \land A \subseteq U)$

Proof

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

Metamath Proof Explorer

Theorem wunex3

Proof