Metamath Proof Explorer

Theorem gruex

Description: Assuming the Tarski-Grothendieck axiom, every set is contained in a Grothendieck universe. (Contributed by Rohan Ridenour, 13-Aug-2023)

		Ref	Expression
	Assertion	gruex	$⊢ \exists y \in Univ x \in y$

Proof

Step	Hyp	Ref	Expression
1		rankon	$⊢ rank (x) \in On$
2		inaex	$⊢ rank (x) \in On \to \exists z \in Inacc rank (x) \in z$
3	1 2	ax-mp	$⊢ \exists z \in Inacc rank (x) \in z$
4		simplr	$⊢ ((z \in Inacc \land rank (x) \in z) \land y = R_{1} (z)) \to rank (x) \in z$
5		inawina	$⊢ z \in Inacc \to z \in {Inacc}_{𝑤}$
6		winaon	$⊢ z \in {Inacc}_{𝑤} \to z \in On$
7	5 6	syl	$⊢ z \in Inacc \to z \in On$
8	7	ad2antrr	$⊢ ((z \in Inacc \land rank (x) \in z) \land y = R_{1} (z)) \to z \in On$
9		vex	$⊢ x \in V$
10	9	rankr1a	$⊢ z \in On \to (x \in R_{1} (z) \leftrightarrow rank (x) \in z)$
11	8 10	syl	$⊢ ((z \in Inacc \land rank (x) \in z) \land y = R_{1} (z)) \to (x \in R_{1} (z) \leftrightarrow rank (x) \in z)$
12	4 11	mpbird	$⊢ ((z \in Inacc \land rank (x) \in z) \land y = R_{1} (z)) \to x \in R_{1} (z)$
13		simpr	$⊢ ((z \in Inacc \land rank (x) \in z) \land y = R_{1} (z)) \to y = R_{1} (z)$
14	12 13	eleqtrrd	$⊢ ((z \in Inacc \land rank (x) \in z) \land y = R_{1} (z)) \to x \in y$
15		simpl	$⊢ (z \in Inacc \land rank (x) \in z) \to z \in Inacc$
16	15	inagrud	$⊢ (z \in Inacc \land rank (x) \in z) \to R_{1} (z) \in Univ$
17	14 16	rspcime	$⊢ (z \in Inacc \land rank (x) \in z) \to \exists y \in Univ x \in y$
18	17	rexlimiva	$⊢ \exists z \in Inacc rank (x) \in z \to \exists y \in Univ x \in y$
19	3 18	ax-mp	$⊢ \exists y \in Univ x \in y$