grur1a

Description: A characterization of Grothendieck universes, part 1. (Contributed by Mario Carneiro, 23-Jun-2013)

		Ref	Expression
	Hypothesis	gruina.1	$⊢ A = U \cap On$
	Assertion	grur1a	$⊢ U \in Univ \to R_{1} (A) \subseteq U$

Proof

Step	Hyp	Ref	Expression
1		gruina.1	$⊢ A = U \cap On$
2		inss1	$⊢ U \cap On \subseteq U$
3	1 2	eqsstri	$⊢ A \subseteq U$
4		sseq2	$⊢ U = \emptyset \to (A \subseteq U \leftrightarrow A \subseteq \emptyset)$
5	3 4	mpbii	$⊢ U = \emptyset \to A \subseteq \emptyset$
6		ss0	$⊢ A \subseteq \emptyset \to A = \emptyset$
7		fveq2	$⊢ A = \emptyset \to R_{1} (A) = R_{1} (\emptyset)$
8		r10	$⊢ R_{1} (\emptyset) = \emptyset$
9	7 8	eqtrdi	$⊢ A = \emptyset \to R_{1} (A) = \emptyset$
10		0ss	$⊢ \emptyset \subseteq U$
11	9 10	eqsstrdi	$⊢ A = \emptyset \to R_{1} (A) \subseteq U$
12	5 6 11	3syl	$⊢ U = \emptyset \to R_{1} (A) \subseteq U$
13	12	a1i	$⊢ U \in Univ \to (U = \emptyset \to R_{1} (A) \subseteq U)$
14	1	gruina	$⊢ (U \in Univ \land U \neq \emptyset) \to A \in Inacc$
15		inawina	$⊢ A \in Inacc \to A \in {Inacc}_{𝑤}$
16		winaon	$⊢ A \in {Inacc}_{𝑤} \to A \in On$
17		winalim	$⊢ A \in {Inacc}_{𝑤} \to Lim A$
18		r1lim	$⊢ (A \in On \land Lim A) \to R_{1} (A) = ⋃_{x \in A} R_{1} (x)$
19	16 17 18	syl2anc	$⊢ A \in {Inacc}_{𝑤} \to R_{1} (A) = ⋃_{x \in A} R_{1} (x)$
20	14 15 19	3syl	$⊢ (U \in Univ \land U \neq \emptyset) \to R_{1} (A) = ⋃_{x \in A} R_{1} (x)$
21		inss2	$⊢ U \cap On \subseteq On$
22	1 21	eqsstri	$⊢ A \subseteq On$
23	22	sseli	$⊢ x \in A \to x \in On$
24		eleq1	$⊢ x = \emptyset \to (x \in A \leftrightarrow \emptyset \in A)$
25		fveq2	$⊢ x = \emptyset \to R_{1} (x) = R_{1} (\emptyset)$
26	25 8	eqtrdi	$⊢ x = \emptyset \to R_{1} (x) = \emptyset$
27	26	eleq1d	$⊢ x = \emptyset \to (R_{1} (x) \in U \leftrightarrow \emptyset \in U)$
28	24 27	imbi12d	$⊢ x = \emptyset \to ((x \in A \to R_{1} (x) \in U) \leftrightarrow (\emptyset \in A \to \emptyset \in U))$
29		eleq1	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
30		fveq2	$⊢ x = y \to R_{1} (x) = R_{1} (y)$
31	30	eleq1d	$⊢ x = y \to (R_{1} (x) \in U \leftrightarrow R_{1} (y) \in U)$
32	29 31	imbi12d	$⊢ x = y \to ((x \in A \to R_{1} (x) \in U) \leftrightarrow (y \in A \to R_{1} (y) \in U))$
33		eleq1	$⊢ x = suc y \to (x \in A \leftrightarrow suc y \in A)$
34		fveq2	$⊢ x = suc y \to R_{1} (x) = R_{1} (suc y)$
35	34	eleq1d	$⊢ x = suc y \to (R_{1} (x) \in U \leftrightarrow R_{1} (suc y) \in U)$
36	33 35	imbi12d	$⊢ x = suc y \to ((x \in A \to R_{1} (x) \in U) \leftrightarrow (suc y \in A \to R_{1} (suc y) \in U))$
37	3	sseli	$⊢ \emptyset \in A \to \emptyset \in U$
38	37	a1i	$⊢ U \in Univ \to (\emptyset \in A \to \emptyset \in U)$
39		simpr	$⊢ (U \in Univ \land suc y \in A) \to suc y \in A$
40		elelsuc	$⊢ suc y \in A \to suc y \in suc A$
41	3	sseli	$⊢ suc y \in A \to suc y \in U$
42	41	ne0d	$⊢ suc y \in A \to U \neq \emptyset$
43	14 15 16	3syl	$⊢ (U \in Univ \land U \neq \emptyset) \to A \in On$
44	42 43	sylan2	$⊢ (U \in Univ \land suc y \in A) \to A \in On$
45		eloni	$⊢ A \in On \to Ord A$
46		ordsucelsuc	$⊢ Ord A \to (y \in A \leftrightarrow suc y \in suc A)$
47	44 45 46	3syl	$⊢ (U \in Univ \land suc y \in A) \to (y \in A \leftrightarrow suc y \in suc A)$
48	40 47	syl5ibr	$⊢ (U \in Univ \land suc y \in A) \to (suc y \in A \to y \in A)$
49	39 48	mpd	$⊢ (U \in Univ \land suc y \in A) \to y \in A$
50		grupw	$⊢ (U \in Univ \land R_{1} (y) \in U) \to 𝒫 R_{1} (y) \in U$
51	50	ex	$⊢ U \in Univ \to (R_{1} (y) \in U \to 𝒫 R_{1} (y) \in U)$
52	51	adantr	$⊢ (U \in Univ \land suc y \in A) \to (R_{1} (y) \in U \to 𝒫 R_{1} (y) \in U)$
53		r1suc	$⊢ y \in On \to R_{1} (suc y) = 𝒫 R_{1} (y)$
54	53	eleq1d	$⊢ y \in On \to (R_{1} (suc y) \in U \leftrightarrow 𝒫 R_{1} (y) \in U)$
55	54	biimprcd	$⊢ 𝒫 R_{1} (y) \in U \to (y \in On \to R_{1} (suc y) \in U)$
56	52 55	syl6	$⊢ (U \in Univ \land suc y \in A) \to (R_{1} (y) \in U \to (y \in On \to R_{1} (suc y) \in U))$
57	49 56	embantd	$⊢ (U \in Univ \land suc y \in A) \to ((y \in A \to R_{1} (y) \in U) \to (y \in On \to R_{1} (suc y) \in U))$
58	57	ex	$⊢ U \in Univ \to (suc y \in A \to ((y \in A \to R_{1} (y) \in U) \to (y \in On \to R_{1} (suc y) \in U)))$
59	58	com23	$⊢ U \in Univ \to ((y \in A \to R_{1} (y) \in U) \to (suc y \in A \to (y \in On \to R_{1} (suc y) \in U)))$
60	59	com4r	$⊢ y \in On \to (U \in Univ \to ((y \in A \to R_{1} (y) \in U) \to (suc y \in A \to R_{1} (suc y) \in U)))$
61		simpr	$⊢ (U \in Univ \land x \in A) \to x \in A$
62	3	sseli	$⊢ x \in A \to x \in U$
63	62	ne0d	$⊢ x \in A \to U \neq \emptyset$
64	63 43	sylan2	$⊢ (U \in Univ \land x \in A) \to A \in On$
65		ontr1	$⊢ A \in On \to ((y \in x \land x \in A) \to y \in A)$
66		pm2.27	$⊢ y \in A \to ((y \in A \to R_{1} (y) \in U) \to R_{1} (y) \in U)$
67	65 66	syl6	$⊢ A \in On \to ((y \in x \land x \in A) \to ((y \in A \to R_{1} (y) \in U) \to R_{1} (y) \in U))$
68	67	expd	$⊢ A \in On \to (y \in x \to (x \in A \to ((y \in A \to R_{1} (y) \in U) \to R_{1} (y) \in U)))$
69	68	com3r	$⊢ x \in A \to (A \in On \to (y \in x \to ((y \in A \to R_{1} (y) \in U) \to R_{1} (y) \in U)))$
70	61 64 69	sylc	$⊢ (U \in Univ \land x \in A) \to (y \in x \to ((y \in A \to R_{1} (y) \in U) \to R_{1} (y) \in U))$
71	70	imp	$⊢ ((U \in Univ \land x \in A) \land y \in x) \to ((y \in A \to R_{1} (y) \in U) \to R_{1} (y) \in U)$
72	71	ralimdva	$⊢ (U \in Univ \land x \in A) \to (\forall y \in x (y \in A \to R_{1} (y) \in U) \to \forall y \in x R_{1} (y) \in U)$
73		gruiun	$⊢ (U \in Univ \land x \in U \land \forall y \in x R_{1} (y) \in U) \to ⋃_{y \in x} R_{1} (y) \in U$
74	73	3expia	$⊢ (U \in Univ \land x \in U) \to (\forall y \in x R_{1} (y) \in U \to ⋃_{y \in x} R_{1} (y) \in U)$
75	62 74	sylan2	$⊢ (U \in Univ \land x \in A) \to (\forall y \in x R_{1} (y) \in U \to ⋃_{y \in x} R_{1} (y) \in U)$
76	72 75	syld	$⊢ (U \in Univ \land x \in A) \to (\forall y \in x (y \in A \to R_{1} (y) \in U) \to ⋃_{y \in x} R_{1} (y) \in U)$
77		vex	$⊢ x \in V$
78		r1lim	$⊢ (x \in V \land Lim x) \to R_{1} (x) = ⋃_{y \in x} R_{1} (y)$
79	77 78	mpan	$⊢ Lim x \to R_{1} (x) = ⋃_{y \in x} R_{1} (y)$
80	79	eleq1d	$⊢ Lim x \to (R_{1} (x) \in U \leftrightarrow ⋃_{y \in x} R_{1} (y) \in U)$
81	80	biimprd	$⊢ Lim x \to (⋃_{y \in x} R_{1} (y) \in U \to R_{1} (x) \in U)$
82	76 81	sylan9r	$⊢ (Lim x \land (U \in Univ \land x \in A)) \to (\forall y \in x (y \in A \to R_{1} (y) \in U) \to R_{1} (x) \in U)$
83	82	exp32	$⊢ Lim x \to (U \in Univ \to (x \in A \to (\forall y \in x (y \in A \to R_{1} (y) \in U) \to R_{1} (x) \in U)))$
84	83	com34	$⊢ Lim x \to (U \in Univ \to (\forall y \in x (y \in A \to R_{1} (y) \in U) \to (x \in A \to R_{1} (x) \in U)))$
85	28 32 36 38 60 84	tfinds2	$⊢ x \in On \to (U \in Univ \to (x \in A \to R_{1} (x) \in U))$
86	85	com3r	$⊢ x \in A \to (x \in On \to (U \in Univ \to R_{1} (x) \in U))$
87	23 86	mpd	$⊢ x \in A \to (U \in Univ \to R_{1} (x) \in U)$
88	87	impcom	$⊢ (U \in Univ \land x \in A) \to R_{1} (x) \in U$
89		gruelss	$⊢ (U \in Univ \land R_{1} (x) \in U) \to R_{1} (x) \subseteq U$
90	88 89	syldan	$⊢ (U \in Univ \land x \in A) \to R_{1} (x) \subseteq U$
91	90	ralrimiva	$⊢ U \in Univ \to \forall x \in A R_{1} (x) \subseteq U$
92		iunss	$⊢ ⋃_{x \in A} R_{1} (x) \subseteq U \leftrightarrow \forall x \in A R_{1} (x) \subseteq U$
93	91 92	sylibr	$⊢ U \in Univ \to ⋃_{x \in A} R_{1} (x) \subseteq U$
94	93	adantr	$⊢ (U \in Univ \land U \neq \emptyset) \to ⋃_{x \in A} R_{1} (x) \subseteq U$
95	20 94	eqsstrd	$⊢ (U \in Univ \land U \neq \emptyset) \to R_{1} (A) \subseteq U$
96	95	ex	$⊢ U \in Univ \to (U \neq \emptyset \to R_{1} (A) \subseteq U)$
97	13 96	pm2.61dne	$⊢ U \in Univ \to R_{1} (A) \subseteq U$

Metamath Proof Explorer

Theorem grur1a

Proof