This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )