r1wunlim

Description: The weak universes in the cumulative hierarchy are exactly the limit ordinals. (Contributed by Mario Carneiro, 2-Jan-2017)

		Ref	Expression
	Assertion	r1wunlim	$⊢ A \in V \to (R_{1} (A) \in WUni \leftrightarrow Lim A)$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (A \in V \land R_{1} (A) \in WUni) \to R_{1} (A) \in WUni$
2	1	wun0	$⊢ (A \in V \land R_{1} (A) \in WUni) \to \emptyset \in R_{1} (A)$
3		elfvdm	$⊢ \emptyset \in R_{1} (A) \to A \in dom R_{1}$
4	2 3	syl	$⊢ (A \in V \land R_{1} (A) \in WUni) \to A \in dom R_{1}$
5		r1fnon	$⊢ R_{1} Fn On$
6	5	fndmi	$⊢ dom R_{1} = On$
7	4 6	eleqtrdi	$⊢ (A \in V \land R_{1} (A) \in WUni) \to A \in On$
8		eloni	$⊢ A \in On \to Ord A$
9	7 8	syl	$⊢ (A \in V \land R_{1} (A) \in WUni) \to Ord A$
10		n0i	$⊢ \emptyset \in R_{1} (A) \to \neg R_{1} (A) = \emptyset$
11	2 10	syl	$⊢ (A \in V \land R_{1} (A) \in WUni) \to \neg R_{1} (A) = \emptyset$
12		fveq2	$⊢ A = \emptyset \to R_{1} (A) = R_{1} (\emptyset)$
13		r10	$⊢ R_{1} (\emptyset) = \emptyset$
14	12 13	eqtrdi	$⊢ A = \emptyset \to R_{1} (A) = \emptyset$
15	11 14	nsyl	$⊢ (A \in V \land R_{1} (A) \in WUni) \to \neg A = \emptyset$
16		suceloni	$⊢ A \in On \to suc A \in On$
17	7 16	syl	$⊢ (A \in V \land R_{1} (A) \in WUni) \to suc A \in On$
18		sucidg	$⊢ A \in On \to A \in suc A$
19	7 18	syl	$⊢ (A \in V \land R_{1} (A) \in WUni) \to A \in suc A$
20		r1ord	$⊢ suc A \in On \to (A \in suc A \to R_{1} (A) \in R_{1} (suc A))$
21	17 19 20	sylc	$⊢ (A \in V \land R_{1} (A) \in WUni) \to R_{1} (A) \in R_{1} (suc A)$
22		r1elwf	$⊢ R_{1} (A) \in R_{1} (suc A) \to R_{1} (A) \in ⋃ R_{1} [On]$
23		wfelirr	$⊢ R_{1} (A) \in ⋃ R_{1} [On] \to \neg R_{1} (A) \in R_{1} (A)$
24	21 22 23	3syl	$⊢ (A \in V \land R_{1} (A) \in WUni) \to \neg R_{1} (A) \in R_{1} (A)$
25		simprr	$⊢ ((A \in V \land R_{1} (A) \in WUni) \land (x \in On \land A = suc x)) \to A = suc x$
26	25	fveq2d	$⊢ ((A \in V \land R_{1} (A) \in WUni) \land (x \in On \land A = suc x)) \to R_{1} (A) = R_{1} (suc x)$
27		r1suc	$⊢ x \in On \to R_{1} (suc x) = 𝒫 R_{1} (x)$
28	27	ad2antrl	$⊢ ((A \in V \land R_{1} (A) \in WUni) \land (x \in On \land A = suc x)) \to R_{1} (suc x) = 𝒫 R_{1} (x)$
29	26 28	eqtrd	$⊢ ((A \in V \land R_{1} (A) \in WUni) \land (x \in On \land A = suc x)) \to R_{1} (A) = 𝒫 R_{1} (x)$
30		simplr	$⊢ ((A \in V \land R_{1} (A) \in WUni) \land (x \in On \land A = suc x)) \to R_{1} (A) \in WUni$
31	7	adantr	$⊢ ((A \in V \land R_{1} (A) \in WUni) \land (x \in On \land A = suc x)) \to A \in On$
32		sucidg	$⊢ x \in On \to x \in suc x$
33	32	ad2antrl	$⊢ ((A \in V \land R_{1} (A) \in WUni) \land (x \in On \land A = suc x)) \to x \in suc x$
34	33 25	eleqtrrd	$⊢ ((A \in V \land R_{1} (A) \in WUni) \land (x \in On \land A = suc x)) \to x \in A$
35		r1ord	$⊢ A \in On \to (x \in A \to R_{1} (x) \in R_{1} (A))$
36	31 34 35	sylc	$⊢ ((A \in V \land R_{1} (A) \in WUni) \land (x \in On \land A = suc x)) \to R_{1} (x) \in R_{1} (A)$
37	30 36	wunpw	$⊢ ((A \in V \land R_{1} (A) \in WUni) \land (x \in On \land A = suc x)) \to 𝒫 R_{1} (x) \in R_{1} (A)$
38	29 37	eqeltrd	$⊢ ((A \in V \land R_{1} (A) \in WUni) \land (x \in On \land A = suc x)) \to R_{1} (A) \in R_{1} (A)$
39	38	rexlimdvaa	$⊢ (A \in V \land R_{1} (A) \in WUni) \to (\exists x \in On A = suc x \to R_{1} (A) \in R_{1} (A))$
40	24 39	mtod	$⊢ (A \in V \land R_{1} (A) \in WUni) \to \neg \exists x \in On A = suc x$
41		ioran	$⊢ \neg (A = \emptyset \lor \exists x \in On A = suc x) \leftrightarrow (\neg A = \emptyset \land \neg \exists x \in On A = suc x)$
42	15 40 41	sylanbrc	$⊢ (A \in V \land R_{1} (A) \in WUni) \to \neg (A = \emptyset \lor \exists x \in On A = suc x)$
43		dflim3	$⊢ Lim A \leftrightarrow (Ord A \land \neg (A = \emptyset \lor \exists x \in On A = suc x))$
44	9 42 43	sylanbrc	$⊢ (A \in V \land R_{1} (A) \in WUni) \to Lim A$
45		r1limwun	$⊢ (A \in V \land Lim A) \to R_{1} (A) \in WUni$
46	44 45	impbida	$⊢ A \in V \to (R_{1} (A) \in WUni \leftrightarrow Lim A)$

Metamath Proof Explorer

Theorem r1wunlim

Proof