Theorem mnupwd

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

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

Proof

Step	Hyp	Ref	Expression
1		mnupwd.1	⊢ 𝑀 = { 𝑘 ∣ ∀ 𝑙 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑘 ∧ ∀ 𝑚 ∃ 𝑛 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ) }
2		mnupwd.2	⊢ ( 𝜑 → 𝑈 ∈ 𝑀 )
3		mnupwd.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
4		0ex	⊢ ∅ ∈ V
5	4	a1i	⊢ ( 𝜑 → ∅ ∈ V )
6	1 2 3 5	mnuop23d	⊢ ( 𝜑 → ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝐴 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ ∅ ) → ∃ 𝑢 ∈ ∅ ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) )
7		simpl	⊢ ( ( 𝒫 𝐴 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ ∅ ) → ∃ 𝑢 ∈ ∅ ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) → 𝒫 𝐴 ⊆ 𝑤 )
8	7	reximi	⊢ ( ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝐴 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ ∅ ) → ∃ 𝑢 ∈ ∅ ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) → ∃ 𝑤 ∈ 𝑈 𝒫 𝐴 ⊆ 𝑤 )
9	6 8	syl	⊢ ( 𝜑 → ∃ 𝑤 ∈ 𝑈 𝒫 𝐴 ⊆ 𝑤 )
10	1 2 9	mnuss2d	⊢ ( 𝜑 → 𝒫 𝐴 ∈ 𝑈 )