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