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 ⊢ℝ≼𝒫ℚ