mnuprd

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

	Ref	Expression
Hypotheses	mnuprd.1	$⊢ M = \{k \| \forall l \in k (𝒫 l \subseteq k \land \forall m \exists n \in k (𝒫 l \subseteq n \land \forall p \in l (\exists q \in k (p \in q \land q \in m) \to \exists r \in m (p \in r \land ⋃ r \subseteq n))))\}$
	mnuprd.2	$⊢ φ \to U \in M$
	mnuprd.3	$⊢ φ \to A \in U$
	mnuprd.4	$⊢ φ \to B \in U$
Assertion	mnuprd	$⊢ φ \to \{A, B\} \in U$

Step	Hyp	Ref	Expression
1		mnuprd.1	$⊢ M = \{k \| \forall l \in k (𝒫 l \subseteq k \land \forall m \exists n \in k (𝒫 l \subseteq n \land \forall p \in l (\exists q \in k (p \in q \land q \in m) \to \exists r \in m (p \in r \land ⋃ r \subseteq n))))\}$
2		mnuprd.2	$⊢ φ \to U \in M$
3		mnuprd.3	$⊢ φ \to A \in U$
4		mnuprd.4	$⊢ φ \to B \in U$
5	2	adantr	$⊢ (φ \land A = \emptyset) \to U \in M$
6	4	adantr	$⊢ (φ \land A = \emptyset) \to B \in U$
7		simpr	$⊢ (φ \land A = \emptyset) \to A = \emptyset$
8		0ss	$⊢ \emptyset \subseteq B$
9	7 8	eqsstrdi	$⊢ (φ \land A = \emptyset) \to A \subseteq B$
10		ssidd	$⊢ (φ \land A = \emptyset) \to B \subseteq B$
11	1 5 6 9 10	mnuprssd	$⊢ (φ \land A = \emptyset) \to \{A, B\} \in U$
12		eqid	$⊢ \{\{\emptyset, \{A\}\}, \{\{\emptyset\}, \{B\}\}\} = \{\{\emptyset, \{A\}\}, \{\{\emptyset\}, \{B\}\}\}$
13	2	adantr	$⊢ (φ \land \neg A = \emptyset) \to U \in M$
14	3	adantr	$⊢ (φ \land \neg A = \emptyset) \to A \in U$
15	4	adantr	$⊢ (φ \land \neg A = \emptyset) \to B \in U$
16		simpr	$⊢ (φ \land \neg A = \emptyset) \to \neg A = \emptyset$
17	1 12 13 14 15 16	mnuprdlem4	$⊢ (φ \land \neg A = \emptyset) \to \{A, B\} \in U$
18	11 17	pm2.61dan	$⊢ φ \to \{A, B\} \in U$

Metamath Proof Explorer