Metamath Proof Explorer


Theorem mnugrud

Description: Minimal universes are Grothendieck universes. (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Hypotheses mnugrud.1 M = k | l k 𝒫 l k m n k 𝒫 l n p l q k p q q m r m p r r n
mnugrud.2 φ U M
Assertion mnugrud φ U Univ

Proof

Step Hyp Ref Expression
1 mnugrud.1 M = k | l k 𝒫 l k m n k 𝒫 l n p l q k p q q m r m p r r n
2 mnugrud.2 φ U M
3 1 2 mnutrd φ Tr U
4 2 adantr φ x U U M
5 simpr φ x U x U
6 1 4 5 mnupwd φ x U 𝒫 x U
7 2 ad2antrr φ x U y U U M
8 5 adantr φ x U y U x U
9 simpr φ x U y U y U
10 1 7 8 9 mnuprd φ x U y U x y U
11 10 ralrimiva φ x U y U x y U
12 2 ad2antrr φ x U y U x U M
13 5 adantr φ x U y U x x U
14 elmapi y U x y : x U
15 14 adantl φ x U y U x y : x U
16 1 12 13 15 mnurnd φ x U y U x ran y U
17 1 12 16 mnuunid φ x U y U x ran y U
18 17 ralrimiva φ x U y U x ran y U
19 6 11 18 3jca φ x U 𝒫 x U y U x y U y U x ran y U
20 19 ralrimiva φ x U 𝒫 x U y U x y U y U x ran y U
21 elgrug U M U Univ Tr U x U 𝒫 x U y U x y U y U x ran y U
22 2 21 syl φ U Univ Tr U x U 𝒫 x U y U x y U y U x ran y U
23 3 20 22 mpbir2and φ U Univ