Metamath Proof Explorer


Theorem mnuprssd

Description: A minimal universe contains pairs of subsets of an element of the universe. (Contributed by Rohan Ridenour, 13-Aug-2023)

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

Proof

Step Hyp Ref Expression
1 mnuprssd.1 𝑀 = { 𝑘 ∣ ∀ 𝑙𝑘 ( 𝒫 𝑙𝑘 ∧ ∀ 𝑚𝑛𝑘 ( 𝒫 𝑙𝑛 ∧ ∀ 𝑝𝑙 ( ∃ 𝑞𝑘 ( 𝑝𝑞𝑞𝑚 ) → ∃ 𝑟𝑚 ( 𝑝𝑟 𝑟𝑛 ) ) ) ) }
2 mnuprssd.2 ( 𝜑𝑈𝑀 )
3 mnuprssd.3 ( 𝜑𝐶𝑈 )
4 mnuprssd.4 ( 𝜑𝐴𝐶 )
5 mnuprssd.5 ( 𝜑𝐵𝐶 )
6 1 2 3 mnupwd ( 𝜑 → 𝒫 𝐶𝑈 )
7 3 4 sselpwd ( 𝜑𝐴 ∈ 𝒫 𝐶 )
8 3 5 sselpwd ( 𝜑𝐵 ∈ 𝒫 𝐶 )
9 7 8 prssd ( 𝜑 → { 𝐴 , 𝐵 } ⊆ 𝒫 𝐶 )
10 1 2 6 9 mnussd ( 𝜑 → { 𝐴 , 𝐵 } ∈ 𝑈 )