f1ocnt

Description: Given a countable set A , number its elements by providing a one-to-one mapping either with NN or an integer range starting from 1. The domain of the function can then be used with iundisjcnt or iundisj2cnt . (Contributed by Thierry Arnoux, 25-Jul-2020)

		Ref	Expression
	Assertion	f1ocnt	$⊢ A ≼ ω \to \exists f (f : dom f \underset{1-1 onto}{⟶} A \land (dom f = ℕ \lor dom f = (1 ..^\|A\| + 1)))$

Proof

Step	Hyp	Ref	Expression
1		f1o0	$⊢ \emptyset : \emptyset \underset{1-1 onto}{⟶} \emptyset$
2		eqidd	$⊢ A = \emptyset \to \emptyset = \emptyset$
3		dm0	$⊢ dom \emptyset = \emptyset$
4	3	a1i	$⊢ A = \emptyset \to dom \emptyset = \emptyset$
5		id	$⊢ A = \emptyset \to A = \emptyset$
6	2 4 5	f1oeq123d	$⊢ A = \emptyset \to (\emptyset : dom \emptyset \underset{1-1 onto}{⟶} A \leftrightarrow \emptyset : \emptyset \underset{1-1 onto}{⟶} \emptyset)$
7	1 6	mpbiri	$⊢ A = \emptyset \to \emptyset : dom \emptyset \underset{1-1 onto}{⟶} A$
8		fveq2	$⊢ A = \emptyset \to \|A\| = \|\emptyset\|$
9		hash0	$⊢ \|\emptyset\| = 0$
10	8 9	syl6eq	$⊢ A = \emptyset \to \|A\| = 0$
11	10	oveq1d	$⊢ A = \emptyset \to \|A\| + 1 = 0 + 1$
12		0p1e1	$⊢ 0 + 1 = 1$
13	11 12	syl6eq	$⊢ A = \emptyset \to \|A\| + 1 = 1$
14	13	oveq2d	$⊢ A = \emptyset \to (1 ..^\|A\| + 1) = (1 ..^1)$
15		fzo0	$⊢ (1 ..^1) = \emptyset$
16	14 15	syl6eq	$⊢ A = \emptyset \to (1 ..^\|A\| + 1) = \emptyset$
17	4 16	eqtr4d	$⊢ A = \emptyset \to dom \emptyset = (1 ..^\|A\| + 1)$
18	17	olcd	$⊢ A = \emptyset \to (dom \emptyset = ℕ \lor dom \emptyset = (1 ..^\|A\| + 1))$
19	7 18	jca	$⊢ A = \emptyset \to (\emptyset : dom \emptyset \underset{1-1 onto}{⟶} A \land (dom \emptyset = ℕ \lor dom \emptyset = (1 ..^\|A\| + 1)))$
20		0ex	$⊢ \emptyset \in V$
21		id	$⊢ f = \emptyset \to f = \emptyset$
22		dmeq	$⊢ f = \emptyset \to dom f = dom \emptyset$
23		eqidd	$⊢ f = \emptyset \to A = A$
24	21 22 23	f1oeq123d	$⊢ f = \emptyset \to (f : dom f \underset{1-1 onto}{⟶} A \leftrightarrow \emptyset : dom \emptyset \underset{1-1 onto}{⟶} A)$
25	22	eqeq1d	$⊢ f = \emptyset \to (dom f = ℕ \leftrightarrow dom \emptyset = ℕ)$
26	22	eqeq1d	$⊢ f = \emptyset \to (dom f = (1 ..^\|A\| + 1) \leftrightarrow dom \emptyset = (1 ..^\|A\| + 1))$
27	25 26	orbi12d	$⊢ f = \emptyset \to ((dom f = ℕ \lor dom f = (1 ..^\|A\| + 1)) \leftrightarrow (dom \emptyset = ℕ \lor dom \emptyset = (1 ..^\|A\| + 1)))$
28	24 27	anbi12d	$⊢ f = \emptyset \to ((f : dom f \underset{1-1 onto}{⟶} A \land (dom f = ℕ \lor dom f = (1 ..^\|A\| + 1))) \leftrightarrow (\emptyset : dom \emptyset \underset{1-1 onto}{⟶} A \land (dom \emptyset = ℕ \lor dom \emptyset = (1 ..^\|A\| + 1))))$
29	20 28	spcev	$⊢ (\emptyset : dom \emptyset \underset{1-1 onto}{⟶} A \land (dom \emptyset = ℕ \lor dom \emptyset = (1 ..^\|A\| + 1))) \to \exists f (f : dom f \underset{1-1 onto}{⟶} A \land (dom f = ℕ \lor dom f = (1 ..^\|A\| + 1)))$
30	19 29	syl	$⊢ A = \emptyset \to \exists f (f : dom f \underset{1-1 onto}{⟶} A \land (dom f = ℕ \lor dom f = (1 ..^\|A\| + 1)))$
31	30	adantl	$⊢ ((A ≼ ω \land A \in Fin) \land A = \emptyset) \to \exists f (f : dom f \underset{1-1 onto}{⟶} A \land (dom f = ℕ \lor dom f = (1 ..^\|A\| + 1)))$
32		f1odm	$⊢ f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to dom f = (1 \dots \|A\|)$
33	32	f1oeq2d	$⊢ f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to (f : dom f \underset{1-1 onto}{⟶} A \leftrightarrow f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)$
34	33	ibir	$⊢ f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to f : dom f \underset{1-1 onto}{⟶} A$
35	34	adantl	$⊢ (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to f : dom f \underset{1-1 onto}{⟶} A$
36	32	adantl	$⊢ (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to dom f = (1 \dots \|A\|)$
37		simpl	$⊢ (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to \|A\| \in ℕ$
38	37	nnzd	$⊢ (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to \|A\| \in ℤ$
39		fzval3	$⊢ \|A\| \in ℤ \to (1 \dots \|A\|) = (1 ..^\|A\| + 1)$
40	38 39	syl	$⊢ (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to (1 \dots \|A\|) = (1 ..^\|A\| + 1)$
41	36 40	eqtrd	$⊢ (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to dom f = (1 ..^\|A\| + 1)$
42	41	olcd	$⊢ (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to (dom f = ℕ \lor dom f = (1 ..^\|A\| + 1))$
43	35 42	jca	$⊢ (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to (f : dom f \underset{1-1 onto}{⟶} A \land (dom f = ℕ \lor dom f = (1 ..^\|A\| + 1)))$
44	43	ex	$⊢ \|A\| \in ℕ \to (f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to (f : dom f \underset{1-1 onto}{⟶} A \land (dom f = ℕ \lor dom f = (1 ..^\|A\| + 1))))$
45	44	eximdv	$⊢ \|A\| \in ℕ \to (\exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to \exists f (f : dom f \underset{1-1 onto}{⟶} A \land (dom f = ℕ \lor dom f = (1 ..^\|A\| + 1))))$
46	45	imp	$⊢ (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to \exists f (f : dom f \underset{1-1 onto}{⟶} A \land (dom f = ℕ \lor dom f = (1 ..^\|A\| + 1)))$
47	46	adantl	$⊢ ((A ≼ ω \land A \in Fin) \land (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \exists f (f : dom f \underset{1-1 onto}{⟶} A \land (dom f = ℕ \lor dom f = (1 ..^\|A\| + 1)))$
48		fz1f1o	$⊢ A \in Fin \to (A = \emptyset \lor (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A))$
49	48	adantl	$⊢ (A ≼ ω \land A \in Fin) \to (A = \emptyset \lor (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A))$
50	31 47 49	mpjaodan	$⊢ (A ≼ ω \land A \in Fin) \to \exists f (f : dom f \underset{1-1 onto}{⟶} A \land (dom f = ℕ \lor dom f = (1 ..^\|A\| + 1)))$
51		isfinite	$⊢ A \in Fin \leftrightarrow A ≺ ω$
52	51	notbii	$⊢ \neg A \in Fin \leftrightarrow \neg A ≺ ω$
53	52	biimpi	$⊢ \neg A \in Fin \to \neg A ≺ ω$
54	53	anim2i	$⊢ (A ≼ ω \land \neg A \in Fin) \to (A ≼ ω \land \neg A ≺ ω)$
55		bren2	$⊢ A \approx ω \leftrightarrow (A ≼ ω \land \neg A ≺ ω)$
56	54 55	sylibr	$⊢ (A ≼ ω \land \neg A \in Fin) \to A \approx ω$
57		nnenom	$⊢ ℕ \approx ω$
58	57	ensymi	$⊢ ω \approx ℕ$
59		entr	$⊢ (A \approx ω \land ω \approx ℕ) \to A \approx ℕ$
60	56 58 59	sylancl	$⊢ (A ≼ ω \land \neg A \in Fin) \to A \approx ℕ$
61		bren	$⊢ A \approx ℕ \leftrightarrow \exists g g : A \underset{1-1 onto}{⟶} ℕ$
62	60 61	sylib	$⊢ (A ≼ ω \land \neg A \in Fin) \to \exists g g : A \underset{1-1 onto}{⟶} ℕ$
63		f1oexbi	$⊢ \exists g g : A \underset{1-1 onto}{⟶} ℕ \leftrightarrow \exists f f : ℕ \underset{1-1 onto}{⟶} A$
64	62 63	sylib	$⊢ (A ≼ ω \land \neg A \in Fin) \to \exists f f : ℕ \underset{1-1 onto}{⟶} A$
65		f1odm	$⊢ f : ℕ \underset{1-1 onto}{⟶} A \to dom f = ℕ$
66	65	f1oeq2d	$⊢ f : ℕ \underset{1-1 onto}{⟶} A \to (f : dom f \underset{1-1 onto}{⟶} A \leftrightarrow f : ℕ \underset{1-1 onto}{⟶} A)$
67	66	ibir	$⊢ f : ℕ \underset{1-1 onto}{⟶} A \to f : dom f \underset{1-1 onto}{⟶} A$
68	65	orcd	$⊢ f : ℕ \underset{1-1 onto}{⟶} A \to (dom f = ℕ \lor dom f = (1 ..^\|A\| + 1))$
69	67 68	jca	$⊢ f : ℕ \underset{1-1 onto}{⟶} A \to (f : dom f \underset{1-1 onto}{⟶} A \land (dom f = ℕ \lor dom f = (1 ..^\|A\| + 1)))$
70	69	eximi	$⊢ \exists f f : ℕ \underset{1-1 onto}{⟶} A \to \exists f (f : dom f \underset{1-1 onto}{⟶} A \land (dom f = ℕ \lor dom f = (1 ..^\|A\| + 1)))$
71	64 70	syl	$⊢ (A ≼ ω \land \neg A \in Fin) \to \exists f (f : dom f \underset{1-1 onto}{⟶} A \land (dom f = ℕ \lor dom f = (1 ..^\|A\| + 1)))$
72	50 71	pm2.61dan	$⊢ A ≼ ω \to \exists f (f : dom f \underset{1-1 onto}{⟶} A \land (dom f = ℕ \lor dom f = (1 ..^\|A\| + 1)))$

Metamath Proof Explorer

Theorem f1ocnt

Proof