wunpr

Description: A weak universe is closed under pairing. (Contributed by Mario Carneiro, 2-Jan-2017)

Step	Hyp	Ref	Expression
1		wununi.1	$⊢ φ \to U \in WUni$
2		wununi.2	$⊢ φ \to A \in U$
3		wunpr.3	$⊢ φ \to B \in U$
4		iswun	$⊢ U \in WUni \to (U \in WUni \leftrightarrow (Tr U \land U \neq \emptyset \land \forall x \in U (⋃ x \in U \land 𝒫 x \in U \land \forall y \in U \{x, y\} \in U)))$
5	4	ibi	$⊢ U \in WUni \to (Tr U \land U \neq \emptyset \land \forall x \in U (⋃ x \in U \land 𝒫 x \in U \land \forall y \in U \{x, y\} \in U))$
6	5	simp3d	$⊢ U \in WUni \to \forall x \in U (⋃ x \in U \land 𝒫 x \in U \land \forall y \in U \{x, y\} \in U)$
7		simp3	$⊢ (⋃ x \in U \land 𝒫 x \in U \land \forall y \in U \{x, y\} \in U) \to \forall y \in U \{x, y\} \in U$
8	7	ralimi	$⊢ \forall x \in U (⋃ x \in U \land 𝒫 x \in U \land \forall y \in U \{x, y\} \in U) \to \forall x \in U \forall y \in U \{x, y\} \in U$
9	1 6 8	3syl	$⊢ φ \to \forall x \in U \forall y \in U \{x, y\} \in U$
10		preq1	$⊢ x = A \to \{x, y\} = \{A, y\}$
11	10	eleq1d	$⊢ x = A \to (\{x, y\} \in U \leftrightarrow \{A, y\} \in U)$
12		preq2	$⊢ y = B \to \{A, y\} = \{A, B\}$
13	12	eleq1d	$⊢ y = B \to (\{A, y\} \in U \leftrightarrow \{A, B\} \in U)$
14	11 13	rspc2va	$⊢ ((A \in U \land B \in U) \land \forall x \in U \forall y \in U \{x, y\} \in U) \to \{A, B\} \in U$
15	2 3 9 14	syl21anc	$⊢ φ \to \{A, B\} \in U$

Metamath Proof Explorer