Theorem xpnnen 7441

Description: The cross product of the set of natural numbers with itself is equinumerous to the set of natural numbers. The key idea is to use nn0opth2t 6598 to show that the mapping from natural numbers z and w to ((z + w)^2) + w is one-to-one.

Assertion

Ref	Expression
xpnnen	|- (NN X. NN) ~~ NN

Proof of Theorem xpnnen

Step	Hyp	Ref	Expression
1		nnex 5881	. . . 4 |- NN e. V
2	1, 1	xpex 3250	. . 3 |- (NN X. NN) e. V
3		elxp5 3440	. . . . 5 |- (x e. (NN X. NN) <-> (x = <.|^||^|x, U.ran { x}>. /\ (|^||^|x e. NN /\ U.ran { x} e. NN)))
4		nnaddclt 5888	. . . . . . 7 |- ((((|^||^|x + U.ran { x})^2) e. NN /\ U.ran { x} e. NN) -> (((|^||^|x + U.ran { x})^2) + U.ran { x}) e. NN)
5		nnaddclt 5888	. . . . . . . 8 |- ((|^||^|x e. NN /\ U.ran { x} e. NN) -> (|^||^|x + U.ran { x}) e. NN)
6		2nn0 6062	. . . . . . . . 9 |- 2 e. NN0
7		nnexpclt 6508	. . . . . . . . 9 |- (((|^||^|x + U.ran { x}) e. NN /\ 2 e. NN0) -> ((|^||^|x + U.ran { x})^2) e. NN)
8	6, 7	mpan2 694	. . . . . . . 8 |- ((|^||^|x + U.ran { x}) e. NN -> ((|^||^|x + U.ran { x})^2) e. NN)
9	5, 8	syl 10	. . . . . . 7 |- ((|^||^|x e. NN /\ U.ran { x} e. NN) -> ((|^||^|x + U.ran { x})^2) e. NN)
10		pm3.27 323	. . . . . . 7 |- ((|^||^|x e. NN /\ U.ran { x} e. NN) -> U.ran { x} e. NN)
11	4, 9, 10	sylanc 471	. . . . . 6 |- ((|^||^|x e. NN /\ U.ran { x} e. NN) -> (((|^||^|x + U.ran { x})^2) + U.ran { x}) e. NN)
12	11	adantl 388	. . . . 5 |- ((x = <.|^||^|x, U.ran { x}>. /\ (|^||^|x e. NN /\ U.ran { x} e. NN)) -> (((|^||^|x + U.ran { x})^2) + U.ran { x}) e. NN)
13	3, 12	sylbi 199	. . . 4 |- (x e. (NN X. NN) -> (((|^||^|x + U.ran { x})^2) + U.ran { x}) e. NN)
14		inteq 2526	. . . . . . . . . . . . . . . . . 18 |- (x = <.z, w>. -> |^|x = |^|<.z, w>.)
15	14	inteqd 2528	. . . . . . . . . . . . . . . . 17 |- (x = <.z, w>. -> |^||^|x = |^||^|<.z, w>.)
16		visset 1804	. . . . . . . . . . . . . . . . . 18 |- z e. V
17	16	op1stb 2903	. . . . . . . . . . . . . . . . 17 |- |^||^|<.z, w>. = z
18	15, 17	syl6eq 1515	. . . . . . . . . . . . . . . 16 |- (x = <.z, w>. -> |^||^|x = z)
19		sneq 2407	. . . . . . . . . . . . . . . . . . 19 |- (x = <.z, w>. -> {x} = {<.z, w>.})
20	19	rneqd 3330	. . . . . . . . . . . . . . . . . 18 |- (x = <.z, w>. -> ran { x} = ran {<.z, w>.})
21	20	unieqd 2502	. . . . . . . . . . . . . . . . 17 |- (x = <.z, w>. -> U.ran { x} = U.ran {<.z, w>.})
22		visset 1804	. . . . . . . . . . . . . . . . . 18 |- w e. V
23	16, 22	op2nda 3438	. . . . . . . . . . . . . . . . 17 |- U.ran {<.z, w>.} = w
24	21, 23	syl6eq 1515	. . . . . . . . . . . . . . . 16 |- (x = <.z, w>. -> U.ran { x} = w)
25	18, 24	opreq12d 3963	. . . . . . . . . . . . . . 15 |- (x = <.z, w>. -> (|^||^|x + U.ran { x}) = (z + w))
26	25	opreq1d 3960	. . . . . . . . . . . . . 14 |- (x = <.z, w>. -> ((|^||^|x + U.ran { x})^2) = ((z + w)^2))
27	26, 24	opreq12d 3963	. . . . . . . . . . . . 13 |- (x = <.z, w>. -> (((|^||^|x + U.ran { x})^2) + U.ran { x}) = (((z + w)^2) + w))
28		inteq 2526	. . . . . . . . . . . . . . . . . 18 |- (y = <.v, u>. -> |^|y = |^|<.v, u>.)
29	28	inteqd 2528	. . . . . . . . . . . . . . . . 17 |- (y = <.v, u>. -> |^||^|y = |^||^|<.v, u>.)
30		visset 1804	. . . . . . . . . . . . . . . . . 18 |- v e. V
31	30	op1stb 2903	. . . . . . . . . . . . . . . . 17 |- |^||^|<.v, u>. = v
32	29, 31	syl6eq 1515	. . . . . . . . . . . . . . . 16 |- (y = <.v, u>. -> |^||^|y = v)
33		sneq 2407	. . . . . . . . . . . . . . . . . . 19 |- (y = <.v, u>. -> {y} = {<.v, u>.})
34	33	rneqd 3330	. . . . . . . . . . . . . . . . . 18 |- (y = <.v, u>. -> ran { y} = ran {<.v, u>.})
35	34	unieqd 2502	. . . . . . . . . . . . . . . . 17 |- (y = <.v, u>. -> U.ran { y} = U.ran {<.v, u>.})
36		visset 1804	. . . . . . . . . . . . . . . . . 18 |- u e. V
37	30, 36	op2nda 3438	. . . . . . . . . . . . . . . . 17 |- U.ran {<.v, u>.} = u
38	35, 37	syl6eq 1515	. . . . . . . . . . . . . . . 16 |- (y = <.v, u>. -> U.ran { y} = u)
39	32, 38	opreq12d 3963	. . . . . . . . . . . . . . 15 |- (y = <.v, u>. -> (|^||^|y + U.ran { y}) = (v + u))
40	39	opreq1d 3960	. . . . . . . . . . . . . 14 |- (y = <.v, u>. -> ((|^||^|y + U.ran { y})^2) = ((v + u)^2))
41	40, 38	opreq12d 3963	. . . . . . . . . . . . 13 |- (y = <.v, u>. -> (((|^||^|y + U.ran { y})^2) + U.ran { y}) = (((v + u)^2) + u))
42	27, 41	eqeqan12d 1482	. . . . . . . . . . . 12 |- ((x = <.z, w>. /\ y = <.v, u>.) -> ((((|^||^|x + U.ran { x})^2) + U.ran { x}) = (((|^||^|y + U.ran { y})^2) + U.ran { y}) <-> (((z + w)^2) + w) = (((v + u)^2) + u)))
43		nn0opth2t 6598	. . . . . . . . . . . . 13 |- (((z e. NN0 /\ w e. NN0) /\ (v e. NN0 /\ u e. NN0)) -> ((((z + w)^2) + w) = (((v + u)^2) + u) <-> (z = v /\ w = u)))
44		nnnn0t 6053	. . . . . . . . . . . . . 14 |- (z e. NN -> z e. NN0)
45		nnnn0t 6053	. . . . . . . . . . . . . 14 |- (w e. NN -> w e. NN0)
46	44, 45	anim12i 333	. . . . . . . . . . . . 13 |- ((z e. NN /\ w e. NN) -> (z e. NN0 /\ w e. NN0))
47		nnnn0t 6053	. . . . . . . . . . . . . 14 |- (v e. NN -> v e. NN0)
48		nnnn0t 6053	. . . . . . . . . . . . . 14 |- (u e. NN -> u e. NN0)
49	47, 48	anim12i 333	. . . . . . . . . . . . 13 |- ((v e. NN /\ u e. NN) -> (v e. NN0 /\ u e. NN0))
50	43, 46, 49	syl2an 454	. . . . . . . . . . . 12 |- (((z e. NN /\ w e. NN) /\ (v e. NN /\ u e. NN)) -> ((((z + w)^2) + w) = (((v + u)^2) + u) <-> (z = v /\ w = u)))
51	42, 50	sylan9bbr 539	. . . . . . . . . . 11 |- ((((z e. NN /\ w e. NN) /\ (v e. NN /\ u e. NN)) /\ (x = <.z, w>. /\ y = <.v, u>.)) -> ((((|^||^|x + U.ran { x})^2) + U.ran { x}) = (((|^||^|y + U.ran { y})^2) + U.ran { y}) <-> (z = v /\ w = u)))
52		eqeq12 1479	. . . . . . . . . . . . 13 |- ((x = <.z, w>. /\ y = <.v, u>.) -> (x = y <-> <.z, w>. = <.v, u>.))
53	16, 22, 36	opth 2777	. . . . . . . . . . . . 13 |- (<.z, w>. = <.v, u>. <-> (z = v /\ w = u))
54	52, 53	syl6bb 534	. . . . . . . . . . . 12 |- ((x = <.z, w>. /\ y = <.v, u>.) -> (x = y <-> (z = v /\ w = u)))
55	54	adantl 388	. . . . . . . . . . 11 |- ((((z e. NN /\ w e. NN) /\ (v e. NN /\ u e. NN)) /\ (x = <.z, w>. /\ y = <.v, u>.)) -> (x = y <-> (z = v /\ w = u)))
56	51, 55	bitr4d 529	. . . . . . . . . 10 |- ((((z e. NN /\ w e. NN) /\ (v e. NN /\ u e. NN)) /\ (x = <.z, w>. /\ y = <.v, u>.)) -> ((((|^||^|x + U.ran { x})^2) + U.ran { x}) = (((|^||^|y + U.ran { y})^2) + U.ran { y}) <-> x = y))
57	56	exp43 384	. . . . . . . . 9 |- ((z e. NN /\ w e. NN) -> ((v e. NN /\ u e. NN) -> (x = <.z, w>. -> (y = <.v, u>. -> ((((|^||^|x + U.ran { x})^2) + U.ran { x}) = (((|^||^|y + U.ran { y})^2) + U.ran { y}) <-> x = y)))))
58	57	com23 32	. . . . . . . 8 |- ((z e. NN /\ w e. NN) -> (x = <.z, w>. -> ((v e. NN /\ u e. NN) -> (y = <.v, u>. -> ((((|^||^|x + U.ran { x})^2) + U.ran { x}) = (((|^||^|y + U.ran { y})^2) + U.ran { y}) <-> x = y)))))
59	58	r19.23aivv 1740	. . . . . . 7 |- (E.z e. NN E.w e. NN x = <.z, w>. -> ((v e. NN /\ u e. NN) -> (y = <.v, u>. -> ((((|^||^|x + U.ran { x})^2) + U.ran { x}) = (((|^||^|y + U.ran { y})^2) + U.ran { y}) <->