Theorem gruun

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

	Ref	Expression
Assertion	gruun	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → ( 𝐴 ∪ 𝐵 ) ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		uniprg	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) )
2	1	3adant1	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) )
3		uniiun	⊢ ∪ { 𝐴 , 𝐵 } = ∪ 𝑥 ∈ { 𝐴 , 𝐵 } 𝑥
4	2 3	eqtr3di	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → ( 𝐴 ∪ 𝐵 ) = ∪ 𝑥 ∈ { 𝐴 , 𝐵 } 𝑥 )
5		simp1	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → 𝑈 ∈ Univ )
6		grupr	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → { 𝐴 , 𝐵 } ∈ 𝑈 )
7		vex	⊢ 𝑥 ∈ V
8	7	elpr	⊢ ( 𝑥 ∈ { 𝐴 , 𝐵 } ↔ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) )
9		eleq1a	⊢ ( 𝐴 ∈ 𝑈 → ( 𝑥 = 𝐴 → 𝑥 ∈ 𝑈 ) )
10		eleq1a	⊢ ( 𝐵 ∈ 𝑈 → ( 𝑥 = 𝐵 → 𝑥 ∈ 𝑈 ) )
11	9 10	jaao	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → 𝑥 ∈ 𝑈 ) )
12	8 11	syl5bi	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → ( 𝑥 ∈ { 𝐴 , 𝐵 } → 𝑥 ∈ 𝑈 ) )
13	12	ralrimiv	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → ∀ 𝑥 ∈ { 𝐴 , 𝐵 } 𝑥 ∈ 𝑈 )
14	13	3adant1	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → ∀ 𝑥 ∈ { 𝐴 , 𝐵 } 𝑥 ∈ 𝑈 )
15		gruiun	⊢ ( ( 𝑈 ∈ Univ ∧ { 𝐴 , 𝐵 } ∈ 𝑈 ∧ ∀ 𝑥 ∈ { 𝐴 , 𝐵 } 𝑥 ∈ 𝑈 ) → ∪ 𝑥 ∈ { 𝐴 , 𝐵 } 𝑥 ∈ 𝑈 )
16	5 6 14 15	syl3anc	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → ∪ 𝑥 ∈ { 𝐴 , 𝐵 } 𝑥 ∈ 𝑈 )
17	4 16	eqeltrd	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → ( 𝐴 ∪ 𝐵 ) ∈ 𝑈 )