Theorem gruun

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

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

Proof

Step	Hyp	Ref	Expression
1		uniprg	|- ( ( A e. U /\ B e. U ) -> U. { A , B } = ( A u. B ) )
2	1	3adant1	|- ( ( U e. Univ /\ A e. U /\ B e. U ) -> U. { A , B } = ( A u. B ) )
3		uniiun	|- U. { A , B } = U_ x e. { A , B } x
4	2 3	eqtr3di	|- ( ( U e. Univ /\ A e. U /\ B e. U ) -> ( A u. B ) = U_ x e. { A , B } x )
5		simp1	|- ( ( U e. Univ /\ A e. U /\ B e. U ) -> U e. Univ )
6		grupr	|- ( ( U e. Univ /\ A e. U /\ B e. U ) -> { A , B } e. U )
7		vex	|- x e. _V
8	7	elpr	|- ( x e. { A , B } <-> ( x = A \/ x = B ) )
9		eleq1a	|- ( A e. U -> ( x = A -> x e. U ) )
10		eleq1a	|- ( B e. U -> ( x = B -> x e. U ) )
11	9 10	jaao	|- ( ( A e. U /\ B e. U ) -> ( ( x = A \/ x = B ) -> x e. U ) )
12	8 11	syl5bi	|- ( ( A e. U /\ B e. U ) -> ( x e. { A , B } -> x e. U ) )
13	12	ralrimiv	|- ( ( A e. U /\ B e. U ) -> A. x e. { A , B } x e. U )
14	13	3adant1	|- ( ( U e. Univ /\ A e. U /\ B e. U ) -> A. x e. { A , B } x e. U )
15		gruiun	|- ( ( U e. Univ /\ { A , B } e. U /\ A. x e. { A , B } x e. U ) -> U_ x e. { A , B } x e. U )
16	5 6 14 15	syl3anc	|- ( ( U e. Univ /\ A e. U /\ B e. U ) -> U_ x e. { A , B } x e. U )
17	4 16	eqeltrd	|- ( ( U e. Univ /\ A e. U /\ B e. U ) -> ( A u. B ) e. U )