Let X and seq be given.
Assume Hseq: sequence_on seq X.
We will prove net_in_space X (sequence_as_net seq).
Set net0 to be the term sequence_as_net seq.
We will prove ∃J le : set, directed_set J le ∧ total_function_on net0 J X ∧ functional_graph net0 ∧ graph_domain_subset net0 J.
We use ω to witness the existential quantifier.
We use (inclusion_rel ω) to witness the existential quantifier.
We will prove directed_set ω (inclusion_rel ω) ∧ total_function_on net0 ω X ∧ functional_graph net0 ∧ graph_domain_subset net0 ω.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is omega_directed_by_inclusion_rel.
We prove the intermediate claim Hg: ∀n : set, n ∈ ω → apply_fun seq n ∈ X.
Let n be given.
Assume Hn: n ∈ ω.
We prove the intermediate claim Hfun: function_on seq ω X.
An exact proof term for the current goal is Hseq.
An exact proof term for the current goal is (Hfun n Hn).
We prove the intermediate claim Hdef: net0 = graph ω (λn : set ⇒ apply_fun seq n).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (total_function_on_graph ω X (λn : set ⇒ apply_fun seq n) Hg).
We prove the intermediate claim Hdef: net0 = graph ω (λn : set ⇒ apply_fun seq n).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (functional_graph_graph ω (λn : set ⇒ apply_fun seq n)).
We prove the intermediate claim Hdef: net0 = graph ω (λn : set ⇒ apply_fun seq n).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (graph_domain_subset_graph ω (λn : set ⇒ apply_fun seq n)).
∎