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∈kp∈q∧q∈m→∃r∈mp∈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∈kp∈q∧q∈m→∃r∈mp∈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∈Ai∈v→∃u∈Ai∈u∧⋃u⊆w
6 simprl ⊢φ∧w∈U∧∀i∈A∃v∈Ai∈v→∃u∈Ai∈u∧⋃u⊆w→w∈U
7 sseq2 ⊢a=w→⋃A⊆a↔⋃A⊆w
8 7 adantl ⊢φ∧w∈U∧∀i∈A∃v∈Ai∈v→∃u∈Ai∈u∧⋃u⊆w∧a=w→⋃A⊆a↔⋃A⊆w
9 elssuni ⊢i∈A→i⊆⋃A
10 9 rgen ⊢∀i∈Ai⊆⋃A
11 simprr ⊢φ∧w∈U∧∀i∈A∃v∈Ai∈v→∃u∈Ai∈u∧⋃u⊆w→∀i∈A∃v∈Ai∈v→∃u∈Ai∈u∧⋃u⊆w
12 eleq2 ⊢v=A→i∈v↔i∈A
13 12 rexsng ⊢A∈U→∃v∈Ai∈v↔i∈A
14 3 13 syl ⊢φ→∃v∈Ai∈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∈Ai∈u∧⋃u⊆w↔i∈A∧⋃A⊆w
20 3 19 syl ⊢φ→∃u∈Ai∈u∧⋃u⊆w↔i∈A∧⋃A⊆w
21 14 20 imbi12d ⊢φ→∃v∈Ai∈v→∃u∈Ai∈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∈Ai∈v→∃u∈Ai∈u∧⋃u⊆w↔i∈A→⋃A⊆w
24 23 imbi2d ⊢φ→i∈A→∃v∈Ai∈v→∃u∈Ai∈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∈Ai∈v→∃u∈Ai∈u∧⋃u⊆w↔i∈A→⋃A⊆w
27 26 ralbidv2 ⊢φ→∀i∈A∃v∈Ai∈v→∃u∈Ai∈u∧⋃u⊆w↔∀i∈A⋃A⊆w
28 27 adantr ⊢φ∧w∈U∧∀i∈A∃v∈Ai∈v→∃u∈Ai∈u∧⋃u⊆w→∀i∈A∃v∈Ai∈v→∃u∈Ai∈u∧⋃u⊆w↔∀i∈A⋃A⊆w
29 11 28 mpbid ⊢φ∧w∈U∧∀i∈A∃v∈Ai∈v→∃u∈Ai∈u∧⋃u⊆w→∀i∈A⋃A⊆w
30 sstr2 ⊢i⊆⋃A→⋃A⊆w→i⊆w
31 30 ral2imi ⊢∀i∈Ai⊆⋃A→∀i∈A⋃A⊆w→∀i∈Ai⊆w
32 10 29 31 mpsyl ⊢φ∧w∈U∧∀i∈A∃v∈Ai∈v→∃u∈Ai∈u∧⋃u⊆w→∀i∈Ai⊆w
33 unissb ⊢⋃A⊆w↔∀i∈Ai⊆w
34 32 33 sylibr ⊢φ∧w∈U∧∀i∈A∃v∈Ai∈v→∃u∈Ai∈u∧⋃u⊆w→⋃A⊆w
35 6 8 34 rspcedvd ⊢φ∧w∈U∧∀i∈A∃v∈Ai∈v→∃u∈Ai∈u∧⋃u⊆w→∃a∈U⋃A⊆a
36 5 35 rexlimddv ⊢φ→∃a∈U⋃A⊆a
37 1 2 36 mnuss2d ⊢φ→⋃A∈U