Theorem gruxp

Description: A Grothendieck universe contains binary cartesian products of its elements. (Contributed by Mario Carneiro, 9-Jun-2013)

	Ref	Expression
Assertion	gruxp	|- ( ( U e. Univ /\ A e. U /\ B e. U ) -> ( A X. B ) e. U )

Proof

Step	Hyp	Ref	Expression
1		gruun	|- ( ( U e. Univ /\ A e. U /\ B e. U ) -> ( A u. B ) e. U )
2		grupw	|- ( ( U e. Univ /\ ( A u. B ) e. U ) -> ~P ( A u. B ) e. U )
3		grupw	|- ( ( U e. Univ /\ ~P ( A u. B ) e. U ) -> ~P ~P ( A u. B ) e. U )
4		xpsspw	|- ( A X. B ) C_ ~P ~P ( A u. B )
5		gruss	|- ( ( U e. Univ /\ ~P ~P ( A u. B ) e. U /\ ( A X. B ) C_ ~P ~P ( A u. B ) ) -> ( A X. B ) e. U )
6	4 5	mp3an3	|- ( ( U e. Univ /\ ~P ~P ( A u. B ) e. U ) -> ( A X. B ) e. U )
7	3 6	syldan	|- ( ( U e. Univ /\ ~P ( A u. B ) e. U ) -> ( A X. B ) e. U )
8	2 7	syldan	|- ( ( U e. Univ /\ ( A u. B ) e. U ) -> ( A X. B ) e. U )
9	8	3ad2antl1	|- ( ( ( U e. Univ /\ A e. U /\ B e. U ) /\ ( A u. B ) e. U ) -> ( A X. B ) e. U )
10	1 9	mpdan	|- ( ( U e. Univ /\ A e. U /\ B e. U ) -> ( A X. B ) e. U )