Metamath Proof Explorer


Theorem hoidifhspval

Description: D is a function that returns the representation of the left side of the difference of a half-open interval and a half-space. Used in Lemma 115F of Fremlin1 p. 31 . (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses hoidifhspval.d D=xaXkXifk=Kifxakakxak
hoidifhspval.y φY
Assertion hoidifhspval φDY=aXkXifk=KifYakakYak

Proof

Step Hyp Ref Expression
1 hoidifhspval.d D=xaXkXifk=Kifxakakxak
2 hoidifhspval.y φY
3 breq1 x=YxakYak
4 id x=Yx=Y
5 3 4 ifbieq2d x=Yifxakakx=ifYakakY
6 5 ifeq1d x=Yifk=Kifxakakxak=ifk=KifYakakYak
7 6 mpteq2dv x=YkXifk=Kifxakakxak=kXifk=KifYakakYak
8 7 mpteq2dv x=YaXkXifk=Kifxakakxak=aXkXifk=KifYakakYak
9 ovex XV
10 9 mptex aXkXifk=KifYakakYakV
11 10 a1i φaXkXifk=KifYakakYakV
12 1 8 2 11 fvmptd3 φDY=aXkXifk=KifYakakYak