Let X and Tx be given.
Assume HXconn: connected_space X Tx.
Assume HXnorm: normal_space X Tx.
Assume Hex: ∃x y : set, x ∈ X ∧ y ∈ X ∧ x ≠ y.
We will prove ¬ countable X.
Assume HcountX: countable X.
Apply Hex to the current goal.
Let x0 be given.
Assume Hexy: ∃y : set, x0 ∈ X ∧ y ∈ X ∧ x0 ≠ y.
Apply Hexy to the current goal.
Let y0 be given.
Assume Hxy0.
We prove the intermediate claim Hpair: x0 ∈ X ∧ y0 ∈ X.
An exact proof term for the current goal is (andEL (x0 ∈ X ∧ y0 ∈ X) (x0 ≠ y0) Hxy0).
We prove the intermediate claim Hneq: x0 ≠ y0.
An exact proof term for the current goal is (andER (x0 ∈ X ∧ y0 ∈ X) (x0 ≠ y0) Hxy0).
We prove the intermediate claim Hx0X: x0 ∈ X.
An exact proof term for the current goal is (andEL (x0 ∈ X) (y0 ∈ X) Hpair).
We prove the intermediate claim Hy0X: y0 ∈ X.
An exact proof term for the current goal is (andER (x0 ∈ X) (y0 ∈ X) Hpair).
We prove the intermediate claim Hone: one_point_sets_closed X Tx.
An exact proof term for the current goal is (andEL (one_point_sets_closed X Tx) (∀A B : set, closed_in X Tx A → closed_in X Tx B → A ∩ B = Empty → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty) HXnorm).
We prove the intermediate claim Hsing: ∀z : set, z ∈ X → closed_in X Tx {z}.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀z : set, z ∈ X → closed_in X Tx {z}) Hone).
We prove the intermediate claim Hx0cl: closed_in X Tx {x0}.
An exact proof term for the current goal is (Hsing x0 Hx0X).
We prove the intermediate claim Hy0cl: closed_in X Tx {y0}.
An exact proof term for the current goal is (Hsing y0 Hy0X).
We prove the intermediate claim HsingDisj: {x0} ∩ {y0} = Empty.
Apply set_ext to the current goal.
Let z be given.
Assume Hz: z ∈ {x0} ∩ {y0}.
We will prove z ∈ Empty.
We prove the intermediate claim Hzx: z ∈ {x0}.
An exact proof term for the current goal is (binintersectE1 {x0} {y0} z Hz).
We prove the intermediate claim Hzy: z ∈ {y0}.
An exact proof term for the current goal is (binintersectE2 {x0} {y0} z Hz).
We prove the intermediate claim HzEqx: z = x0.
An exact proof term for the current goal is (SingE x0 z Hzx).
We prove the intermediate claim HzEqy: z = y0.
An exact proof term for the current goal is (SingE y0 z Hzy).
We prove the intermediate claim Hxy: x0 = y0.
rewrite the current goal using HzEqx (from right to left).
rewrite the current goal using HzEqy (from left to right).
Use reflexivity.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hneq Hxy).
An exact proof term for the current goal is (Subq_Empty ({x0} ∩ {y0})).
We prove the intermediate claim H0le1: Rle 0 1.
An exact proof term for the current goal is (Rlt_implies_Rle 0 1 Rlt_0_1).
We prove the intermediate claim Hexf: ∃f : set, continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) f ∧ (∀x : set, x ∈ {x0} → apply_fun f x = 0) ∧ (∀x : set, x ∈ {y0} → apply_fun f x = 1).
An exact proof term for the current goal is (Urysohn_lemma X Tx {x0} {y0} 0 1 H0le1 HXnorm Hx0cl Hy0cl HsingDisj).
Apply Hexf to the current goal.
Let f be given.
Assume Hfpack.
We prove the intermediate claim Hfcore: (continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) f ∧ (∀x : set, x ∈ {x0} → apply_fun f x = 0)).
An exact proof term for the current goal is (andEL (continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) f ∧ (∀x : set, x ∈ {x0} → apply_fun f x = 0)) (∀x : set, x ∈ {y0} → apply_fun f x = 1) Hfpack).
We prove the intermediate claim HfcontI: continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) f.
An exact proof term for the current goal is (andEL (continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) f) (∀x : set, x ∈ {x0} → apply_fun f x = 0) Hfcore).
We prove the intermediate claim Hfx0: apply_fun f x0 = 0.
An exact proof term for the current goal is (andER (continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) f) (∀x : set, x ∈ {x0} → apply_fun f x = 0) Hfcore x0 (SingI x0)).
We prove the intermediate claim Hfy0: ∀x : set, x ∈ {y0} → apply_fun f x = 1.
An exact proof term for the current goal is (andER (continuous_map X Tx (closed_interval 0 1) (closed_interval_topology 0 1) f ∧ (∀x : set, x ∈ {x0} → apply_fun f x = 0)) (∀x : set, x ∈ {y0} → apply_fun f x = 1) Hfpack).
We prove the intermediate claim Hfy0val: apply_fun f y0 = 1.
An exact proof term for the current goal is (Hfy0 y0 (SingI y0)).
We prove the intermediate claim HI_sub_R: closed_interval 0 1 ⊆ R.
An exact proof term for the current goal is (closed_interval_sub_R 0 1).
We prove the intermediate claim HTstd: topology_on R R_standard_topology.
An exact proof term for the current goal is R_standard_topology_is_topology.
We prove the intermediate claim HTyEq: closed_interval_topology 0 1 = subspace_topology R R_standard_topology (closed_interval 0 1).
Use reflexivity.
We prove the intermediate claim HcontRstd: continuous_map X Tx R R_standard_topology f.
An exact proof term for the current goal is (continuous_map_range_expand X Tx (closed_interval 0 1) (closed_interval_topology 0 1) R R_standard_topology f HfcontI HI_sub_R HTstd HTyEq).
We prove the intermediate claim HcontR: continuous_map X Tx R (order_topology R) f.
rewrite the current goal using standard_topology_is_order_topology (from left to right).
An exact proof term for the current goal is HcontRstd.
We prove the intermediate claim HsoR: simply_ordered_set R.
An exact proof term for the current goal is simply_ordered_set_R.
We prove the intermediate claim HsubImg: closed_interval 0 1 ⊆ image_of f X.
Let r be given.
Assume HrI: r ∈ closed_interval 0 1.
We will prove r ∈ image_of f X.
We prove the intermediate claim HrR: r ∈ R.
An exact proof term for the current goal is (SepE1 R (λz : set ⇒ ¬ (Rlt z 0) ∧ ¬ (Rlt 1 z)) r HrI).
We prove the intermediate claim Hrprop: ¬ (Rlt r 0) ∧ ¬ (Rlt 1 r).
An exact proof term for the current goal is (SepE2 R (λz : set ⇒ ¬ (Rlt z 0) ∧ ¬ (Rlt 1 z)) r HrI).
We prove the intermediate claim Hnlt0: ¬ (Rlt r 0).
An exact proof term for the current goal is (andEL (¬ (Rlt r 0)) (¬ (Rlt 1 r)) Hrprop).
We prove the intermediate claim Hnlt1: ¬ (Rlt 1 r).
An exact proof term for the current goal is (andER (¬ (Rlt r 0)) (¬ (Rlt 1 r)) Hrprop).
We prove the intermediate claim H0R: 0 ∈ R.
An exact proof term for the current goal is (RleE_left 0 1 H0le1).
We prove the intermediate claim H1R: 1 ∈ R.
An exact proof term for the current goal is (RleE_right 0 1 H0le1).
We prove the intermediate claim H0ler: Rle 0 r.
An exact proof term for the current goal is (RleI 0 r H0R HrR Hnlt0).
We prove the intermediate claim Hrle1: Rle r 1.
An exact proof term for the current goal is (RleI r 1 HrR H1R Hnlt1).
We prove the intermediate claim Hbetw: between_in_order R (apply_fun f x0) r (apply_fun f y0).
rewrite the current goal using Hfx0 (from left to right).
rewrite the current goal using Hfy0val (from left to right).
Apply (xm (r = 0)) to the current goal.
Assume Hr0: r = 0.
rewrite the current goal using Hr0 (from left to right).
An exact proof term for the current goal is (between_in_orderI_eq_left R 0 1).
Assume Hrneq0: ¬ (r = 0).
Apply (xm (r = 1)) to the current goal.
Assume Hr1: r = 1.
rewrite the current goal using Hr1 (from left to right).
An exact proof term for the current goal is (between_in_orderI_eq_right R 0 1).
Assume Hrneq1: ¬ (r = 1).
We prove the intermediate claim H0ltr: Rlt 0 r.
We prove the intermediate claim Hneq0': ¬ (0 = r).
Assume H0r: 0 = r.
Apply Hrneq0 to the current goal.
rewrite the current goal using H0r (from right to left).
Use reflexivity.
An exact proof term for the current goal is (Rle_neq_implies_Rlt 0 r H0ler Hneq0').
We prove the intermediate claim Hrl1: Rlt r 1.
An exact proof term for the current goal is (Rle_neq_implies_Rlt r 1 Hrle1 Hrneq1).
We prove the intermediate claim Hord0r: order_rel R 0 r.
An exact proof term for the current goal is (Rlt_implies_order_rel_R 0 r H0ltr).
We prove the intermediate claim Hordr1: order_rel R r 1.
An exact proof term for the current goal is (Rlt_implies_order_rel_R r 1 Hrl1).
An exact proof term for the current goal is (between_in_orderI_left R 0 r 1 Hord0r Hordr1).
We prove the intermediate claim Hexc: ∃c : set, c ∈ X ∧ apply_fun f c = r.
An exact proof term for the current goal is (intermediate_value_theorem X Tx R f x0 y0 r HXconn HsoR HcontR Hx0X Hy0X HrR Hbetw).
Apply Hexc to the current goal.
Let c be given.
Assume Hcpack.
We prove the intermediate claim HcX: c ∈ X.
An exact proof term for the current goal is (andEL (c ∈ X) (apply_fun f c = r) Hcpack).
We prove the intermediate claim HcEq: apply_fun f c = r.
An exact proof term for the current goal is (andER (c ∈ X) (apply_fun f c = r) Hcpack).
rewrite the current goal using HcEq (from right to left).
An exact proof term for the current goal is (ReplI X (λx : set ⇒ apply_fun f x) c HcX).
We prove the intermediate claim HfunI: function_on f X (closed_interval 0 1).
An exact proof term for the current goal is (continuous_map_function_on X Tx (closed_interval 0 1) (closed_interval_topology 0 1) f HfcontI).
We prove the intermediate claim HimgSub: image_of f X ⊆ closed_interval 0 1.
An exact proof term for the current goal is (image_of_sub_codomain f X (closed_interval 0 1) X HfunI (Subq_ref X)).
We prove the intermediate claim HimgEq: image_of f X = closed_interval 0 1.
Apply set_ext to the current goal.
An exact proof term for the current goal is HimgSub.
An exact proof term for the current goal is HsubImg.
We prove the intermediate claim HimgCount: countable (image_of f X).
An exact proof term for the current goal is (countable_image X HcountX (λx : set ⇒ apply_fun f x)).
We prove the intermediate claim HICount: countable (closed_interval 0 1).
rewrite the current goal using HimgEq (from right to left).
An exact proof term for the current goal is HimgCount.
Apply FalseE to the current goal.
An exact proof term for the current goal is (closed_interval_0_1_uncountable HICount).
∎