r1limwun

Description: Each limit stage in the cumulative hierarchy is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017)

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

Proof

Step	Hyp	Ref	Expression
1		r1tr	$⊢ Tr R_{1} (A)$
2	1	a1i	$⊢ (A \in V \land Lim A) \to Tr R_{1} (A)$
3		limelon	$⊢ (A \in V \land Lim A) \to A \in On$
4		r1fnon	$⊢ R_{1} Fn On$
5	4	fndmi	$⊢ dom R_{1} = On$
6	3 5	eleqtrrdi	$⊢ (A \in V \land Lim A) \to A \in dom R_{1}$
7		onssr1	$⊢ A \in dom R_{1} \to A \subseteq R_{1} (A)$
8	6 7	syl	$⊢ (A \in V \land Lim A) \to A \subseteq R_{1} (A)$
9		0ellim	$⊢ Lim A \to \emptyset \in A$
10	9	adantl	$⊢ (A \in V \land Lim A) \to \emptyset \in A$
11	8 10	sseldd	$⊢ (A \in V \land Lim A) \to \emptyset \in R_{1} (A)$
12	11	ne0d	$⊢ (A \in V \land Lim A) \to R_{1} (A) \neq \emptyset$
13		rankuni	$⊢ rank (⋃ x) = ⋃ rank (x)$
14		rankon	$⊢ rank (x) \in On$
15		eloni	$⊢ rank (x) \in On \to Ord rank (x)$
16		orduniss	$⊢ Ord rank (x) \to ⋃ rank (x) \subseteq rank (x)$
17	14 15 16	mp2b	$⊢ ⋃ rank (x) \subseteq rank (x)$
18	17	a1i	$⊢ ((A \in V \land Lim A) \land x \in R_{1} (A)) \to ⋃ rank (x) \subseteq rank (x)$
19		rankr1ai	$⊢ x \in R_{1} (A) \to rank (x) \in A$
20	19	adantl	$⊢ ((A \in V \land Lim A) \land x \in R_{1} (A)) \to rank (x) \in A$
21		onuni	$⊢ rank (x) \in On \to ⋃ rank (x) \in On$
22	14 21	ax-mp	$⊢ ⋃ rank (x) \in On$
23	3	adantr	$⊢ ((A \in V \land Lim A) \land x \in R_{1} (A)) \to A \in On$
24		ontr2	$⊢ (⋃ rank (x) \in On \land A \in On) \to ((⋃ rank (x) \subseteq rank (x) \land rank (x) \in A) \to ⋃ rank (x) \in A)$
25	22 23 24	sylancr	$⊢ ((A \in V \land Lim A) \land x \in R_{1} (A)) \to ((⋃ rank (x) \subseteq rank (x) \land rank (x) \in A) \to ⋃ rank (x) \in A)$
26	18 20 25	mp2and	$⊢ ((A \in V \land Lim A) \land x \in R_{1} (A)) \to ⋃ rank (x) \in A$
27	13 26	eqeltrid	$⊢ ((A \in V \land Lim A) \land x \in R_{1} (A)) \to rank (⋃ x) \in A$
28		r1elwf	$⊢ x \in R_{1} (A) \to x \in ⋃ R_{1} [On]$
29	28	adantl	$⊢ ((A \in V \land Lim A) \land x \in R_{1} (A)) \to x \in ⋃ R_{1} [On]$
30		uniwf	$⊢ x \in ⋃ R_{1} [On] \leftrightarrow ⋃ x \in ⋃ R_{1} [On]$
31	29 30	sylib	$⊢ ((A \in V \land Lim A) \land x \in R_{1} (A)) \to ⋃ x \in ⋃ R_{1} [On]$
32	6	adantr	$⊢ ((A \in V \land Lim A) \land x \in R_{1} (A)) \to A \in dom R_{1}$
33		rankr1ag	$⊢ (⋃ x \in ⋃ R_{1} [On] \land A \in dom R_{1}) \to (⋃ x \in R_{1} (A) \leftrightarrow rank (⋃ x) \in A)$
34	31 32 33	syl2anc	$⊢ ((A \in V \land Lim A) \land x \in R_{1} (A)) \to (⋃ x \in R_{1} (A) \leftrightarrow rank (⋃ x) \in A)$
35	27 34	mpbird	$⊢ ((A \in V \land Lim A) \land x \in R_{1} (A)) \to ⋃ x \in R_{1} (A)$
36		r1pwcl	$⊢ Lim A \to (x \in R_{1} (A) \leftrightarrow 𝒫 x \in R_{1} (A))$
37	36	adantl	$⊢ (A \in V \land Lim A) \to (x \in R_{1} (A) \leftrightarrow 𝒫 x \in R_{1} (A))$
38	37	biimpa	$⊢ ((A \in V \land Lim A) \land x \in R_{1} (A)) \to 𝒫 x \in R_{1} (A)$
39	28	ad2antlr	$⊢ (((A \in V \land Lim A) \land x \in R_{1} (A)) \land y \in R_{1} (A)) \to x \in ⋃ R_{1} [On]$
40		r1elwf	$⊢ y \in R_{1} (A) \to y \in ⋃ R_{1} [On]$
41	40	adantl	$⊢ (((A \in V \land Lim A) \land x \in R_{1} (A)) \land y \in R_{1} (A)) \to y \in ⋃ R_{1} [On]$
42		rankprb	$⊢ (x \in ⋃ R_{1} [On] \land y \in ⋃ R_{1} [On]) \to rank (\{x, y\}) = suc (rank (x) \cup rank (y))$
43	39 41 42	syl2anc	$⊢ (((A \in V \land Lim A) \land x \in R_{1} (A)) \land y \in R_{1} (A)) \to rank (\{x, y\}) = suc (rank (x) \cup rank (y))$
44		limord	$⊢ Lim A \to Ord A$
45	44	ad3antlr	$⊢ (((A \in V \land Lim A) \land x \in R_{1} (A)) \land y \in R_{1} (A)) \to Ord A$
46	20	adantr	$⊢ (((A \in V \land Lim A) \land x \in R_{1} (A)) \land y \in R_{1} (A)) \to rank (x) \in A$
47		rankr1ai	$⊢ y \in R_{1} (A) \to rank (y) \in A$
48	47	adantl	$⊢ (((A \in V \land Lim A) \land x \in R_{1} (A)) \land y \in R_{1} (A)) \to rank (y) \in A$
49		ordunel	$⊢ (Ord A \land rank (x) \in A \land rank (y) \in A) \to rank (x) \cup rank (y) \in A$
50	45 46 48 49	syl3anc	$⊢ (((A \in V \land Lim A) \land x \in R_{1} (A)) \land y \in R_{1} (A)) \to rank (x) \cup rank (y) \in A$
51		limsuc	$⊢ Lim A \to (rank (x) \cup rank (y) \in A \leftrightarrow suc (rank (x) \cup rank (y)) \in A)$
52	51	ad3antlr	$⊢ (((A \in V \land Lim A) \land x \in R_{1} (A)) \land y \in R_{1} (A)) \to (rank (x) \cup rank (y) \in A \leftrightarrow suc (rank (x) \cup rank (y)) \in A)$
53	50 52	mpbid	$⊢ (((A \in V \land Lim A) \land x \in R_{1} (A)) \land y \in R_{1} (A)) \to suc (rank (x) \cup rank (y)) \in A$
54	43 53	eqeltrd	$⊢ (((A \in V \land Lim A) \land x \in R_{1} (A)) \land y \in R_{1} (A)) \to rank (\{x, y\}) \in A$
55		prwf	$⊢ (x \in ⋃ R_{1} [On] \land y \in ⋃ R_{1} [On]) \to \{x, y\} \in ⋃ R_{1} [On]$
56	39 41 55	syl2anc	$⊢ (((A \in V \land Lim A) \land x \in R_{1} (A)) \land y \in R_{1} (A)) \to \{x, y\} \in ⋃ R_{1} [On]$
57	32	adantr	$⊢ (((A \in V \land Lim A) \land x \in R_{1} (A)) \land y \in R_{1} (A)) \to A \in dom R_{1}$
58		rankr1ag	$⊢ (\{x, y\} \in ⋃ R_{1} [On] \land A \in dom R_{1}) \to (\{x, y\} \in R_{1} (A) \leftrightarrow rank (\{x, y\}) \in A)$
59	56 57 58	syl2anc	$⊢ (((A \in V \land Lim A) \land x \in R_{1} (A)) \land y \in R_{1} (A)) \to (\{x, y\} \in R_{1} (A) \leftrightarrow rank (\{x, y\}) \in A)$
60	54 59	mpbird	$⊢ (((A \in V \land Lim A) \land x \in R_{1} (A)) \land y \in R_{1} (A)) \to \{x, y\} \in R_{1} (A)$
61	60	ralrimiva	$⊢ ((A \in V \land Lim A) \land x \in R_{1} (A)) \to \forall y \in R_{1} (A) \{x, y\} \in R_{1} (A)$
62	35 38 61	3jca	$⊢ ((A \in V \land Lim A) \land x \in R_{1} (A)) \to (⋃ x \in R_{1} (A) \land 𝒫 x \in R_{1} (A) \land \forall y \in R_{1} (A) \{x, y\} \in R_{1} (A))$
63	62	ralrimiva	$⊢ (A \in V \land Lim A) \to \forall x \in R_{1} (A) (⋃ x \in R_{1} (A) \land 𝒫 x \in R_{1} (A) \land \forall y \in R_{1} (A) \{x, y\} \in R_{1} (A))$
64		fvex	$⊢ R_{1} (A) \in V$
65		iswun	$⊢ R_{1} (A) \in V \to (R_{1} (A) \in WUni \leftrightarrow (Tr R_{1} (A) \land R_{1} (A) \neq \emptyset \land \forall x \in R_{1} (A) (⋃ x \in R_{1} (A) \land 𝒫 x \in R_{1} (A) \land \forall y \in R_{1} (A) \{x, y\} \in R_{1} (A))))$
66	64 65	ax-mp	$⊢ R_{1} (A) \in WUni \leftrightarrow (Tr R_{1} (A) \land R_{1} (A) \neq \emptyset \land \forall x \in R_{1} (A) (⋃ x \in R_{1} (A) \land 𝒫 x \in R_{1} (A) \land \forall y \in R_{1} (A) \{x, y\} \in R_{1} (A)))$
67	2 12 63 66	syl3anbrc	$⊢ (A \in V \land Lim A) \to R_{1} (A) \in WUni$

Metamath Proof Explorer

Theorem r1limwun

Proof