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	⊢ ¬ 𝐹 : ℕ –onto→ ℝ

Proof

Step	Hyp	Ref	Expression
1		forn	⊢ ( 𝐹 : ℕ –onto→ ℝ → ran 𝐹 = ℝ )
2	1	difeq2d	⊢ ( 𝐹 : ℕ –onto→ ℝ → ( ℝ ∖ ran 𝐹 ) = ( ℝ ∖ ℝ ) )
3		difid	⊢ ( ℝ ∖ ℝ ) = ∅
4	2 3	eqtrdi	⊢ ( 𝐹 : ℕ –onto→ ℝ → ( ℝ ∖ ran 𝐹 ) = ∅ )
5		reex	⊢ ℝ ∈ V
6	5 5	xpex	⊢ ( ℝ × ℝ ) ∈ V
7	6 5	mpoex	⊢ ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1st ‘ 𝑥 ) + ( 2nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ 𝑥 ) ) / 2 ) , ( 2nd ‘ 𝑥 ) ⟩ ) ) ∈ V
8	7	isseti	⊢ ∃ 𝑑 𝑑 = ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1st ‘ 𝑥 ) + ( 2nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ 𝑥 ) ) / 2 ) , ( 2nd ‘ 𝑥 ) ⟩ ) )
9		fof	⊢ ( 𝐹 : ℕ –onto→ ℝ → 𝐹 : ℕ ⟶ ℝ )
10	9	adantr	⊢ ( ( 𝐹 : ℕ –onto→ ℝ ∧ 𝑑 = ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1st ‘ 𝑥 ) + ( 2nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ 𝑥 ) ) / 2 ) , ( 2nd ‘ 𝑥 ) ⟩ ) ) ) → 𝐹 : ℕ ⟶ ℝ )
11		simpr	⊢ ( ( 𝐹 : ℕ –onto→ ℝ ∧ 𝑑 = ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1st ‘ 𝑥 ) + ( 2nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ 𝑥 ) ) / 2 ) , ( 2nd ‘ 𝑥 ) ⟩ ) ) ) → 𝑑 = ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1st ‘ 𝑥 ) + ( 2nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ 𝑥 ) ) / 2 ) , ( 2nd ‘ 𝑥 ) ⟩ ) ) )
12		eqid	⊢ ( { ⟨ 0 , ⟨ 0 , 1 ⟩ ⟩ } ∪ 𝐹 ) = ( { ⟨ 0 , ⟨ 0 , 1 ⟩ ⟩ } ∪ 𝐹 )
13		eqid	⊢ seq 0 ( 𝑑 , ( { ⟨ 0 , ⟨ 0 , 1 ⟩ ⟩ } ∪ 𝐹 ) ) = seq 0 ( 𝑑 , ( { ⟨ 0 , ⟨ 0 , 1 ⟩ ⟩ } ∪ 𝐹 ) )
14		eqid	⊢ sup ( ran ( 1st ∘ seq 0 ( 𝑑 , ( { ⟨ 0 , ⟨ 0 , 1 ⟩ ⟩ } ∪ 𝐹 ) ) ) , ℝ , < ) = sup ( ran ( 1st ∘ seq 0 ( 𝑑 , ( { ⟨ 0 , ⟨ 0 , 1 ⟩ ⟩ } ∪ 𝐹 ) ) ) , ℝ , < )
15	10 11 12 13 14	ruclem12	⊢ ( ( 𝐹 : ℕ –onto→ ℝ ∧ 𝑑 = ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1st ‘ 𝑥 ) + ( 2nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ 𝑥 ) ) / 2 ) , ( 2nd ‘ 𝑥 ) ⟩ ) ) ) → sup ( ran ( 1st ∘ seq 0 ( 𝑑 , ( { ⟨ 0 , ⟨ 0 , 1 ⟩ ⟩ } ∪ 𝐹 ) ) ) , ℝ , < ) ∈ ( ℝ ∖ ran 𝐹 ) )
16		n0i	⊢ ( sup ( ran ( 1st ∘ seq 0 ( 𝑑 , ( { ⟨ 0 , ⟨ 0 , 1 ⟩ ⟩ } ∪ 𝐹 ) ) ) , ℝ , < ) ∈ ( ℝ ∖ ran 𝐹 ) → ¬ ( ℝ ∖ ran 𝐹 ) = ∅ )
17	15 16	syl	⊢ ( ( 𝐹 : ℕ –onto→ ℝ ∧ 𝑑 = ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1st ‘ 𝑥 ) + ( 2nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ 𝑥 ) ) / 2 ) , ( 2nd ‘ 𝑥 ) ⟩ ) ) ) → ¬ ( ℝ ∖ ran 𝐹 ) = ∅ )
18	17	ex	⊢ ( 𝐹 : ℕ –onto→ ℝ → ( 𝑑 = ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1st ‘ 𝑥 ) + ( 2nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ 𝑥 ) ) / 2 ) , ( 2nd ‘ 𝑥 ) ⟩ ) ) → ¬ ( ℝ ∖ ran 𝐹 ) = ∅ ) )
19	18	exlimdv	⊢ ( 𝐹 : ℕ –onto→ ℝ → ( ∃ 𝑑 𝑑 = ( 𝑥 ∈ ( ℝ × ℝ ) , 𝑦 ∈ ℝ ↦ ⦋ ( ( ( 1st ‘ 𝑥 ) + ( 2nd ‘ 𝑥 ) ) / 2 ) / 𝑚 ⦌ if ( 𝑚 < 𝑦 , ⟨ ( 1st ‘ 𝑥 ) , 𝑚 ⟩ , ⟨ ( ( 𝑚 + ( 2nd ‘ 𝑥 ) ) / 2 ) , ( 2nd ‘ 𝑥 ) ⟩ ) ) → ¬ ( ℝ ∖ ran 𝐹 ) = ∅ ) )
20	8 19	mpi	⊢ ( 𝐹 : ℕ –onto→ ℝ → ¬ ( ℝ ∖ ran 𝐹 ) = ∅ )
21	4 20	pm2.65i	⊢ ¬ 𝐹 : ℕ –onto→ ℝ