qnnen

Description: The rational numbers are countable. This proof does not use the Axiom of Choice, even though it uses an onto function, because the base set ( ZZ X. NN ) is numerable. Exercise 2 of Enderton p. 133. For purposes of the Metamath 100 list, we are considering Mario Carneiro's revision as the date this proof was completed. This is Metamath 100 proof #3. (Contributed by NM, 31-Jul-2004) (Revised by Mario Carneiro, 3-Mar-2013)

		Ref	Expression
	Assertion	qnnen	\|- QQ ~~ NN

Proof

Step	Hyp	Ref	Expression
1		omelon	\|- _om e. On
2		nnenom	\|- NN ~~ _om
3	2	ensymi	\|- _om ~~ NN
4		isnumi	\|- ( ( _om e. On /\ _om ~~ NN ) -> NN e. dom card )
5	1 3 4	mp2an	\|- NN e. dom card
6		znnen	\|- ZZ ~~ NN
7		ennum	\|- ( ZZ ~~ NN -> ( ZZ e. dom card <-> NN e. dom card ) )
8	6 7	ax-mp	\|- ( ZZ e. dom card <-> NN e. dom card )
9	5 8	mpbir	\|- ZZ e. dom card
10		xpnum	\|- ( ( ZZ e. dom card /\ NN e. dom card ) -> ( ZZ X. NN ) e. dom card )
11	9 5 10	mp2an	\|- ( ZZ X. NN ) e. dom card
12		eqid	\|- ( x e. ZZ , y e. NN \|-> ( x / y ) ) = ( x e. ZZ , y e. NN \|-> ( x / y ) )
13		ovex	\|- ( x / y ) e. _V
14	12 13	fnmpoi	\|- ( x e. ZZ , y e. NN \|-> ( x / y ) ) Fn ( ZZ X. NN )
15	12	rnmpo	\|- ran ( x e. ZZ , y e. NN \|-> ( x / y ) ) = { z \| E. x e. ZZ E. y e. NN z = ( x / y ) }
16		elq	\|- ( z e. QQ <-> E. x e. ZZ E. y e. NN z = ( x / y ) )
17	16	eqabi	\|- QQ = { z \| E. x e. ZZ E. y e. NN z = ( x / y ) }
18	15 17	eqtr4i	\|- ran ( x e. ZZ , y e. NN \|-> ( x / y ) ) = QQ
19		df-fo	\|- ( ( x e. ZZ , y e. NN \|-> ( x / y ) ) : ( ZZ X. NN ) -onto-> QQ <-> ( ( x e. ZZ , y e. NN \|-> ( x / y ) ) Fn ( ZZ X. NN ) /\ ran ( x e. ZZ , y e. NN \|-> ( x / y ) ) = QQ ) )
20	14 18 19	mpbir2an	\|- ( x e. ZZ , y e. NN \|-> ( x / y ) ) : ( ZZ X. NN ) -onto-> QQ
21		fodomnum	\|- ( ( ZZ X. NN ) e. dom card -> ( ( x e. ZZ , y e. NN \|-> ( x / y ) ) : ( ZZ X. NN ) -onto-> QQ -> QQ ~<_ ( ZZ X. NN ) ) )
22	11 20 21	mp2	\|- QQ ~<_ ( ZZ X. NN )
23		nnex	\|- NN e. _V
24	23	enref	\|- NN ~~ NN
25		xpen	\|- ( ( ZZ ~~ NN /\ NN ~~ NN ) -> ( ZZ X. NN ) ~~ ( NN X. NN ) )
26	6 24 25	mp2an	\|- ( ZZ X. NN ) ~~ ( NN X. NN )
27		xpnnen	\|- ( NN X. NN ) ~~ NN
28	26 27	entri	\|- ( ZZ X. NN ) ~~ NN
29		domentr	\|- ( ( QQ ~<_ ( ZZ X. NN ) /\ ( ZZ X. NN ) ~~ NN ) -> QQ ~<_ NN )
30	22 28 29	mp2an	\|- QQ ~<_ NN
31		qex	\|- QQ e. _V
32		nnssq	\|- NN C_ QQ
33		ssdomg	\|- ( QQ e. _V -> ( NN C_ QQ -> NN ~<_ QQ ) )
34	31 32 33	mp2	\|- NN ~<_ QQ
35		sbth	\|- ( ( QQ ~<_ NN /\ NN ~<_ QQ ) -> QQ ~~ NN )
36	30 34 35	mp2an	\|- QQ ~~ NN

Metamath Proof Explorer

Theorem qnnen

Proof