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	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ∈ 𝑈 )