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	|- E. y e. Univ x e. y

Proof

Step	Hyp	Ref	Expression
1		rankon	|- ( rank ` x ) e. On
2		inaex	|- ( ( rank ` x ) e. On -> E. z e. Inacc ( rank ` x ) e. z )
3	1 2	ax-mp	|- E. z e. Inacc ( rank ` x ) e. z
4		simplr	|- ( ( ( z e. Inacc /\ ( rank ` x ) e. z ) /\ y = ( R1 ` z ) ) -> ( rank ` x ) e. z )
5		inawina	|- ( z e. Inacc -> z e. InaccW )
6		winaon	|- ( z e. InaccW -> z e. On )
7	5 6	syl	|- ( z e. Inacc -> z e. On )
8	7	ad2antrr	|- ( ( ( z e. Inacc /\ ( rank ` x ) e. z ) /\ y = ( R1 ` z ) ) -> z e. On )
9		vex	|- x e. _V
10	9	rankr1a	|- ( z e. On -> ( x e. ( R1 ` z ) <-> ( rank ` x ) e. z ) )
11	8 10	syl	|- ( ( ( z e. Inacc /\ ( rank ` x ) e. z ) /\ y = ( R1 ` z ) ) -> ( x e. ( R1 ` z ) <-> ( rank ` x ) e. z ) )
12	4 11	mpbird	|- ( ( ( z e. Inacc /\ ( rank ` x ) e. z ) /\ y = ( R1 ` z ) ) -> x e. ( R1 ` z ) )
13		simpr	|- ( ( ( z e. Inacc /\ ( rank ` x ) e. z ) /\ y = ( R1 ` z ) ) -> y = ( R1 ` z ) )
14	12 13	eleqtrrd	|- ( ( ( z e. Inacc /\ ( rank ` x ) e. z ) /\ y = ( R1 ` z ) ) -> x e. y )
15		simpl	|- ( ( z e. Inacc /\ ( rank ` x ) e. z ) -> z e. Inacc )
16	15	inagrud	|- ( ( z e. Inacc /\ ( rank ` x ) e. z ) -> ( R1 ` z ) e. Univ )
17	14 16	rspcime	|- ( ( z e. Inacc /\ ( rank ` x ) e. z ) -> E. y e. Univ x e. y )
18	17	rexlimiva	|- ( E. z e. Inacc ( rank ` x ) e. z -> E. y e. Univ x e. y )
19	3 18	ax-mp	|- E. y e. Univ x e. y