Theorem icoreresf

Description: Closed-below, open-above intervals of reals map to subsets of reals. (Contributed by ML, 25-Jul-2020)

	Ref	Expression
Assertion	icoreresf	|- ( [,) |` ( RR X. RR ) ) : ( RR X. RR ) --> ~P RR

Proof

Step	Hyp	Ref	Expression
1		rexpssxrxp	|- ( RR X. RR ) C_ ( RR* X. RR* )
2		df-ico	|- [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
3	2	ixxf	|- [,) : ( RR* X. RR* ) --> ~P RR*
4		ffn	|- ( [,) : ( RR* X. RR* ) --> ~P RR* -> [,) Fn ( RR* X. RR* ) )
5		fnssresb	|- ( [,) Fn ( RR* X. RR* ) -> ( ( [,) |` ( RR X. RR ) ) Fn ( RR X. RR ) <-> ( RR X. RR ) C_ ( RR* X. RR* ) ) )
6	3 4 5	mp2b	|- ( ( [,) |` ( RR X. RR ) ) Fn ( RR X. RR ) <-> ( RR X. RR ) C_ ( RR* X. RR* ) )
7	1 6	mpbir	|- ( [,) |` ( RR X. RR ) ) Fn ( RR X. RR )
8		eqid	|- ( [,) |` ( RR X. RR ) ) = ( [,) |` ( RR X. RR ) )
9	8	icorempo	|- ( [,) |` ( RR X. RR ) ) = ( x e. RR , y e. RR |-> { z e. RR | ( x <_ z /\ z < y ) } )
10	9	rneqi	|- ran ( [,) |` ( RR X. RR ) ) = ran ( x e. RR , y e. RR |-> { z e. RR | ( x <_ z /\ z < y ) } )
11		ssrab2	|- { z e. RR | ( x <_ z /\ z < y ) } C_ RR
12		reex	|- RR e. _V
13	12	elpw2	|- ( { z e. RR | ( x <_ z /\ z < y ) } e. ~P RR <-> { z e. RR | ( x <_ z /\ z < y ) } C_ RR )
14	11 13	mpbir	|- { z e. RR | ( x <_ z /\ z < y ) } e. ~P RR
15	14	rgen2w	|- A. x e. RR A. y e. RR { z e. RR | ( x <_ z /\ z < y ) } e. ~P RR
16		eqid	|- ( x e. RR , y e. RR |-> { z e. RR | ( x <_ z /\ z < y ) } ) = ( x e. RR , y e. RR |-> { z e. RR | ( x <_ z /\ z < y ) } )
17	16	rnmpo	|- ran ( x e. RR , y e. RR |-> { z e. RR | ( x <_ z /\ z < y ) } ) = { l | E. x e. RR E. y e. RR l = { z e. RR | ( x <_ z /\ z < y ) } }
18	17	eqabri	|- ( l e. ran ( x e. RR , y e. RR |-> { z e. RR | ( x <_ z /\ z < y ) } ) <-> E. x e. RR E. y e. RR l = { z e. RR | ( x <_ z /\ z < y ) } )
19		simpl	|- ( ( A. x e. RR A. y e. RR { z e. RR | ( x <_ z /\ z < y ) } e. ~P RR /\ E. x e. RR E. y e. RR l = { z e. RR | ( x <_ z /\ z < y ) } ) -> A. x e. RR A. y e. RR { z e. RR | ( x <_ z /\ z < y ) } e. ~P RR )
20		simpr	|- ( ( A. x e. RR A. y e. RR { z e. RR | ( x <_ z /\ z < y ) } e. ~P RR /\ E. x e. RR E. y e. RR l = { z e. RR | ( x <_ z /\ z < y ) } ) -> E. x e. RR E. y e. RR l = { z e. RR | ( x <_ z /\ z < y ) } )
21	19 20	r19.29d2r	|- ( ( A. x e. RR A. y e. RR { z e. RR | ( x <_ z /\ z < y ) } e. ~P RR /\ E. x e. RR E. y e. RR l = { z e. RR | ( x <_ z /\ z < y ) } ) -> E. x e. RR E. y e. RR ( { z e. RR | ( x <_ z /\ z < y ) } e. ~P RR /\ l = { z e. RR | ( x <_ z /\ z < y ) } ) )
22		eleq1	|- ( l = { z e. RR | ( x <_ z /\ z < y ) } -> ( l e. ~P RR <-> { z e. RR | ( x <_ z /\ z < y ) } e. ~P RR ) )
23	22	biimparc	|- ( ( { z e. RR | ( x <_ z /\ z < y ) } e. ~P RR /\ l = { z e. RR | ( x <_ z /\ z < y ) } ) -> l e. ~P RR )
24	23	a1i	|- ( ( x e. RR /\ y e. RR ) -> ( ( { z e. RR | ( x <_ z /\ z < y ) } e. ~P RR /\ l = { z e. RR | ( x <_ z /\ z < y ) } ) -> l e. ~P RR ) )
25	24	rexlimivv	|- ( E. x e. RR E. y e. RR ( { z e. RR | ( x <_ z /\ z < y ) } e. ~P RR /\ l = { z e. RR | ( x <_ z /\ z < y ) } ) -> l e. ~P RR )
26	21 25	syl	|- ( ( A. x e. RR A. y e. RR { z e. RR | ( x <_ z /\ z < y ) } e. ~P RR /\ E. x e. RR E. y e. RR l = { z e. RR | ( x <_ z /\ z < y ) } ) -> l e. ~P RR )
27	26	ex	|- ( A. x e. RR A. y e. RR { z e. RR | ( x <_ z /\ z < y ) } e. ~P RR -> ( E. x e. RR E. y e. RR l = { z e. RR | ( x <_ z /\ z < y ) } -> l e. ~P RR ) )
28	18 27	biimtrid	|- ( A. x e. RR A. y e. RR { z e. RR | ( x <_ z /\ z < y ) } e. ~P RR -> ( l e. ran ( x e. RR , y e. RR |-> { z e. RR | ( x <_ z /\ z < y ) } ) -> l e. ~P RR ) )
29	28	ssrdv	|- ( A. x e. RR A. y e. RR { z e. RR | ( x <_ z /\ z < y ) } e. ~P RR -> ran ( x e. RR , y e. RR |-> { z e. RR | ( x <_ z /\ z < y ) } ) C_ ~P RR )
30	15 29	ax-mp	|- ran ( x e. RR , y e. RR |-> { z e. RR | ( x <_ z /\ z < y ) } ) C_ ~P RR
31	10 30	eqsstri	|- ran ( [,) |` ( RR X. RR ) ) C_ ~P RR
32		df-f	|- ( ( [,) |` ( RR X. RR ) ) : ( RR X. RR ) --> ~P RR <-> ( ( [,) |` ( RR X. RR ) ) Fn ( RR X. RR ) /\ ran ( [,) |` ( RR X. RR ) ) C_ ~P RR ) )
33	7 31 32	mpbir2an	|- ( [,) |` ( RR X. RR ) ) : ( RR X. RR ) --> ~P RR