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	⊢ { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑎 } ⊆ ℚ
4	1	elpw2	⊢ ( { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑎 } ∈ 𝒫 ℚ ↔ { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑎 } ⊆ ℚ )
5	3 4	mpbir	⊢ { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑎 } ∈ 𝒫 ℚ
6	5	a1i	⊢ ( 𝑎 ∈ ℝ → { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑎 } ∈ 𝒫 ℚ )
7		lttri2	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( 𝑎 ≠ 𝑏 ↔ ( 𝑎 < 𝑏 ∨ 𝑏 < 𝑎 ) ) )
8		rpnnen3lem	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ 𝑎 < 𝑏 ) → { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑎 } ≠ { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑏 } )
9		rpnnen3lem	⊢ ( ( ( 𝑏 ∈ ℝ ∧ 𝑎 ∈ ℝ ) ∧ 𝑏 < 𝑎 ) → { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑏 } ≠ { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑎 } )
10	9	ancom1s	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ 𝑏 < 𝑎 ) → { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑏 } ≠ { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑎 } )
11	10	necomd	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ 𝑏 < 𝑎 ) → { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑎 } ≠ { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑏 } )
12	8 11	jaodan	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑎 < 𝑏 ∨ 𝑏 < 𝑎 ) ) → { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑎 } ≠ { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑏 } )
13	12	ex	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( ( 𝑎 < 𝑏 ∨ 𝑏 < 𝑎 ) → { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑎 } ≠ { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑏 } ) )
14	7 13	sylbid	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( 𝑎 ≠ 𝑏 → { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑎 } ≠ { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑏 } ) )
15	14	necon4d	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑎 } = { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑏 } → 𝑎 = 𝑏 ) )
16		breq2	⊢ ( 𝑎 = 𝑏 → ( 𝑐 < 𝑎 ↔ 𝑐 < 𝑏 ) )
17	16	rabbidv	⊢ ( 𝑎 = 𝑏 → { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑎 } = { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑏 } )
18	15 17	impbid1	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑎 } = { 𝑐 ∈ ℚ ∣ 𝑐 < 𝑏 } ↔ 𝑎 = 𝑏 ) )
19	6 18	dom2	⊢ ( 𝒫 ℚ ∈ V → ℝ ≼ 𝒫 ℚ )
20	2 19	ax-mp	⊢ ℝ ≼ 𝒫 ℚ