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		fndm	$⊢ R_{1} Fn On \to dom R_{1} = On$
7	5 6	ax-mp	$⊢ dom R_{1} = On$
8	4 7	eleqtrdi	$⊢ (A \in V \land R_{1} (A) \in WUni) \to A \in On$
9		eloni	$⊢ A \in On \to Ord A$
10	8 9	syl	$⊢ (A \in V \land R_{1} (A) \in WUni) \to Ord A$
11		n0i	$⊢ \emptyset \in R_{1} (A) \to \neg R_{1} (A) = \emptyset$
12	2 11	syl	$⊢ (A \in V \land R_{1} (A) \in WUni) \to \neg R_{1} (A) = \emptyset$
13		fveq2	$⊢ A = \emptyset \to R_{1} (A) = R_{1} (\emptyset)$
14		r10	$⊢ R_{1} (\emptyset) = \emptyset$
15	13 14	syl6eq	$⊢ A = \emptyset \to R_{1} (A) = \emptyset$
16	12 15	nsyl	$⊢ (A \in V \land R_{1} (A) \in WUni) \to \neg A = \emptyset$
17		suceloni	$⊢ A \in On \to suc A \in On$
18	8 17	syl	$⊢ (A \in V \land R_{1} (A) \in WUni) \to suc A \in On$
19		sucidg	$⊢ A \in On \to A \in suc A$
20	8 19	syl	$⊢ (A \in V \land R_{1} (A) \in WUni) \to A \in suc A$
21		r1ord	$⊢ suc A \in On \to (A \in suc A \to R_{1} (A) \in R_{1} (suc A))$
22	18 20 21	sylc	$⊢ (A \in V \land R_{1} (A) \in WUni) \to R_{1} (A) \in R_{1} (suc A)$
23		r1elwf	$⊢ R_{1} (A) \in R_{1} (suc A) \to R_{1} (A) \in ⋃ R_{1} [On]$
24		wfelirr	$⊢ R_{1} (A) \in ⋃ R_{1} [On] \to \neg R_{1} (A) \in R_{1} (A)$
25	22 23 24	3syl	$⊢ (A \in V \land R_{1} (A) \in WUni) \to \neg R_{1} (A) \in R_{1} (A)$
26		simprr	$⊢ ((A \in V \land R_{1} (A) \in WUni) \land (x \in On \land A = suc x)) \to A = suc x$
27	26	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)$
28		r1suc	$⊢ x \in On \to R_{1} (suc x) = 𝒫 R_{1} (x)$
29	28	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)$
30	27 29	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)$
31		simplr	$⊢ ((A \in V \land R_{1} (A) \in WUni) \land (x \in On \land A = suc x)) \to R_{1} (A) \in WUni$
32	8	adantr	$⊢ ((A \in V \land R_{1} (A) \in WUni) \land (x \in On \land A = suc x)) \to A \in On$
33		sucidg	$⊢ x \in On \to x \in suc x$
34	33	ad2antrl	$⊢ ((A \in V \land R_{1} (A) \in WUni) \land (x \in On \land A = suc x)) \to x \in suc x$
35	34 26	eleqtrrd	$⊢ ((A \in V \land R_{1} (A) \in WUni) \land (x \in On \land A = suc x)) \to x \in A$
36		r1ord	$⊢ A \in On \to (x \in A \to R_{1} (x) \in R_{1} (A))$
37	32 35 36	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)$
38	31 37	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)$
39	30 38	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)$
40	39	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))$
41	25 40	mtod	$⊢ (A \in V \land R_{1} (A) \in WUni) \to \neg \exists x \in On A = suc x$
42		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)$
43	16 41 42	sylanbrc	$⊢ (A \in V \land R_{1} (A) \in WUni) \to \neg (A = \emptyset \lor \exists x \in On A = suc x)$
44		dflim3	$⊢ Lim A \leftrightarrow (Ord A \land \neg (A = \emptyset \lor \exists x \in On A = suc x))$
45	10 43 44	sylanbrc	$⊢ (A \in V \land R_{1} (A) \in WUni) \to Lim A$
46		r1limwun	$⊢ (A \in V \land Lim A) \to R_{1} (A) \in WUni$
47	45 46	impbida	$⊢ A \in V \to (R_{1} (A) \in WUni \leftrightarrow Lim A)$

Metamath Proof Explorer

Theorem r1wunlim

Proof