Theorem mnuund

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

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

Proof

Step	Hyp	Ref	Expression
1		mnuund.1	⊢ 𝑀 = { 𝑘 ∣ ∀ 𝑙 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑘 ∧ ∀ 𝑚 ∃ 𝑛 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ) }
2		mnuund.2	⊢ ( 𝜑 → 𝑈 ∈ 𝑀 )
3		mnuund.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
4		mnuund.4	⊢ ( 𝜑 → 𝐵 ∈ 𝑈 )
5		uniprg	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) )
6	3 4 5	syl2anc	⊢ ( 𝜑 → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) )
7	1 2 3 4	mnuprd	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ∈ 𝑈 )
8	1 2 7	mnuunid	⊢ ( 𝜑 → ∪ { 𝐴 , 𝐵 } ∈ 𝑈 )
9	6 8	eqeltrrd	⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) ∈ 𝑈 )