Let X, Tx, Y, Ty, f and A be given.
Assume Hcont: continuous_map X Tx Y Ty f.
Assume HG: Gdelta_in Y Ty A.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (continuous_map_topology_dom X Tx Y Ty f Hcont).
We prove the intermediate claim HTy: topology_on Y Ty.
An exact proof term for the current goal is (continuous_map_topology_cod X Tx Y Ty f Hcont).
Apply HG to the current goal.
Let Fam be given.
Assume HGpack.
We prove the intermediate claim Hcore: countable_set Fam ∧ ∀U ∈ Fam, open_in Y Ty U.
An exact proof term for the current goal is (andEL (countable_set Fam ∧ ∀U ∈ Fam, open_in Y Ty U) (intersection_over_family Y Fam = A) HGpack).
We prove the intermediate claim HIntEq: intersection_over_family Y Fam = A.
An exact proof term for the current goal is (andER (countable_set Fam ∧ ∀U ∈ Fam, open_in Y Ty U) (intersection_over_family Y Fam = A) HGpack).
We prove the intermediate claim HcountFam: countable_set Fam.
An exact proof term for the current goal is (andEL (countable_set Fam) (∀U ∈ Fam, open_in Y Ty U) Hcore).
We prove the intermediate claim HopFam: ∀U ∈ Fam, open_in Y Ty U.
An exact proof term for the current goal is (andER (countable_set Fam) (∀U ∈ Fam, open_in Y Ty U) Hcore).
Set Fam' to be the term {preimage_of X f U|U ∈ Fam}.
We will prove ∃Fam0 : set, countable_set Fam0 ∧ (∀V ∈ Fam0, open_in X Tx V) ∧ intersection_over_family X Fam0 = preimage_of X f A.
We use Fam' to witness the existential quantifier.
We will prove countable_set Fam' ∧ (∀V ∈ Fam', open_in X Tx V) ∧ intersection_over_family X Fam' = preimage_of X f A.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (countable_image Fam HcountFam (λU : set ⇒ preimage_of X f U)).
Let V be given.
Assume HV: V ∈ Fam'.
We will prove open_in X Tx V.
Apply (ReplE_impred Fam (λU : set ⇒ preimage_of X f U) V HV (open_in X Tx V)) to the current goal.
Let U be given.
Assume HU: U ∈ Fam.
Assume HVe: V = preimage_of X f U.
rewrite the current goal using HVe (from left to right).
We prove the intermediate claim HUopen: open_in Y Ty U.
An exact proof term for the current goal is (HopFam U HU).
We prove the intermediate claim HUinTy: U ∈ Ty.
An exact proof term for the current goal is (andER (topology_on Y Ty) (U ∈ Ty) HUopen).
We will prove open_in X Tx (preimage_of X f U).
We will prove topology_on X Tx ∧ preimage_of X f U ∈ Tx.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
An exact proof term for the current goal is (andER ((topology_on X Tx ∧ topology_on Y Ty) ∧ function_on f X Y) (∀V0 : set, V0 ∈ Ty → preimage_of X f V0 ∈ Tx) Hcont U HUinTy).
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ intersection_over_family X Fam'.
We will prove x ∈ preimage_of X f A.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ ∀U0 : set, U0 ∈ Fam' → x0 ∈ U0) x Hx).
We prove the intermediate claim HxAll: ∀V : set, V ∈ Fam' → x ∈ V.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∀U0 : set, U0 ∈ Fam' → x0 ∈ U0) x Hx).
We prove the intermediate claim HpreDef: preimage_of X f A = {x0 ∈ X|apply_fun f x0 ∈ A}.
Use reflexivity.
rewrite the current goal using HpreDef (from left to right).
Apply (SepI X (λx0 : set ⇒ apply_fun f x0 ∈ A) x HxX) to the current goal.
We will prove apply_fun f x ∈ A.
rewrite the current goal using HIntEq (from right to left).
We prove the intermediate claim HfXY: function_on f X Y.
An exact proof term for the current goal is (continuous_map_function_on X Tx Y Ty f Hcont).
We prove the intermediate claim HIntYDef: intersection_over_family Y Fam = {y0 ∈ Y|∀U0 : set, U0 ∈ Fam → y0 ∈ U0}.
Use reflexivity.
rewrite the current goal using HIntYDef (from left to right).
Apply (SepI Y (λy0 : set ⇒ ∀U0 : set, U0 ∈ Fam → y0 ∈ U0) (apply_fun f x) (HfXY x HxX)) to the current goal.
Let U0 be given.
Assume HU0: U0 ∈ Fam.
We will prove apply_fun f x ∈ U0.
We prove the intermediate claim HVinFam': preimage_of X f U0 ∈ Fam'.
An exact proof term for the current goal is (ReplI Fam (λU : set ⇒ preimage_of X f U) U0 HU0).
We prove the intermediate claim HxPre: x ∈ preimage_of X f U0.
An exact proof term for the current goal is (HxAll (preimage_of X f U0) HVinFam').
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun f x0 ∈ U0) x HxPre).
Let x be given.
Assume Hx: x ∈ preimage_of X f A.
We will prove x ∈ intersection_over_family X Fam'.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun f x0 ∈ A) x Hx).
We prove the intermediate claim HIntXDef: intersection_over_family X Fam' = {x0 ∈ X|∀V0 : set, V0 ∈ Fam' → x0 ∈ V0}.
Use reflexivity.
rewrite the current goal using HIntXDef (from left to right).
Apply (SepI X (λx0 : set ⇒ ∀V0 : set, V0 ∈ Fam' → x0 ∈ V0) x HxX) to the current goal.
Let V0 be given.
Assume HV0: V0 ∈ Fam'.
Apply (ReplE_impred Fam (λU : set ⇒ preimage_of X f U) V0 HV0 (x ∈ V0)) to the current goal.
Let U0 be given.
Assume HU0: U0 ∈ Fam.
Assume HV0eq: V0 = preimage_of X f U0.
rewrite the current goal using HV0eq (from left to right).
We will prove x ∈ preimage_of X f U0.
We prove the intermediate claim HpreU0Def: preimage_of X f U0 = {x0 ∈ X|apply_fun f x0 ∈ U0}.
Use reflexivity.
rewrite the current goal using HpreU0Def (from left to right).
Apply (SepI X (λx0 : set ⇒ apply_fun f x0 ∈ U0) x HxX) to the current goal.
We prove the intermediate claim HfxA: apply_fun f x ∈ A.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun f x0 ∈ A) x Hx).
We prove the intermediate claim HfxInt: apply_fun f x ∈ intersection_over_family Y Fam.
rewrite the current goal using HIntEq (from left to right).
An exact proof term for the current goal is HfxA.
We prove the intermediate claim HfxAll: ∀U1 : set, U1 ∈ Fam → apply_fun f x ∈ U1.
An exact proof term for the current goal is (SepE2 Y (λy0 : set ⇒ ∀U1 : set, U1 ∈ Fam → y0 ∈ U1) (apply_fun f x) HfxInt).
An exact proof term for the current goal is (HfxAll U0 HU0).
∎