grur1cld

Description: Grothendieck universes are closed under the cumulative hierarchy function. (Contributed by Rohan Ridenour, 8-Aug-2023)

	Ref	Expression
Hypotheses	grur1cld.1	$⊢ φ \to G \in Univ$
	grur1cld.2	$⊢ φ \to A \in G$
Assertion	grur1cld	$⊢ φ \to R_{1} (A) \in G$

Proof

Step	Hyp	Ref	Expression
1		grur1cld.1	$⊢ φ \to G \in Univ$
2		grur1cld.2	$⊢ φ \to A \in G$
3	2	adantr	$⊢ (φ \land A \in On) \to A \in G$
4		eleq1	$⊢ x = \emptyset \to (x \in G \leftrightarrow \emptyset \in G)$
5		fveq2	$⊢ x = \emptyset \to R_{1} (x) = R_{1} (\emptyset)$
6	5	eleq1d	$⊢ x = \emptyset \to (R_{1} (x) \in G \leftrightarrow R_{1} (\emptyset) \in G)$
7	4 6	imbi12d	$⊢ x = \emptyset \to ((x \in G \to R_{1} (x) \in G) \leftrightarrow (\emptyset \in G \to R_{1} (\emptyset) \in G))$
8		eleq1	$⊢ x = y \to (x \in G \leftrightarrow y \in G)$
9		fveq2	$⊢ x = y \to R_{1} (x) = R_{1} (y)$
10	9	eleq1d	$⊢ x = y \to (R_{1} (x) \in G \leftrightarrow R_{1} (y) \in G)$
11	8 10	imbi12d	$⊢ x = y \to ((x \in G \to R_{1} (x) \in G) \leftrightarrow (y \in G \to R_{1} (y) \in G))$
12		eleq1	$⊢ x = suc y \to (x \in G \leftrightarrow suc y \in G)$
13		fveq2	$⊢ x = suc y \to R_{1} (x) = R_{1} (suc y)$
14	13	eleq1d	$⊢ x = suc y \to (R_{1} (x) \in G \leftrightarrow R_{1} (suc y) \in G)$
15	12 14	imbi12d	$⊢ x = suc y \to ((x \in G \to R_{1} (x) \in G) \leftrightarrow (suc y \in G \to R_{1} (suc y) \in G))$
16		eleq1	$⊢ x = A \to (x \in G \leftrightarrow A \in G)$
17		fveq2	$⊢ x = A \to R_{1} (x) = R_{1} (A)$
18	17	eleq1d	$⊢ x = A \to (R_{1} (x) \in G \leftrightarrow R_{1} (A) \in G)$
19	16 18	imbi12d	$⊢ x = A \to ((x \in G \to R_{1} (x) \in G) \leftrightarrow (A \in G \to R_{1} (A) \in G))$
20		r10	$⊢ R_{1} (\emptyset) = \emptyset$
21	1 2	gru0eld	$⊢ φ \to \emptyset \in G$
22	20 21	eqeltrid	$⊢ φ \to R_{1} (\emptyset) \in G$
23	22	adantr	$⊢ (φ \land A \in On) \to R_{1} (\emptyset) \in G$
24	23	a1d	$⊢ (φ \land A \in On) \to (\emptyset \in G \to R_{1} (\emptyset) \in G)$
25		simpl1	$⊢ (((φ \land A \in On) \land y \in On \land (y \in G \to R_{1} (y) \in G)) \land suc y \in G) \to (φ \land A \in On)$
26		simpl2	$⊢ (((φ \land A \in On) \land y \in On \land (y \in G \to R_{1} (y) \in G)) \land suc y \in G) \to y \in On$
27	1	adantr	$⊢ (φ \land A \in On) \to G \in Univ$
28	25 27	syl	$⊢ (((φ \land A \in On) \land y \in On \land (y \in G \to R_{1} (y) \in G)) \land suc y \in G) \to G \in Univ$
29		simpr	$⊢ (((φ \land A \in On) \land y \in On \land (y \in G \to R_{1} (y) \in G)) \land suc y \in G) \to suc y \in G$
30		sssucid	$⊢ y \subseteq suc y$
31	30	a1i	$⊢ (((φ \land A \in On) \land y \in On \land (y \in G \to R_{1} (y) \in G)) \land suc y \in G) \to y \subseteq suc y$
32		gruss	$⊢ (G \in Univ \land suc y \in G \land y \subseteq suc y) \to y \in G$
33	28 29 31 32	syl3anc	$⊢ (((φ \land A \in On) \land y \in On \land (y \in G \to R_{1} (y) \in G)) \land suc y \in G) \to y \in G$
34		simpl3	$⊢ (((φ \land A \in On) \land y \in On \land (y \in G \to R_{1} (y) \in G)) \land suc y \in G) \to (y \in G \to R_{1} (y) \in G)$
35	33 34	mpd	$⊢ (((φ \land A \in On) \land y \in On \land (y \in G \to R_{1} (y) \in G)) \land suc y \in G) \to R_{1} (y) \in G$
36		r1suc	$⊢ y \in On \to R_{1} (suc y) = 𝒫 R_{1} (y)$
37	36	3ad2ant2	$⊢ ((φ \land A \in On) \land y \in On \land R_{1} (y) \in G) \to R_{1} (suc y) = 𝒫 R_{1} (y)$
38	27	3ad2ant1	$⊢ ((φ \land A \in On) \land y \in On \land R_{1} (y) \in G) \to G \in Univ$
39		simp3	$⊢ ((φ \land A \in On) \land y \in On \land R_{1} (y) \in G) \to R_{1} (y) \in G$
40		grupw	$⊢ (G \in Univ \land R_{1} (y) \in G) \to 𝒫 R_{1} (y) \in G$
41	38 39 40	syl2anc	$⊢ ((φ \land A \in On) \land y \in On \land R_{1} (y) \in G) \to 𝒫 R_{1} (y) \in G$
42	37 41	eqeltrd	$⊢ ((φ \land A \in On) \land y \in On \land R_{1} (y) \in G) \to R_{1} (suc y) \in G$
43	25 26 35 42	syl3anc	$⊢ (((φ \land A \in On) \land y \in On \land (y \in G \to R_{1} (y) \in G)) \land suc y \in G) \to R_{1} (suc y) \in G$
44	43	ex	$⊢ ((φ \land A \in On) \land y \in On \land (y \in G \to R_{1} (y) \in G)) \to (suc y \in G \to R_{1} (suc y) \in G)$
45		simpr	$⊢ (((φ \land A \in On) \land Lim x \land \forall y \in x (y \in G \to R_{1} (y) \in G)) \land x \in G) \to x \in G$
46		simpl2	$⊢ (((φ \land A \in On) \land Lim x \land \forall y \in x (y \in G \to R_{1} (y) \in G)) \land x \in G) \to Lim x$
47		r1lim	$⊢ (x \in G \land Lim x) \to R_{1} (x) = ⋃_{y \in x} R_{1} (y)$
48	45 46 47	syl2anc	$⊢ (((φ \land A \in On) \land Lim x \land \forall y \in x (y \in G \to R_{1} (y) \in G)) \land x \in G) \to R_{1} (x) = ⋃_{y \in x} R_{1} (y)$
49		simpl1	$⊢ (((φ \land A \in On) \land Lim x \land \forall y \in x (y \in G \to R_{1} (y) \in G)) \land x \in G) \to (φ \land A \in On)$
50	49 27	syl	$⊢ (((φ \land A \in On) \land Lim x \land \forall y \in x (y \in G \to R_{1} (y) \in G)) \land x \in G) \to G \in Univ$
51		simpl3	$⊢ (((φ \land A \in On) \land Lim x \land \forall y \in x (y \in G \to R_{1} (y) \in G)) \land x \in G) \to \forall y \in x (y \in G \to R_{1} (y) \in G)$
52		simpl1l	$⊢ (((φ \land A \in On) \land Lim x \land \forall y \in x (y \in G \to R_{1} (y) \in G)) \land x \in G) \to φ$
53		simpl1	$⊢ ((φ \land Lim x \land x \in G) \land y \in x) \to φ$
54	53 1	syl	$⊢ ((φ \land Lim x \land x \in G) \land y \in x) \to G \in Univ$
55		simpl3	$⊢ ((φ \land Lim x \land x \in G) \land y \in x) \to x \in G$
56		simpl2	$⊢ ((φ \land Lim x \land x \in G) \land y \in x) \to Lim x$
57		limord	$⊢ Lim x \to Ord x$
58	56 57	syl	$⊢ ((φ \land Lim x \land x \in G) \land y \in x) \to Ord x$
59		simpr	$⊢ ((φ \land Lim x \land x \in G) \land y \in x) \to y \in x$
60		ordelss	$⊢ (Ord x \land y \in x) \to y \subseteq x$
61	58 59 60	syl2anc	$⊢ ((φ \land Lim x \land x \in G) \land y \in x) \to y \subseteq x$
62		gruss	$⊢ (G \in Univ \land x \in G \land y \subseteq x) \to y \in G$
63	54 55 61 62	syl3anc	$⊢ ((φ \land Lim x \land x \in G) \land y \in x) \to y \in G$
64	63	ralrimiva	$⊢ (φ \land Lim x \land x \in G) \to \forall y \in x y \in G$
65	52 46 45 64	syl3anc	$⊢ (((φ \land A \in On) \land Lim x \land \forall y \in x (y \in G \to R_{1} (y) \in G)) \land x \in G) \to \forall y \in x y \in G$
66		ralim	$⊢ \forall y \in x (y \in G \to R_{1} (y) \in G) \to (\forall y \in x y \in G \to \forall y \in x R_{1} (y) \in G)$
67	51 65 66	sylc	$⊢ (((φ \land A \in On) \land Lim x \land \forall y \in x (y \in G \to R_{1} (y) \in G)) \land x \in G) \to \forall y \in x R_{1} (y) \in G$
68		gruiun	$⊢ (G \in Univ \land x \in G \land \forall y \in x R_{1} (y) \in G) \to ⋃_{y \in x} R_{1} (y) \in G$
69	50 45 67 68	syl3anc	$⊢ (((φ \land A \in On) \land Lim x \land \forall y \in x (y \in G \to R_{1} (y) \in G)) \land x \in G) \to ⋃_{y \in x} R_{1} (y) \in G$
70	48 69	eqeltrd	$⊢ (((φ \land A \in On) \land Lim x \land \forall y \in x (y \in G \to R_{1} (y) \in G)) \land x \in G) \to R_{1} (x) \in G$
71	70	ex	$⊢ ((φ \land A \in On) \land Lim x \land \forall y \in x (y \in G \to R_{1} (y) \in G)) \to (x \in G \to R_{1} (x) \in G)$
72		simpr	$⊢ (φ \land A \in On) \to A \in On$
73	7 11 15 19 24 44 71 72	tfindsd	$⊢ (φ \land A \in On) \to (A \in G \to R_{1} (A) \in G)$
74	3 73	mpd	$⊢ (φ \land A \in On) \to R_{1} (A) \in G$
75		r1fnon	$⊢ R_{1} Fn On$
76		fndm	$⊢ R_{1} Fn On \to dom R_{1} = On$
77	75 76	ax-mp	$⊢ dom R_{1} = On$
78	77	eleq2i	$⊢ A \in dom R_{1} \leftrightarrow A \in On$
79		ndmfv	$⊢ \neg A \in dom R_{1} \to R_{1} (A) = \emptyset$
80	78 79	sylnbir	$⊢ \neg A \in On \to R_{1} (A) = \emptyset$
81	80	adantl	$⊢ (φ \land \neg A \in On) \to R_{1} (A) = \emptyset$
82	21	adantr	$⊢ (φ \land \neg A \in On) \to \emptyset \in G$
83	81 82	eqeltrd	$⊢ (φ \land \neg A \in On) \to R_{1} (A) \in G$
84	74 83	pm2.61dan	$⊢ φ \to R_{1} (A) \in G$

Metamath Proof Explorer

Theorem grur1cld

Proof