Theorem qnnen 12499

Description: The rational numbers are countably infinite. Corollary 8.1.23 of [AczelRathjen], p. 75. This is Metamath 100 proof #3. (Contributed by Jim Kingdon, 11-Aug-2023.)

Assertion

Ref	Expression
qnnen	|- QQ ~~ NN

Proof of Theorem qnnen

Dummy variables f g p q are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		qdceq 10289	. . 3 |- ( ( p e. QQ /\ q e. QQ ) -> DECID p = q )
2	1	rgen2a 2544	. 2 |- A. p e. QQ A. q e. QQ DECID p = q
3		znnen 12466	. . . . . . . 8 |- ZZ ~~ NN
4		nnex 8966	. . . . . . . . 9 |- NN e. _V
5	4	enref 6799	. . . . . . . 8 |- NN ~~ NN
6		xpen 6881	. . . . . . . 8 |- ( ( ZZ ~~ NN /\ NN ~~ NN ) -> ( ZZ X. NN ) ~~ ( NN X. NN ) )
7	3, 5, 6	mp2an 426	. . . . . . 7 |- ( ZZ X. NN ) ~~ ( NN X. NN )
8		xpnnen 12462	. . . . . . 7 |- ( NN X. NN ) ~~ NN
9	7, 8	entri 6820	. . . . . 6 |- ( ZZ X. NN ) ~~ NN
10		nnenom 10477	. . . . . 6 |- NN ~~ om
11	9, 10	entri 6820	. . . . 5 |- ( ZZ X. NN ) ~~ om
12	11	ensymi 6816	. . . 4 |- om ~~ ( ZZ X. NN )
13		bren 6781	. . . 4 |- ( om ~~ ( ZZ X. NN ) <-> E. g g : om -1-1-onto-> ( ZZ X. NN ) )
14	12, 13	mpbi 145	. . 3 |- E. g g : om -1-1-onto-> ( ZZ X. NN )
15		f1ofo 5494	. . . . 5 |- ( g : om -1-1-onto-> ( ZZ X. NN ) -> g : om -onto-> ( ZZ X. NN ) )
16		divfnzn 9663	. . . . . . . . 9 |- ( / |` ( ZZ X. NN ) ) Fn ( ZZ X. NN )
17		fnfun 5339	. . . . . . . . 9 |- ( ( / |` ( ZZ X. NN ) ) Fn ( ZZ X. NN ) -> Fun ( / |` ( ZZ X. NN ) ) )
18	16, 17	ax-mp 5	. . . . . . . 8 |- Fun ( / |` ( ZZ X. NN ) )
19		fndm 5341	. . . . . . . . 9 |- ( ( / |` ( ZZ X. NN ) ) Fn ( ZZ X. NN ) -> dom ( / |` ( ZZ X. NN ) ) = ( ZZ X. NN ) )
20		eqimss2 3229	. . . . . . . . 9 |- ( dom ( / |` ( ZZ X. NN ) ) = ( ZZ X. NN ) -> ( ZZ X. NN ) C_ dom ( / |` ( ZZ X. NN ) ) )
21	16, 19, 20	mp2b 8	. . . . . . . 8 |- ( ZZ X. NN ) C_ dom ( / |` ( ZZ X. NN ) )
22		fores 5473	. . . . . . . 8 |- ( ( Fun ( / |` ( ZZ X. NN ) ) /\ ( ZZ X. NN ) C_ dom ( / |` ( ZZ X. NN ) ) ) -> ( ( / |` ( ZZ X. NN ) ) |` ( ZZ X. NN ) ) : ( ZZ X. NN ) -onto-> ( ( / |` ( ZZ X. NN ) ) " ( ZZ X. NN ) ) )
23	18, 21, 22	mp2an 426	. . . . . . 7 |- ( ( / |` ( ZZ X. NN ) ) |` ( ZZ X. NN ) ) : ( ZZ X. NN ) -onto-> ( ( / |` ( ZZ X. NN ) ) " ( ZZ X. NN ) )
24		resima 4965	. . . . . . . . 9 |- ( ( / |` ( ZZ X. NN ) ) " ( ZZ X. NN ) ) = ( / " ( ZZ X. NN ) )
25		df-q 9662	. . . . . . . . 9 |- QQ = ( / " ( ZZ X. NN ) )
26	24, 25	eqtr4i 2213	. . . . . . . 8 |- ( ( / |` ( ZZ X. NN ) ) " ( ZZ X. NN ) ) = QQ
27		foeq3 5462	. . . . . . . 8 |- ( ( ( / |` ( ZZ X. NN ) ) " ( ZZ X. NN ) ) = QQ -> ( ( ( / |` ( ZZ X. NN ) ) |` ( ZZ X. NN ) ) : ( ZZ X. NN ) -onto-> ( ( / |` ( ZZ X. NN ) ) " ( ZZ X. NN ) ) <-> ( ( / |` ( ZZ X. NN ) ) |` ( ZZ X. NN ) ) : ( ZZ X. NN ) -onto-> QQ ) )
28	26, 27	ax-mp 5	. . . . . . 7 |- ( ( ( / |` ( ZZ X. NN ) ) |` ( ZZ X. NN ) ) : ( ZZ X. NN ) -onto-> ( ( / |` ( ZZ X. NN ) ) " ( ZZ X. NN ) ) <-> ( ( / |` ( ZZ X. NN ) ) |` ( ZZ X. NN ) ) : ( ZZ X. NN ) -onto-> QQ )
29	23, 28	mpbi 145	. . . . . 6 |- ( ( / |` ( ZZ X. NN ) ) |` ( ZZ X. NN ) ) : ( ZZ X. NN ) -onto-> QQ
30		foco 5474	. . . . . 6 |- ( ( ( ( / |` ( ZZ X. NN ) ) |` ( ZZ X. NN ) ) : ( ZZ X. NN ) -onto-> QQ /\ g : om -onto-> ( ZZ X. NN ) ) -> ( ( ( / |` ( ZZ X. NN ) ) |` ( ZZ X. NN ) ) o. g ) : om -onto-> QQ )
31	29, 30	mpan 424	. . . . 5 |- ( g : om -onto-> ( ZZ X. NN ) -> ( ( ( / |` ( ZZ X. NN ) ) |` ( ZZ X. NN ) ) o. g ) : om -onto-> QQ )
32		zex 9303	. . . . . . . . 9 |- ZZ e. _V
33	32, 4	xpex 4766	. . . . . . . 8 |- ( ZZ X. NN ) e. _V
34		resfunexg 5765	. . . . . . . 8 |- ( ( Fun ( / |` ( ZZ X. NN ) ) /\ ( ZZ X. NN ) e. _V ) -> ( ( / |` ( ZZ X. NN ) ) |` ( ZZ X. NN ) ) e. _V )
35	18, 33, 34	mp2an 426	. . . . . . 7 |- ( ( / |` ( ZZ X. NN ) ) |` ( ZZ X. NN ) ) e. _V
36		vex 2759	. . . . . . 7 |- g e. _V
37	35, 36	coex 5199	. . . . . 6 |- ( ( ( / |` ( ZZ X. NN ) ) |` ( ZZ X. NN ) ) o. g ) e. _V
38		foeq1 5460	. . . . . 6 |- ( f = ( ( ( / |` ( ZZ X. NN ) ) |` ( ZZ X. NN ) ) o. g ) -> ( f : om -onto-> QQ <-> ( ( ( / |` ( ZZ X. NN ) ) |` ( ZZ X. NN ) ) o. g ) : om -onto-> QQ ) )
39	37, 38	spcev 2851	. . . . 5 |- ( ( ( ( / |` ( ZZ X. NN ) ) |` ( ZZ X. NN ) ) o. g ) : om -onto-> QQ -> E. f f : om -onto-> QQ )
40	15, 31, 39	3syl 17	. . . 4 |- ( g : om -1-1-onto-> ( ZZ X. NN ) -> E. f f : om -onto-> QQ )
41	40	exlimiv 1609	. . 3 |- ( E. g g : om -1-1-onto-> ( ZZ X. NN ) -> E. f f : om -onto-> QQ )
42	14, 41	ax-mp 5	. 2 |- E. f f : om -onto-> QQ
43	10	ensymi 6816	. . 3 |- om ~~ NN
44		qex 9674	. . . 4 |- QQ e. _V
45		nnssq 9671	. . . 4 |- NN C_ QQ
46		ssdomg 6812	. . . 4 |- ( QQ e. _V -> ( NN C_ QQ -> NN ~<_ QQ ) )
47	44, 45, 46	mp2 16	. . 3 |- NN ~<_ QQ
48		endomtr 6824	. . 3 |- ( ( om ~~ NN /\ NN ~<_ QQ ) -> om ~<_ QQ )
49	43, 47, 48	mp2an 426	. 2 |- om ~<_ QQ
50		ctinf 12498	. 2 |- ( QQ ~~ NN <-> ( A. p e. QQ A. q e. QQ DECID p = q /\ E. f f : om -onto-> QQ /\ om ~<_ QQ ) )
51	2, 42, 49, 50	mpbir3an 1181	1 |- QQ ~~ NN

Syntax hints:   <-> wb 105  DECID wdc 835   = wceq 1364   E.wex 1503   e. wcel 2160   A.wral 2468   _Vcvv 2756   C_ wss 3148   class class class wbr 4025   omcom 4614   X. cxp 4649   dom cdm 4651   |` cres 4653   "cima 4654   o. ccom 4655   Fun wfun 5236   Fn wfn 5237   -onto->wfo 5240   -1-1-onto->wf1o 5241   ~~ cen 6772   ~<_ cdom 6773   / cdiv 8670   NNcn 8960   ZZcz 9294   QQcq 9661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-coll 4140  ax-sep 4143  ax-nul 4151  ax-pow 4199  ax-pr 4234  ax-un 4458  ax-setind 4561  ax-iinf 4612  ax-cnex 7942  ax-resscn 7943  ax-1cn 7944  ax-1re 7945  ax-icn 7946  ax-addcl 7947  ax-addrcl 7948  ax-mulcl 7949  ax-mulrcl 7950  ax-addcom 7951  ax-mulcom 7952  ax-addass 7953  ax-mulass 7954  ax-distr 7955  ax-i2m1 7956  ax-0lt1 7957  ax-1rid 7958  ax-0id 7959  ax-rnegex 7960  ax-precex 7961  ax-cnre 7962  ax-pre-ltirr 7963  ax-pre-ltwlin 7964  ax-pre-lttrn 7965  ax-pre-apti 7966  ax-pre-ltadd 7967  ax-pre-mulgt0 7968  ax-pre-mulext 7969  ax-arch 7970

This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-xor 1387  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-nel 2456  df-ral 2473  df-rex 2474  df-reu 2475  df-rmo 2476  df-rab 2477  df-v 2758  df-sbc 2982  df-csb 3077  df-dif 3150  df-un 3152  df-in 3154  df-ss 3161  df-nul 3442  df-if 3554  df-pw 3599  df-sn 3620  df-pr 3621  df-op 3623  df-uni 3832  df-int 3867  df-iun 3910  df-br 4026  df-opab 4087  df-mpt 4088  df-tr 4124  df-id 4318  df-po 4321  df-iso 4322  df-iord 4391  df-on 4393  df-ilim 4394  df-suc 4396  df-iom 4615  df-xp 4657  df-rel 4658  df-cnv 4659  df-co 4660  df-dm 4661  df-rn 4662  df-res 4663  df-ima 4664  df-iota 5203  df-fun 5244  df-fn 5245  df-f 5246  df-f1 5247  df-fo 5248  df-f1o 5249  df-fv 5250  df-riota 5859  df-ov 5907  df-oprab 5908  df-mpo 5909  df-1st 6173  df-2nd 6174  df-recs 6338  df-frec 6424  df-1o 6449  df-er 6567  df-pm 6685  df-en 6775  df-dom 6776  df-fin 6777  df-dju 7076  df-inl 7085  df-inr 7086  df-case 7122  df-pnf 8035  df-mnf 8036  df-xr 8037  df-ltxr 8038  df-le 8039  df-sub 8171  df-neg 8172  df-reap 8573  df-ap 8580  df-div 8671  df-inn 8961  df-2 9019  df-n0 9218  df-z 9295  df-uz 9570  df-q 9662  df-rp 9696  df-fz 10051  df-fl 10313  df-mod 10366  df-seqfrec 10491  df-exp 10566  df-dvds 11842

This theorem is referenced by: (None)