Theorem gruop

Description: A Grothendieck universe contains ordered pairs of its elements. (Contributed by Mario Carneiro, 10-Jun-2013)

	Ref	Expression
Assertion	gruop	|- ( ( U e. Univ /\ A e. U /\ B e. U ) -> <. A , B >. e. U )

Proof

Step	Hyp	Ref	Expression
1		dfopg	|- ( ( A e. U /\ B e. U ) -> <. A , B >. = { { A } , { A , B } } )
2	1	3adant1	|- ( ( U e. Univ /\ A e. U /\ B e. U ) -> <. A , B >. = { { A } , { A , B } } )
3		simp1	|- ( ( U e. Univ /\ A e. U /\ B e. U ) -> U e. Univ )
4		grusn	|- ( ( U e. Univ /\ A e. U ) -> { A } e. U )
5	4	3adant3	|- ( ( U e. Univ /\ A e. U /\ B e. U ) -> { A } e. U )
6		grupr	|- ( ( U e. Univ /\ A e. U /\ B e. U ) -> { A , B } e. U )
7		grupr	|- ( ( U e. Univ /\ { A } e. U /\ { A , B } e. U ) -> { { A } , { A , B } } e. U )
8	3 5 6 7	syl3anc	|- ( ( U e. Univ /\ A e. U /\ B e. U ) -> { { A } , { A , B } } e. U )
9	2 8	eqeltrd	|- ( ( U e. Univ /\ A e. U /\ B e. U ) -> <. A , B >. e. U )