Theorem ixxf 9464

Description: The set of intervals of extended reals maps to subsets of extended reals. (Contributed by FL, 14-Jun-2007.) (Revised by Mario Carneiro, 16-Nov-2013.)

Hypothesis

Ref	Expression
ixx.1	|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )

Assertion

Ref	Expression
ixxf	|- O : ( RR* X. RR* ) --> ~P RR*

Distinct variable groups:   x, y, z, R   x, S, y, z

Allowed substitution hints:   O( x, y, z)

Proof of Theorem ixxf

Step	Hyp	Ref	Expression
1		ssrab2 3121	. . . 4 |- { z e. RR* | ( x R z /\ z S y ) } C_ RR*
2		xrex 9422	. . . . 5 |- RR* e. _V
3	2	elpw2 4014	. . . 4 |- ( { z e. RR* | ( x R z /\ z S y ) } e. ~P RR* <-> { z e. RR* | ( x R z /\ z S y ) } C_ RR* )
4	1, 3	mpbir 145	. . 3 |- { z e. RR* | ( x R z /\ z S y ) } e. ~P RR*
5	4	rgen2w 2442	. 2 |- A. x e. RR* A. y e. RR* { z e. RR* | ( x R z /\ z S y ) } e. ~P RR*
6		ixx.1	. . 3 |- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )
7	6	fmpt2 6009	. 2 |- ( A. x e. RR* A. y e. RR* { z e. RR* | ( x R z /\ z S y ) } e. ~P RR* <-> O : ( RR* X. RR* ) --> ~P RR* )
8	5, 7	mpbi 144	1 |- O : ( RR* X. RR* ) --> ~P RR*

Syntax hints:   /\ wa 103   = wceq 1296   e. wcel 1445   A.wral 2370   {crab 2374   C_ wss 3013   ~Pcpw 3449   class class class wbr 3867   X. cxp 4465   -->wf 5045   |-> cmpt2 5692   RR*cxr 7618

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-13 1456  ax-14 1457  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-sep 3978  ax-pow 4030  ax-pr 4060  ax-un 4284  ax-cnex 7533  ax-resscn 7534

This theorem depends on definitions:  df-bi 116  df-3an 929  df-tru 1299  df-nf 1402  df-sb 1700  df-eu 1958  df-mo 1959  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-ral 2375  df-rex 2376  df-rab 2379  df-v 2635  df-sbc 2855  df-csb 2948  df-un 3017  df-in 3019  df-ss 3026  df-pw 3451  df-sn 3472  df-pr 3473  df-op 3475  df-uni 3676  df-iun 3754  df-br 3868  df-opab 3922  df-mpt 3923  df-id 4144  df-xp 4473  df-rel 4474  df-cnv 4475  df-co 4476  df-dm 4477  df-rn 4478  df-res 4479  df-ima 4480  df-iota 5014  df-fun 5051  df-fn 5052  df-f 5053  df-fv 5057  df-oprab 5694  df-mpt2 5695  df-1st 5949  df-2nd 5950  df-pnf 7621  df-mnf 7622  df-xr 7623

This theorem is referenced by:  ixxex  9465  ixxssxr  9466  iccf  9538