Metamath Proof Explorer

Theorem rpnnen3

Description: Dedekind cut injection of RR into ~P QQ . (Contributed by Stefan O'Rear, 18-Jan-2015)

Ref Expression
Assertion rpnnen3 ⊢ ℝ ≼ 𝒫 ℚ

Proof

Step Hyp Ref Expression
1 qex ⊢ ℚ ∈ V
2 1 pwex ⊢ 𝒫 ℚ ∈ V
3 ssrab2 ⊢ c ∈ ℚ | c < a ⊆ ℚ
4 1 elpw2 ⊢ c ∈ ℚ | c < a ∈ 𝒫 ℚ ↔ c ∈ ℚ | c < a ⊆ ℚ
5 3 4 mpbir ⊢ c ∈ ℚ | c < a ∈ 𝒫 ℚ
6 5 a1i ⊢ a ∈ ℝ → c ∈ ℚ | c < a ∈ 𝒫 ℚ
7 lttri2 ⊢ a ∈ ℝ ∧ b ∈ ℝ → a ≠ b ↔ a < b ∨ b < a
8 rpnnen3lem ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ a < b → c ∈ ℚ | c < a ≠ c ∈ ℚ | c < b
9 rpnnen3lem ⊢ b ∈ ℝ ∧ a ∈ ℝ ∧ b < a → c ∈ ℚ | c < b ≠ c ∈ ℚ | c < a
10 9 ancom1s ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ b < a → c ∈ ℚ | c < b ≠ c ∈ ℚ | c < a
11 10 necomd ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ b < a → c ∈ ℚ | c < a ≠ c ∈ ℚ | c < b
12 8 11 jaodan ⊢ a ∈ ℝ ∧ b ∈ ℝ ∧ a < b ∨ b < a → c ∈ ℚ | c < a ≠ c ∈ ℚ | c < b
13 12 ex ⊢ a ∈ ℝ ∧ b ∈ ℝ → a < b ∨ b < a → c ∈ ℚ | c < a ≠ c ∈ ℚ | c < b
14 7 13 sylbid ⊢ a ∈ ℝ ∧ b ∈ ℝ → a ≠ b → c ∈ ℚ | c < a ≠ c ∈ ℚ | c < b
15 14 necon4d ⊢ a ∈ ℝ ∧ b ∈ ℝ → c ∈ ℚ | c < a = c ∈ ℚ | c < b → a = b
16 breq2 ⊢ a = b → c < a ↔ c < b
17 16 rabbidv ⊢ a = b → c ∈ ℚ | c < a = c ∈ ℚ | c < b
18 15 17 impbid1 ⊢ a ∈ ℝ ∧ b ∈ ℝ → c ∈ ℚ | c < a = c ∈ ℚ | c < b ↔ a = b
19 6 18 dom2 ⊢ 𝒫 ℚ ∈ V → ℝ ≼ 𝒫 ℚ
20 2 19 ax-mp ⊢ ℝ ≼ 𝒫 ℚ