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 M = k | l k 𝒫 l k m n k 𝒫 l n p l q k p q q m r m p r r n
mnuprssd.2 φ U M
mnuprssd.3 φ C U
mnuprssd.4 φ A C
mnuprssd.5 φ B C
Assertion mnuprssd φ A B U

Proof

Step Hyp Ref Expression
1 mnuprssd.1 M = k | l k 𝒫 l k m n k 𝒫 l n p l q k p q q m r m p r r n
2 mnuprssd.2 φ U M
3 mnuprssd.3 φ C U
4 mnuprssd.4 φ A C
5 mnuprssd.5 φ B C
6 1 2 3 mnupwd φ 𝒫 C U
7 3 4 sselpwd φ A 𝒫 C
8 3 5 sselpwd φ B 𝒫 C
9 7 8 prssd φ A B 𝒫 C
10 1 2 6 9 mnussd φ A B U