Metamath Proof Explorer

Theorem mnuprdlem4

Description: Lemma for mnuprd . General case. (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Hypotheses mnuprdlem4.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 ) ) ) ) }
mnuprdlem4.2 
|- F = { { (/) , { A } } , { { (/) } , { B } } }
mnuprdlem4.3 
|- ( ph -> U e. M )
mnuprdlem4.4 
|- ( ph -> A e. U )
mnuprdlem4.5 
|- ( ph -> B e. U )
mnuprdlem4.6 
|- ( ph -> -. A = (/) )
Assertion mnuprdlem4 
|- ( ph -> { A , B } e. U )

Proof

Step Hyp Ref Expression
1 mnuprdlem4.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 mnuprdlem4.2 
 |-  F = { { (/) , { A } } , { { (/) } , { B } } }
3 mnuprdlem4.3 
 |-  ( ph -> U e. M )
4 mnuprdlem4.4 
 |-  ( ph -> A e. U )
5 mnuprdlem4.5 
 |-  ( ph -> B e. U )
6 mnuprdlem4.6 
 |-  ( ph -> -. A = (/) )
7 1 3 4 mnu0eld 
 |-  ( ph -> (/) e. U )
8 1 3 7 mnusnd 
 |-  ( ph -> { (/) } e. U )
9 0ss 
 |-  (/) C_ { (/) }
10 ssid 
 |-  { (/) } C_ { (/) }
11 1 3 8 9 10 mnuprss2d 
 |-  ( ph -> { (/) , { (/) } } e. U )
12 1 3 4 mnusnd 
 |-  ( ph -> { A } e. U )
13 0ss 
 |-  (/) C_ { A }
14 ssid 
 |-  { A } C_ { A }
15 1 3 12 13 14 mnuprss2d 
 |-  ( ph -> { (/) , { A } } e. U )
16 0ss 
 |-  (/) C_ B
17 ssid 
 |-  B C_ B
18 1 3 5 16 17 mnuprss2d 
 |-  ( ph -> { (/) , B } e. U )
19 snsspr1 
 |-  { (/) } C_ { (/) , B }
20 snsspr2 
 |-  { B } C_ { (/) , B }
21 1 3 18 19 20 mnuprss2d 
 |-  ( ph -> { { (/) } , { B } } e. U )
22 15 21 prssd 
 |-  ( ph -> { { (/) , { A } } , { { (/) } , { B } } } C_ U )
23 2 22 eqsstrid 
 |-  ( ph -> F C_ U )
24 1 3 11 23 mnuop3d 
 |-  ( ph -> E. w e. U A. i e. { (/) , { (/) } } ( E. v e. F i e. v -> E. u e. F ( i e. u /\ U. u C_ w ) ) )
25 simprl 
 |-  ( ( ph /\ ( w e. U /\ A. i e. { (/) , { (/) } } ( E. v e. F i e. v -> E. u e. F ( i e. u /\ U. u C_ w ) ) ) ) -> w e. U )
26 eleq2w 
 |-  ( a = w -> ( A e. a <-> A e. w ) )
27 eleq2w 
 |-  ( a = w -> ( B e. a <-> B e. w ) )
28 26 27 anbi12d 
 |-  ( a = w -> ( ( A e. a /\ B e. a ) <-> ( A e. w /\ B e. w ) ) )
29 28 adantl 
 |-  ( ( ( ph /\ ( w e. U /\ A. i e. { (/) , { (/) } } ( E. v e. F i e. v -> E. u e. F ( i e. u /\ U. u C_ w ) ) ) ) /\ a = w ) -> ( ( A e. a /\ B e. a ) <-> ( A e. w /\ B e. w ) ) )
30 4 adantr 
 |-  ( ( ph /\ ( w e. U /\ A. i e. { (/) , { (/) } } ( E. v e. F i e. v -> E. u e. F ( i e. u /\ U. u C_ w ) ) ) ) -> A e. U )
31 5 adantr 
 |-  ( ( ph /\ ( w e. U /\ A. i e. { (/) , { (/) } } ( E. v e. F i e. v -> E. u e. F ( i e. u /\ U. u C_ w ) ) ) ) -> B e. U )
32 nfv 
 |-  F/ i ph
33 nfv 
 |-  F/ i w e. U
34 nfra1 
 |-  F/ i A. i e. { (/) , { (/) } } ( E. v e. F i e. v -> E. u e. F ( i e. u /\ U. u C_ w ) )
35 33 34 nfan 
 |-  F/ i ( w e. U /\ A. i e. { (/) , { (/) } } ( E. v e. F i e. v -> E. u e. F ( i e. u /\ U. u C_ w ) ) )
36 32 35 nfan 
 |-  F/ i ( ph /\ ( w e. U /\ A. i e. { (/) , { (/) } } ( E. v e. F i e. v -> E. u e. F ( i e. u /\ U. u C_ w ) ) ) )
37 2 36 mnuprdlem3 
 |-  ( ( ph /\ ( w e. U /\ A. i e. { (/) , { (/) } } ( E. v e. F i e. v -> E. u e. F ( i e. u /\ U. u C_ w ) ) ) ) -> A. i e. { (/) , { (/) } } E. v e. F i e. v )
38 ralim 
 |-  ( A. i e. { (/) , { (/) } } ( E. v e. F i e. v -> E. u e. F ( i e. u /\ U. u C_ w ) ) -> ( A. i e. { (/) , { (/) } } E. v e. F i e. v -> A. i e. { (/) , { (/) } } E. u e. F ( i e. u /\ U. u C_ w ) ) )
39 38 ad2antll 
 |-  ( ( ph /\ ( w e. U /\ A. i e. { (/) , { (/) } } ( E. v e. F i e. v -> E. u e. F ( i e. u /\ U. u C_ w ) ) ) ) -> ( A. i e. { (/) , { (/) } } E. v e. F i e. v -> A. i e. { (/) , { (/) } } E. u e. F ( i e. u /\ U. u C_ w ) ) )
40 37 39 mpd 
 |-  ( ( ph /\ ( w e. U /\ A. i e. { (/) , { (/) } } ( E. v e. F i e. v -> E. u e. F ( i e. u /\ U. u C_ w ) ) ) ) -> A. i e. { (/) , { (/) } } E. u e. F ( i e. u /\ U. u C_ w ) )
41 2 30 31 40 mnuprdlem1 
 |-  ( ( ph /\ ( w e. U /\ A. i e. { (/) , { (/) } } ( E. v e. F i e. v -> E. u e. F ( i e. u /\ U. u C_ w ) ) ) ) -> A e. w )
42 6 adantr 
 |-  ( ( ph /\ ( w e. U /\ A. i e. { (/) , { (/) } } ( E. v e. F i e. v -> E. u e. F ( i e. u /\ U. u C_ w ) ) ) ) -> -. A = (/) )
43 2 31 42 40 mnuprdlem2 
 |-  ( ( ph /\ ( w e. U /\ A. i e. { (/) , { (/) } } ( E. v e. F i e. v -> E. u e. F ( i e. u /\ U. u C_ w ) ) ) ) -> B e. w )
44 41 43 jca 
 |-  ( ( ph /\ ( w e. U /\ A. i e. { (/) , { (/) } } ( E. v e. F i e. v -> E. u e. F ( i e. u /\ U. u C_ w ) ) ) ) -> ( A e. w /\ B e. w ) )
45 25 29 44 rspcedvd 
 |-  ( ( ph /\ ( w e. U /\ A. i e. { (/) , { (/) } } ( E. v e. F i e. v -> E. u e. F ( i e. u /\ U. u C_ w ) ) ) ) -> E. a e. U ( A e. a /\ B e. a ) )
46 24 45 rexlimddv 
 |-  ( ph -> E. a e. U ( A e. a /\ B e. a ) )
47 3 adantr 
 |-  ( ( ph /\ ( a e. U /\ ( A e. a /\ B e. a ) ) ) -> U e. M )
48 simprl 
 |-  ( ( ph /\ ( a e. U /\ ( A e. a /\ B e. a ) ) ) -> a e. U )
49 simprrl 
 |-  ( ( ph /\ ( a e. U /\ ( A e. a /\ B e. a ) ) ) -> A e. a )
50 simprrr 
 |-  ( ( ph /\ ( a e. U /\ ( A e. a /\ B e. a ) ) ) -> B e. a )
51 49 50 prssd 
 |-  ( ( ph /\ ( a e. U /\ ( A e. a /\ B e. a ) ) ) -> { A , B } C_ a )
52 1 47 48 51 mnussd 
 |-  ( ( ph /\ ( a e. U /\ ( A e. a /\ B e. a ) ) ) -> { A , B } e. U )
53 46 52 rexlimddv 
 |-  ( ph -> { A , B } e. U )