Theorem mnuprd

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

	Ref	Expression
Hypotheses	mnuprd.1	|- M = { k | A. l e. k ( ~P l C_ k /\ A. m E. n e. k ( ~P l C_ n /\ A. p e. l ( E. q e. k ( p e. q /\ q e. m ) -> E. r e. m ( p e. r /\ U. r C_ n ) ) ) ) }
	mnuprd.2	|- ( ph -> U e. M )
	mnuprd.3	|- ( ph -> A e. U )
	mnuprd.4	|- ( ph -> B e. U )
Assertion	mnuprd	|- ( ph -> { A , B } e. U )

Proof

Step	Hyp	Ref	Expression
1		mnuprd.1	|- M = { k | A. l e. k ( ~P l C_ k /\ A. m E. n e. k ( ~P l C_ n /\ A. p e. l ( E. q e. k ( p e. q /\ q e. m ) -> E. r e. m ( p e. r /\ U. r C_ n ) ) ) ) }
2		mnuprd.2	|- ( ph -> U e. M )
3		mnuprd.3	|- ( ph -> A e. U )
4		mnuprd.4	|- ( ph -> B e. U )
5	2	adantr	|- ( ( ph /\ A = (/) ) -> U e. M )
6	4	adantr	|- ( ( ph /\ A = (/) ) -> B e. U )
7		simpr	|- ( ( ph /\ A = (/) ) -> A = (/) )
8		0ss	|- (/) C_ B
9	7 8	eqsstrdi	|- ( ( ph /\ A = (/) ) -> A C_ B )
10		ssidd	|- ( ( ph /\ A = (/) ) -> B C_ B )
11	1 5 6 9 10	mnuprssd	|- ( ( ph /\ A = (/) ) -> { A , B } e. U )
12		eqid	|- { { (/) , { A } } , { { (/) } , { B } } } = { { (/) , { A } } , { { (/) } , { B } } }
13	2	adantr	|- ( ( ph /\ -. A = (/) ) -> U e. M )
14	3	adantr	|- ( ( ph /\ -. A = (/) ) -> A e. U )
15	4	adantr	|- ( ( ph /\ -. A = (/) ) -> B e. U )
16		simpr	|- ( ( ph /\ -. A = (/) ) -> -. A = (/) )
17	1 12 13 14 15 16	mnuprdlem4	|- ( ( ph /\ -. A = (/) ) -> { A , B } e. U )
18	11 17	pm2.61dan	|- ( ph -> { A , B } e. U )