Metamath Proof Explorer


Theorem mnuop3d

Description: Third operation of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Hypotheses mnuop3d.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 ) ) ) ) }
mnuop3d.2
|- ( ph -> U e. M )
mnuop3d.3
|- ( ph -> A e. U )
mnuop3d.4
|- ( ph -> F C_ U )
Assertion mnuop3d
|- ( ph -> E. w e. U A. i e. A ( E. v e. F i e. v -> E. u e. F ( i e. u /\ U. u C_ w ) ) )

Proof

Step Hyp Ref Expression
1 mnuop3d.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 mnuop3d.2
 |-  ( ph -> U e. M )
3 mnuop3d.3
 |-  ( ph -> A e. U )
4 mnuop3d.4
 |-  ( ph -> F C_ U )
5 2 4 sselpwd
 |-  ( ph -> F e. ~P U )
6 1 2 3 5 mnuop23d
 |-  ( ph -> E. w e. U ( ~P A C_ w /\ A. i e. A ( E. v e. U ( i e. v /\ v e. F ) -> E. u e. F ( i e. u /\ U. u C_ w ) ) ) )
7 4 sseld
 |-  ( ph -> ( v e. F -> v e. U ) )
8 7 adantrd
 |-  ( ph -> ( ( v e. F /\ i e. v ) -> v e. U ) )
9 pm3.22
 |-  ( ( v e. F /\ i e. v ) -> ( i e. v /\ v e. F ) )
10 8 9 jca2
 |-  ( ph -> ( ( v e. F /\ i e. v ) -> ( v e. U /\ ( i e. v /\ v e. F ) ) ) )
11 10 reximdv2
 |-  ( ph -> ( E. v e. F i e. v -> E. v e. U ( i e. v /\ v e. F ) ) )
12 11 imim1d
 |-  ( ph -> ( ( E. v e. U ( i e. v /\ v e. F ) -> E. u e. F ( i e. u /\ U. u C_ w ) ) -> ( E. v e. F i e. v -> E. u e. F ( i e. u /\ U. u C_ w ) ) ) )
13 12 ralimdv
 |-  ( ph -> ( A. i e. A ( E. v e. U ( i e. v /\ v e. F ) -> E. u e. F ( i e. u /\ U. u C_ w ) ) -> A. i e. A ( E. v e. F i e. v -> E. u e. F ( i e. u /\ U. u C_ w ) ) ) )
14 13 adantld
 |-  ( ph -> ( ( ~P A C_ w /\ A. i e. A ( E. v e. U ( i e. v /\ v e. F ) -> E. u e. F ( i e. u /\ U. u C_ w ) ) ) -> A. i e. A ( E. v e. F i e. v -> E. u e. F ( i e. u /\ U. u C_ w ) ) ) )
15 14 reximdv
 |-  ( ph -> ( E. w e. U ( ~P A C_ w /\ A. i e. A ( E. v e. U ( i e. v /\ v e. F ) -> E. u e. F ( i e. u /\ U. u C_ w ) ) ) -> E. w e. U A. i e. A ( E. v e. F i e. v -> E. u e. F ( i e. u /\ U. u C_ w ) ) ) )
16 6 15 mpd
 |-  ( ph -> E. w e. U A. i e. A ( E. v e. F i e. v -> E. u e. F ( i e. u /\ U. u C_ w ) ) )