Theorem transitive_closed_Union

Proof
01. 1 ⊢ ∀x. x ∈ M → transitive x, hypo.
02. 2 ⊢ u ∈ ⋃M, hypo.
03. 2 ⊢ ∃x. x ∈ M ∧ u ∈ x, Union_elim 2.
04. 4 ⊢ x ∈ M ∧ u ∈ x, hypo.
05. 4 ⊢ x ∈ M, conj_eliml 4.
06. 4 ⊢ u ∈ x, conj_elimr 4.
07. 1, 4 ⊢ transitive x, uq_bounded_elim 1 5.
08. 1, 4 ⊢ u ⊆ x, transitive_elim 7 6.
09. 9 ⊢ y ∈ u, hypo.
10. 1, 4, 9 ⊢ y ∈ x, incl_elim 8 9.
11. 1, 4, 9 ⊢ y ∈ ⋃M, Union_intro 5 10.
12. 1, 4 ⊢ y ∈ u → y ∈ ⋃M, subj_intro 11.
13. 1, 4 ⊢ ∀y. y ∈ u → y ∈ ⋃M, uq_intro 12.
14. 1, 4 ⊢ u ⊆ ⋃M, incl_intro 13.
15. 1, 2 ⊢ u ⊆ ⋃M, ex_elim 3 14.
16. 1 ⊢ u ∈ ⋃M → u ⊆ ⋃M, subj_intro 15.
17. 1 ⊢ ∀u. u ∈ ⋃M → u ⊆ ⋃M, uq_intro 16.
18. 1 ⊢ transitive (⋃M), transitive_intro 17.
transitive_closed_Union. ⊢ (∀x. x ∈ M → transitive x) →
  transitive (⋃M), subj_intro 18.

Dependencies
The given proof depends on three axioms:
comp, eq_refl, eq_subst.