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) Avoid ax-pow . (Revised by BTernaryTau, 11-Nov-2024)

		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		0fi	$⊢ \emptyset \in Fin$
18		ensymfib	$⊢ \emptyset \in Fin \to (\emptyset \approx z \leftrightarrow z \approx \emptyset)$
19	17 18	ax-mp	$⊢ \emptyset \approx z \leftrightarrow z \approx \emptyset$
20		en0	$⊢ z \approx \emptyset \leftrightarrow z = \emptyset$
21		eqcom	$⊢ z = \emptyset \leftrightarrow \emptyset = z$
22	20 21	bitri	$⊢ z \approx \emptyset \leftrightarrow \emptyset = z$
23	19 22	sylbb	$⊢ \emptyset \approx z \to \emptyset = z$
24	23	rgenw	$⊢ \forall z \in ω (\emptyset \approx z \to \emptyset = z)$
25		nn0suc	$⊢ w \in ω \to (w = \emptyset \lor \exists z \in ω w = suc z)$
26		en0	$⊢ suc y \approx \emptyset \leftrightarrow suc y = \emptyset$
27		breq2	$⊢ w = \emptyset \to (suc y \approx w \leftrightarrow suc y \approx \emptyset)$
28		eqeq2	$⊢ w = \emptyset \to (suc y = w \leftrightarrow suc y = \emptyset)$
29	27 28	bibi12d	$⊢ w = \emptyset \to ((suc y \approx w \leftrightarrow suc y = w) \leftrightarrow (suc y \approx \emptyset \leftrightarrow suc y = \emptyset))$
30	26 29	mpbiri	$⊢ w = \emptyset \to (suc y \approx w \leftrightarrow suc y = w)$
31	30	biimpd	$⊢ w = \emptyset \to (suc y \approx w \to suc y = w)$
32	31	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))$
33		nfv	$⊢ Ⅎ z y \in ω$
34		nfra1	$⊢ Ⅎ z \forall z \in ω (y \approx z \to y = z)$
35	33 34	nfan	$⊢ Ⅎ z (y \in ω \land \forall z \in ω (y \approx z \to y = z))$
36		nfv	$⊢ Ⅎ z (suc y \approx w \to suc y = w)$
37		vex	$⊢ y \in V$
38	37	phplem2	$⊢ (y \in ω \land z \in ω) \to (suc y \approx suc z \to y \approx z)$
39	38	imim1d	$⊢ (y \in ω \land z \in ω) \to ((y \approx z \to y = z) \to (suc y \approx suc z \to y = z))$
40	39	ex	$⊢ y \in ω \to (z \in ω \to ((y \approx z \to y = z) \to (suc y \approx suc z \to y = z)))$
41	40	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)))$
42		rsp	$⊢ \forall z \in ω (y \approx z \to y = z) \to (z \in ω \to (y \approx z \to y = z))$
43	41 42	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))$
44		suceq	$⊢ y = z \to suc y = suc z$
45	43 44	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))$
46		breq2	$⊢ w = suc z \to (suc y \approx w \leftrightarrow suc y \approx suc z)$
47		eqeq2	$⊢ w = suc z \to (suc y = w \leftrightarrow suc y = suc z)$
48	46 47	imbi12d	$⊢ w = suc z \to ((suc y \approx w \to suc y = w) \leftrightarrow (suc y \approx suc z \to suc y = suc z))$
49	48	biimprcd	$⊢ (suc y \approx suc z \to suc y = suc z) \to (w = suc z \to (suc y \approx w \to suc y = w))$
50	45 49	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)))$
51	35 36 50	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))$
52	32 51	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))$
53	52	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)))$
54	25 53	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)))$
55	54	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))$
56		breq2	$⊢ w = z \to (suc y \approx w \leftrightarrow suc y \approx z)$
57		eqeq2	$⊢ w = z \to (suc y = w \leftrightarrow suc y = z)$
58	56 57	imbi12d	$⊢ w = z \to ((suc y \approx w \to suc y = w) \leftrightarrow (suc y \approx z \to suc y = z))$
59	58	cbvralvw	$⊢ \forall w \in ω (suc y \approx w \to suc y = w) \leftrightarrow \forall z \in ω (suc y \approx z \to suc y = z)$
60	55 59	imbitrdi	$⊢ y \in ω \to (\forall z \in ω (y \approx z \to y = z) \to \forall z \in ω (suc y \approx z \to suc y = z))$
61	4 8 12 16 24 60	finds	$⊢ A \in ω \to \forall z \in ω (A \approx z \to A = z)$
62		breq2	$⊢ z = B \to (A \approx z \leftrightarrow A \approx B)$
63		eqeq2	$⊢ z = B \to (A = z \leftrightarrow A = B)$
64	62 63	imbi12d	$⊢ z = B \to ((A \approx z \to A = z) \leftrightarrow (A \approx B \to A = B))$
65	64	rspcv	$⊢ B \in ω \to (\forall z \in ω (A \approx z \to A = z) \to (A \approx B \to A = B))$
66	61 65	mpan9	$⊢ (A \in ω \land B \in ω) \to (A \approx B \to A = B)$
67		enrefnn	$⊢ A \in ω \to A \approx A$
68		breq2	$⊢ A = B \to (A \approx A \leftrightarrow A \approx B)$
69	67 68	syl5ibcom	$⊢ A \in ω \to (A = B \to A \approx B)$
70	69	adantr	$⊢ (A \in ω \land B \in ω) \to (A = B \to A \approx B)$
71	66 70	impbid	$⊢ (A \in ω \land B \in ω) \to (A \approx B \leftrightarrow A = B)$

Metamath Proof Explorer

Theorem nneneq

Proof