Metamath Proof Explorer

Theorem grupr

Description: A Grothendieck universe contains pairs derived from its elements. (Contributed by Mario Carneiro, 9-Jun-2013)

Ref Expression
Assertion grupr 
|- ( ( U e. Univ /\ A e. U /\ B e. U ) -> { A , B } e. U )

Proof

Step Hyp Ref Expression
1 elgrug 
 |-  ( U e. Univ -> ( U e. Univ <-> ( Tr U /\ A. x e. U ( ~P x e. U /\ A. y e. U { x , y } e. U /\ A. y e. ( U ^m x ) U. ran y e. U ) ) ) )
2 1 ibi 
 |-  ( U e. Univ -> ( Tr U /\ A. x e. U ( ~P x e. U /\ A. y e. U { x , y } e. U /\ A. y e. ( U ^m x ) U. ran y e. U ) ) )
3 2 simprd 
 |-  ( U e. Univ -> A. x e. U ( ~P x e. U /\ A. y e. U { x , y } e. U /\ A. y e. ( U ^m x ) U. ran y e. U ) )
4 preq2 
 |-  ( y = B -> { x , y } = { x , B } )
5 4 eleq1d 
 |-  ( y = B -> ( { x , y } e. U <-> { x , B } e. U ) )
6 5 rspccv 
 |-  ( A. y e. U { x , y } e. U -> ( B e. U -> { x , B } e. U ) )
7 6 3ad2ant2 
 |-  ( ( ~P x e. U /\ A. y e. U { x , y } e. U /\ A. y e. ( U ^m x ) U. ran y e. U ) -> ( B e. U -> { x , B } e. U ) )
8 7 com12 
 |-  ( B e. U -> ( ( ~P x e. U /\ A. y e. U { x , y } e. U /\ A. y e. ( U ^m x ) U. ran y e. U ) -> { x , B } e. U ) )
9 8 ralimdv 
 |-  ( B e. U -> ( A. x e. U ( ~P x e. U /\ A. y e. U { x , y } e. U /\ A. y e. ( U ^m x ) U. ran y e. U ) -> A. x e. U { x , B } e. U ) )
10 3 9 syl5com 
 |-  ( U e. Univ -> ( B e. U -> A. x e. U { x , B } e. U ) )
11 preq1 
 |-  ( x = A -> { x , B } = { A , B } )
12 11 eleq1d 
 |-  ( x = A -> ( { x , B } e. U <-> { A , B } e. U ) )
13 12 rspccv 
 |-  ( A. x e. U { x , B } e. U -> ( A e. U -> { A , B } e. U ) )
14 10 13 syl6 
 |-  ( U e. Univ -> ( B e. U -> ( A e. U -> { A , B } e. U ) ) )
15 14 com23 
 |-  ( U e. Univ -> ( A e. U -> ( B e. U -> { A , B } e. U ) ) )
16 15 3imp 
 |-  ( ( U e. Univ /\ A e. U /\ B e. U ) -> { A , B } e. U )