rp-isfinite6

Description: A set is said to be finite if it is either empty or it can be put in one-to-one correspondence with all the natural numbers between 1 and some n e. NN . (Contributed by RP, 10-Mar-2020)

		Ref	Expression
	Assertion	rp-isfinite6	$⊢ A \in Fin \leftrightarrow (A = \emptyset \lor \exists n \in ℕ (1 \dots n) \approx A)$

Proof

Step	Hyp	Ref	Expression
1		exmid	$⊢ (A = \emptyset \lor \neg A = \emptyset)$
2	1	biantrur	$⊢ A \in Fin \leftrightarrow ((A = \emptyset \lor \neg A = \emptyset) \land A \in Fin)$
3		andir	$⊢ ((A = \emptyset \lor \neg A = \emptyset) \land A \in Fin) \leftrightarrow ((A = \emptyset \land A \in Fin) \lor (\neg A = \emptyset \land A \in Fin))$
4	2 3	bitri	$⊢ A \in Fin \leftrightarrow ((A = \emptyset \land A \in Fin) \lor (\neg A = \emptyset \land A \in Fin))$
5		simpl	$⊢ (A = \emptyset \land A \in Fin) \to A = \emptyset$
6		0fin	$⊢ \emptyset \in Fin$
7		eleq1a	$⊢ \emptyset \in Fin \to (A = \emptyset \to A \in Fin)$
8	6 7	ax-mp	$⊢ A = \emptyset \to A \in Fin$
9	8	ancli	$⊢ A = \emptyset \to (A = \emptyset \land A \in Fin)$
10	5 9	impbii	$⊢ (A = \emptyset \land A \in Fin) \leftrightarrow A = \emptyset$
11		rp-isfinite5	$⊢ A \in Fin \leftrightarrow \exists n \in ℕ_{0} (1 \dots n) \approx A$
12		df-rex	$⊢ \exists n \in ℕ_{0} (1 \dots n) \approx A \leftrightarrow \exists n (n \in ℕ_{0} \land (1 \dots n) \approx A)$
13	11 12	bitri	$⊢ A \in Fin \leftrightarrow \exists n (n \in ℕ_{0} \land (1 \dots n) \approx A)$
14	13	anbi2i	$⊢ (\neg A = \emptyset \land A \in Fin) \leftrightarrow (\neg A = \emptyset \land \exists n (n \in ℕ_{0} \land (1 \dots n) \approx A))$
15		df-rex	$⊢ \exists n \in ℕ (1 \dots n) \approx A \leftrightarrow \exists n (n \in ℕ \land (1 \dots n) \approx A)$
16		en0	$⊢ A \approx \emptyset \leftrightarrow A = \emptyset$
17		ensymb	$⊢ A \approx \emptyset \leftrightarrow \emptyset \approx A$
18	16 17	bitr3i	$⊢ A = \emptyset \leftrightarrow \emptyset \approx A$
19	18	notbii	$⊢ \neg A = \emptyset \leftrightarrow \neg \emptyset \approx A$
20		elnn0	$⊢ n \in ℕ_{0} \leftrightarrow (n \in ℕ \lor n = 0)$
21	20	anbi1i	$⊢ (n \in ℕ_{0} \land (1 \dots n) \approx A) \leftrightarrow ((n \in ℕ \lor n = 0) \land (1 \dots n) \approx A)$
22		andir	$⊢ ((n \in ℕ \lor n = 0) \land (1 \dots n) \approx A) \leftrightarrow ((n \in ℕ \land (1 \dots n) \approx A) \lor (n = 0 \land (1 \dots n) \approx A))$
23	21 22	bitri	$⊢ (n \in ℕ_{0} \land (1 \dots n) \approx A) \leftrightarrow ((n \in ℕ \land (1 \dots n) \approx A) \lor (n = 0 \land (1 \dots n) \approx A))$
24	19 23	anbi12i	$⊢ (\neg A = \emptyset \land (n \in ℕ_{0} \land (1 \dots n) \approx A)) \leftrightarrow (\neg \emptyset \approx A \land ((n \in ℕ \land (1 \dots n) \approx A) \lor (n = 0 \land (1 \dots n) \approx A)))$
25		andi	$⊢ (\neg \emptyset \approx A \land ((n \in ℕ \land (1 \dots n) \approx A) \lor (n = 0 \land (1 \dots n) \approx A))) \leftrightarrow ((\neg \emptyset \approx A \land (n \in ℕ \land (1 \dots n) \approx A)) \lor (\neg \emptyset \approx A \land (n = 0 \land (1 \dots n) \approx A)))$
26	24 25	bitri	$⊢ (\neg A = \emptyset \land (n \in ℕ_{0} \land (1 \dots n) \approx A)) \leftrightarrow ((\neg \emptyset \approx A \land (n \in ℕ \land (1 \dots n) \approx A)) \lor (\neg \emptyset \approx A \land (n = 0 \land (1 \dots n) \approx A)))$
27		3anass	$⊢ (\neg \emptyset \approx A \land n \in ℕ \land (1 \dots n) \approx A) \leftrightarrow (\neg \emptyset \approx A \land (n \in ℕ \land (1 \dots n) \approx A))$
28		3anass	$⊢ (\neg \emptyset \approx A \land n = 0 \land (1 \dots n) \approx A) \leftrightarrow (\neg \emptyset \approx A \land (n = 0 \land (1 \dots n) \approx A))$
29	27 28	orbi12i	$⊢ ((\neg \emptyset \approx A \land n \in ℕ \land (1 \dots n) \approx A) \lor (\neg \emptyset \approx A \land n = 0 \land (1 \dots n) \approx A)) \leftrightarrow ((\neg \emptyset \approx A \land (n \in ℕ \land (1 \dots n) \approx A)) \lor (\neg \emptyset \approx A \land (n = 0 \land (1 \dots n) \approx A)))$
30	26 29	sylbb2	$⊢ (\neg A = \emptyset \land (n \in ℕ_{0} \land (1 \dots n) \approx A)) \to ((\neg \emptyset \approx A \land n \in ℕ \land (1 \dots n) \approx A) \lor (\neg \emptyset \approx A \land n = 0 \land (1 \dots n) \approx A))$
31		simp2	$⊢ (\neg \emptyset \approx A \land n \in ℕ \land (1 \dots n) \approx A) \to n \in ℕ$
32		oveq2	$⊢ n = 0 \to (1 \dots n) = (1 \dots 0)$
33		fz10	$⊢ (1 \dots 0) = \emptyset$
34	32 33	eqtrdi	$⊢ n = 0 \to (1 \dots n) = \emptyset$
35		simp2	$⊢ (\neg \emptyset \approx A \land (1 \dots n) = \emptyset \land (1 \dots n) \approx A) \to (1 \dots n) = \emptyset$
36		simp3	$⊢ (\neg \emptyset \approx A \land (1 \dots n) = \emptyset \land (1 \dots n) \approx A) \to (1 \dots n) \approx A$
37	35 36	eqbrtrrd	$⊢ (\neg \emptyset \approx A \land (1 \dots n) = \emptyset \land (1 \dots n) \approx A) \to \emptyset \approx A$
38		simp1	$⊢ (\neg \emptyset \approx A \land (1 \dots n) = \emptyset \land (1 \dots n) \approx A) \to \neg \emptyset \approx A$
39	37 38	pm2.21dd	$⊢ (\neg \emptyset \approx A \land (1 \dots n) = \emptyset \land (1 \dots n) \approx A) \to n \in ℕ$
40	34 39	syl3an2	$⊢ (\neg \emptyset \approx A \land n = 0 \land (1 \dots n) \approx A) \to n \in ℕ$
41	31 40	jaoi	$⊢ ((\neg \emptyset \approx A \land n \in ℕ \land (1 \dots n) \approx A) \lor (\neg \emptyset \approx A \land n = 0 \land (1 \dots n) \approx A)) \to n \in ℕ$
42	30 41	syl	$⊢ (\neg A = \emptyset \land (n \in ℕ_{0} \land (1 \dots n) \approx A)) \to n \in ℕ$
43		simprr	$⊢ (\neg A = \emptyset \land (n \in ℕ_{0} \land (1 \dots n) \approx A)) \to (1 \dots n) \approx A$
44	42 43	jca	$⊢ (\neg A = \emptyset \land (n \in ℕ_{0} \land (1 \dots n) \approx A)) \to (n \in ℕ \land (1 \dots n) \approx A)$
45		nngt0	$⊢ n \in ℕ \to 0 < n$
46		hash0	$⊢ \|\emptyset\| = 0$
47	46	a1i	$⊢ n \in ℕ \to \|\emptyset\| = 0$
48		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
49		hashfz1	$⊢ n \in ℕ_{0} \to \|(1 \dots n)\| = n$
50	48 49	syl	$⊢ n \in ℕ \to \|(1 \dots n)\| = n$
51	45 47 50	3brtr4d	$⊢ n \in ℕ \to \|\emptyset\| < \|(1 \dots n)\|$
52		fzfi	$⊢ (1 \dots n) \in Fin$
53		hashsdom	$⊢ (\emptyset \in Fin \land (1 \dots n) \in Fin) \to (\|\emptyset\| < \|(1 \dots n)\| \leftrightarrow \emptyset ≺ (1 \dots n))$
54	6 52 53	mp2an	$⊢ \|\emptyset\| < \|(1 \dots n)\| \leftrightarrow \emptyset ≺ (1 \dots n)$
55	51 54	sylib	$⊢ n \in ℕ \to \emptyset ≺ (1 \dots n)$
56	55	anim1i	$⊢ (n \in ℕ \land (1 \dots n) \approx A) \to (\emptyset ≺ (1 \dots n) \land (1 \dots n) \approx A)$
57		sdomentr	$⊢ (\emptyset ≺ (1 \dots n) \land (1 \dots n) \approx A) \to \emptyset ≺ A$
58		sdomnen	$⊢ \emptyset ≺ A \to \neg \emptyset \approx A$
59	57 58	syl	$⊢ (\emptyset ≺ (1 \dots n) \land (1 \dots n) \approx A) \to \neg \emptyset \approx A$
60		en0r	$⊢ \emptyset \approx A \leftrightarrow A = \emptyset$
61	60	notbii	$⊢ \neg \emptyset \approx A \leftrightarrow \neg A = \emptyset$
62	59 61	sylib	$⊢ (\emptyset ≺ (1 \dots n) \land (1 \dots n) \approx A) \to \neg A = \emptyset$
63	56 62	syl	$⊢ (n \in ℕ \land (1 \dots n) \approx A) \to \neg A = \emptyset$
64	48	anim1i	$⊢ (n \in ℕ \land (1 \dots n) \approx A) \to (n \in ℕ_{0} \land (1 \dots n) \approx A)$
65	63 64	jca	$⊢ (n \in ℕ \land (1 \dots n) \approx A) \to (\neg A = \emptyset \land (n \in ℕ_{0} \land (1 \dots n) \approx A))$
66	44 65	impbii	$⊢ (\neg A = \emptyset \land (n \in ℕ_{0} \land (1 \dots n) \approx A)) \leftrightarrow (n \in ℕ \land (1 \dots n) \approx A)$
67	66	exbii	$⊢ \exists n (\neg A = \emptyset \land (n \in ℕ_{0} \land (1 \dots n) \approx A)) \leftrightarrow \exists n (n \in ℕ \land (1 \dots n) \approx A)$
68		19.42v	$⊢ \exists n (\neg A = \emptyset \land (n \in ℕ_{0} \land (1 \dots n) \approx A)) \leftrightarrow (\neg A = \emptyset \land \exists n (n \in ℕ_{0} \land (1 \dots n) \approx A))$
69	15 67 68	3bitr2ri	$⊢ (\neg A = \emptyset \land \exists n (n \in ℕ_{0} \land (1 \dots n) \approx A)) \leftrightarrow \exists n \in ℕ (1 \dots n) \approx A$
70	14 69	bitri	$⊢ (\neg A = \emptyset \land A \in Fin) \leftrightarrow \exists n \in ℕ (1 \dots n) \approx A$
71	10 70	orbi12i	$⊢ ((A = \emptyset \land A \in Fin) \lor (\neg A = \emptyset \land A \in Fin)) \leftrightarrow (A = \emptyset \lor \exists n \in ℕ (1 \dots n) \approx A)$
72	4 71	bitri	$⊢ A \in Fin \leftrightarrow (A = \emptyset \lor \exists n \in ℕ (1 \dots n) \approx A)$

Metamath Proof Explorer

Theorem rp-isfinite6

Proof