grur1

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

		Ref	Expression
	Hypothesis	gruina.1	$⊢ A = U \cap On$
	Assertion	grur1	$⊢ (U \in Univ \land U \in ⋃ R_{1} [On]) \to U = R_{1} (A)$

Proof

Step	Hyp	Ref	Expression
1		gruina.1	$⊢ A = U \cap On$
2		nss	$⊢ \neg U \subseteq R_{1} (A) \leftrightarrow \exists x (x \in U \land \neg x \in R_{1} (A))$
3		fveqeq2	$⊢ y = x \to (rank (y) = A \leftrightarrow rank (x) = A)$
4	3	rspcev	$⊢ (x \in U \land rank (x) = A) \to \exists y \in U rank (y) = A$
5	4	ex	$⊢ x \in U \to (rank (x) = A \to \exists y \in U rank (y) = A)$
6	5	ad2antrl	$⊢ ((U \in Univ \land U \in ⋃ R_{1} [On]) \land (x \in U \land \neg x \in R_{1} (A))) \to (rank (x) = A \to \exists y \in U rank (y) = A)$
7		simplr	$⊢ ((U \in Univ \land U \in ⋃ R_{1} [On]) \land (x \in U \land \neg x \in R_{1} (A))) \to U \in ⋃ R_{1} [On]$
8		simprl	$⊢ ((U \in Univ \land U \in ⋃ R_{1} [On]) \land (x \in U \land \neg x \in R_{1} (A))) \to x \in U$
9		r1elssi	$⊢ U \in ⋃ R_{1} [On] \to U \subseteq ⋃ R_{1} [On]$
10	9	sseld	$⊢ U \in ⋃ R_{1} [On] \to (x \in U \to x \in ⋃ R_{1} [On])$
11	7 8 10	sylc	$⊢ ((U \in Univ \land U \in ⋃ R_{1} [On]) \land (x \in U \land \neg x \in R_{1} (A))) \to x \in ⋃ R_{1} [On]$
12		tcrank	$⊢ x \in ⋃ R_{1} [On] \to rank (x) = rank [TC (x)]$
13	11 12	syl	$⊢ ((U \in Univ \land U \in ⋃ R_{1} [On]) \land (x \in U \land \neg x \in R_{1} (A))) \to rank (x) = rank [TC (x)]$
14	13	eleq2d	$⊢ ((U \in Univ \land U \in ⋃ R_{1} [On]) \land (x \in U \land \neg x \in R_{1} (A))) \to (A \in rank (x) \leftrightarrow A \in rank [TC (x)])$
15		gruelss	$⊢ (U \in Univ \land x \in U) \to x \subseteq U$
16		grutr	$⊢ U \in Univ \to Tr U$
17	16	adantr	$⊢ (U \in Univ \land x \in U) \to Tr U$
18		vex	$⊢ x \in V$
19		tcmin	$⊢ x \in V \to ((x \subseteq U \land Tr U) \to TC (x) \subseteq U)$
20	18 19	ax-mp	$⊢ (x \subseteq U \land Tr U) \to TC (x) \subseteq U$
21	15 17 20	syl2anc	$⊢ (U \in Univ \land x \in U) \to TC (x) \subseteq U$
22		rankf	$⊢ rank : ⋃ R_{1} [On] ⟶ On$
23		ffun	$⊢ rank : ⋃ R_{1} [On] ⟶ On \to Fun rank$
24	22 23	ax-mp	$⊢ Fun rank$
25		fvelima	$⊢ (Fun rank \land A \in rank [TC (x)]) \to \exists y \in TC (x) rank (y) = A$
26	24 25	mpan	$⊢ A \in rank [TC (x)] \to \exists y \in TC (x) rank (y) = A$
27		ssrexv	$⊢ TC (x) \subseteq U \to (\exists y \in TC (x) rank (y) = A \to \exists y \in U rank (y) = A)$
28	21 26 27	syl2im	$⊢ (U \in Univ \land x \in U) \to (A \in rank [TC (x)] \to \exists y \in U rank (y) = A)$
29	28	ad2ant2r	$⊢ ((U \in Univ \land U \in ⋃ R_{1} [On]) \land (x \in U \land \neg x \in R_{1} (A))) \to (A \in rank [TC (x)] \to \exists y \in U rank (y) = A)$
30	14 29	sylbid	$⊢ ((U \in Univ \land U \in ⋃ R_{1} [On]) \land (x \in U \land \neg x \in R_{1} (A))) \to (A \in rank (x) \to \exists y \in U rank (y) = A)$
31		simprr	$⊢ ((U \in Univ \land U \in ⋃ R_{1} [On]) \land (x \in U \land \neg x \in R_{1} (A))) \to \neg x \in R_{1} (A)$
32		ne0i	$⊢ x \in U \to U \neq \emptyset$
33	1	gruina	$⊢ (U \in Univ \land U \neq \emptyset) \to A \in Inacc$
34	32 33	sylan2	$⊢ (U \in Univ \land x \in U) \to A \in Inacc$
35		inawina	$⊢ A \in Inacc \to A \in {Inacc}_{𝑤}$
36		winaon	$⊢ A \in {Inacc}_{𝑤} \to A \in On$
37	34 35 36	3syl	$⊢ (U \in Univ \land x \in U) \to A \in On$
38		r1fnon	$⊢ R_{1} Fn On$
39		fndm	$⊢ R_{1} Fn On \to dom R_{1} = On$
40	38 39	ax-mp	$⊢ dom R_{1} = On$
41	37 40	eleqtrrdi	$⊢ (U \in Univ \land x \in U) \to A \in dom R_{1}$
42	41	ad2ant2r	$⊢ ((U \in Univ \land U \in ⋃ R_{1} [On]) \land (x \in U \land \neg x \in R_{1} (A))) \to A \in dom R_{1}$
43		rankr1ag	$⊢ (x \in ⋃ R_{1} [On] \land A \in dom R_{1}) \to (x \in R_{1} (A) \leftrightarrow rank (x) \in A)$
44	11 42 43	syl2anc	$⊢ ((U \in Univ \land U \in ⋃ R_{1} [On]) \land (x \in U \land \neg x \in R_{1} (A))) \to (x \in R_{1} (A) \leftrightarrow rank (x) \in A)$
45	31 44	mtbid	$⊢ ((U \in Univ \land U \in ⋃ R_{1} [On]) \land (x \in U \land \neg x \in R_{1} (A))) \to \neg rank (x) \in A$
46		rankon	$⊢ rank (x) \in On$
47		eloni	$⊢ rank (x) \in On \to Ord rank (x)$
48		eloni	$⊢ A \in On \to Ord A$
49		ordtri3or	$⊢ (Ord rank (x) \land Ord A) \to (rank (x) \in A \lor rank (x) = A \lor A \in rank (x))$
50	47 48 49	syl2an	$⊢ (rank (x) \in On \land A \in On) \to (rank (x) \in A \lor rank (x) = A \lor A \in rank (x))$
51	46 37 50	sylancr	$⊢ (U \in Univ \land x \in U) \to (rank (x) \in A \lor rank (x) = A \lor A \in rank (x))$
52		3orass	$⊢ (rank (x) \in A \lor rank (x) = A \lor A \in rank (x)) \leftrightarrow (rank (x) \in A \lor (rank (x) = A \lor A \in rank (x)))$
53	51 52	sylib	$⊢ (U \in Univ \land x \in U) \to (rank (x) \in A \lor (rank (x) = A \lor A \in rank (x)))$
54	53	ord	$⊢ (U \in Univ \land x \in U) \to (\neg rank (x) \in A \to (rank (x) = A \lor A \in rank (x)))$
55	54	ad2ant2r	$⊢ ((U \in Univ \land U \in ⋃ R_{1} [On]) \land (x \in U \land \neg x \in R_{1} (A))) \to (\neg rank (x) \in A \to (rank (x) = A \lor A \in rank (x)))$
56	45 55	mpd	$⊢ ((U \in Univ \land U \in ⋃ R_{1} [On]) \land (x \in U \land \neg x \in R_{1} (A))) \to (rank (x) = A \lor A \in rank (x))$
57	6 30 56	mpjaod	$⊢ ((U \in Univ \land U \in ⋃ R_{1} [On]) \land (x \in U \land \neg x \in R_{1} (A))) \to \exists y \in U rank (y) = A$
58	57	ex	$⊢ (U \in Univ \land U \in ⋃ R_{1} [On]) \to ((x \in U \land \neg x \in R_{1} (A)) \to \exists y \in U rank (y) = A)$
59	58	exlimdv	$⊢ (U \in Univ \land U \in ⋃ R_{1} [On]) \to (\exists x (x \in U \land \neg x \in R_{1} (A)) \to \exists y \in U rank (y) = A)$
60	2 59	biimtrid	$⊢ (U \in Univ \land U \in ⋃ R_{1} [On]) \to (\neg U \subseteq R_{1} (A) \to \exists y \in U rank (y) = A)$
61		simpll	$⊢ ((U \in Univ \land U \in ⋃ R_{1} [On]) \land (y \in U \land rank (y) = A)) \to U \in Univ$
62		ne0i	$⊢ y \in U \to U \neq \emptyset$
63	62 33	sylan2	$⊢ (U \in Univ \land y \in U) \to A \in Inacc$
64	63	ad2ant2r	$⊢ ((U \in Univ \land U \in ⋃ R_{1} [On]) \land (y \in U \land rank (y) = A)) \to A \in Inacc$
65	64 35 36	3syl	$⊢ ((U \in Univ \land U \in ⋃ R_{1} [On]) \land (y \in U \land rank (y) = A)) \to A \in On$
66		simprl	$⊢ ((U \in Univ \land U \in ⋃ R_{1} [On]) \land (y \in U \land rank (y) = A)) \to y \in U$
67		fveq2	$⊢ rank (y) = A \to cf (rank (y)) = cf (A)$
68	67	ad2antll	$⊢ ((U \in Univ \land U \in ⋃ R_{1} [On]) \land (y \in U \land rank (y) = A)) \to cf (rank (y)) = cf (A)$
69		elina	$⊢ A \in Inacc \leftrightarrow (A \neq \emptyset \land cf (A) = A \land \forall x \in A 𝒫 x ≺ A)$
70	69	simp2bi	$⊢ A \in Inacc \to cf (A) = A$
71	64 70	syl	$⊢ ((U \in Univ \land U \in ⋃ R_{1} [On]) \land (y \in U \land rank (y) = A)) \to cf (A) = A$
72	68 71	eqtrd	$⊢ ((U \in Univ \land U \in ⋃ R_{1} [On]) \land (y \in U \land rank (y) = A)) \to cf (rank (y)) = A$
73		rankcf	$⊢ \neg y ≺ cf (rank (y))$
74		fvex	$⊢ cf (rank (y)) \in V$
75		vex	$⊢ y \in V$
76		domtri	$⊢ (cf (rank (y)) \in V \land y \in V) \to (cf (rank (y)) ≼ y \leftrightarrow \neg y ≺ cf (rank (y)))$
77	74 75 76	mp2an	$⊢ cf (rank (y)) ≼ y \leftrightarrow \neg y ≺ cf (rank (y))$
78	73 77	mpbir	$⊢ cf (rank (y)) ≼ y$
79	72 78	eqbrtrrdi	$⊢ ((U \in Univ \land U \in ⋃ R_{1} [On]) \land (y \in U \land rank (y) = A)) \to A ≼ y$
80		grudomon	$⊢ (U \in Univ \land A \in On \land (y \in U \land A ≼ y)) \to A \in U$
81	61 65 66 79 80	syl112anc	$⊢ ((U \in Univ \land U \in ⋃ R_{1} [On]) \land (y \in U \land rank (y) = A)) \to A \in U$
82		elin	$⊢ A \in (U \cap On) \leftrightarrow (A \in U \land A \in On)$
83	82	biimpri	$⊢ (A \in U \land A \in On) \to A \in (U \cap On)$
84	83 1	eleqtrrdi	$⊢ (A \in U \land A \in On) \to A \in A$
85		ordirr	$⊢ Ord A \to \neg A \in A$
86	48 85	syl	$⊢ A \in On \to \neg A \in A$
87	86	adantl	$⊢ (A \in U \land A \in On) \to \neg A \in A$
88	84 87	pm2.21dd	$⊢ (A \in U \land A \in On) \to U \subseteq R_{1} (A)$
89	81 65 88	syl2anc	$⊢ ((U \in Univ \land U \in ⋃ R_{1} [On]) \land (y \in U \land rank (y) = A)) \to U \subseteq R_{1} (A)$
90	89	rexlimdvaa	$⊢ (U \in Univ \land U \in ⋃ R_{1} [On]) \to (\exists y \in U rank (y) = A \to U \subseteq R_{1} (A))$
91	60 90	syld	$⊢ (U \in Univ \land U \in ⋃ R_{1} [On]) \to (\neg U \subseteq R_{1} (A) \to U \subseteq R_{1} (A))$
92	91	pm2.18d	$⊢ (U \in Univ \land U \in ⋃ R_{1} [On]) \to U \subseteq R_{1} (A)$
93	1	grur1a	$⊢ U \in Univ \to R_{1} (A) \subseteq U$
94	93	adantr	$⊢ (U \in Univ \land U \in ⋃ R_{1} [On]) \to R_{1} (A) \subseteq U$
95	92 94	eqssd	$⊢ (U \in Univ \land U \in ⋃ R_{1} [On]) \to U = R_{1} (A)$

Metamath Proof Explorer

Theorem grur1

Proof