Theorem mnuunid

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

	Ref	Expression
Hypotheses	mnuunid.1	⊢ 𝑀 = { 𝑘 ∣ ∀ 𝑙 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑘 ∧ ∀ 𝑚 ∃ 𝑛 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ) }
	mnuunid.2	⊢ ( 𝜑 → 𝑈 ∈ 𝑀 )
	mnuunid.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
Assertion	mnuunid	⊢ ( 𝜑 → ∪ 𝐴 ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		mnuunid.1	⊢ 𝑀 = { 𝑘 ∣ ∀ 𝑙 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑘 ∧ ∀ 𝑚 ∃ 𝑛 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ) }
2		mnuunid.2	⊢ ( 𝜑 → 𝑈 ∈ 𝑀 )
3		mnuunid.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
4	3	snssd	⊢ ( 𝜑 → { 𝐴 } ⊆ 𝑈 )
5	1 2 3 4	mnuop3d	⊢ ( 𝜑 → ∃ 𝑤 ∈ 𝑈 ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ { 𝐴 } 𝑖 ∈ 𝑣 → ∃ 𝑢 ∈ { 𝐴 } ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) )
6		simprl	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑈 ∧ ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ { 𝐴 } 𝑖 ∈ 𝑣 → ∃ 𝑢 ∈ { 𝐴 } ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) → 𝑤 ∈ 𝑈 )
7		sseq2	⊢ ( 𝑎 = 𝑤 → ( ∪ 𝐴 ⊆ 𝑎 ↔ ∪ 𝐴 ⊆ 𝑤 ) )
8	7	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑈 ∧ ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ { 𝐴 } 𝑖 ∈ 𝑣 → ∃ 𝑢 ∈ { 𝐴 } ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) ∧ 𝑎 = 𝑤 ) → ( ∪ 𝐴 ⊆ 𝑎 ↔ ∪ 𝐴 ⊆ 𝑤 ) )
9		elssuni	⊢ ( 𝑖 ∈ 𝐴 → 𝑖 ⊆ ∪ 𝐴 )
10	9	rgen	⊢ ∀ 𝑖 ∈ 𝐴 𝑖 ⊆ ∪ 𝐴
11		simprr	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑈 ∧ ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ { 𝐴 } 𝑖 ∈ 𝑣 → ∃ 𝑢 ∈ { 𝐴 } ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) → ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ { 𝐴 } 𝑖 ∈ 𝑣 → ∃ 𝑢 ∈ { 𝐴 } ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) )
12		eleq2	⊢ ( 𝑣 = 𝐴 → ( 𝑖 ∈ 𝑣 ↔ 𝑖 ∈ 𝐴 ) )
13	12	rexsng	⊢ ( 𝐴 ∈ 𝑈 → ( ∃ 𝑣 ∈ { 𝐴 } 𝑖 ∈ 𝑣 ↔ 𝑖 ∈ 𝐴 ) )
14	3 13	syl	⊢ ( 𝜑 → ( ∃ 𝑣 ∈ { 𝐴 } 𝑖 ∈ 𝑣 ↔ 𝑖 ∈ 𝐴 ) )
15		eleq2	⊢ ( 𝑢 = 𝐴 → ( 𝑖 ∈ 𝑢 ↔ 𝑖 ∈ 𝐴 ) )
16		unieq	⊢ ( 𝑢 = 𝐴 → ∪ 𝑢 = ∪ 𝐴 )
17	16	sseq1d	⊢ ( 𝑢 = 𝐴 → ( ∪ 𝑢 ⊆ 𝑤 ↔ ∪ 𝐴 ⊆ 𝑤 ) )
18	15 17	anbi12d	⊢ ( 𝑢 = 𝐴 → ( ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ↔ ( 𝑖 ∈ 𝐴 ∧ ∪ 𝐴 ⊆ 𝑤 ) ) )
19	18	rexsng	⊢ ( 𝐴 ∈ 𝑈 → ( ∃ 𝑢 ∈ { 𝐴 } ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ↔ ( 𝑖 ∈ 𝐴 ∧ ∪ 𝐴 ⊆ 𝑤 ) ) )
20	3 19	syl	⊢ ( 𝜑 → ( ∃ 𝑢 ∈ { 𝐴 } ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ↔ ( 𝑖 ∈ 𝐴 ∧ ∪ 𝐴 ⊆ 𝑤 ) ) )
21	14 20	imbi12d	⊢ ( 𝜑 → ( ( ∃ 𝑣 ∈ { 𝐴 } 𝑖 ∈ 𝑣 → ∃ 𝑢 ∈ { 𝐴 } ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ↔ ( 𝑖 ∈ 𝐴 → ( 𝑖 ∈ 𝐴 ∧ ∪ 𝐴 ⊆ 𝑤 ) ) ) )
22		anclb	⊢ ( ( 𝑖 ∈ 𝐴 → ∪ 𝐴 ⊆ 𝑤 ) ↔ ( 𝑖 ∈ 𝐴 → ( 𝑖 ∈ 𝐴 ∧ ∪ 𝐴 ⊆ 𝑤 ) ) )
23	21 22	bitr4di	⊢ ( 𝜑 → ( ( ∃ 𝑣 ∈ { 𝐴 } 𝑖 ∈ 𝑣 → ∃ 𝑢 ∈ { 𝐴 } ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ↔ ( 𝑖 ∈ 𝐴 → ∪ 𝐴 ⊆ 𝑤 ) ) )
24	23	imbi2d	⊢ ( 𝜑 → ( ( 𝑖 ∈ 𝐴 → ( ∃ 𝑣 ∈ { 𝐴 } 𝑖 ∈ 𝑣 → ∃ 𝑢 ∈ { 𝐴 } ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ↔ ( 𝑖 ∈ 𝐴 → ( 𝑖 ∈ 𝐴 → ∪ 𝐴 ⊆ 𝑤 ) ) ) )
25		pm5.4	⊢ ( ( 𝑖 ∈ 𝐴 → ( 𝑖 ∈ 𝐴 → ∪ 𝐴 ⊆ 𝑤 ) ) ↔ ( 𝑖 ∈ 𝐴 → ∪ 𝐴 ⊆ 𝑤 ) )
26	24 25	bitrdi	⊢ ( 𝜑 → ( ( 𝑖 ∈ 𝐴 → ( ∃ 𝑣 ∈ { 𝐴 } 𝑖 ∈ 𝑣 → ∃ 𝑢 ∈ { 𝐴 } ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ↔ ( 𝑖 ∈ 𝐴 → ∪ 𝐴 ⊆ 𝑤 ) ) )
27	26	ralbidv2	⊢ ( 𝜑 → ( ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ { 𝐴 } 𝑖 ∈ 𝑣 → ∃ 𝑢 ∈ { 𝐴 } ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ↔ ∀ 𝑖 ∈ 𝐴 ∪ 𝐴 ⊆ 𝑤 ) )
28	27	adantr	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑈 ∧ ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ { 𝐴 } 𝑖 ∈ 𝑣 → ∃ 𝑢 ∈ { 𝐴 } ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) → ( ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ { 𝐴 } 𝑖 ∈ 𝑣 → ∃ 𝑢 ∈ { 𝐴 } ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ↔ ∀ 𝑖 ∈ 𝐴 ∪ 𝐴 ⊆ 𝑤 ) )
29	11 28	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑈 ∧ ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ { 𝐴 } 𝑖 ∈ 𝑣 → ∃ 𝑢 ∈ { 𝐴 } ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) → ∀ 𝑖 ∈ 𝐴 ∪ 𝐴 ⊆ 𝑤 )
30		sstr2	⊢ ( 𝑖 ⊆ ∪ 𝐴 → ( ∪ 𝐴 ⊆ 𝑤 → 𝑖 ⊆ 𝑤 ) )
31	30	ral2imi	⊢ ( ∀ 𝑖 ∈ 𝐴 𝑖 ⊆ ∪ 𝐴 → ( ∀ 𝑖 ∈ 𝐴 ∪ 𝐴 ⊆ 𝑤 → ∀ 𝑖 ∈ 𝐴 𝑖 ⊆ 𝑤 ) )
32	10 29 31	mpsyl	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑈 ∧ ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ { 𝐴 } 𝑖 ∈ 𝑣 → ∃ 𝑢 ∈ { 𝐴 } ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) → ∀ 𝑖 ∈ 𝐴 𝑖 ⊆ 𝑤 )
33		unissb	⊢ ( ∪ 𝐴 ⊆ 𝑤 ↔ ∀ 𝑖 ∈ 𝐴 𝑖 ⊆ 𝑤 )
34	32 33	sylibr	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑈 ∧ ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ { 𝐴 } 𝑖 ∈ 𝑣 → ∃ 𝑢 ∈ { 𝐴 } ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) → ∪ 𝐴 ⊆ 𝑤 )
35	6 8 34	rspcedvd	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑈 ∧ ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ { 𝐴 } 𝑖 ∈ 𝑣 → ∃ 𝑢 ∈ { 𝐴 } ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) → ∃ 𝑎 ∈ 𝑈 ∪ 𝐴 ⊆ 𝑎 )
36	5 35	rexlimddv	⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝑈 ∪ 𝐴 ⊆ 𝑎 )
37	1 2 36	mnuss2d	⊢ ( 𝜑 → ∪ 𝐴 ∈ 𝑈 )