Let X, Tx and U be given.
Assume H: partition_of_unity_dominated X Tx U.
Apply (partition_of_unity_dominated_ex_family_pred X Tx U H) to the current goal.
Let P be given.
Assume HP: partition_of_unity_family X Tx U P.
We use P to witness the existential quantifier.
We prove the intermediate claim HA: P ⊆ function_space X R.
An exact proof term for the current goal is (partition_of_unity_family_sub_function_space X Tx U P HP).
We prove the intermediate claim HB: ∀f : set, f ∈ P → continuous_map X Tx R R_standard_topology f.
An exact proof term for the current goal is (partition_of_unity_family_continuous X Tx U P HP).
We prove the intermediate claim HC: ∀f x : set, f ∈ P → x ∈ X → apply_fun f x ∈ unit_interval.
An exact proof term for the current goal is (partition_of_unity_family_unit_interval X Tx U P HP).
We prove the intermediate claim HD: ∀f : set, f ∈ P → ∃u : set, u ∈ U ∧ support_of X Tx f ⊆ u.
An exact proof term for the current goal is (partition_of_unity_family_support_dominated X Tx U P HP).
We prove the intermediate claim HE: ∀x : set, x ∈ X → ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃F0 : set, finite F0 ∧ F0 ⊆ P ∧ ∀f : set, f ∈ P → support_of X Tx f ∩ N ≠ Empty → f ∈ F0.
An exact proof term for the current goal is (partition_of_unity_family_supports_locally_finite X Tx U P HP).
We will prove P ⊆ function_space X R ∧ (∀f : set, f ∈ P → continuous_map X Tx R R_standard_topology f) ∧ (∀f x : set, f ∈ P → x ∈ X → apply_fun f x ∈ unit_interval) ∧ (∀f : set, f ∈ P → ∃u : set, u ∈ U ∧ support_of X Tx f ⊆ u) ∧ (∀x : set, x ∈ X → ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃F0 : set, finite F0 ∧ F0 ⊆ P ∧ ∀f : set, f ∈ P → support_of X Tx f ∩ N ≠ Empty → f ∈ F0).
Apply andI to the current goal.
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 HA.
An exact proof term for the current goal is HB.
An exact proof term for the current goal is HC.
An exact proof term for the current goal is HD.
An exact proof term for the current goal is HE.
∎