Metamath Proof Explorer

Theorem mnuunid

Description: Minimal universes are closed under union. (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Hypotheses mnuunid.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 ) ) ) ) }
mnuunid.2 
|- ( ph -> U e. M )
mnuunid.3 
|- ( ph -> A e. U )
Assertion mnuunid 
|- ( ph -> U. A e. U )

Proof

Step Hyp Ref Expression
1 mnuunid.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 mnuunid.2 
 |-  ( ph -> U e. M )
3 mnuunid.3 
 |-  ( ph -> A e. U )
4 3 snssd 
 |-  ( ph -> { A } C_ U )
5 1 2 3 4 mnuop3d 
 |-  ( ph -> E. w e. U A. i e. A ( E. v e. { A } i e. v -> E. u e. { A } ( i e. u /\ U. u C_ w ) ) )
6 simprl 
 |-  ( ( ph /\ ( w e. U /\ A. i e. A ( E. v e. { A } i e. v -> E. u e. { A } ( i e. u /\ U. u C_ w ) ) ) ) -> w e. U )
7 sseq2 
 |-  ( a = w -> ( U. A C_ a <-> U. A C_ w ) )
8 7 adantl 
 |-  ( ( ( ph /\ ( w e. U /\ A. i e. A ( E. v e. { A } i e. v -> E. u e. { A } ( i e. u /\ U. u C_ w ) ) ) ) /\ a = w ) -> ( U. A C_ a <-> U. A C_ w ) )
9 elssuni 
 |-  ( i e. A -> i C_ U. A )
10 9 rgen 
 |-  A. i e. A i C_ U. A
11 simprr 
 |-  ( ( ph /\ ( w e. U /\ A. i e. A ( E. v e. { A } i e. v -> E. u e. { A } ( i e. u /\ U. u C_ w ) ) ) ) -> A. i e. A ( E. v e. { A } i e. v -> E. u e. { A } ( i e. u /\ U. u C_ w ) ) )
12 eleq2 
 |-  ( v = A -> ( i e. v <-> i e. A ) )
13 12 rexsng 
 |-  ( A e. U -> ( E. v e. { A } i e. v <-> i e. A ) )
14 3 13 syl 
 |-  ( ph -> ( E. v e. { A } i e. v <-> i e. A ) )
15 eleq2 
 |-  ( u = A -> ( i e. u <-> i e. A ) )
16 unieq 
 |-  ( u = A -> U. u = U. A )
17 16 sseq1d 
 |-  ( u = A -> ( U. u C_ w <-> U. A C_ w ) )
18 15 17 anbi12d 
 |-  ( u = A -> ( ( i e. u /\ U. u C_ w ) <-> ( i e. A /\ U. A C_ w ) ) )
19 18 rexsng 
 |-  ( A e. U -> ( E. u e. { A } ( i e. u /\ U. u C_ w ) <-> ( i e. A /\ U. A C_ w ) ) )
20 3 19 syl 
 |-  ( ph -> ( E. u e. { A } ( i e. u /\ U. u C_ w ) <-> ( i e. A /\ U. A C_ w ) ) )
21 14 20 imbi12d 
 |-  ( ph -> ( ( E. v e. { A } i e. v -> E. u e. { A } ( i e. u /\ U. u C_ w ) ) <-> ( i e. A -> ( i e. A /\ U. A C_ w ) ) ) )
22 anclb 
 |-  ( ( i e. A -> U. A C_ w ) <-> ( i e. A -> ( i e. A /\ U. A C_ w ) ) )
23 21 22 bitr4di 
 |-  ( ph -> ( ( E. v e. { A } i e. v -> E. u e. { A } ( i e. u /\ U. u C_ w ) ) <-> ( i e. A -> U. A C_ w ) ) )
24 23 imbi2d 
 |-  ( ph -> ( ( i e. A -> ( E. v e. { A } i e. v -> E. u e. { A } ( i e. u /\ U. u C_ w ) ) ) <-> ( i e. A -> ( i e. A -> U. A C_ w ) ) ) )
25 pm5.4 
 |-  ( ( i e. A -> ( i e. A -> U. A C_ w ) ) <-> ( i e. A -> U. A C_ w ) )
26 24 25 bitrdi 
 |-  ( ph -> ( ( i e. A -> ( E. v e. { A } i e. v -> E. u e. { A } ( i e. u /\ U. u C_ w ) ) ) <-> ( i e. A -> U. A C_ w ) ) )
27 26 ralbidv2 
 |-  ( ph -> ( A. i e. A ( E. v e. { A } i e. v -> E. u e. { A } ( i e. u /\ U. u C_ w ) ) <-> A. i e. A U. A C_ w ) )
28 27 adantr 
 |-  ( ( ph /\ ( w e. U /\ A. i e. A ( E. v e. { A } i e. v -> E. u e. { A } ( i e. u /\ U. u C_ w ) ) ) ) -> ( A. i e. A ( E. v e. { A } i e. v -> E. u e. { A } ( i e. u /\ U. u C_ w ) ) <-> A. i e. A U. A C_ w ) )
29 11 28 mpbid 
 |-  ( ( ph /\ ( w e. U /\ A. i e. A ( E. v e. { A } i e. v -> E. u e. { A } ( i e. u /\ U. u C_ w ) ) ) ) -> A. i e. A U. A C_ w )
30 sstr2 
 |-  ( i C_ U. A -> ( U. A C_ w -> i C_ w ) )
31 30 ral2imi 
 |-  ( A. i e. A i C_ U. A -> ( A. i e. A U. A C_ w -> A. i e. A i C_ w ) )
32 10 29 31 mpsyl 
 |-  ( ( ph /\ ( w e. U /\ A. i e. A ( E. v e. { A } i e. v -> E. u e. { A } ( i e. u /\ U. u C_ w ) ) ) ) -> A. i e. A i C_ w )
33 unissb 
 |-  ( U. A C_ w <-> A. i e. A i C_ w )
34 32 33 sylibr 
 |-  ( ( ph /\ ( w e. U /\ A. i e. A ( E. v e. { A } i e. v -> E. u e. { A } ( i e. u /\ U. u C_ w ) ) ) ) -> U. A C_ w )
35 6 8 34 rspcedvd 
 |-  ( ( ph /\ ( w e. U /\ A. i e. A ( E. v e. { A } i e. v -> E. u e. { A } ( i e. u /\ U. u C_ w ) ) ) ) -> E. a e. U U. A C_ a )
36 5 35 rexlimddv 
 |-  ( ph -> E. a e. U U. A C_ a )
37 1 2 36 mnuss2d 
 |-  ( ph -> U. A e. U )