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 uniprg ⊢A∈U∧B∈U→⋃AB=A∪B
2 1 3adant1 ⊢U∈Univ∧A∈U∧B∈U→⋃AB=A∪B
3 uniiun ⊢⋃AB=⋃x∈ABx
4 2 3 eqtr3di ⊢U∈Univ∧A∈U∧B∈U→A∪B=⋃x∈ABx
5 simp1 ⊢U∈Univ∧A∈U∧B∈U→U∈Univ
6 grupr ⊢U∈Univ∧A∈U∧B∈U→AB∈U
7 vex ⊢x∈V
8 7 elpr ⊢x∈AB↔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 biimtrid ⊢A∈U∧B∈U→x∈AB→x∈U
13 12 ralrimiv ⊢A∈U∧B∈U→∀x∈ABx∈U
14 13 3adant1 ⊢U∈Univ∧A∈U∧B∈U→∀x∈ABx∈U
15 gruiun ⊢U∈Univ∧AB∈U∧∀x∈ABx∈U→⋃x∈ABx∈U
16 5 6 14 15 syl3anc ⊢U∈Univ∧A∈U∧B∈U→⋃x∈ABx∈U
17 4 16 eqeltrd ⊢U∈Univ∧A∈U∧B∈U→A∪B∈U