Theorem nneneq 4512

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 2623	. . . . . 6 |- (z = B -> (A ~~ z <-> A ~~ B))
2		eqeq2 1484	. . . . . 6 |- (z = B -> (A = z <-> A = B))
3	1, 2	imbi12d 626	. . . . 5 |- (z = B -> ((A ~~ z -> A = z) <-> (A ~~ B -> A = B)))
4	3	rcla4v 1873	. . . 4 |- (B e. om -> (A.z e. om (A ~~ z -> A = z) -> (A ~~ B -> A = B)))
5		breq1 2622	. . . . . . 7 |- (x = (/) -> (x ~~ z <-> (/) ~~ z))
6		eqeq1 1481	. . . . . . 7 |- (x = (/) -> (x = z <-> (/) = z))
7	5, 6	imbi12d 626	. . . . . 6 |- (x = (/) -> ((x ~~ z -> x = z) <-> ((/) ~~ z -> (/) = z)))
8	7	ralbidv 1663	. . . . 5 |- (x = (/) -> (A.z e. om (x ~~ z -> x = z) <-> A.z e. om ((/) ~~ z -> (/) = z)))
9		breq1 2622	. . . . . . 7 |- (x = y -> (x ~~ z <-> y ~~ z))
10		eqeq1 1481	. . . . . . 7 |- (x = y -> (x = z <-> y = z))
11	9, 10	imbi12d 626	. . . . . 6 |- (x = y -> ((x ~~ z -> x = z) <-> (y ~~ z -> y = z)))
12	11	ralbidv 1663	. . . . 5 |- (x = y -> (A.z e. om (x ~~ z -> x = z) <-> A.z e. om (y ~~ z -> y = z)))
13		breq1 2622	. . . . . . 7 |- (x = suc y -> (x ~~ z <-> suc y ~~ z))
14		eqeq1 1481	. . . . . . 7 |- (x = suc y -> (x = z <-> suc y = z))
15	13, 14	imbi12d 626	. . . . . 6 |- (x = suc y -> ((x ~~ z -> x = z) <-> (suc y ~~ z -> suc y = z)))
16	15	ralbidv 1663	. . . . 5 |- (x = suc y -> (A.z e. om (x ~~ z -> x = z) <-> A.z e. om (suc y ~~ z -> suc y = z)))
17		breq1 2622	. . . . . . 7 |- (x = A -> (x ~~ z <-> A ~~ z))
18		eqeq1 1481	. . . . . . 7 |- (x = A -> (x = z <-> A = z))
19	17, 18	imbi12d 626	. . . . . 6 |- (x = A -> ((x ~~ z -> x = z) <-> (A ~~ z -> A = z)))
20	19	ralbidv 1663	. . . . 5 |- (x = A -> (A.z e. om (x ~~ z -> x = z) <-> A.z e. om (A ~~ z -> A = z)))
21		visset 1813	. . . . . . . . 9 |- z e. V
22	21	ensym 4412	. . . . . . . 8 |- ((/) ~~ z -> z ~~ (/))
23		en0 4423	. . . . . . . . 9 |- (z ~~ (/) <-> z = (/))
24		eqcom 1477	. . . . . . . . 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 1698	. . . . 5 |- A.z e. om ((/) ~~ z -> (/) = z)
29		en0 4423	. . . . . . . . . . . . 13 |- (suc y ~~ (/) <-> suc y = (/))
30		breq2 2623	. . . . . . . . . . . . . 14 |- (w = (/) -> (suc y ~~ w <-> suc y ~~ (/)))
31		eqeq2 1484	. . . . . . . . . . . . . 14 |- (w = (/) -> (suc y = w <-> suc y = (/)))
32	30, 31	bibi12d 629	. . . . . . . . . . . . 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 971	. . . . . . . . . . . 12 |- (y e. om -> A.z y e. om)
37		hbra1 1687	. . . . . . . . . . . 12 |- (A.z e. om (y ~~ z -> y = z) -> A.zA.z e. om (y ~~ z -> y = z))
38	36, 37	hban 1009	. . . . . . . . . . 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 971	. . . . . . . . . . 11 |- ((suc y ~~ w -> suc y = w) -> A.z(suc y ~~ w -> suc y = w))
40		visset 1813	. . . . . . . . . . . . . . . . . . 19 |- y e. V
41	40, 21	phplem4 4511	. . . . . . . . . . . . . . . . . 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 1694	. . . . . . . . . . . . . . 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 3034	. . . . . . . . . . . . 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 2623	. . . . . . . . . . . . . 14 |- (w = suc z -> (suc y ~~ w <-> suc y ~~ suc z))
51		eqeq2 1484	. . . . . . . . . . . . . 14 |- (w = suc z -> (suc y = w <-> suc y = suc z))
52	50, 51	imbi12d 626	. . . . . . . . . . . . 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 1745	. . . . . . . . . 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 3154	. . . . . . . 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 1718	. . . . . 6 |- (y e. om -> (A.z e. om (y ~~ z -> y = z) -> A.w e. om (suc y ~~ w -> suc y = w)))
61		breq2 2623	. . . . . . . 8 |- (w = z -> (suc y ~~ w <-> suc y ~~ z))
62		eqeq2 1484	. . . . . . . 8 |- (w = z -> (suc y = w <-> suc y = z))
63	61, 62	imbi12d 626	. . . . . . 7 |- (w = z -> ((suc y ~~ w -> suc y = w) <-> (suc y ~~ z -> suc y = z)))
64	63	cbvralv 1800	. . . . . 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 3156	. . . 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 4392	. . 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 516	1 |- ((A e. om /\ B e. om) -> (A ~~ B <-> A = B))

Syntax hints:   -> wi 3   <-> wb 146   \/ wo 222   /\ wa 223   = wceq 956   e. wcel 958  A.wral 1645  E.wrex 1646  (/)c0 2280   class class class wbr 2619  suc csuc 2950  omcom 3131   ~~ cen 4364

This theorem is referenced by:  php 4513  onomeneq 4519  nnsdomo 4522

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-9 965  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-rep 2693  ax-sep 2703