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 | A. l e. k ( ~P l C_ k /\ A. m E. n e. k ( ~P l C_ n /\ A. p e. l ( E. q e. k ( p e. q /\ q e. m ) -> E. r e. m ( p e. r /\ U. r C_ n ) ) ) ) }
mnugrud.2 
|- ( ph -> U e. M )
Assertion mnugrud 
|- ( ph -> U e. Univ )

Proof

Step Hyp Ref Expression
1 mnugrud.1 
 |-  M = { k | A. l e. k ( ~P l C_ k /\ A. m E. n e. k ( ~P l C_ n /\ A. p e. l ( E. q e. k ( p e. q /\ q e. m ) -> E. r e. m ( p e. r /\ U. r C_ n ) ) ) ) }
2 mnugrud.2 
 |-  ( ph -> U e. M )
3 1 2 mnutrd 
 |-  ( ph -> Tr U )
4 2 adantr 
 |-  ( ( ph /\ x e. U ) -> U e. M )
5 simpr 
 |-  ( ( ph /\ x e. U ) -> x e. U )
6 1 4 5 mnupwd 
 |-  ( ( ph /\ x e. U ) -> ~P x e. U )
7 2 ad2antrr 
 |-  ( ( ( ph /\ x e. U ) /\ y e. U ) -> U e. M )
8 5 adantr 
 |-  ( ( ( ph /\ x e. U ) /\ y e. U ) -> x e. U )
9 simpr 
 |-  ( ( ( ph /\ x e. U ) /\ y e. U ) -> y e. U )
10 1 7 8 9 mnuprd 
 |-  ( ( ( ph /\ x e. U ) /\ y e. U ) -> { x , y } e. U )
11 10 ralrimiva 
 |-  ( ( ph /\ x e. U ) -> A. y e. U { x , y } e. U )
12 2 ad2antrr 
 |-  ( ( ( ph /\ x e. U ) /\ y e. ( U ^m x ) ) -> U e. M )
13 5 adantr 
 |-  ( ( ( ph /\ x e. U ) /\ y e. ( U ^m x ) ) -> x e. U )
14 elmapi 
 |-  ( y e. ( U ^m x ) -> y : x --> U )
15 14 adantl 
 |-  ( ( ( ph /\ x e. U ) /\ y e. ( U ^m x ) ) -> y : x --> U )
16 1 12 13 15 mnurnd 
 |-  ( ( ( ph /\ x e. U ) /\ y e. ( U ^m x ) ) -> ran y e. U )
17 1 12 16 mnuunid 
 |-  ( ( ( ph /\ x e. U ) /\ y e. ( U ^m x ) ) -> U. ran y e. U )
18 17 ralrimiva 
 |-  ( ( ph /\ x e. U ) -> A. y e. ( U ^m x ) U. ran y e. U )
19 6 11 18 3jca 
 |-  ( ( ph /\ x e. U ) -> ( ~P x e. U /\ A. y e. U { x , y } e. U /\ A. y e. ( U ^m x ) U. ran y e. U ) )
20 19 ralrimiva 
 |-  ( ph -> A. x e. U ( ~P x e. U /\ A. y e. U { x , y } e. U /\ A. y e. ( U ^m x ) U. ran y e. U ) )
21 elgrug 
 |-  ( U e. M -> ( U e. Univ <-> ( Tr U /\ A. x e. U ( ~P x e. U /\ A. y e. U { x , y } e. U /\ A. y e. ( U ^m x ) U. ran y e. U ) ) ) )
22 2 21 syl 
 |-  ( ph -> ( U e. Univ <-> ( Tr U /\ A. x e. U ( ~P x e. U /\ A. y e. U { x , y } e. U /\ A. y e. ( U ^m x ) U. ran y e. U ) ) ) )
23 3 20 22 mpbir2and 
 |-  ( ph -> U e. Univ )