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 | l k 𝒫 l k m n k 𝒫 l n p l q k p q q m r m p r r n
mnuunid.2 φ U M
mnuunid.3 φ A U
Assertion mnuunid φ A U

Proof

Step Hyp Ref Expression
1 mnuunid.1 M = k | l k 𝒫 l k m n k 𝒫 l n p l q k p q q m r m p r r n
2 mnuunid.2 φ U M
3 mnuunid.3 φ A U
4 3 snssd φ A U
5 1 2 3 4 mnuop3d φ w U i A v A i v u A i u u w
6 simprl φ w U i A v A i v u A i u u w w U
7 sseq2 a = w A a A w
8 7 adantl φ w U i A v A i v u A i u u w a = w A a A w
9 elssuni i A i A
10 9 rgen i A i A
11 simprr φ w U i A v A i v u A i u u w i A v A i v u A i u u w
12 eleq2 v = A i v i A
13 12 rexsng A U v A i v i A
14 3 13 syl φ v A i v i A
15 eleq2 u = A i u i A
16 unieq u = A u = A
17 16 sseq1d u = A u w A w
18 15 17 anbi12d u = A i u u w i A A w
19 18 rexsng A U u A i u u w i A A w
20 3 19 syl φ u A i u u w i A A w
21 14 20 imbi12d φ v A i v u A i u u w i A i A A w
22 anclb i A A w i A i A A w
23 21 22 bitr4di φ v A i v u A i u u w i A A w
24 23 imbi2d φ i A v A i v u A i u u w i A i A A w
25 pm5.4 i A i A A w i A A w
26 24 25 bitrdi φ i A v A i v u A i u u w i A A w
27 26 ralbidv2 φ i A v A i v u A i u u w i A A w
28 27 adantr φ w U i A v A i v u A i u u w i A v A i v u A i u u w i A A w
29 11 28 mpbid φ w U i A v A i v u A i u u w i A A w
30 sstr2 i A A w i w
31 30 ral2imi i A i A i A A w i A i w
32 10 29 31 mpsyl φ w U i A v A i v u A i u u w i A i w
33 unissb A w i A i w
34 32 33 sylibr φ w U i A v A i v u A i u u w A w
35 6 8 34 rspcedvd φ w U i A v A i v u A i u u w a U A a
36 5 35 rexlimddv φ a U A a
37 1 2 36 mnuss2d φ A U