Metamath Proof Explorer

Theorem ismnuprim

Description: Express the predicate on U in ismnu using only primitives. (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Assertion ismnuprim 
|- ( 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 ) ) ) ) <-> A. z ( z e. U -> A. f -. A. w ( w e. U -> -. A. v -. ( ( A. t ( t e. v -> t e. z ) -> -. ( v e. U -> -. v e. w ) ) -> -. A. i ( i e. z -> ( v e. U -> ( 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 19.28v 
 |-  ( A. f ( ~P z C_ U /\ 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 ) ) ) ) <-> ( ~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 ) ) ) ) )
2 r19.42v 
 |-  ( E. w e. U ( ~P z C_ 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 ) ) ) ) <-> ( ~P z C_ U /\ 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 ) ) ) ) )
3 19.26 
 |-  ( A. v ( ( v C_ z -> ( v e. U /\ v e. w ) ) /\ A. i e. z ( ( v e. U /\ i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) <-> ( A. v ( v C_ z -> ( v e. U /\ v e. w ) ) /\ A. v A. i e. z ( ( v e. U /\ i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) )
4 19.26 
 |-  ( A. v ( ( v C_ z -> v e. U ) /\ ( v C_ z -> v e. w ) ) <-> ( A. v ( v C_ z -> v e. U ) /\ A. v ( v C_ z -> v e. w ) ) )
5 jcab 
 |-  ( ( v C_ z -> ( v e. U /\ v e. w ) ) <-> ( ( v C_ z -> v e. U ) /\ ( v C_ z -> v e. w ) ) )
6 5 albii 
 |-  ( A. v ( v C_ z -> ( v e. U /\ v e. w ) ) <-> A. v ( ( v C_ z -> v e. U ) /\ ( v C_ z -> v e. w ) ) )
7 pwss 
 |-  ( ~P z C_ U <-> A. v ( v C_ z -> v e. U ) )
8 pwss 
 |-  ( ~P z C_ w <-> A. v ( v C_ z -> v e. w ) )
9 7 8 anbi12i 
 |-  ( ( ~P z C_ U /\ ~P z C_ w ) <-> ( A. v ( v C_ z -> v e. U ) /\ A. v ( v C_ z -> v e. w ) ) )
10 4 6 9 3bitr4i 
 |-  ( A. v ( v C_ z -> ( v e. U /\ v e. w ) ) <-> ( ~P z C_ U /\ ~P z C_ w ) )
11 ralcom4 
 |-  ( A. i e. z A. v ( ( v e. U /\ i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) <-> A. v A. i e. z ( ( v e. U /\ i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) )
12 19.23v 
 |-  ( A. v ( ( v e. U /\ i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) <-> ( E. v ( v e. U /\ i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) )
13 3anass 
 |-  ( ( v e. U /\ i e. v /\ v e. f ) <-> ( v e. U /\ ( i e. v /\ v e. f ) ) )
14 13 exbii 
 |-  ( E. v ( v e. U /\ i e. v /\ v e. f ) <-> E. v ( v e. U /\ ( i e. v /\ v e. f ) ) )
15 df-rex 
 |-  ( E. v e. U ( i e. v /\ v e. f ) <-> E. v ( v e. U /\ ( i e. v /\ v e. f ) ) )
16 14 15 bitr4i 
 |-  ( E. v ( v e. U /\ i e. v /\ v e. f ) <-> E. v e. U ( i e. v /\ v e. f ) )
17 16 imbi1i 
 |-  ( ( E. v ( v e. U /\ i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) <-> ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) )
18 12 17 bitri 
 |-  ( A. v ( ( v e. U /\ i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) <-> ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) )
19 18 ralbii 
 |-  ( A. i e. z A. v ( ( v e. U /\ i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u 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 ) ) )
20 11 19 bitr3i 
 |-  ( A. v A. i e. z ( ( v e. U /\ i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u 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 ) ) )
21 10 20 anbi12i 
 |-  ( ( A. v ( v C_ z -> ( v e. U /\ v e. w ) ) /\ A. v A. i e. z ( ( v e. U /\ i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) <-> ( ( ~P z C_ 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 ) ) ) )
22 anass 
 |-  ( ( ( ~P z C_ 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 ) ) ) <-> ( ~P z C_ 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 ) ) ) ) )
23 21 22 bitri 
 |-  ( ( A. v ( v C_ z -> ( v e. U /\ v e. w ) ) /\ A. v A. i e. z ( ( v e. U /\ i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) <-> ( ~P z C_ 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 ) ) ) ) )
24 3 23 bitri 
 |-  ( A. v ( ( v C_ z -> ( v e. U /\ v e. w ) ) /\ A. i e. z ( ( v e. U /\ i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) <-> ( ~P z C_ 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 ) ) ) ) )
25 dfss2 
 |-  ( v C_ z <-> A. t ( t e. v -> t e. z ) )
26 df-an 
 |-  ( ( v e. U /\ v e. w ) <-> -. ( v e. U -> -. v e. w ) )
27 25 26 imbi12i 
 |-  ( ( v C_ z -> ( v e. U /\ v e. w ) ) <-> ( A. t ( t e. v -> t e. z ) -> -. ( v e. U -> -. v e. w ) ) )
28 3impexp 
 |-  ( ( ( v e. U /\ i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) <-> ( v e. U -> ( i e. v -> ( v e. f -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) )
29 biid 
 |-  ( i e. u <-> i e. u )
30 expanduniss 
 |-  ( U. u C_ w <-> A. o ( o e. u -> A. s ( s e. o -> s e. w ) ) )
31 29 30 expandan 
 |-  ( ( i e. u /\ U. u C_ w ) <-> -. ( i e. u -> -. A. o ( o e. u -> A. s ( s e. o -> s e. w ) ) ) )
32 31 expandrexn 
 |-  ( E. u e. f ( i e. u /\ U. u C_ w ) <-> -. A. u ( u e. f -> ( i e. u -> -. A. o ( o e. u -> A. s ( s e. o -> s e. w ) ) ) ) )
33 32 imbi2i 
 |-  ( ( v e. f -> E. u e. f ( i e. u /\ U. u C_ w ) ) <-> ( v e. f -> -. A. u ( u e. f -> ( i e. u -> -. A. o ( o e. u -> A. s ( s e. o -> s e. w ) ) ) ) ) )
34 33 imbi2i 
 |-  ( ( i e. v -> ( v e. f -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) <-> ( 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 ) ) ) ) ) ) )
35 34 imbi2i 
 |-  ( ( v e. U -> ( i e. v -> ( v e. f -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) <-> ( v e. U -> ( 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 ) ) ) ) ) ) ) )
36 28 35 bitri 
 |-  ( ( ( v e. U /\ i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) <-> ( v e. U -> ( 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 ) ) ) ) ) ) ) )
37 36 expandral 
 |-  ( A. i e. z ( ( v e. U /\ i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) <-> A. i ( i e. z -> ( v e. U -> ( 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 ) ) ) ) ) ) ) ) )
38 27 37 expandan 
 |-  ( ( ( v C_ z -> ( v e. U /\ v e. w ) ) /\ A. i e. z ( ( v e. U /\ i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) <-> -. ( ( A. t ( t e. v -> t e. z ) -> -. ( v e. U -> -. v e. w ) ) -> -. A. i ( i e. z -> ( v e. U -> ( 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 ) ) ) ) ) ) ) ) ) )
39 38 albii 
 |-  ( A. v ( ( v C_ z -> ( v e. U /\ v e. w ) ) /\ A. i e. z ( ( v e. U /\ i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) <-> A. v -. ( ( A. t ( t e. v -> t e. z ) -> -. ( v e. U -> -. v e. w ) ) -> -. A. i ( i e. z -> ( v e. U -> ( 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 ) ) ) ) ) ) ) ) ) )
40 24 39 bitr3i 
 |-  ( ( ~P z C_ 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 ) ) ) ) <-> A. v -. ( ( A. t ( t e. v -> t e. z ) -> -. ( v e. U -> -. v e. w ) ) -> -. A. i ( i e. z -> ( v e. U -> ( 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 ) ) ) ) ) ) ) ) ) )
41 40 expandrex 
 |-  ( E. w e. U ( ~P z C_ 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 ) ) ) ) <-> -. A. w ( w e. U -> -. A. v -. ( ( A. t ( t e. v -> t e. z ) -> -. ( v e. U -> -. v e. w ) ) -> -. A. i ( i e. z -> ( v e. U -> ( 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 ) ) ) ) ) ) ) ) ) ) )
42 2 41 bitr3i 
 |-  ( ( ~P z C_ U /\ 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 ) ) ) ) <-> -. A. w ( w e. U -> -. A. v -. ( ( A. t ( t e. v -> t e. z ) -> -. ( v e. U -> -. v e. w ) ) -> -. A. i ( i e. z -> ( v e. U -> ( 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 ) ) ) ) ) ) ) ) ) ) )
43 42 albii 
 |-  ( A. f ( ~P z C_ U /\ 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 ) ) ) ) <-> A. f -. A. w ( w e. U -> -. A. v -. ( ( A. t ( t e. v -> t e. z ) -> -. ( v e. U -> -. v e. w ) ) -> -. A. i ( i e. z -> ( v e. U -> ( 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 ) ) ) ) ) ) ) ) ) ) )
44 1 43 bitr3i 
 |-  ( ( ~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 ) ) ) ) <-> A. f -. A. w ( w e. U -> -. A. v -. ( ( A. t ( t e. v -> t e. z ) -> -. ( v e. U -> -. v e. w ) ) -> -. A. i ( i e. z -> ( v e. U -> ( 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 ) ) ) ) ) ) ) ) ) ) )
45 44 expandral 
 |-  ( 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 ) ) ) ) <-> A. z ( z e. U -> A. f -. A. w ( w e. U -> -. A. v -. ( ( A. t ( t e. v -> t e. z ) -> -. ( v e. U -> -. v e. w ) ) -> -. A. i ( i e. z -> ( v e. U -> ( 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 ) ) ) ) ) ) ) ) ) ) ) )