Theorem rpnnen1lem6

Description: Lemma for rpnnen1 . (Contributed by Mario Carneiro, 12-May-2013) (Revised by NM, 15-Aug-2021) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	rpnnen1lem.1	⊢ 𝑇 = { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 }
	rpnnen1lem.2	⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) )
	rpnnen1lem.n	⊢ ℕ ∈ V
	rpnnen1lem.q	⊢ ℚ ∈ V
Assertion	rpnnen1lem6	⊢ ℝ ≼ ( ℚ ↑m ℕ )

Proof

Step	Hyp	Ref	Expression
1		rpnnen1lem.1	⊢ 𝑇 = { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 }
2		rpnnen1lem.2	⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) )
3		rpnnen1lem.n	⊢ ℕ ∈ V
4		rpnnen1lem.q	⊢ ℚ ∈ V
5		ovex	⊢ ( ℚ ↑m ℕ ) ∈ V
6	1 2 3 4	rpnnen1lem1	⊢ ( 𝑥 ∈ ℝ → ( 𝐹 ‘ 𝑥 ) ∈ ( ℚ ↑m ℕ ) )
7		rneq	⊢ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → ran ( 𝐹 ‘ 𝑥 ) = ran ( 𝐹 ‘ 𝑦 ) )
8	7	supeq1d	⊢ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) = sup ( ran ( 𝐹 ‘ 𝑦 ) , ℝ , < ) )
9	1 2 3 4	rpnnen1lem5	⊢ ( 𝑥 ∈ ℝ → sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) = 𝑥 )
10		fveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
11	10	rneqd	⊢ ( 𝑥 = 𝑦 → ran ( 𝐹 ‘ 𝑥 ) = ran ( 𝐹 ‘ 𝑦 ) )
12	11	supeq1d	⊢ ( 𝑥 = 𝑦 → sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) = sup ( ran ( 𝐹 ‘ 𝑦 ) , ℝ , < ) )
13		id	⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
14	12 13	eqeq12d	⊢ ( 𝑥 = 𝑦 → ( sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) = 𝑥 ↔ sup ( ran ( 𝐹 ‘ 𝑦 ) , ℝ , < ) = 𝑦 ) )
15	14 9	vtoclga	⊢ ( 𝑦 ∈ ℝ → sup ( ran ( 𝐹 ‘ 𝑦 ) , ℝ , < ) = 𝑦 )
16	9 15	eqeqan12d	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) = sup ( ran ( 𝐹 ‘ 𝑦 ) , ℝ , < ) ↔ 𝑥 = 𝑦 ) )
17	8 16	imbitrid	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
18	17 10	impbid1	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ 𝑥 = 𝑦 ) )
19	6 18	dom2	⊢ ( ( ℚ ↑m ℕ ) ∈ V → ℝ ≼ ( ℚ ↑m ℕ ) )
20	5 19	ax-mp	⊢ ℝ ≼ ( ℚ ↑m ℕ )