Metamath Proof Explorer


Theorem mnussd

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

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

Proof

Step Hyp Ref Expression
1 mnussd.1 𝑀 = { 𝑘 ∣ ∀ 𝑙𝑘 ( 𝒫 𝑙𝑘 ∧ ∀ 𝑚𝑛𝑘 ( 𝒫 𝑙𝑛 ∧ ∀ 𝑝𝑙 ( ∃ 𝑞𝑘 ( 𝑝𝑞𝑞𝑚 ) → ∃ 𝑟𝑚 ( 𝑝𝑟 𝑟𝑛 ) ) ) ) }
2 mnussd.2 ( 𝜑𝑈𝑀 )
3 mnussd.3 ( 𝜑𝐴𝑈 )
4 mnussd.4 ( 𝜑𝐵𝐴 )
5 1 2 3 mnuop123d ( 𝜑 → ( 𝒫 𝐴𝑈 ∧ ∀ 𝑓𝑤𝑈 ( 𝒫 𝐴𝑤 ∧ ∀ 𝑖𝐴 ( ∃ 𝑣𝑈 ( 𝑖𝑣𝑣𝑓 ) → ∃ 𝑢𝑓 ( 𝑖𝑢 𝑢𝑤 ) ) ) ) )
6 5 simpld ( 𝜑 → 𝒫 𝐴𝑈 )
7 3 4 sselpwd ( 𝜑𝐵 ∈ 𝒫 𝐴 )
8 6 7 sseldd ( 𝜑𝐵𝑈 )