Theorem Union_is_supremum

Together with Union_is_upper_bound it states that ⋃M is the supremum of M with respect to the inclusion order. See Intersection_is_infimum for the dual statement.

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

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