This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ℕ )