gruina

Description: If a Grothendieck universe U is nonempty, then the height of the ordinals in U is a strongly inaccessible cardinal. (Contributed by Mario Carneiro, 17-Jun-2013)

		Ref	Expression
	Hypothesis	gruina.1	$⊢ A = U \cap On$
	Assertion	gruina	$⊢ (U \in Univ \land U \neq \emptyset) \to A \in Inacc$

Proof

Step	Hyp	Ref	Expression
1		gruina.1	$⊢ A = U \cap On$
2		n0	$⊢ U \neq \emptyset \leftrightarrow \exists x x \in U$
3		0ss	$⊢ \emptyset \subseteq x$
4		gruss	$⊢ (U \in Univ \land x \in U \land \emptyset \subseteq x) \to \emptyset \in U$
5	3 4	mp3an3	$⊢ (U \in Univ \land x \in U) \to \emptyset \in U$
6		0elon	$⊢ \emptyset \in On$
7		elin	$⊢ \emptyset \in (U \cap On) \leftrightarrow (\emptyset \in U \land \emptyset \in On)$
8	5 6 7	sylanblrc	$⊢ (U \in Univ \land x \in U) \to \emptyset \in (U \cap On)$
9	8 1	eleqtrrdi	$⊢ (U \in Univ \land x \in U) \to \emptyset \in A$
10	9	ne0d	$⊢ (U \in Univ \land x \in U) \to A \neq \emptyset$
11	10	expcom	$⊢ x \in U \to (U \in Univ \to A \neq \emptyset)$
12	11	exlimiv	$⊢ \exists x x \in U \to (U \in Univ \to A \neq \emptyset)$
13	2 12	sylbi	$⊢ U \neq \emptyset \to (U \in Univ \to A \neq \emptyset)$
14	13	impcom	$⊢ (U \in Univ \land U \neq \emptyset) \to A \neq \emptyset$
15		grutr	$⊢ U \in Univ \to Tr U$
16		tron	$⊢ Tr On$
17		trin	$⊢ (Tr U \land Tr On) \to Tr (U \cap On)$
18	15 16 17	sylancl	$⊢ U \in Univ \to Tr (U \cap On)$
19		inss2	$⊢ U \cap On \subseteq On$
20		epweon	$⊢ E We On$
21		wess	$⊢ U \cap On \subseteq On \to (E We On \to E We (U \cap On))$
22	19 20 21	mp2	$⊢ E We (U \cap On)$
23		df-ord	$⊢ Ord (U \cap On) \leftrightarrow (Tr (U \cap On) \land E We (U \cap On))$
24	18 22 23	sylanblrc	$⊢ U \in Univ \to Ord (U \cap On)$
25		inex1g	$⊢ U \in Univ \to U \cap On \in V$
26		elon2	$⊢ U \cap On \in On \leftrightarrow (Ord (U \cap On) \land U \cap On \in V)$
27	24 25 26	sylanbrc	$⊢ U \in Univ \to U \cap On \in On$
28	1 27	eqeltrid	$⊢ U \in Univ \to A \in On$
29	28	adantr	$⊢ (U \in Univ \land U \neq \emptyset) \to A \in On$
30		eloni	$⊢ A \in On \to Ord A$
31		ordirr	$⊢ Ord A \to \neg A \in A$
32	30 31	syl	$⊢ A \in On \to \neg A \in A$
33		elin	$⊢ A \in (U \cap On) \leftrightarrow (A \in U \land A \in On)$
34	33	biimpri	$⊢ (A \in U \land A \in On) \to A \in (U \cap On)$
35	34 1	eleqtrrdi	$⊢ (A \in U \land A \in On) \to A \in A$
36	35	expcom	$⊢ A \in On \to (A \in U \to A \in A)$
37	32 36	mtod	$⊢ A \in On \to \neg A \in U$
38	29 37	syl	$⊢ (U \in Univ \land U \neq \emptyset) \to \neg A \in U$
39		inss1	$⊢ U \cap On \subseteq U$
40	1 39	eqsstri	$⊢ A \subseteq U$
41	40	sseli	$⊢ x \in A \to x \in U$
42		vpwex	$⊢ 𝒫 x \in V$
43	42	canth2	$⊢ 𝒫 x ≺ 𝒫 𝒫 x$
44	42	pwex	$⊢ 𝒫 𝒫 x \in V$
45	44	cardid	$⊢ card (𝒫 𝒫 x) \approx 𝒫 𝒫 x$
46	45	ensymi	$⊢ 𝒫 𝒫 x \approx card (𝒫 𝒫 x)$
47	28	adantr	$⊢ (U \in Univ \land x \in U) \to A \in On$
48		grupw	$⊢ (U \in Univ \land x \in U) \to 𝒫 x \in U$
49		grupw	$⊢ (U \in Univ \land 𝒫 x \in U) \to 𝒫 𝒫 x \in U$
50	48 49	syldan	$⊢ (U \in Univ \land x \in U) \to 𝒫 𝒫 x \in U$
51	28	adantr	$⊢ (U \in Univ \land 𝒫 𝒫 x \in U) \to A \in On$
52		endom	$⊢ card (𝒫 𝒫 x) \approx 𝒫 𝒫 x \to card (𝒫 𝒫 x) ≼ 𝒫 𝒫 x$
53	45 52	ax-mp	$⊢ card (𝒫 𝒫 x) ≼ 𝒫 𝒫 x$
54		cardon	$⊢ card (𝒫 𝒫 x) \in On$
55		grudomon	$⊢ (U \in Univ \land card (𝒫 𝒫 x) \in On \land (𝒫 𝒫 x \in U \land card (𝒫 𝒫 x) ≼ 𝒫 𝒫 x)) \to card (𝒫 𝒫 x) \in U$
56	54 55	mp3an2	$⊢ (U \in Univ \land (𝒫 𝒫 x \in U \land card (𝒫 𝒫 x) ≼ 𝒫 𝒫 x)) \to card (𝒫 𝒫 x) \in U$
57	53 56	mpanr2	$⊢ (U \in Univ \land 𝒫 𝒫 x \in U) \to card (𝒫 𝒫 x) \in U$
58		elin	$⊢ card (𝒫 𝒫 x) \in (U \cap On) \leftrightarrow (card (𝒫 𝒫 x) \in U \land card (𝒫 𝒫 x) \in On)$
59	58	biimpri	$⊢ (card (𝒫 𝒫 x) \in U \land card (𝒫 𝒫 x) \in On) \to card (𝒫 𝒫 x) \in (U \cap On)$
60	59 1	eleqtrrdi	$⊢ (card (𝒫 𝒫 x) \in U \land card (𝒫 𝒫 x) \in On) \to card (𝒫 𝒫 x) \in A$
61	57 54 60	sylancl	$⊢ (U \in Univ \land 𝒫 𝒫 x \in U) \to card (𝒫 𝒫 x) \in A$
62		onelss	$⊢ A \in On \to (card (𝒫 𝒫 x) \in A \to card (𝒫 𝒫 x) \subseteq A)$
63	51 61 62	sylc	$⊢ (U \in Univ \land 𝒫 𝒫 x \in U) \to card (𝒫 𝒫 x) \subseteq A$
64	50 63	syldan	$⊢ (U \in Univ \land x \in U) \to card (𝒫 𝒫 x) \subseteq A$
65		ssdomg	$⊢ A \in On \to (card (𝒫 𝒫 x) \subseteq A \to card (𝒫 𝒫 x) ≼ A)$
66	47 64 65	sylc	$⊢ (U \in Univ \land x \in U) \to card (𝒫 𝒫 x) ≼ A$
67		endomtr	$⊢ (𝒫 𝒫 x \approx card (𝒫 𝒫 x) \land card (𝒫 𝒫 x) ≼ A) \to 𝒫 𝒫 x ≼ A$
68	46 66 67	sylancr	$⊢ (U \in Univ \land x \in U) \to 𝒫 𝒫 x ≼ A$
69		sdomdomtr	$⊢ (𝒫 x ≺ 𝒫 𝒫 x \land 𝒫 𝒫 x ≼ A) \to 𝒫 x ≺ A$
70	43 68 69	sylancr	$⊢ (U \in Univ \land x \in U) \to 𝒫 x ≺ A$
71	41 70	sylan2	$⊢ (U \in Univ \land x \in A) \to 𝒫 x ≺ A$
72	71	ralrimiva	$⊢ U \in Univ \to \forall x \in A 𝒫 x ≺ A$
73		inawinalem	$⊢ A \in On \to (\forall x \in A 𝒫 x ≺ A \to \forall x \in A \exists y \in A x ≺ y)$
74	28 72 73	sylc	$⊢ U \in Univ \to \forall x \in A \exists y \in A x ≺ y$
75	74	adantr	$⊢ (U \in Univ \land U \neq \emptyset) \to \forall x \in A \exists y \in A x ≺ y$
76		winainflem	$⊢ (A \neq \emptyset \land A \in On \land \forall x \in A \exists y \in A x ≺ y) \to ω \subseteq A$
77	14 29 75 76	syl3anc	$⊢ (U \in Univ \land U \neq \emptyset) \to ω \subseteq A$
78		vex	$⊢ x \in V$
79	78	canth2	$⊢ x ≺ 𝒫 x$
80		sdomtr	$⊢ (x ≺ 𝒫 x \land 𝒫 x ≺ A) \to x ≺ A$
81	79 71 80	sylancr	$⊢ (U \in Univ \land x \in A) \to x ≺ A$
82	81	ralrimiva	$⊢ U \in Univ \to \forall x \in A x ≺ A$
83		iscard	$⊢ card (A) = A \leftrightarrow (A \in On \land \forall x \in A x ≺ A)$
84	28 82 83	sylanbrc	$⊢ U \in Univ \to card (A) = A$
85		cardlim	$⊢ ω \subseteq card (A) \leftrightarrow Lim card (A)$
86		sseq2	$⊢ card (A) = A \to (ω \subseteq card (A) \leftrightarrow ω \subseteq A)$
87		limeq	$⊢ card (A) = A \to (Lim card (A) \leftrightarrow Lim A)$
88	86 87	bibi12d	$⊢ card (A) = A \to ((ω \subseteq card (A) \leftrightarrow Lim card (A)) \leftrightarrow (ω \subseteq A \leftrightarrow Lim A))$
89	85 88	mpbii	$⊢ card (A) = A \to (ω \subseteq A \leftrightarrow Lim A)$
90	84 89	syl	$⊢ U \in Univ \to (ω \subseteq A \leftrightarrow Lim A)$
91	90	adantr	$⊢ (U \in Univ \land U \neq \emptyset) \to (ω \subseteq A \leftrightarrow Lim A)$
92	77 91	mpbid	$⊢ (U \in Univ \land U \neq \emptyset) \to Lim A$
93		cflm	$⊢ (A \in On \land Lim A) \to cf (A) = ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\}$
94	29 92 93	syl2anc	$⊢ (U \in Univ \land U \neq \emptyset) \to cf (A) = ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\}$
95		cardon	$⊢ card (y) \in On$
96		eleq1	$⊢ x = card (y) \to (x \in On \leftrightarrow card (y) \in On)$
97	95 96	mpbiri	$⊢ x = card (y) \to x \in On$
98	97	adantr	$⊢ (x = card (y) \land (y \subseteq A \land A = ⋃ y)) \to x \in On$
99	98	exlimiv	$⊢ \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y)) \to x \in On$
100	99	abssi	$⊢ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\} \subseteq On$
101		fvex	$⊢ cf (A) \in V$
102	94 101	eqeltrrdi	$⊢ (U \in Univ \land U \neq \emptyset) \to ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\} \in V$
103		intex	$⊢ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\} \neq \emptyset \leftrightarrow ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\} \in V$
104	102 103	sylibr	$⊢ (U \in Univ \land U \neq \emptyset) \to \{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\} \neq \emptyset$
105		onint	$⊢ (\{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\} \subseteq On \land \{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\} \neq \emptyset) \to ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\} \in \{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\}$
106	100 104 105	sylancr	$⊢ (U \in Univ \land U \neq \emptyset) \to ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\} \in \{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\}$
107	94 106	eqeltrd	$⊢ (U \in Univ \land U \neq \emptyset) \to cf (A) \in \{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\}$
108		eqeq1	$⊢ x = cf (A) \to (x = card (y) \leftrightarrow cf (A) = card (y))$
109	108	anbi1d	$⊢ x = cf (A) \to ((x = card (y) \land (y \subseteq A \land A = ⋃ y)) \leftrightarrow (cf (A) = card (y) \land (y \subseteq A \land A = ⋃ y)))$
110	109	exbidv	$⊢ x = cf (A) \to (\exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y)) \leftrightarrow \exists y (cf (A) = card (y) \land (y \subseteq A \land A = ⋃ y)))$
111	101 110	elab	$⊢ cf (A) \in \{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\} \leftrightarrow \exists y (cf (A) = card (y) \land (y \subseteq A \land A = ⋃ y))$
112	107 111	sylib	$⊢ (U \in Univ \land U \neq \emptyset) \to \exists y (cf (A) = card (y) \land (y \subseteq A \land A = ⋃ y))$
113		simp2rr	$⊢ ((U \in Univ \land U \neq \emptyset) \land (cf (A) = card (y) \land (y \subseteq A \land A = ⋃ y)) \land cf (A) \in A) \to A = ⋃ y$
114		simp1l	$⊢ ((U \in Univ \land U \neq \emptyset) \land (cf (A) = card (y) \land (y \subseteq A \land A = ⋃ y)) \land cf (A) \in A) \to U \in Univ$
115		simp2rl	$⊢ ((U \in Univ \land U \neq \emptyset) \land (cf (A) = card (y) \land (y \subseteq A \land A = ⋃ y)) \land cf (A) \in A) \to y \subseteq A$
116	115 40	sstrdi	$⊢ ((U \in Univ \land U \neq \emptyset) \land (cf (A) = card (y) \land (y \subseteq A \land A = ⋃ y)) \land cf (A) \in A) \to y \subseteq U$
117	40	sseli	$⊢ cf (A) \in A \to cf (A) \in U$
118	117	3ad2ant3	$⊢ ((U \in Univ \land U \neq \emptyset) \land (cf (A) = card (y) \land (y \subseteq A \land A = ⋃ y)) \land cf (A) \in A) \to cf (A) \in U$
119		simp2l	$⊢ ((U \in Univ \land U \neq \emptyset) \land (cf (A) = card (y) \land (y \subseteq A \land A = ⋃ y)) \land cf (A) \in A) \to cf (A) = card (y)$
120		vex	$⊢ y \in V$
121	120	cardid	$⊢ card (y) \approx y$
122	119 121	eqbrtrdi	$⊢ ((U \in Univ \land U \neq \emptyset) \land (cf (A) = card (y) \land (y \subseteq A \land A = ⋃ y)) \land cf (A) \in A) \to cf (A) \approx y$
123		gruen	$⊢ (U \in Univ \land y \subseteq U \land (cf (A) \in U \land cf (A) \approx y)) \to y \in U$
124	114 116 118 122 123	syl112anc	$⊢ ((U \in Univ \land U \neq \emptyset) \land (cf (A) = card (y) \land (y \subseteq A \land A = ⋃ y)) \land cf (A) \in A) \to y \in U$
125		gruuni	$⊢ (U \in Univ \land y \in U) \to ⋃ y \in U$
126	114 124 125	syl2anc	$⊢ ((U \in Univ \land U \neq \emptyset) \land (cf (A) = card (y) \land (y \subseteq A \land A = ⋃ y)) \land cf (A) \in A) \to ⋃ y \in U$
127	113 126	eqeltrd	$⊢ ((U \in Univ \land U \neq \emptyset) \land (cf (A) = card (y) \land (y \subseteq A \land A = ⋃ y)) \land cf (A) \in A) \to A \in U$
128	127	3exp	$⊢ (U \in Univ \land U \neq \emptyset) \to ((cf (A) = card (y) \land (y \subseteq A \land A = ⋃ y)) \to (cf (A) \in A \to A \in U))$
129	128	exlimdv	$⊢ (U \in Univ \land U \neq \emptyset) \to (\exists y (cf (A) = card (y) \land (y \subseteq A \land A = ⋃ y)) \to (cf (A) \in A \to A \in U))$
130	112 129	mpd	$⊢ (U \in Univ \land U \neq \emptyset) \to (cf (A) \in A \to A \in U)$
131	38 130	mtod	$⊢ (U \in Univ \land U \neq \emptyset) \to \neg cf (A) \in A$
132		cfon	$⊢ cf (A) \in On$
133		cfle	$⊢ cf (A) \subseteq A$
134		onsseleq	$⊢ (cf (A) \in On \land A \in On) \to (cf (A) \subseteq A \leftrightarrow (cf (A) \in A \lor cf (A) = A))$
135	133 134	mpbii	$⊢ (cf (A) \in On \land A \in On) \to (cf (A) \in A \lor cf (A) = A)$
136	132 135	mpan	$⊢ A \in On \to (cf (A) \in A \lor cf (A) = A)$
137	136	ord	$⊢ A \in On \to (\neg cf (A) \in A \to cf (A) = A)$
138	29 131 137	sylc	$⊢ (U \in Univ \land U \neq \emptyset) \to cf (A) = A$
139	72	adantr	$⊢ (U \in Univ \land U \neq \emptyset) \to \forall x \in A 𝒫 x ≺ A$
140		elina	$⊢ A \in Inacc \leftrightarrow (A \neq \emptyset \land cf (A) = A \land \forall x \in A 𝒫 x ≺ A)$
141	14 138 139 140	syl3anbrc	$⊢ (U \in Univ \land U \neq \emptyset) \to A \in Inacc$

Metamath Proof Explorer

Theorem gruina

Proof