Metamath Proof Explorer

Theorem ismnu

Description: The hypothesis of this theorem defines a class M of sets that we temporarily call "minimal universes", and which will turn out in grumnueq to be exactly Grothendicek universes. Minimal universes are sets which satisfy the predicate on y in rr-groth , except for the x e. y clause.

A minimal universe is closed under subsets ( mnussd ), powersets ( mnupwd ), and an operation which is similar to a combination of collection and union ( mnuop3d ), from which closure under pairing ( mnuprd ), unions ( mnuunid ), and function ranges ( mnurnd ) can be deduced, from which equivalence with Grothendieck universes ( grumnueq ) can be deduced. (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Hypothesis ismnu.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 ) ) ) ) }
Assertion ismnu 
|- ( U e. V -> ( U e. M <-> A. z e. U ( ~P z C_ U /\ A. f E. w e. U ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ismnu.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 simpr 
 |-  ( ( k = U /\ l = z ) -> l = z )
3 2 pweqd 
 |-  ( ( k = U /\ l = z ) -> ~P l = ~P z )
4 simpl 
 |-  ( ( k = U /\ l = z ) -> k = U )
5 3 4 sseq12d 
 |-  ( ( k = U /\ l = z ) -> ( ~P l C_ k <-> ~P z C_ U ) )
6 3 3adant3 
 |-  ( ( k = U /\ l = z /\ m = f ) -> ~P l = ~P z )
7 6 adantr 
 |-  ( ( ( k = U /\ l = z /\ m = f ) /\ n = w ) -> ~P l = ~P z )
8 simpr 
 |-  ( ( ( k = U /\ l = z /\ m = f ) /\ n = w ) -> n = w )
9 7 8 sseq12d 
 |-  ( ( ( k = U /\ l = z /\ m = f ) /\ n = w ) -> ( ~P l C_ n <-> ~P z C_ w ) )
10 simpl3 
 |-  ( ( ( ( k = U /\ l = z /\ m = f ) /\ n = w /\ p = i ) /\ q = v ) -> p = i )
11 simpr 
 |-  ( ( ( ( k = U /\ l = z /\ m = f ) /\ n = w /\ p = i ) /\ q = v ) -> q = v )
12 10 11 eleq12d 
 |-  ( ( ( ( k = U /\ l = z /\ m = f ) /\ n = w /\ p = i ) /\ q = v ) -> ( p e. q <-> i e. v ) )
13 simpl13 
 |-  ( ( ( ( k = U /\ l = z /\ m = f ) /\ n = w /\ p = i ) /\ q = v ) -> m = f )
14 11 13 eleq12d 
 |-  ( ( ( ( k = U /\ l = z /\ m = f ) /\ n = w /\ p = i ) /\ q = v ) -> ( q e. m <-> v e. f ) )
15 12 14 anbi12d 
 |-  ( ( ( ( k = U /\ l = z /\ m = f ) /\ n = w /\ p = i ) /\ q = v ) -> ( ( p e. q /\ q e. m ) <-> ( i e. v /\ v e. f ) ) )
16 simpl11 
 |-  ( ( ( ( k = U /\ l = z /\ m = f ) /\ n = w /\ p = i ) /\ q = v ) -> k = U )
17 15 16 cbvrexdva2 
 |-  ( ( ( k = U /\ l = z /\ m = f ) /\ n = w /\ p = i ) -> ( E. q e. k ( p e. q /\ q e. m ) <-> E. v e. U ( i e. v /\ v e. f ) ) )
18 simpl3 
 |-  ( ( ( ( k = U /\ l = z /\ m = f ) /\ n = w /\ p = i ) /\ r = u ) -> p = i )
19 simpr 
 |-  ( ( ( ( k = U /\ l = z /\ m = f ) /\ n = w /\ p = i ) /\ r = u ) -> r = u )
20 18 19 eleq12d 
 |-  ( ( ( ( k = U /\ l = z /\ m = f ) /\ n = w /\ p = i ) /\ r = u ) -> ( p e. r <-> i e. u ) )
21 19 unieqd 
 |-  ( ( ( ( k = U /\ l = z /\ m = f ) /\ n = w /\ p = i ) /\ r = u ) -> U. r = U. u )
22 simpl2 
 |-  ( ( ( ( k = U /\ l = z /\ m = f ) /\ n = w /\ p = i ) /\ r = u ) -> n = w )
23 21 22 sseq12d 
 |-  ( ( ( ( k = U /\ l = z /\ m = f ) /\ n = w /\ p = i ) /\ r = u ) -> ( U. r C_ n <-> U. u C_ w ) )
24 20 23 anbi12d 
 |-  ( ( ( ( k = U /\ l = z /\ m = f ) /\ n = w /\ p = i ) /\ r = u ) -> ( ( p e. r /\ U. r C_ n ) <-> ( i e. u /\ U. u C_ w ) ) )
25 simpl13 
 |-  ( ( ( ( k = U /\ l = z /\ m = f ) /\ n = w /\ p = i ) /\ r = u ) -> m = f )
26 24 25 cbvrexdva2 
 |-  ( ( ( k = U /\ l = z /\ m = f ) /\ n = w /\ p = i ) -> ( E. r e. m ( p e. r /\ U. r C_ n ) <-> E. u e. f ( i e. u /\ U. u C_ w ) ) )
27 17 26 imbi12d 
 |-  ( ( ( k = U /\ l = z /\ m = f ) /\ n = w /\ p = i ) -> ( ( E. q e. k ( p e. q /\ q e. m ) -> E. r e. m ( p e. r /\ U. r C_ n ) ) <-> ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) )
28 27 3expa 
 |-  ( ( ( ( k = U /\ l = z /\ m = f ) /\ n = w ) /\ p = i ) -> ( ( E. q e. k ( p e. q /\ q e. m ) -> E. r e. m ( p e. r /\ U. r C_ n ) ) <-> ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) )
29 simpll2 
 |-  ( ( ( ( k = U /\ l = z /\ m = f ) /\ n = w ) /\ p = i ) -> l = z )
30 28 29 cbvraldva2 
 |-  ( ( ( k = U /\ l = z /\ m = f ) /\ n = w ) -> ( 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 ) ) <-> A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) )
31 9 30 anbi12d 
 |-  ( ( ( k = U /\ l = z /\ m = f ) /\ n = w ) -> ( ( ~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 ) ) ) <-> ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) )
32 simpl1 
 |-  ( ( ( k = U /\ l = z /\ m = f ) /\ n = w ) -> k = U )
33 31 32 cbvrexdva2 
 |-  ( ( k = U /\ l = z /\ m = f ) -> ( 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 ) ) ) <-> E. w e. U ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) )
34 33 3expa 
 |-  ( ( ( k = U /\ l = z ) /\ m = f ) -> ( 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 ) ) ) <-> E. w e. U ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) )
35 34 cbvaldvaw 
 |-  ( ( k = U /\ l = z ) -> ( 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 ) ) ) <-> A. f E. w e. U ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) )
36 5 35 anbi12d 
 |-  ( ( k = U /\ l = z ) -> ( ( ~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 ) ) ) ) <-> ( ~P z C_ U /\ A. f E. w e. U ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) ) )
37 36 4 cbvraldva2 
 |-  ( k = U -> ( 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 ) ) ) ) <-> A. z e. U ( ~P z C_ U /\ A. f E. w e. U ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) ) )
38 37 1 elab2g 
 |-  ( U e. V -> ( U e. M <-> A. z e. U ( ~P z C_ U /\ A. f E. w e. U ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) ) )