Metamath Proof Explorer

Theorem gruun

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

Ref Expression
Assertion gruun ⊢ U ∈ Univ ∧ A ∈ U ∧ B ∈ U → A ∪ B ∈ U

Proof

Step Hyp Ref Expression
1 uniiun ⊢ ⋃ A B = ⋃ x ∈ A B x
2 uniprg ⊢ A ∈ U ∧ B ∈ U → ⋃ A B = A ∪ B
3 2 3adant1 ⊢ U ∈ Univ ∧ A ∈ U ∧ B ∈ U → ⋃ A B = A ∪ B
4 1 3 syl5reqr ⊢ U ∈ Univ ∧ A ∈ U ∧ B ∈ U → A ∪ B = ⋃ x ∈ A B x
5 simp1 ⊢ U ∈ Univ ∧ A ∈ U ∧ B ∈ U → U ∈ Univ
6 grupr ⊢ U ∈ Univ ∧ A ∈ U ∧ B ∈ U → A B ∈ U
7 vex ⊢ x ∈ V
8 7 elpr ⊢ x ∈ A B ↔ x = A ∨ x = B
9 eleq1a ⊢ A ∈ U → x = A → x ∈ U
10 eleq1a ⊢ B ∈ U → x = B → x ∈ U
11 9 10 jaao ⊢ A ∈ U ∧ B ∈ U → x = A ∨ x = B → x ∈ U
12 8 11 syl5bi ⊢ A ∈ U ∧ B ∈ U → x ∈ A B → x ∈ U
13 12 ralrimiv ⊢ A ∈ U ∧ B ∈ U → ∀ x ∈ A B x ∈ U
14 13 3adant1 ⊢ U ∈ Univ ∧ A ∈ U ∧ B ∈ U → ∀ x ∈ A B x ∈ U
15 gruiun ⊢ U ∈ Univ ∧ A B ∈ U ∧ ∀ x ∈ A B x ∈ U → ⋃ x ∈ A B x ∈ U
16 5 6 14 15 syl3anc ⊢ U ∈ Univ ∧ A ∈ U ∧ B ∈ U → ⋃ x ∈ A B x ∈ U
17 4 16 eqeltrd ⊢ U ∈ Univ ∧ A ∈ U ∧ B ∈ U → A ∪ B ∈ U