Theorem wunpr

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

	Ref	Expression
Hypotheses	wununi.1	|- ( ph -> U e. WUni )
	wununi.2	|- ( ph -> A e. U )
	wunpr.3	|- ( ph -> B e. U )
Assertion	wunpr	|- ( ph -> { A , B } e. U )

Proof

Step	Hyp	Ref	Expression
1		wununi.1	|- ( ph -> U e. WUni )
2		wununi.2	|- ( ph -> A e. U )
3		wunpr.3	|- ( ph -> B e. U )
4		iswun	|- ( U e. WUni -> ( U e. WUni <-> ( Tr U /\ U =/= (/) /\ A. x e. U ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) ) ) )
5	4	ibi	|- ( U e. WUni -> ( Tr U /\ U =/= (/) /\ A. x e. U ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) ) )
6	5	simp3d	|- ( U e. WUni -> A. x e. U ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) )
7		simp3	|- ( ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) -> A. y e. U { x , y } e. U )
8	7	ralimi	|- ( A. x e. U ( U. x e. U /\ ~P x e. U /\ A. y e. U { x , y } e. U ) -> A. x e. U A. y e. U { x , y } e. U )
9	1 6 8	3syl	|- ( ph -> A. x e. U A. y e. U { x , y } e. U )
10		preq1	|- ( x = A -> { x , y } = { A , y } )
11	10	eleq1d	|- ( x = A -> ( { x , y } e. U <-> { A , y } e. U ) )
12		preq2	|- ( y = B -> { A , y } = { A , B } )
13	12	eleq1d	|- ( y = B -> ( { A , y } e. U <-> { A , B } e. U ) )
14	11 13	rspc2va	|- ( ( ( A e. U /\ B e. U ) /\ A. x e. U A. y e. U { x , y } e. U ) -> { A , B } e. U )
15	2 3 9 14	syl21anc	|- ( ph -> { A , B } e. U )