Metamath Proof Explorer


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 )