Theorem rpnnen3

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

	Ref	Expression
Assertion	rpnnen3	|- RR ~<_ ~P QQ

Proof

Step	Hyp	Ref	Expression
1		qex	|- QQ e. _V
2	1	pwex	|- ~P QQ e. _V
3		ssrab2	|- { c e. QQ | c < a } C_ QQ
4	1	elpw2	|- ( { c e. QQ | c < a } e. ~P QQ <-> { c e. QQ | c < a } C_ QQ )
5	3 4	mpbir	|- { c e. QQ | c < a } e. ~P QQ
6	5	a1i	|- ( a e. RR -> { c e. QQ | c < a } e. ~P QQ )
7		lttri2	|- ( ( a e. RR /\ b e. RR ) -> ( a =/= b <-> ( a < b \/ b < a ) ) )
8		rpnnen3lem	|- ( ( ( a e. RR /\ b e. RR ) /\ a < b ) -> { c e. QQ | c < a } =/= { c e. QQ | c < b } )
9		rpnnen3lem	|- ( ( ( b e. RR /\ a e. RR ) /\ b < a ) -> { c e. QQ | c < b } =/= { c e. QQ | c < a } )
10	9	ancom1s	|- ( ( ( a e. RR /\ b e. RR ) /\ b < a ) -> { c e. QQ | c < b } =/= { c e. QQ | c < a } )
11	10	necomd	|- ( ( ( a e. RR /\ b e. RR ) /\ b < a ) -> { c e. QQ | c < a } =/= { c e. QQ | c < b } )
12	8 11	jaodan	|- ( ( ( a e. RR /\ b e. RR ) /\ ( a < b \/ b < a ) ) -> { c e. QQ | c < a } =/= { c e. QQ | c < b } )
13	12	ex	|- ( ( a e. RR /\ b e. RR ) -> ( ( a < b \/ b < a ) -> { c e. QQ | c < a } =/= { c e. QQ | c < b } ) )
14	7 13	sylbid	|- ( ( a e. RR /\ b e. RR ) -> ( a =/= b -> { c e. QQ | c < a } =/= { c e. QQ | c < b } ) )
15	14	necon4d	|- ( ( a e. RR /\ b e. RR ) -> ( { c e. QQ | c < a } = { c e. QQ | c < b } -> a = b ) )
16		breq2	|- ( a = b -> ( c < a <-> c < b ) )
17	16	rabbidv	|- ( a = b -> { c e. QQ | c < a } = { c e. QQ | c < b } )
18	15 17	impbid1	|- ( ( a e. RR /\ b e. RR ) -> ( { c e. QQ | c < a } = { c e. QQ | c < b } <-> a = b ) )
19	6 18	dom2	|- ( ~P QQ e. _V -> RR ~<_ ~P QQ )
20	2 19	ax-mp	|- RR ~<_ ~P QQ