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	⊢ ∃ 𝑦 ∈ Univ 𝑥 ∈ 𝑦

Proof

Step	Hyp	Ref	Expression
1		rankon	⊢ ( rank ‘ 𝑥 ) ∈ On
2		inaex	⊢ ( ( rank ‘ 𝑥 ) ∈ On → ∃ 𝑧 ∈ Inacc ( rank ‘ 𝑥 ) ∈ 𝑧 )
3	1 2	ax-mp	⊢ ∃ 𝑧 ∈ Inacc ( rank ‘ 𝑥 ) ∈ 𝑧
4		simplr	⊢ ( ( ( 𝑧 ∈ Inacc ∧ ( rank ‘ 𝑥 ) ∈ 𝑧 ) ∧ 𝑦 = ( 𝑅1 ‘ 𝑧 ) ) → ( rank ‘ 𝑥 ) ∈ 𝑧 )
5		inawina	⊢ ( 𝑧 ∈ Inacc → 𝑧 ∈ Inaccw )
6		winaon	⊢ ( 𝑧 ∈ Inaccw → 𝑧 ∈ On )
7	5 6	syl	⊢ ( 𝑧 ∈ Inacc → 𝑧 ∈ On )
8	7	ad2antrr	⊢ ( ( ( 𝑧 ∈ Inacc ∧ ( rank ‘ 𝑥 ) ∈ 𝑧 ) ∧ 𝑦 = ( 𝑅1 ‘ 𝑧 ) ) → 𝑧 ∈ On )
9		vex	⊢ 𝑥 ∈ V
10	9	rankr1a	⊢ ( 𝑧 ∈ On → ( 𝑥 ∈ ( 𝑅1 ‘ 𝑧 ) ↔ ( rank ‘ 𝑥 ) ∈ 𝑧 ) )
11	8 10	syl	⊢ ( ( ( 𝑧 ∈ Inacc ∧ ( rank ‘ 𝑥 ) ∈ 𝑧 ) ∧ 𝑦 = ( 𝑅1 ‘ 𝑧 ) ) → ( 𝑥 ∈ ( 𝑅1 ‘ 𝑧 ) ↔ ( rank ‘ 𝑥 ) ∈ 𝑧 ) )
12	4 11	mpbird	⊢ ( ( ( 𝑧 ∈ Inacc ∧ ( rank ‘ 𝑥 ) ∈ 𝑧 ) ∧ 𝑦 = ( 𝑅1 ‘ 𝑧 ) ) → 𝑥 ∈ ( 𝑅1 ‘ 𝑧 ) )
13		simpr	⊢ ( ( ( 𝑧 ∈ Inacc ∧ ( rank ‘ 𝑥 ) ∈ 𝑧 ) ∧ 𝑦 = ( 𝑅1 ‘ 𝑧 ) ) → 𝑦 = ( 𝑅1 ‘ 𝑧 ) )
14	12 13	eleqtrrd	⊢ ( ( ( 𝑧 ∈ Inacc ∧ ( rank ‘ 𝑥 ) ∈ 𝑧 ) ∧ 𝑦 = ( 𝑅1 ‘ 𝑧 ) ) → 𝑥 ∈ 𝑦 )
15		simpl	⊢ ( ( 𝑧 ∈ Inacc ∧ ( rank ‘ 𝑥 ) ∈ 𝑧 ) → 𝑧 ∈ Inacc )
16	15	inagrud	⊢ ( ( 𝑧 ∈ Inacc ∧ ( rank ‘ 𝑥 ) ∈ 𝑧 ) → ( 𝑅1 ‘ 𝑧 ) ∈ Univ )
17	14 16	rspcime	⊢ ( ( 𝑧 ∈ Inacc ∧ ( rank ‘ 𝑥 ) ∈ 𝑧 ) → ∃ 𝑦 ∈ Univ 𝑥 ∈ 𝑦 )
18	17	rexlimiva	⊢ ( ∃ 𝑧 ∈ Inacc ( rank ‘ 𝑥 ) ∈ 𝑧 → ∃ 𝑦 ∈ Univ 𝑥 ∈ 𝑦 )
19	3 18	ax-mp	⊢ ∃ 𝑦 ∈ Univ 𝑥 ∈ 𝑦