Theorem wunpr

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

	Ref	Expression
Hypotheses	wununi.1	$$⊢\phi \to U\in \mathrm{WUni}$$
	wununi.2	$$⊢\phi \to A\in U$$
	wunpr.3	$$⊢\phi \to B\in U$$
Assertion	wunpr	$$⊢\phi \to \left\{A,B\right\}\in U$$

Proof

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