Metamath Proof Explorer

Theorem rr-grothprimbi

Description: Express "every set is contained in a Grothendieck universe" using only primitives. The right side (without the outermost universal quantifier) is proven as rr-grothprim . (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Assertion rr-grothprimbi 
|- ( A. x E. y e. Univ x e. y <-> A. x -. A. y ( x e. y -> -. A. z ( z e. y -> A. f -. A. w ( w e. y -> -. A. v -. ( ( A. t ( t e. v -> t e. z ) -> -. ( v e. y -> -. v e. w ) ) -> -. A. i ( i e. z -> ( v e. y -> ( i e. v -> ( v e. f -> -. A. u ( u e. f -> ( i e. u -> -. A. o ( o e. u -> A. s ( s e. o -> s e. w ) ) ) ) ) ) ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 df-rex 
 |-  ( E. y e. Univ x e. y <-> E. y ( y e. Univ /\ x e. y ) )
2 ancom 
 |-  ( ( y e. Univ /\ x e. y ) <-> ( x e. y /\ y e. Univ ) )
3 biid 
 |-  ( x e. y <-> x e. y )
4 grumnueq 
 |-  Univ = { 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 ) ) ) ) }
5 4 ismnu 
 |-  ( y e. _V -> ( y e. Univ <-> A. z e. y ( ~P z C_ y /\ A. f E. w e. y ( ~P z C_ w /\ A. i e. z ( E. v e. y ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) ) )
6 5 elv 
 |-  ( y e. Univ <-> A. z e. y ( ~P z C_ y /\ A. f E. w e. y ( ~P z C_ w /\ A. i e. z ( E. v e. y ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) )
7 ismnuprim 
 |-  ( A. z e. y ( ~P z C_ y /\ A. f E. w e. y ( ~P z C_ w /\ A. i e. z ( E. v e. y ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) <-> A. z ( z e. y -> A. f -. A. w ( w e. y -> -. A. v -. ( ( A. t ( t e. v -> t e. z ) -> -. ( v e. y -> -. v e. w ) ) -> -. A. i ( i e. z -> ( v e. y -> ( i e. v -> ( v e. f -> -. A. u ( u e. f -> ( i e. u -> -. A. o ( o e. u -> A. s ( s e. o -> s e. w ) ) ) ) ) ) ) ) ) ) ) )
8 6 7 bitri 
 |-  ( y e. Univ <-> A. z ( z e. y -> A. f -. A. w ( w e. y -> -. A. v -. ( ( A. t ( t e. v -> t e. z ) -> -. ( v e. y -> -. v e. w ) ) -> -. A. i ( i e. z -> ( v e. y -> ( i e. v -> ( v e. f -> -. A. u ( u e. f -> ( i e. u -> -. A. o ( o e. u -> A. s ( s e. o -> s e. w ) ) ) ) ) ) ) ) ) ) ) )
9 3 8 expandan 
 |-  ( ( x e. y /\ y e. Univ ) <-> -. ( x e. y -> -. A. z ( z e. y -> A. f -. A. w ( w e. y -> -. A. v -. ( ( A. t ( t e. v -> t e. z ) -> -. ( v e. y -> -. v e. w ) ) -> -. A. i ( i e. z -> ( v e. y -> ( i e. v -> ( v e. f -> -. A. u ( u e. f -> ( i e. u -> -. A. o ( o e. u -> A. s ( s e. o -> s e. w ) ) ) ) ) ) ) ) ) ) ) ) )
10 2 9 bitri 
 |-  ( ( y e. Univ /\ x e. y ) <-> -. ( x e. y -> -. A. z ( z e. y -> A. f -. A. w ( w e. y -> -. A. v -. ( ( A. t ( t e. v -> t e. z ) -> -. ( v e. y -> -. v e. w ) ) -> -. A. i ( i e. z -> ( v e. y -> ( i e. v -> ( v e. f -> -. A. u ( u e. f -> ( i e. u -> -. A. o ( o e. u -> A. s ( s e. o -> s e. w ) ) ) ) ) ) ) ) ) ) ) ) )
11 10 expandexn 
 |-  ( E. y ( y e. Univ /\ x e. y ) <-> -. A. y ( x e. y -> -. A. z ( z e. y -> A. f -. A. w ( w e. y -> -. A. v -. ( ( A. t ( t e. v -> t e. z ) -> -. ( v e. y -> -. v e. w ) ) -> -. A. i ( i e. z -> ( v e. y -> ( i e. v -> ( v e. f -> -. A. u ( u e. f -> ( i e. u -> -. A. o ( o e. u -> A. s ( s e. o -> s e. w ) ) ) ) ) ) ) ) ) ) ) ) )
12 1 11 bitri 
 |-  ( E. y e. Univ x e. y <-> -. A. y ( x e. y -> -. A. z ( z e. y -> A. f -. A. w ( w e. y -> -. A. v -. ( ( A. t ( t e. v -> t e. z ) -> -. ( v e. y -> -. v e. w ) ) -> -. A. i ( i e. z -> ( v e. y -> ( i e. v -> ( v e. f -> -. A. u ( u e. f -> ( i e. u -> -. A. o ( o e. u -> A. s ( s e. o -> s e. w ) ) ) ) ) ) ) ) ) ) ) ) )
13 12 albii 
 |-  ( A. x E. y e. Univ x e. y <-> A. x -. A. y ( x e. y -> -. A. z ( z e. y -> A. f -. A. w ( w e. y -> -. A. v -. ( ( A. t ( t e. v -> t e. z ) -> -. ( v e. y -> -. v e. w ) ) -> -. A. i ( i e. z -> ( v e. y -> ( i e. v -> ( v e. f -> -. A. u ( u e. f -> ( i e. u -> -. A. o ( o e. u -> A. s ( s e. o -> s e. w ) ) ) ) ) ) ) ) ) ) ) ) )