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 ⊢ ∃ y ∈ Univ x ∈ y

Proof

Step Hyp Ref Expression
1 rankon ⊢ rank ⁡ x ∈ On
2 inaex ⊢ rank ⁡ x ∈ On → ∃ z ∈ Inacc rank ⁡ x ∈ z
3 1 2 ax-mp ⊢ ∃ z ∈ Inacc rank ⁡ x ∈ z
4 simplr ⊢ z ∈ Inacc ∧ rank ⁡ x ∈ z ∧ y = R1 ⁡ z → rank ⁡ x ∈ z
5 inawina ⊢ z ∈ Inacc → z ∈ Inacc 𝑤
6 winaon ⊢ z ∈ Inacc 𝑤 → z ∈ On
7 5 6 syl ⊢ z ∈ Inacc → z ∈ On
8 7 ad2antrr ⊢ z ∈ Inacc ∧ rank ⁡ x ∈ z ∧ y = R1 ⁡ z → z ∈ On
9 vex ⊢ x ∈ V
10 9 rankr1a ⊢ z ∈ On → x ∈ R1 ⁡ z ↔ rank ⁡ x ∈ z
11 8 10 syl ⊢ z ∈ Inacc ∧ rank ⁡ x ∈ z ∧ y = R1 ⁡ z → x ∈ R1 ⁡ z ↔ rank ⁡ x ∈ z
12 4 11 mpbird ⊢ z ∈ Inacc ∧ rank ⁡ x ∈ z ∧ y = R1 ⁡ z → x ∈ R1 ⁡ z
13 simpr ⊢ z ∈ Inacc ∧ rank ⁡ x ∈ z ∧ y = R1 ⁡ z → y = R1 ⁡ z
14 12 13 eleqtrrd ⊢ z ∈ Inacc ∧ rank ⁡ x ∈ z ∧ y = R1 ⁡ z → x ∈ y
15 simpl ⊢ z ∈ Inacc ∧ rank ⁡ x ∈ z → z ∈ Inacc
16 15 inagrud ⊢ z ∈ Inacc ∧ rank ⁡ x ∈ z → R1 ⁡ z ∈ Univ
17 14 16 rspcime ⊢ z ∈ Inacc ∧ rank ⁡ x ∈ z → ∃ y ∈ Univ x ∈ y
18 17 rexlimiva ⊢ ∃ z ∈ Inacc rank ⁡ x ∈ z → ∃ y ∈ Univ x ∈ y
19 3 18 ax-mp ⊢ ∃ y ∈ Univ x ∈ y