Metamath Proof Explorer

Theorem ruclem13

Description: Lemma for ruc . There is no function that maps NN onto RR . (Use nex if you want this in the form -. E. f f : NN -onto-> RR .) (Contributed by NM, 14-Oct-2004) (Proof shortened by Fan Zheng, 6-Jun-2016)

Ref Expression
Assertion ruclem13 
|- -. F : NN -onto-> RR

Proof

Step Hyp Ref Expression
1 forn 
 |-  ( F : NN -onto-> RR -> ran F = RR )
2 1 difeq2d 
 |-  ( F : NN -onto-> RR -> ( RR \ ran F ) = ( RR \ RR ) )
3 difid 
 |-  ( RR \ RR ) = (/)
4 2 3 eqtrdi 
 |-  ( F : NN -onto-> RR -> ( RR \ ran F ) = (/) )
5 reex 
 |-  RR e. _V
6 5 5 xpex 
 |-  ( RR X. RR ) e. _V
7 6 5 mpoex 
 |-  ( x e. ( RR X. RR ) , y e. RR |-> [_ ( ( ( 1st ` x ) + ( 2nd ` x ) ) / 2 ) / m ]_ if ( m < y , <. ( 1st ` x ) , m >. , <. ( ( m + ( 2nd ` x ) ) / 2 ) , ( 2nd ` x ) >. ) ) e. _V
8 7 isseti 
 |-  E. d d = ( x e. ( RR X. RR ) , y e. RR |-> [_ ( ( ( 1st ` x ) + ( 2nd ` x ) ) / 2 ) / m ]_ if ( m < y , <. ( 1st ` x ) , m >. , <. ( ( m + ( 2nd ` x ) ) / 2 ) , ( 2nd ` x ) >. ) )
9 fof 
 |-  ( F : NN -onto-> RR -> F : NN --> RR )
10 9 adantr 
 |-  ( ( F : NN -onto-> RR /\ d = ( x e. ( RR X. RR ) , y e. RR |-> [_ ( ( ( 1st ` x ) + ( 2nd ` x ) ) / 2 ) / m ]_ if ( m < y , <. ( 1st ` x ) , m >. , <. ( ( m + ( 2nd ` x ) ) / 2 ) , ( 2nd ` x ) >. ) ) ) -> F : NN --> RR )
11 simpr 
 |-  ( ( F : NN -onto-> RR /\ d = ( x e. ( RR X. RR ) , y e. RR |-> [_ ( ( ( 1st ` x ) + ( 2nd ` x ) ) / 2 ) / m ]_ if ( m < y , <. ( 1st ` x ) , m >. , <. ( ( m + ( 2nd ` x ) ) / 2 ) , ( 2nd ` x ) >. ) ) ) -> d = ( x e. ( RR X. RR ) , y e. RR |-> [_ ( ( ( 1st ` x ) + ( 2nd ` x ) ) / 2 ) / m ]_ if ( m < y , <. ( 1st ` x ) , m >. , <. ( ( m + ( 2nd ` x ) ) / 2 ) , ( 2nd ` x ) >. ) ) )
12 eqid 
 |-  ( { <. 0 , <. 0 , 1 >. >. } u. F ) = ( { <. 0 , <. 0 , 1 >. >. } u. F )
13 eqid 
 |-  seq 0 ( d , ( { <. 0 , <. 0 , 1 >. >. } u. F ) ) = seq 0 ( d , ( { <. 0 , <. 0 , 1 >. >. } u. F ) )
14 eqid 
 |-  sup ( ran ( 1st o. seq 0 ( d , ( { <. 0 , <. 0 , 1 >. >. } u. F ) ) ) , RR , < ) = sup ( ran ( 1st o. seq 0 ( d , ( { <. 0 , <. 0 , 1 >. >. } u. F ) ) ) , RR , < )
15 10 11 12 13 14 ruclem12 
 |-  ( ( F : NN -onto-> RR /\ d = ( x e. ( RR X. RR ) , y e. RR |-> [_ ( ( ( 1st ` x ) + ( 2nd ` x ) ) / 2 ) / m ]_ if ( m < y , <. ( 1st ` x ) , m >. , <. ( ( m + ( 2nd ` x ) ) / 2 ) , ( 2nd ` x ) >. ) ) ) -> sup ( ran ( 1st o. seq 0 ( d , ( { <. 0 , <. 0 , 1 >. >. } u. F ) ) ) , RR , < ) e. ( RR \ ran F ) )
16 n0i 
 |-  ( sup ( ran ( 1st o. seq 0 ( d , ( { <. 0 , <. 0 , 1 >. >. } u. F ) ) ) , RR , < ) e. ( RR \ ran F ) -> -. ( RR \ ran F ) = (/) )
17 15 16 syl 
 |-  ( ( F : NN -onto-> RR /\ d = ( x e. ( RR X. RR ) , y e. RR |-> [_ ( ( ( 1st ` x ) + ( 2nd ` x ) ) / 2 ) / m ]_ if ( m < y , <. ( 1st ` x ) , m >. , <. ( ( m + ( 2nd ` x ) ) / 2 ) , ( 2nd ` x ) >. ) ) ) -> -. ( RR \ ran F ) = (/) )
18 17 ex 
 |-  ( F : NN -onto-> RR -> ( d = ( x e. ( RR X. RR ) , y e. RR |-> [_ ( ( ( 1st ` x ) + ( 2nd ` x ) ) / 2 ) / m ]_ if ( m < y , <. ( 1st ` x ) , m >. , <. ( ( m + ( 2nd ` x ) ) / 2 ) , ( 2nd ` x ) >. ) ) -> -. ( RR \ ran F ) = (/) ) )
19 18 exlimdv 
 |-  ( F : NN -onto-> RR -> ( E. d d = ( x e. ( RR X. RR ) , y e. RR |-> [_ ( ( ( 1st ` x ) + ( 2nd ` x ) ) / 2 ) / m ]_ if ( m < y , <. ( 1st ` x ) , m >. , <. ( ( m + ( 2nd ` x ) ) / 2 ) , ( 2nd ` x ) >. ) ) -> -. ( RR \ ran F ) = (/) ) )
20 8 19 mpi 
 |-  ( F : NN -onto-> RR -> -. ( RR \ ran F ) = (/) )
21 4 20 pm2.65i 
 |-  -. F : NN -onto-> RR