Apply Empty_Subq_eq to the current goal.
Let p be given.
Assume Hp: p ∈ Sorgenfrey_plane_diag_rational ∩ Sorgenfrey_plane_diag_irrational.
We will prove p ∈ Empty.
We prove the intermediate claim HpA: p ∈ Sorgenfrey_plane_diag_rational.
An exact proof term for the current goal is (binintersectE1 Sorgenfrey_plane_diag_rational Sorgenfrey_plane_diag_irrational p Hp).
We prove the intermediate claim HpB: p ∈ Sorgenfrey_plane_diag_irrational.
An exact proof term for the current goal is (binintersectE2 Sorgenfrey_plane_diag_rational Sorgenfrey_plane_diag_irrational p Hp).
We prove the intermediate claim Hexx: ∃x ∈ rational_numbers, p = (x,minus_SNo x).
An exact proof term for the current goal is (ReplE rational_numbers (λx0 : set ⇒ (x0,minus_SNo x0)) p HpA).
Apply Hexx to the current goal.
Let x be given.
Assume Hxpair.
We prove the intermediate claim HxQ: x ∈ rational_numbers.
An exact proof term for the current goal is (andEL (x ∈ rational_numbers) (p = (x,minus_SNo x)) Hxpair).
We prove the intermediate claim Hpeq1: p = (x,minus_SNo x).
An exact proof term for the current goal is (andER (x ∈ rational_numbers) (p = (x,minus_SNo x)) Hxpair).
We prove the intermediate claim Hexy: ∃y ∈ (Sorgenfrey_line ∖ rational_numbers), p = (y,minus_SNo y).
An exact proof term for the current goal is (ReplE (Sorgenfrey_line ∖ rational_numbers) (λy0 : set ⇒ (y0,minus_SNo y0)) p HpB).
Apply Hexy to the current goal.
Let y be given.
Assume Hypair.
We prove the intermediate claim HyIrr: y ∈ (Sorgenfrey_line ∖ rational_numbers).
An exact proof term for the current goal is (andEL (y ∈ (Sorgenfrey_line ∖ rational_numbers)) (p = (y,minus_SNo y)) Hypair).
We prove the intermediate claim Hpeq2: p = (y,minus_SNo y).
An exact proof term for the current goal is (andER (y ∈ (Sorgenfrey_line ∖ rational_numbers)) (p = (y,minus_SNo y)) Hypair).
We prove the intermediate claim Hp0x: (p 0) = x.
rewrite the current goal using Hpeq1 (from left to right) at position 1.
An exact proof term for the current goal is (tuple_2_0_eq x (minus_SNo x)).
We prove the intermediate claim Hp0y: (p 0) = y.
rewrite the current goal using Hpeq2 (from left to right) at position 1.
An exact proof term for the current goal is (tuple_2_0_eq y (minus_SNo y)).
We prove the intermediate claim HxEqy: x = y.
rewrite the current goal using Hp0x (from right to left).
An exact proof term for the current goal is Hp0y.
We prove the intermediate claim HynQ: y ∉ rational_numbers.
An exact proof term for the current goal is (setminusE2 Sorgenfrey_line rational_numbers y HyIrr).
Apply FalseE to the current goal.
We will prove False.
We prove the intermediate claim HyQ: y ∈ rational_numbers.
rewrite the current goal using HxEqy (from right to left).
An exact proof term for the current goal is HxQ.
An exact proof term for the current goal is (HynQ HyQ).
∎