Metamath Proof Explorer

Theorem grumnud

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

Ref Expression
Hypotheses grumnud.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 ) ) ) ) }
grumnud.2 
|- ( ph -> G e. Univ )
Assertion grumnud 
|- ( ph -> G e. M )

Proof

Step Hyp Ref Expression
1 grumnud.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 grumnud.2 
 |-  ( ph -> G e. Univ )
3 eqid 
 |-  ( { <. b , c >. | E. d ( U. d = c /\ d e. f /\ b e. d ) } i^i ( G X. G ) ) = ( { <. b , c >. | E. d ( U. d = c /\ d e. f /\ b e. d ) } i^i ( G X. G ) )
4 brxp 
 |-  ( i ( G X. G ) h <-> ( i e. G /\ h e. G ) )
5 brin 
 |-  ( i ( { <. b , c >. | E. d ( U. d = c /\ d e. f /\ b e. d ) } i^i ( G X. G ) ) h <-> ( i { <. b , c >. | E. d ( U. d = c /\ d e. f /\ b e. d ) } h /\ i ( G X. G ) h ) )
6 5 rbaib 
 |-  ( i ( G X. G ) h -> ( i ( { <. b , c >. | E. d ( U. d = c /\ d e. f /\ b e. d ) } i^i ( G X. G ) ) h <-> i { <. b , c >. | E. d ( U. d = c /\ d e. f /\ b e. d ) } h ) )
7 4 6 sylbir 
 |-  ( ( i e. G /\ h e. G ) -> ( i ( { <. b , c >. | E. d ( U. d = c /\ d e. f /\ b e. d ) } i^i ( G X. G ) ) h <-> i { <. b , c >. | E. d ( U. d = c /\ d e. f /\ b e. d ) } h ) )
8 vex 
 |-  i e. _V
9 vex 
 |-  h e. _V
10 simpr 
 |-  ( ( ( b = i /\ c = h ) /\ d = j ) -> d = j )
11 10 unieqd 
 |-  ( ( ( b = i /\ c = h ) /\ d = j ) -> U. d = U. j )
12 simplr 
 |-  ( ( ( b = i /\ c = h ) /\ d = j ) -> c = h )
13 11 12 eqeq12d 
 |-  ( ( ( b = i /\ c = h ) /\ d = j ) -> ( U. d = c <-> U. j = h ) )
14 elequ1 
 |-  ( d = j -> ( d e. f <-> j e. f ) )
15 14 adantl 
 |-  ( ( ( b = i /\ c = h ) /\ d = j ) -> ( d e. f <-> j e. f ) )
16 eleq12 
 |-  ( ( b = i /\ d = j ) -> ( b e. d <-> i e. j ) )
17 16 adantlr 
 |-  ( ( ( b = i /\ c = h ) /\ d = j ) -> ( b e. d <-> i e. j ) )
18 13 15 17 3anbi123d 
 |-  ( ( ( b = i /\ c = h ) /\ d = j ) -> ( ( U. d = c /\ d e. f /\ b e. d ) <-> ( U. j = h /\ j e. f /\ i e. j ) ) )
19 18 cbvexdvaw 
 |-  ( ( b = i /\ c = h ) -> ( E. d ( U. d = c /\ d e. f /\ b e. d ) <-> E. j ( U. j = h /\ j e. f /\ i e. j ) ) )
20 eqid 
 |-  { <. b , c >. | E. d ( U. d = c /\ d e. f /\ b e. d ) } = { <. b , c >. | E. d ( U. d = c /\ d e. f /\ b e. d ) }
21 8 9 19 20 braba 
 |-  ( i { <. b , c >. | E. d ( U. d = c /\ d e. f /\ b e. d ) } h <-> E. j ( U. j = h /\ j e. f /\ i e. j ) )
22 7 21 bitrdi 
 |-  ( ( i e. G /\ h e. G ) -> ( i ( { <. b , c >. | E. d ( U. d = c /\ d e. f /\ b e. d ) } i^i ( G X. G ) ) h <-> E. j ( U. j = h /\ j e. f /\ i e. j ) ) )
23 simplr3 
 |-  ( ( ( h e. ( ( { <. b , c >. | E. d ( U. d = c /\ d e. f /\ b e. d ) } i^i ( G X. G ) ) Coll z ) /\ ( U. j = h /\ j e. f /\ i e. j ) ) /\ u = j ) -> i e. j )
24 simpr 
 |-  ( ( ( h e. ( ( { <. b , c >. | E. d ( U. d = c /\ d e. f /\ b e. d ) } i^i ( G X. G ) ) Coll z ) /\ ( U. j = h /\ j e. f /\ i e. j ) ) /\ u = j ) -> u = j )
25 23 24 eleqtrrd 
 |-  ( ( ( h e. ( ( { <. b , c >. | E. d ( U. d = c /\ d e. f /\ b e. d ) } i^i ( G X. G ) ) Coll z ) /\ ( U. j = h /\ j e. f /\ i e. j ) ) /\ u = j ) -> i e. u )
26 24 unieqd 
 |-  ( ( ( h e. ( ( { <. b , c >. | E. d ( U. d = c /\ d e. f /\ b e. d ) } i^i ( G X. G ) ) Coll z ) /\ ( U. j = h /\ j e. f /\ i e. j ) ) /\ u = j ) -> U. u = U. j )
27 simplr1 
 |-  ( ( ( h e. ( ( { <. b , c >. | E. d ( U. d = c /\ d e. f /\ b e. d ) } i^i ( G X. G ) ) Coll z ) /\ ( U. j = h /\ j e. f /\ i e. j ) ) /\ u = j ) -> U. j = h )
28 26 27 eqtrd 
 |-  ( ( ( h e. ( ( { <. b , c >. | E. d ( U. d = c /\ d e. f /\ b e. d ) } i^i ( G X. G ) ) Coll z ) /\ ( U. j = h /\ j e. f /\ i e. j ) ) /\ u = j ) -> U. u = h )
29 simpll 
 |-  ( ( ( h e. ( ( { <. b , c >. | E. d ( U. d = c /\ d e. f /\ b e. d ) } i^i ( G X. G ) ) Coll z ) /\ ( U. j = h /\ j e. f /\ i e. j ) ) /\ u = j ) -> h e. ( ( { <. b , c >. | E. d ( U. d = c /\ d e. f /\ b e. d ) } i^i ( G X. G ) ) Coll z ) )
30 28 29 eqeltrd 
 |-  ( ( ( h e. ( ( { <. b , c >. | E. d ( U. d = c /\ d e. f /\ b e. d ) } i^i ( G X. G ) ) Coll z ) /\ ( U. j = h /\ j e. f /\ i e. j ) ) /\ u = j ) -> U. u e. ( ( { <. b , c >. | E. d ( U. d = c /\ d e. f /\ b e. d ) } i^i ( G X. G ) ) Coll z ) )
31 25 30 jca 
 |-  ( ( ( h e. ( ( { <. b , c >. | E. d ( U. d = c /\ d e. f /\ b e. d ) } i^i ( G X. G ) ) Coll z ) /\ ( U. j = h /\ j e. f /\ i e. j ) ) /\ u = j ) -> ( i e. u /\ U. u e. ( ( { <. b , c >. | E. d ( U. d = c /\ d e. f /\ b e. d ) } i^i ( G X. G ) ) Coll z ) ) )
32 simpr2 
 |-  ( ( h e. ( ( { <. b , c >. | E. d ( U. d = c /\ d e. f /\ b e. d ) } i^i ( G X. G ) ) Coll z ) /\ ( U. j = h /\ j e. f /\ i e. j ) ) -> j e. f )
33 31 32 rspcime 
 |-  ( ( h e. ( ( { <. b , c >. | E. d ( U. d = c /\ d e. f /\ b e. d ) } i^i ( G X. G ) ) Coll z ) /\ ( U. j = h /\ j e. f /\ i e. j ) ) -> E. u e. f ( i e. u /\ U. u e. ( ( { <. b , c >. | E. d ( U. d = c /\ d e. f /\ b e. d ) } i^i ( G X. G ) ) Coll z ) ) )
34 1 2 3 22 33 grumnudlem 
 |-  ( ph -> G e. M )