clop_idem

Theorem clop_idem

Theorem. clop_idem
closure_operator H U → X ⊆ U → app H (app H X) = app H X

Proof
01. 1 ⊢ closure_operator H U, hypo.
02. 2 ⊢ X ⊆ U, hypo.
03. 1 ⊢ ∀X. X ⊆ U → app H (app H X) ⊆ app H X,
  lsubj_conj_elimr clop_equi 1.
04. 1, 2 ⊢ app H (app H X) ⊆ app H X, uq_bounded_elim 3 2.
05. 1, 2 ⊢ app H X ⊆ U, clop_app_in_cod 1 2.
06. 1, 2 ⊢ app H X ⊆ app H (app H X), clop_extensivity 1 5.
07. 1, 2 ⊢ app H (app H X) = app H X, incl_antisym 4 6.
clop_idem. ⊢ closure_operator H U →
  X ⊆ U → app H (app H X) = app H X, subj_intro_ii 7.

Dependencies
The given proof depends on seven axioms:
comp, efq, eq_refl, eq_subst, ext, lem, subset.