Metamath Proof Explorer


Theorem mnutrcld

Description: Minimal universes contain the elements of their elements. (Contributed by Rohan Ridenour, 13-Aug-2023)

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

Proof

Step Hyp Ref Expression
1 mnutrcld.1 𝑀 = { 𝑘 ∣ ∀ 𝑙𝑘 ( 𝒫 𝑙𝑘 ∧ ∀ 𝑚𝑛𝑘 ( 𝒫 𝑙𝑛 ∧ ∀ 𝑝𝑙 ( ∃ 𝑞𝑘 ( 𝑝𝑞𝑞𝑚 ) → ∃ 𝑟𝑚 ( 𝑝𝑟 𝑟𝑛 ) ) ) ) }
2 mnutrcld.2 ( 𝜑𝑈𝑀 )
3 mnutrcld.3 ( 𝜑𝐴𝑈 )
4 mnutrcld.4 ( 𝜑𝐵𝐴 )
5 1 2 3 mnuunid ( 𝜑 𝐴𝑈 )
6 elssuni ( 𝐵𝐴𝐵 𝐴 )
7 4 6 syl ( 𝜑𝐵 𝐴 )
8 1 2 5 7 mnussd ( 𝜑𝐵𝑈 )