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	$$⊢\neg F:\mathbb{N}\underset{onto}{⟶}ℝ$$

Proof

Step	Hyp	Ref	Expression
1		forn	$$⊢F:\mathbb{N}\underset{onto}{⟶}ℝ\to \mathrm{ran}F=ℝ$$
2	1	difeq2d	$$⊢F:\mathbb{N}\underset{onto}{⟶}ℝ\to ℝ\setminus \mathrm{ran}F=ℝ\setminus ℝ$$
3		difid	$$⊢ℝ\setminus ℝ=\varnothing$$
4	2 3	eqtrdi	$$⊢F:\mathbb{N}\underset{onto}{⟶}ℝ\to ℝ\setminus \mathrm{ran}F=\varnothing$$
5		reex	$$⊢ℝ\in \mathrm{V}$$
6	5 5	xpex	$$⊢{ℝ}^2\in \mathrm{V}$$
7	6 5	mpoex	$$⊢\left(x\in {ℝ}^2,y\in ℝ⟼⦋\left(\frac{1^{st}\left(x\right)+2^{nd}\left(x\right)}{2}\right)/m⦌if\left(m<y,⟨1^{st}\left(x\right),m⟩,⟨\frac{m+2^{nd}\left(x\right)}{2},2^{nd}\left(x\right)⟩\right)\right)\in \mathrm{V}$$
8	7	isseti	$$⊢\exists dd=\left(x\in {ℝ}^2,y\in ℝ⟼⦋\left(\frac{1^{st}\left(x\right)+2^{nd}\left(x\right)}{2}\right)/m⦌if\left(m<y,⟨1^{st}\left(x\right),m⟩,⟨\frac{m+2^{nd}\left(x\right)}{2},2^{nd}\left(x\right)⟩\right)\right)$$
9		fof	$$⊢F:\mathbb{N}\underset{onto}{⟶}ℝ\to F:\mathbb{N}⟶ℝ$$
10	9	adantr	$$⊢\left(F:\mathbb{N}\underset{onto}{⟶}ℝ\wedge d=\left(x\in {ℝ}^2,y\in ℝ⟼⦋\left(\frac{1^{st}\left(x\right)+2^{nd}\left(x\right)}{2}\right)/m⦌if\left(m<y,⟨1^{st}\left(x\right),m⟩,⟨\frac{m+2^{nd}\left(x\right)}{2},2^{nd}\left(x\right)⟩\right)\right)\right)\to F:\mathbb{N}⟶ℝ$$
11		simpr	$$⊢\left(F:\mathbb{N}\underset{onto}{⟶}ℝ\wedge d=\left(x\in {ℝ}^2,y\in ℝ⟼⦋\left(\frac{1^{st}\left(x\right)+2^{nd}\left(x\right)}{2}\right)/m⦌if\left(m<y,⟨1^{st}\left(x\right),m⟩,⟨\frac{m+2^{nd}\left(x\right)}{2},2^{nd}\left(x\right)⟩\right)\right)\right)\to d=\left(x\in {ℝ}^2,y\in ℝ⟼⦋\left(\frac{1^{st}\left(x\right)+2^{nd}\left(x\right)}{2}\right)/m⦌if\left(m<y,⟨1^{st}\left(x\right),m⟩,⟨\frac{m+2^{nd}\left(x\right)}{2},2^{nd}\left(x\right)⟩\right)\right)$$
12		eqid	$$⊢\left\{⟨0,⟨0,1⟩⟩\right\}\cup F=\left\{⟨0,⟨0,1⟩⟩\right\}\cup F$$
13		eqid	$$⊢seq0\left(d,\left(\left\{⟨0,⟨0,1⟩⟩\right\}\cup F\right)\right)=seq0\left(d,\left(\left\{⟨0,⟨0,1⟩⟩\right\}\cup F\right)\right)$$
14		eqid	$$⊢sup\left(\mathrm{ran}\left(1^{st}\circ seq0\left(d,\left(\left\{⟨0,⟨0,1⟩⟩\right\}\cup F\right)\right)\right),ℝ,<\right)=sup\left(\mathrm{ran}\left(1^{st}\circ seq0\left(d,\left(\left\{⟨0,⟨0,1⟩⟩\right\}\cup F\right)\right)\right),ℝ,<\right)$$
15	10 11 12 13 14	ruclem12	$$⊢\left(F:\mathbb{N}\underset{onto}{⟶}ℝ\wedge d=\left(x\in {ℝ}^2,y\in ℝ⟼⦋\left(\frac{1^{st}\left(x\right)+2^{nd}\left(x\right)}{2}\right)/m⦌if\left(m<y,⟨1^{st}\left(x\right),m⟩,⟨\frac{m+2^{nd}\left(x\right)}{2},2^{nd}\left(x\right)⟩\right)\right)\right)\to sup\left(\mathrm{ran}\left(1^{st}\circ seq0\left(d,\left(\left\{⟨0,⟨0,1⟩⟩\right\}\cup F\right)\right)\right),ℝ,<\right)\in \left(ℝ\setminus \mathrm{ran}F\right)$$
16		n0i	$$⊢sup\left(\mathrm{ran}\left(1^{st}\circ seq0\left(d,\left(\left\{⟨0,⟨0,1⟩⟩\right\}\cup F\right)\right)\right),ℝ,<\right)\in \left(ℝ\setminus \mathrm{ran}F\right)\to \neg ℝ\setminus \mathrm{ran}F=\varnothing$$
17	15 16	syl	$$⊢\left(F:\mathbb{N}\underset{onto}{⟶}ℝ\wedge d=\left(x\in {ℝ}^2,y\in ℝ⟼⦋\left(\frac{1^{st}\left(x\right)+2^{nd}\left(x\right)}{2}\right)/m⦌if\left(m<y,⟨1^{st}\left(x\right),m⟩,⟨\frac{m+2^{nd}\left(x\right)}{2},2^{nd}\left(x\right)⟩\right)\right)\right)\to \neg ℝ\setminus \mathrm{ran}F=\varnothing$$
18	17	ex	$$⊢F:\mathbb{N}\underset{onto}{⟶}ℝ\to \left(d=\left(x\in {ℝ}^2,y\in ℝ⟼⦋\left(\frac{1^{st}\left(x\right)+2^{nd}\left(x\right)}{2}\right)/m⦌if\left(m<y,⟨1^{st}\left(x\right),m⟩,⟨\frac{m+2^{nd}\left(x\right)}{2},2^{nd}\left(x\right)⟩\right)\right)\to \neg ℝ\setminus \mathrm{ran}F=\varnothing \right)$$
19	18	exlimdv	$$⊢F:\mathbb{N}\underset{onto}{⟶}ℝ\to \left(\exists dd=\left(x\in {ℝ}^2,y\in ℝ⟼⦋\left(\frac{1^{st}\left(x\right)+2^{nd}\left(x\right)}{2}\right)/m⦌if\left(m<y,⟨1^{st}\left(x\right),m⟩,⟨\frac{m+2^{nd}\left(x\right)}{2},2^{nd}\left(x\right)⟩\right)\right)\to \neg ℝ\setminus \mathrm{ran}F=\varnothing \right)$$
20	8 19	mpi	$$⊢F:\mathbb{N}\underset{onto}{⟶}ℝ\to \neg ℝ\setminus \mathrm{ran}F=\varnothing$$
21	4 20	pm2.65i	$$⊢\neg F:\mathbb{N}\underset{onto}{⟶}ℝ$$