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 : onto

Proof

Step Hyp Ref Expression
1 forn F : onto ran F =
2 1 difeq2d F : onto ran F =
3 difid =
4 2 3 eqtrdi F : onto ran F =
5 reex V
6 5 5 xpex 2 V
7 6 5 mpoex x 2 , y 1 st x + 2 nd x 2 / m if m < y 1 st x m m + 2 nd x 2 2 nd x V
8 7 isseti d d = x 2 , y 1 st x + 2 nd x 2 / m if m < y 1 st x m m + 2 nd x 2 2 nd x
9 fof F : onto F :
10 9 adantr F : onto d = x 2 , y 1 st x + 2 nd x 2 / m if m < y 1 st x m m + 2 nd x 2 2 nd x F :
11 simpr F : onto d = x 2 , y 1 st x + 2 nd x 2 / m if m < y 1 st x m m + 2 nd x 2 2 nd x d = x 2 , y 1 st x + 2 nd x 2 / m if m < y 1 st x m m + 2 nd x 2 2 nd x
12 eqid 0 0 1 F = 0 0 1 F
13 eqid seq 0 d 0 0 1 F = seq 0 d 0 0 1 F
14 eqid sup ran 1 st seq 0 d 0 0 1 F < = sup ran 1 st seq 0 d 0 0 1 F <
15 10 11 12 13 14 ruclem12 F : onto d = x 2 , y 1 st x + 2 nd x 2 / m if m < y 1 st x m m + 2 nd x 2 2 nd x sup ran 1 st seq 0 d 0 0 1 F < ran F
16 n0i sup ran 1 st seq 0 d 0 0 1 F < ran F ¬ ran F =
17 15 16 syl F : onto d = x 2 , y 1 st x + 2 nd x 2 / m if m < y 1 st x m m + 2 nd x 2 2 nd x ¬ ran F =
18 17 ex F : onto d = x 2 , y 1 st x + 2 nd x 2 / m if m < y 1 st x m m + 2 nd x 2 2 nd x ¬ ran F =
19 18 exlimdv F : onto d d = x 2 , y 1 st x + 2 nd x 2 / m if m < y 1 st x m m + 2 nd x 2 2 nd x ¬ ran F =
20 8 19 mpi F : onto ¬ ran F =
21 4 20 pm2.65i ¬ F : onto