Theorem univ_closed_union

Proof
01. 1 ⊢ univ U, hypo.
02. 1 ⊢ ∅ ∈ U, univ_contains_empty_set 1.
03. 1 ⊢ power ∅ ∈ U, univ_closed_power 1 2.
04. 1 ⊢ {∅} ∈ U, eq_subst power_empty_set 3, P u ↔ u ∈ U.
05. 1 ⊢ power {∅} ∈ U, univ_closed_power 1 4.
06. ⊢ power {∅} = {∅, {∅}}, power_sg empty_set_is_set.
07. 1 ⊢ {∅, {∅}} ∈ U, eq_subst 6 5, P u ↔ u ∈ U.
08. 8 ⊢ x ∈ U, hypo.
09. 9 ⊢ y ∈ U, hypo.
10. ⊢ set ∅, empty_set_is_set.
11. ⊢ set {∅}, set_sg 10.
12. 8 ⊢ map {(∅, x)} {∅} U, sg_map 10 8.
13. 9 ⊢ map {({∅}, y)} {{∅}} U, sg_map 11 9.
14. ⊢ {∅} ∩ {{∅}} = ∅,
  disjoint_sg_from_neq 10 11 zero_neq_one.
15. 8, 9 ⊢ map {(∅, x), ({∅}, y)} {∅, {∅}} U,
  map_union_eq_rngs 12 13 14.
16. 1, 8, 9 ⊢ ⋃(img {(∅, x), ({∅}, y)} {∅, {∅}}) ∈ U,
  univ_closed_family_union 1 7 15.
17. 8 ⊢ set x, set_intro 8.
18. 9 ⊢ set y, set_intro 9.
19. 8, 9 ⊢ img {(∅, x), ({∅}, y)} {∅, {∅}} = {x, y}, img_graph2 17 18.
20. 1, 8, 9 ⊢ ⋃{x, y} ∈ U, eq_subst 19 16, P t ↔ ⋃t ∈ U.
21. 8, 9 ⊢ set x ∧ set y, conj_intro 17 18.
22. 8, 9 ⊢ ⋃{x, y} = x ∪ y, Union_pair_set 21.
23. 1, 8, 9 ⊢ x ∪ y ∈ U, eq_subst 22 20, P t ↔ t ∈ U.
univ_closed_union. ⊢ univ U → x ∈ U → y ∈ U → x ∪ y ∈ U,
  subj_intro_iii 23.

Dependencies
The given proof depends on 10 axioms:
comp, efq, eq_refl, eq_subst, ext, infinity, lem, pairing, subset, union.