Theorem xpnnen 4927

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 4726 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 4431	. . . 4 |- NN e. V
2	1, 1	xpex 2488	. . 3 |- (NN X. NN) e. V
3		elxp5 2641	. . . . 5 |- (x e. (NN X. NN) <-> (x = <.|^||^|x, U.ran {x}>. /\ (|^||^|x e. NN /\ U.ran {x} e. NN)))
4		nnaddclt 4436	. . . . . . 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 4436	. . . . . . . 8 |- ((|^||^|x e. NN /\ U.ran {x} e. NN) -> (|^||^|x + U.ran {x}) e. NN)
6		2nn 4487	. . . . . . . . 9 |- 2 e. NN
7		nnexpclt 4691	. . . . . . . . 9 |- (((|^||^|x + U.ran {x}) e. NN /\ 2 e. NN) -> ((|^||^|x + U.ran {x})^2) e. NN)
8	6, 7	mpan2 519	. . . . . . . 8 |- ((|^||^|x + U.ran {x}) e. NN -> ((|^||^|x + U.ran {x})^2) e. NN)
9	5, 8	syl 12	. . . . . . 7 |- ((|^||^|x e. NN /\ U.ran {x} e. NN) -> ((|^||^|x + U.ran {x})^2) e. NN)
10		pm3.27 260	. . . . . . 7 |- ((|^||^|x e. NN /\ U.ran {x} e. NN) -> U.ran {x} e. NN)
11	4, 9, 10	sylanc 361	. . . . . 6 |- ((|^||^|x e. NN /\ U.ran {x} e. NN) -> (((|^||^|x + U.ran {x})^2) + U.ran {x}) e. NN)
12	11	adantl 305	. . . . 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 174	. . . 4 |- (x e. (NN X. NN) -> (((|^||^|x + U.ran {x})^2) + U.ran {x}) e. NN)
14		inteq 1968	. . . . . . . . . . . . . . . . . 18 |- (x = <.z, w>. -> |^|x = |^|<.z, w>.)
15	14	inteqd 1970	. . . . . . . . . . . . . . . . 17 |- (x = <.z, w>. -> |^||^|x = |^||^|<.z, w>.)
16		visset 1350	. . . . . . . . . . . . . . . . . 18 |- z e. V
17	16	op1stb 1992	. . . . . . . . . . . . . . . . 17 |- |^||^|<.z, w>. = z
18	15, 17	syl6eq 1140	. . . . . . . . . . . . . . . 16 |- (x = <.z, w>. -> |^||^|x = z)
19		sneq 1816	. . . . . . . . . . . . . . . . . . 19 |- (x = <.z, w>. -> {x} = {<.z, w>.})
20	19	rneqd 2557	. . . . . . . . . . . . . . . . . 18 |- (x = <.z, w>. -> ran {x} = ran {<.z, w>.})
21	20	unieqd 1929	. . . . . . . . . . . . . . . . 17 |- (x = <.z, w>. -> U.ran {x} = U.ran {<.z, w>.})
22		visset 1350	. . . . . . . . . . . . . . . . . 18 |- w e. V
23	16, 22	op2nda 2639	. . . . . . . . . . . . . . . . 17 |- U.ran {<.z, w>.} = w
24	21, 23	syl6eq 1140	. . . . . . . . . . . . . . . 16 |- (x = <.z, w>. -> U.ran {x} = w)
25	18, 24	opreq12d 3014	. . . . . . . . . . . . . . 15 |- (x = <.z, w>. -> (|^||^|x + U.ran {x}) = (z + w))
26	25	opreq1d 3012	. . . . . . . . . . . . . 14 |- (x = <.z, w>. -> ((|^||^|x + U.ran {x})^2) = ((z + w)^2))
27	26, 24	opreq12d 3014	. . . . . . . . . . . . 13 |- (x = <.z, w>. -> (((|^||^|x + U.ran {x})^2) + U.ran {x}) = (((z + w)^2) + w))
28		inteq 1968	. . . . . . . . . . . . . . . . . 18 |- (y = <.v, u>. -> |^|y = |^|<.v, u>.)
29	28	inteqd 1970	. . . . . . . . . . . . . . . . 17 |- (y = <.v, u>. -> |^||^|y = |^||^|<.v, u>.)
30		visset 1350	. . . . . . . . . . . . . . . . . 18 |- v e. V
31	30	op1stb 1992	. . . . . . . . . . . . . . . . 17 |- |^||^|<.v, u>. = v
32	29, 31	syl6eq 1140	. . . . . . . . . . . . . . . 16 |- (y = <.v, u>. -> |^||^|y = v)
33		sneq 1816	. . . . . . . . . . . . . . . . . . 19 |- (y = <.v, u>. -> {y} = {<.v, u>.})
34	33	rneqd 2557	. . . . . . . . . . . . . . . . . 18 |- (y = <.v, u>. -> ran {y} = ran {<.v, u>.})
35	34	unieqd 1929	. . . . . . . . . . . . . . . . 17 |- (y = <.v, u>. -> U.ran {y} = U.ran {<.v, u>.})
36		visset 1350	. . . . . . . . . . . . . . . . . 18 |- u e. V
37	30, 36	op2nda 2639	. . . . . . . . . . . . . . . . 17 |- U.ran {<.v, u>.} = u
38	35, 37	syl6eq 1140	. . . . . . . . . . . . . . . 16 |- (y = <.v, u>. -> U.ran {y} = u)
39	32, 38	opreq12d 3014	. . . . . . . . . . . . . . 15 |- (y = <.v, u>. -> (|^||^|y + U.ran {y}) = (v + u))
40	39	opreq1d 3012	. . . . . . . . . . . . . 14 |- (y = <.v, u>. -> ((|^||^|y + U.ran {y})^2) = ((v + u)^2))
41	40, 38	opreq12d 3014	. . . . . . . . . . . . 13 |- (y = <.v, u>. -> (((|^||^|y + U.ran {y})^2) + U.ran {y}) = (((v + u)^2) + u))
42	27, 41	cleqan12d 1116	. . . . . . . . . . . 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 4726	. . . . . . . . . . . . 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 4541	. . . . . . . . . . . . . 14 |- (z e. NN -> z e. NN0)
45		nnnn0t 4541	. . . . . . . . . . . . . 14 |- (w e. NN -> w e. NN0)
46	44, 45	anim12i 268	. . . . . . . . . . . . 13 |- ((z e. NN /\ w e. NN) -> (z e. NN0 /\ w e. NN0))
47		nnnn0t 4541	. . . . . . . . . . . . . 14 |- (v e. NN -> v e. NN0)
48		nnnn0t 4541	. . . . . . . . . . . . . 14 |- (u e. NN -> u e. NN0)
49	47, 48	anim12i 268	. . . . . . . . . . . . 13 |- ((v e. NN /\ u e. NN) -> (v e. NN0 /\ u e. NN0))
50	43, 46, 49	syl2an 349	. . . . . . . . . . . 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 419	. . . . . . . . . . 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		cleq12 1113	. . . . . . . . . . . . 13 |- ((x = <.z, w>. /\ y = <.v, u>.) -> (x = y <-> <.z, w>. = <.v, u>.))
53	16, 22, 36	opth 1898	. . . . . . . . . . . . 13 |- (<.z, w>. = <.v, u>. <-> (z = v /\ w = u))
54	52, 53	syl6bb 414	. . . . . . . . . . . 12 |- ((x = <.z, w>. /\ y = <.v, u>.) -> (x = y <-> (z = v /\ w = u)))
55	54	adantl 305	. . . . . . . . . . 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 409	. . . . . . . . . 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 301	. . . . . . . . 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 1287	. . . . . . 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}) <-> x = y))))
60	59	r19.23advv 1288	. . . . . 6 |- (E.z e. NN E.w e. NN x = <.z, w>. -> (E.v e. NN E.u e. NN y = <.v, u>. -> ((((|^||^|x + U.ran {x})^2) + U.ran {x