Let J, le, X and net be given.

Assume HdirJ: directed_set J le.

Assume Hnettot: total_function_on net J X.

Assume Hnetdom: graph_domain_subset net J.

We will prove subnet_of net net.

We will prove ∃J0 leJ0 K0 leK0 X0 phi0 : set, directed_set J0 leJ0 ∧ directed_set K0 leK0 ∧ total_function_on net J0 X0 ∧ functional_graph net ∧ total_function_on net K0 X0 ∧ functional_graph net ∧ total_function_on phi0 K0 J0 ∧ functional_graph phi0 ∧ graph_domain_subset net J0 ∧ graph_domain_subset net K0 ∧ graph_domain_subset phi0 K0 ∧ (∀i j : set, i ∈ K0 → j ∈ K0 → (i,j) ∈ leK0 → (apply_fun phi0 i,apply_fun phi0 j) ∈ leJ0) ∧ (∀j : set, j ∈ J0 → ∃k : set, k ∈ K0 ∧ (j,apply_fun phi0 k) ∈ leJ0) ∧ (∀k : set, k ∈ K0 → apply_fun net k = apply_fun net (apply_fun phi0 k)).

We use J to witness the existential quantifier.

We use le to witness the existential quantifier.

We use J to witness the existential quantifier.

We use le to witness the existential quantifier.

We use X to witness the existential quantifier.

We use {(y,y)|y ∈ J} to witness the existential quantifier.

We will prove directed_set J le ∧ directed_set J le ∧ total_function_on net J X ∧ functional_graph net ∧ total_function_on net J X ∧ functional_graph net ∧ total_function_on {(y,y)|y ∈ J} J J ∧ functional_graph {(y,y)|y ∈ J} ∧ graph_domain_subset net J ∧ graph_domain_subset net J ∧ graph_domain_subset {(y,y)|y ∈ J} J ∧ (∀i j : set, i ∈ J → j ∈ J → (i,j) ∈ le → (apply_fun {(y,y)|y ∈ J} i,apply_fun {(y,y)|y ∈ J} j) ∈ le) ∧ (∀j : set, j ∈ J → ∃k : set, k ∈ J ∧ (j,apply_fun {(y,y)|y ∈ J} k) ∈ le) ∧ (∀k : set, k ∈ J → apply_fun net k = apply_fun net (apply_fun {(y,y)|y ∈ J} k)).

We prove the intermediate claim Hrefl: ∀j : set, j ∈ J → (j,j) ∈ le.

An exact proof term for the current goal is (directed_set_refl J le HdirJ).

We prove the intermediate claim Hmono_id: ∀i j : set, i ∈ J → j ∈ J → (i,j) ∈ le → (apply_fun {(y,y)|y ∈ J} i,apply_fun {(y,y)|y ∈ J} j) ∈ le.

Let i and j be given.

Assume HiJ: i ∈ J.

Assume HjJ: j ∈ J.

Assume Hij: (i,j) ∈ le.

rewrite the current goal using (identity_function_apply J i HiJ) (from left to right).

rewrite the current goal using (identity_function_apply J j HjJ) (from left to right).

An exact proof term for the current goal is Hij.

We prove the intermediate claim Hcofinal_id: ∀j : set, j ∈ J → ∃k : set, k ∈ J ∧ (j,apply_fun {(y,y)|y ∈ J} k) ∈ le.

Let j be given.

Assume HjJ: j ∈ J.

We use j to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HjJ.

rewrite the current goal using (identity_function_apply J j HjJ) (from left to right).

An exact proof term for the current goal is (Hrefl j HjJ).

We prove the intermediate claim Hvals_id: ∀k : set, k ∈ J → apply_fun net k = apply_fun net (apply_fun {(y,y)|y ∈ J} k).

Let k be given.

Assume HkJ: k ∈ J.

rewrite the current goal using (identity_function_apply J k HkJ) (from left to right).

Use reflexivity.

Apply and14I to the current goal.

An exact proof term for the current goal is HdirJ.

An exact proof term for the current goal is Hnettot.

An exact proof term for the current goal is Hnetgraph.

An exact proof term for the current goal is Hnettot.

An exact proof term for the current goal is Hnetgraph.

An exact proof term for the current goal is (identity_total_function_on J).

An exact proof term for the current goal is (functional_graph_graph J (λy : set ⇒ y)).

An exact proof term for the current goal is Hnetdom.

An exact proof term for the current goal is (graph_domain_subset_graph J (λy : set ⇒ y)).

An exact proof term for the current goal is Hmono_id.

An exact proof term for the current goal is Hcofinal_id.

An exact proof term for the current goal is Hvals_id.

∎