nneneq

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. (Contributed by NM, 28-May-1998)

		Ref	Expression
	Assertion	nneneq	$⊢ (A \in ω \land B \in ω) \to (A \approx B \leftrightarrow A = B)$

Proof

Step	Hyp	Ref	Expression
1		breq1	$⊢ x = \emptyset \to (x \approx z \leftrightarrow \emptyset \approx z)$
2		eqeq1	$⊢ x = \emptyset \to (x = z \leftrightarrow \emptyset = z)$
3	1 2	imbi12d	$⊢ x = \emptyset \to ((x \approx z \to x = z) \leftrightarrow (\emptyset \approx z \to \emptyset = z))$
4	3	ralbidv	$⊢ x = \emptyset \to (\forall z \in ω (x \approx z \to x = z) \leftrightarrow \forall z \in ω (\emptyset \approx z \to \emptyset = z))$
5		breq1	$⊢ x = y \to (x \approx z \leftrightarrow y \approx z)$
6		eqeq1	$⊢ x = y \to (x = z \leftrightarrow y = z)$
7	5 6	imbi12d	$⊢ x = y \to ((x \approx z \to x = z) \leftrightarrow (y \approx z \to y = z))$
8	7	ralbidv	$⊢ x = y \to (\forall z \in ω (x \approx z \to x = z) \leftrightarrow \forall z \in ω (y \approx z \to y = z))$
9		breq1	$⊢ x = suc y \to (x \approx z \leftrightarrow suc y \approx z)$
10		eqeq1	$⊢ x = suc y \to (x = z \leftrightarrow suc y = z)$
11	9 10	imbi12d	$⊢ x = suc y \to ((x \approx z \to x = z) \leftrightarrow (suc y \approx z \to suc y = z))$
12	11	ralbidv	$⊢ x = suc y \to (\forall z \in ω (x \approx z \to x = z) \leftrightarrow \forall z \in ω (suc y \approx z \to suc y = z))$
13		breq1	$⊢ x = A \to (x \approx z \leftrightarrow A \approx z)$
14		eqeq1	$⊢ x = A \to (x = z \leftrightarrow A = z)$
15	13 14	imbi12d	$⊢ x = A \to ((x \approx z \to x = z) \leftrightarrow (A \approx z \to A = z))$
16	15	ralbidv	$⊢ x = A \to (\forall z \in ω (x \approx z \to x = z) \leftrightarrow \forall z \in ω (A \approx z \to A = z))$
17		ensym	$⊢ \emptyset \approx z \to z \approx \emptyset$
18		en0	$⊢ z \approx \emptyset \leftrightarrow z = \emptyset$
19		eqcom	$⊢ z = \emptyset \leftrightarrow \emptyset = z$
20	18 19	bitri	$⊢ z \approx \emptyset \leftrightarrow \emptyset = z$
21	17 20	sylib	$⊢ \emptyset \approx z \to \emptyset = z$
22	21	rgenw	$⊢ \forall z \in ω (\emptyset \approx z \to \emptyset = z)$
23		nn0suc	$⊢ w \in ω \to (w = \emptyset \lor \exists z \in ω w = suc z)$
24		en0	$⊢ suc y \approx \emptyset \leftrightarrow suc y = \emptyset$
25		breq2	$⊢ w = \emptyset \to (suc y \approx w \leftrightarrow suc y \approx \emptyset)$
26		eqeq2	$⊢ w = \emptyset \to (suc y = w \leftrightarrow suc y = \emptyset)$
27	25 26	bibi12d	$⊢ w = \emptyset \to ((suc y \approx w \leftrightarrow suc y = w) \leftrightarrow (suc y \approx \emptyset \leftrightarrow suc y = \emptyset))$
28	24 27	mpbiri	$⊢ w = \emptyset \to (suc y \approx w \leftrightarrow suc y = w)$
29	28	biimpd	$⊢ w = \emptyset \to (suc y \approx w \to suc y = w)$
30	29	a1i	$⊢ (y \in ω \land \forall z \in ω (y \approx z \to y = z)) \to (w = \emptyset \to (suc y \approx w \to suc y = w))$
31		nfv	$⊢ Ⅎ z y \in ω$
32		nfra1	$⊢ Ⅎ z \forall z \in ω (y \approx z \to y = z)$
33	31 32	nfan	$⊢ Ⅎ z (y \in ω \land \forall z \in ω (y \approx z \to y = z))$
34		nfv	$⊢ Ⅎ z (suc y \approx w \to suc y = w)$
35		vex	$⊢ y \in V$
36		vex	$⊢ z \in V$
37	35 36	phplem4	$⊢ (y \in ω \land z \in ω) \to (suc y \approx suc z \to y \approx z)$
38	37	imim1d	$⊢ (y \in ω \land z \in ω) \to ((y \approx z \to y = z) \to (suc y \approx suc z \to y = z))$
39	38	ex	$⊢ y \in ω \to (z \in ω \to ((y \approx z \to y = z) \to (suc y \approx suc z \to y = z)))$
40	39	a2d	$⊢ y \in ω \to ((z \in ω \to (y \approx z \to y = z)) \to (z \in ω \to (suc y \approx suc z \to y = z)))$
41		rsp	$⊢ \forall z \in ω (y \approx z \to y = z) \to (z \in ω \to (y \approx z \to y = z))$
42	40 41	impel	$⊢ (y \in ω \land \forall z \in ω (y \approx z \to y = z)) \to (z \in ω \to (suc y \approx suc z \to y = z))$
43		suceq	$⊢ y = z \to suc y = suc z$
44	42 43	syl8	$⊢ (y \in ω \land \forall z \in ω (y \approx z \to y = z)) \to (z \in ω \to (suc y \approx suc z \to suc y = suc z))$
45		breq2	$⊢ w = suc z \to (suc y \approx w \leftrightarrow suc y \approx suc z)$
46		eqeq2	$⊢ w = suc z \to (suc y = w \leftrightarrow suc y = suc z)$
47	45 46	imbi12d	$⊢ w = suc z \to ((suc y \approx w \to suc y = w) \leftrightarrow (suc y \approx suc z \to suc y = suc z))$
48	47	biimprcd	$⊢ (suc y \approx suc z \to suc y = suc z) \to (w = suc z \to (suc y \approx w \to suc y = w))$
49	44 48	syl6	$⊢ (y \in ω \land \forall z \in ω (y \approx z \to y = z)) \to (z \in ω \to (w = suc z \to (suc y \approx w \to suc y = w)))$
50	33 34 49	rexlimd	$⊢ (y \in ω \land \forall z \in ω (y \approx z \to y = z)) \to (\exists z \in ω w = suc z \to (suc y \approx w \to suc y = w))$
51	30 50	jaod	$⊢ (y \in ω \land \forall z \in ω (y \approx z \to y = z)) \to ((w = \emptyset \lor \exists z \in ω w = suc z) \to (suc y \approx w \to suc y = w))$
52	51	ex	$⊢ y \in ω \to (\forall z \in ω (y \approx z \to y = z) \to ((w = \emptyset \lor \exists z \in ω w = suc z) \to (suc y \approx w \to suc y = w)))$
53	23 52	syl7	$⊢ y \in ω \to (\forall z \in ω (y \approx z \to y = z) \to (w \in ω \to (suc y \approx w \to suc y = w)))$
54	53	ralrimdv	$⊢ y \in ω \to (\forall z \in ω (y \approx z \to y = z) \to \forall w \in ω (suc y \approx w \to suc y = w))$
55		breq2	$⊢ w = z \to (suc y \approx w \leftrightarrow suc y \approx z)$
56		eqeq2	$⊢ w = z \to (suc y = w \leftrightarrow suc y = z)$
57	55 56	imbi12d	$⊢ w = z \to ((suc y \approx w \to suc y = w) \leftrightarrow (suc y \approx z \to suc y = z))$
58	57	cbvralvw	$⊢ \forall w \in ω (suc y \approx w \to suc y = w) \leftrightarrow \forall z \in ω (suc y \approx z \to suc y = z)$
59	54 58	syl6ib	$⊢ y \in ω \to (\forall z \in ω (y \approx z \to y = z) \to \forall z \in ω (suc y \approx z \to suc y = z))$
60	4 8 12 16 22 59	finds	$⊢ A \in ω \to \forall z \in ω (A \approx z \to A = z)$
61		breq2	$⊢ z = B \to (A \approx z \leftrightarrow A \approx B)$
62		eqeq2	$⊢ z = B \to (A = z \leftrightarrow A = B)$
63	61 62	imbi12d	$⊢ z = B \to ((A \approx z \to A = z) \leftrightarrow (A \approx B \to A = B))$
64	63	rspcv	$⊢ B \in ω \to (\forall z \in ω (A \approx z \to A = z) \to (A \approx B \to A = B))$
65	60 64	mpan9	$⊢ (A \in ω \land B \in ω) \to (A \approx B \to A = B)$
66		eqeng	$⊢ A \in ω \to (A = B \to A \approx B)$
67	66	adantr	$⊢ (A \in ω \land B \in ω) \to (A = B \to A \approx B)$
68	65 67	impbid	$⊢ (A \in ω \land B \in ω) \to (A \approx B \leftrightarrow A = B)$

Metamath Proof Explorer

Theorem nneneq

Proof