Theorem nneneq 4498

Description: Two equinumerous natural numbers are equal. Proposition 10.20 of [TakeutiZaring] p. 90 and its converse. Also compare Corollary 6E of [Enderton] p. 136.

Assertion

Ref	Expression
nneneq	|- ((A e. om /\ B e. om) -> (A ~~ B <-> A = B))

Proof of Theorem nneneq

Step	Hyp	Ref	Expression
1		breq2 2618	. . . . . 6 |- (z = B -> (A ~~ z <-> A ~~ B))
2		eqeq2 1481	. . . . . 6 |- (z = B -> (A = z <-> A = B))
3	1, 2	imbi12d 625	. . . . 5 |- (z = B -> ((A ~~ z -> A = z) <-> (A ~~ B -> A = B)))
4	3	rcla4v 1869	. . . 4 |- (B e. om -> (A.z e. om (A ~~ z -> A = z) -> (A ~~ B -> A = B)))
5		breq1 2617	. . . . . . 7 |- (x = (/) -> (x ~~ z <-> (/) ~~ z))
6		eqeq1 1478	. . . . . . 7 |- (x = (/) -> (x = z <-> (/) = z))
7	5, 6	imbi12d 625	. . . . . 6 |- (x = (/) -> ((x ~~ z -> x = z) <-> ((/) ~~ z -> (/) = z)))
8	7	ralbidv 1660	. . . . 5 |- (x = (/) -> (A.z e. om (x ~~ z -> x = z) <-> A.z e. om ((/) ~~ z -> (/) = z)))
9		breq1 2617	. . . . . . 7 |- (x = y -> (x ~~ z <-> y ~~ z))
10		eqeq1 1478	. . . . . . 7 |- (x = y -> (x = z <-> y = z))
11	9, 10	imbi12d 625	. . . . . 6 |- (x = y -> ((x ~~ z -> x = z) <-> (y ~~ z -> y = z)))
12	11	ralbidv 1660	. . . . 5 |- (x = y -> (A.z e. om (x ~~ z -> x = z) <-> A.z e. om (y ~~ z -> y = z)))
13		breq1 2617	. . . . . . 7 |- (x = suc y -> (x ~~ z <-> suc y ~~ z))
14		eqeq1 1478	. . . . . . 7 |- (x = suc y -> (x = z <-> suc y = z))
15	13, 14	imbi12d 625	. . . . . 6 |- (x = suc y -> ((x ~~ z -> x = z) <-> (suc y ~~ z -> suc y = z)))
16	15	ralbidv 1660	. . . . 5 |- (x = suc y -> (A.z e. om (x ~~ z -> x = z) <-> A.z e. om (suc y ~~ z -> suc y = z)))
17		breq1 2617	. . . . . . 7 |- (x = A -> (x ~~ z <-> A ~~ z))
18		eqeq1 1478	. . . . . . 7 |- (x = A -> (x = z <-> A = z))
19	17, 18	imbi12d 625	. . . . . 6 |- (x = A -> ((x ~~ z -> x = z) <-> (A ~~ z -> A = z)))
20	19	ralbidv 1660	. . . . 5 |- (x = A -> (A.z e. om (x ~~ z -> x = z) <-> A.z e. om (A ~~ z -> A = z)))
21		visset 1809	. . . . . . . . 9 |- z e. V
22	21	ensym 4399	. . . . . . . 8 |- ((/) ~~ z -> z ~~ (/))
23		en0 4410	. . . . . . . . 9 |- (z ~~ (/) <-> z = (/))
24		eqcom 1474	. . . . . . . . 9 |- (z = (/) <-> (/) = z)
25	23, 24	bitr 173	. . . . . . . 8 |- (z ~~ (/) <-> (/) = z)
26	22, 25	sylib 198	. . . . . . 7 |- ((/) ~~ z -> (/) = z)
27	26	a1i 8	. . . . . 6 |- (z e. om -> ((/) ~~ z -> (/) = z))
28	27	rgen 1695	. . . . 5 |- A.z e. om ((/) ~~ z -> (/) = z)
29		en0 4410	. . . . . . . . . . . . 13 |- (suc y ~~ (/) <-> suc y = (/))
30		breq2 2618	. . . . . . . . . . . . . 14 |- (w = (/) -> (suc y ~~ w <-> suc y ~~ (/)))
31		eqeq2 1481	. . . . . . . . . . . . . 14 |- (w = (/) -> (suc y = w <-> suc y = (/)))
32	30, 31	bibi12d 628	. . . . . . . . . . . . 13 |- (w = (/) -> ((suc y ~~ w <-> suc y = w) <-> (suc y ~~ (/) <-> suc y = (/))))
33	29, 32	mpbiri 194	. . . . . . . . . . . 12 |- (w = (/) -> (suc y ~~ w <-> suc y = w))
34	33	biimpd 153	. . . . . . . . . . 11 |- (w = (/) -> (suc y ~~ w -> suc y = w))
35	34	a1i 8	. . . . . . . . . 10 |- ((y e. om /\ A.z e. om (y ~~ z -> y = z)) -> (w = (/) -> (suc y ~~ w -> suc y = w)))
36		ax-17 969	. . . . . . . . . . . 12 |- (y e. om -> A.z y e. om)
37		hbra1 1684	. . . . . . . . . . . 12 |- (A.z e. om (y ~~ z -> y = z) -> A.zA.z e. om (y ~~ z -> y = z))
38	36, 37	hban 1007	. . . . . . . . . . 11 |- ((y e. om /\ A.z e. om (y ~~ z -> y = z)) -> A.z(y e. om /\ A.z e. om (y ~~ z -> y = z)))
39		ax-17 969	. . . . . . . . . . 11 |- ((suc y ~~ w -> suc y = w) -> A.z(suc y ~~ w -> suc y = w))
40		visset 1809	. . . . . . . . . . . . . . . . . . 19 |- y e. V
41	40, 21	phplem4 4497	. . . . . . . . . . . . . . . . . 18 |- ((y e. om /\ z e. om) -> (suc y ~~ suc z -> y ~~ z))
42	41	imim1d 28	. . . . . . . . . . . . . . . . 17 |- ((y e. om /\ z e. om) -> ((y ~~ z -> y = z) -> (suc y ~~ suc z -> y = z)))
43	42	ex 373	. . . . . . . . . . . . . . . 16 |- (y e. om -> (z e. om -> ((y ~~ z -> y = z) -> (suc y ~~ suc z -> y = z))))
44	43	a2d 13	. . . . . . . . . . . . . . 15 |- (y e. om -> ((z e. om -> (y ~~ z -> y = z)) -> (z e. om -> (suc y ~~ suc z -> y = z))))
45		ra4 1691	. . . . . . . . . . . . . . 15 |- (A.z e. om (y ~~ z -> y = z) -> (z e. om -> (y ~~ z -> y = z)))
46	44, 45	syl5 21	. . . . . . . . . . . . . 14 |- (y e. om -> (A.z e. om (y ~~ z -> y = z) -> (z e. om -> (suc y ~~ suc z -> y = z))))
47	46	imp 350	. . . . . . . . . . . . 13 |- ((y e. om /\ A.z e. om (y ~~ z -> y = z)) -> (z e. om -> (suc y ~~ suc z -> y = z)))
48		suceq 3029	. . . . . . . . . . . . 13 |- (y = z -> suc y = suc z)
49	47, 48	syl8 24	. . . . . . . . . . . 12 |- ((y e. om /\ A.z e. om (y ~~ z -> y = z)) -> (z e. om -> (suc y ~~ suc z -> suc y = suc z)))
50		breq2 2618	. . . . . . . . . . . . . 14 |- (w = suc z -> (suc y ~~ w <-> suc y ~~ suc z))
51		eqeq2 1481	. . . . . . . . . . . . . 14 |- (w = suc z -> (suc y = w <-> suc y = suc z))
52	50, 51	imbi12d 625	. . . . . . . . . . . . 13 |- (w = suc z -> ((suc y ~~ w -> suc y = w) <-> (suc y ~~ suc z -> suc y = suc z)))
53	52	biimprcd 156	. . . . . . . . . . . 12 |- ((suc y ~~ suc z -> suc y = suc z) -> (w = suc z -> (suc y ~~ w -> suc y = w)))
54	49, 53	syl6 22	. . . . . . . . . . 11 |- ((y e. om /\ A.z e. om (y ~~ z -> y = z)) -> (z e. om -> (w = suc z -> (suc y ~~ w -> suc y = w))))
55	38, 39, 54	r19.23ad 1742	. . . . . . . . . 10 |- ((y e. om /\ A.z e. om (y ~~ z -> y = z)) -> (E.z e. om w = suc z -> (suc y ~~ w -> suc y = w)))
56	35, 55	jaod 424	. . . . . . . . 9 |- ((y e. om /\ A.z e. om (y ~~ z -> y = z)) -> ((w = (/) \/ E.z e. om w = suc z) -> (suc y ~~ w -> suc y = w)))
57	56	ex 373	. . . . . . . 8 |- (y e. om -> (A.z e. om (y ~~ z -> y = z) -> ((w = (/) \/ E.z e. om w = suc z) -> (suc y ~~ w -> suc y = w))))
58		nn0suc 3149	. . . . . . . 8 |- (w e. om -> (w = (/) \/ E.z e. om w = suc z))
59	57, 58	syl7 23	. . . . . . 7 |- (y e. om -> (A.z e. om (y ~~ z -> y = z) -> (w e. om -> (suc y ~~ w -> suc y = w))))
60	59	r19.21adv 1715	. . . . . 6 |- (y e. om -> (A.z e. om (y ~~ z -> y = z) -> A.w e. om (suc y ~~ w -> suc y = w)))
61		breq2 2618	. . . . . . . 8 |- (w = z -> (suc y ~~ w <-> suc y ~~ z))
62		eqeq2 1481	. . . . . . . 8 |- (w = z -> (suc y = w <-> suc y = z))
63	61, 62	imbi12d 625	. . . . . . 7 |- (w = z -> ((suc y ~~ w -> suc y = w) <-> (suc y ~~ z -> suc y = z)))
64	63	cbvralv 1796	. . . . . 6 |- (A.w e. om (suc y ~~ w -> suc y = w) <-> A.z e. om (suc y ~~ z -> suc y = z))
65	60, 64	syl6ib 212	. . . . 5 |- (y e. om -> (A.z e. om (y ~~ z -> y = z) -> A.z e. om (suc y ~~ z -> suc y = z)))
66	8, 12, 16, 20, 28, 65	finds 3151	. . . 4 |- (A e. om -> A.z e. om (A ~~ z -> A = z))
67	4, 66	syl5 21	. . 3 |- (B e. om -> (A e. om -> (A ~~ B -> A = B)))
68	67	impcom 351	. 2 |- ((A e. om /\ B e. om) -> (A ~~ B -> A = B))
69		eqeng 4379	. . 3 |- (A e. om -> (A = B -> A ~~ B))
70	69	adantr 389	. 2 |- ((A e. om /\ B e. om) -> (A = B -> A ~~ B))
71	68, 70	impbid 515	1 |- ((A e. om /\ B e. om) -> (A ~~ B <-> A = B))

Syntax hints:   -> wi 3   <-> wb 146   \/ wo 222   /\ wa 223   = wceq 954   e. wcel 956  A.wral 1642  E.wrex 1643  (/)c0 2276   class class class wbr 2614  suc csuc 2945  omcom 3126   ~~ cen 4354

This theorem is referenced by:  php 4499  onomeneq 4504  nnsdomo 4507

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-9 963  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-rep 2688  ax-sep 2698  ax-nul 27