Theorem mnuprd

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

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

Proof

Step	Hyp	Ref	Expression
1		mnuprd.1	⊢ 𝑀 = { 𝑘 ∣ ∀ 𝑙 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑘 ∧ ∀ 𝑚 ∃ 𝑛 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ) }
2		mnuprd.2	⊢ ( 𝜑 → 𝑈 ∈ 𝑀 )
3		mnuprd.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
4		mnuprd.4	⊢ ( 𝜑 → 𝐵 ∈ 𝑈 )
5	2	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → 𝑈 ∈ 𝑀 )
6	4	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → 𝐵 ∈ 𝑈 )
7		simpr	⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → 𝐴 = ∅ )
8		0ss	⊢ ∅ ⊆ 𝐵
9	7 8	eqsstrdi	⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → 𝐴 ⊆ 𝐵 )
10		ssidd	⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → 𝐵 ⊆ 𝐵 )
11	1 5 6 9 10	mnuprssd	⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → { 𝐴 , 𝐵 } ∈ 𝑈 )
12		eqid	⊢ { { ∅ , { 𝐴 } } , { { ∅ } , { 𝐵 } } } = { { ∅ , { 𝐴 } } , { { ∅ } , { 𝐵 } } }
13	2	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → 𝑈 ∈ 𝑀 )
14	3	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → 𝐴 ∈ 𝑈 )
15	4	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → 𝐵 ∈ 𝑈 )
16		simpr	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → ¬ 𝐴 = ∅ )
17	1 12 13 14 15 16	mnuprdlem4	⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → { 𝐴 , 𝐵 } ∈ 𝑈 )
18	11 17	pm2.61dan	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ∈ 𝑈 )