2lgslem1b

	Ref	Expression
Hypotheses	2lgslem1b.i	$⊢ I = (A \dots B)$
	2lgslem1b.f	$⊢ F = (j \in I ⟼ j \cdot 2)$
Assertion	2lgslem1b	$⊢ F : I \underset{1-1 onto}{⟶} \{x \in ℤ \| \exists i \in I x = i \cdot 2\}$

Proof

Step	Hyp	Ref	Expression
1		2lgslem1b.i	$⊢ I = (A \dots B)$
2		2lgslem1b.f	$⊢ F = (j \in I ⟼ j \cdot 2)$
3		eqeq1	$⊢ x = j \cdot 2 \to (x = i \cdot 2 \leftrightarrow j \cdot 2 = i \cdot 2)$
4	3	rexbidv	$⊢ x = j \cdot 2 \to (\exists i \in I x = i \cdot 2 \leftrightarrow \exists i \in I j \cdot 2 = i \cdot 2)$
5		elfzelz	$⊢ j \in (A \dots B) \to j \in ℤ$
6	5 1	eleq2s	$⊢ j \in I \to j \in ℤ$
7		2z	$⊢ 2 \in ℤ$
8	7	a1i	$⊢ j \in I \to 2 \in ℤ$
9	6 8	zmulcld	$⊢ j \in I \to j \cdot 2 \in ℤ$
10		id	$⊢ j \in I \to j \in I$
11		oveq1	$⊢ i = j \to i \cdot 2 = j \cdot 2$
12	11	eqeq2d	$⊢ i = j \to (j \cdot 2 = i \cdot 2 \leftrightarrow j \cdot 2 = j \cdot 2)$
13	12	adantl	$⊢ (j \in I \land i = j) \to (j \cdot 2 = i \cdot 2 \leftrightarrow j \cdot 2 = j \cdot 2)$
14		eqidd	$⊢ j \in I \to j \cdot 2 = j \cdot 2$
15	10 13 14	rspcedvd	$⊢ j \in I \to \exists i \in I j \cdot 2 = i \cdot 2$
16	4 9 15	elrabd	$⊢ j \in I \to j \cdot 2 \in \{x \in ℤ \| \exists i \in I x = i \cdot 2\}$
17	2 16	fmpti	$⊢ F : I ⟶ \{x \in ℤ \| \exists i \in I x = i \cdot 2\}$
18		oveq1	$⊢ j = y \to j \cdot 2 = y \cdot 2$
19		simpl	$⊢ (y \in I \land z \in I) \to y \in I$
20		ovexd	$⊢ (y \in I \land z \in I) \to y \cdot 2 \in V$
21	2 18 19 20	fvmptd3	$⊢ (y \in I \land z \in I) \to F (y) = y \cdot 2$
22		oveq1	$⊢ j = z \to j \cdot 2 = z \cdot 2$
23		simpr	$⊢ (y \in I \land z \in I) \to z \in I$
24		ovexd	$⊢ (y \in I \land z \in I) \to z \cdot 2 \in V$
25	2 22 23 24	fvmptd3	$⊢ (y \in I \land z \in I) \to F (z) = z \cdot 2$
26	21 25	eqeq12d	$⊢ (y \in I \land z \in I) \to (F (y) = F (z) \leftrightarrow y \cdot 2 = z \cdot 2)$
27		elfzelz	$⊢ y \in (A \dots B) \to y \in ℤ$
28	27 1	eleq2s	$⊢ y \in I \to y \in ℤ$
29	28	zcnd	$⊢ y \in I \to y \in ℂ$
30	29	adantr	$⊢ (y \in I \land z \in I) \to y \in ℂ$
31		elfzelz	$⊢ z \in (A \dots B) \to z \in ℤ$
32	31 1	eleq2s	$⊢ z \in I \to z \in ℤ$
33	32	zcnd	$⊢ z \in I \to z \in ℂ$
34	33	adantl	$⊢ (y \in I \land z \in I) \to z \in ℂ$
35		2cnd	$⊢ (y \in I \land z \in I) \to 2 \in ℂ$
36		2ne0	$⊢ 2 \neq 0$
37	36	a1i	$⊢ (y \in I \land z \in I) \to 2 \neq 0$
38	30 34 35 37	mulcan2d	$⊢ (y \in I \land z \in I) \to (y \cdot 2 = z \cdot 2 \leftrightarrow y = z)$
39	38	biimpd	$⊢ (y \in I \land z \in I) \to (y \cdot 2 = z \cdot 2 \to y = z)$
40	26 39	sylbid	$⊢ (y \in I \land z \in I) \to (F (y) = F (z) \to y = z)$
41	40	rgen2	$⊢ \forall y \in I \forall z \in I (F (y) = F (z) \to y = z)$
42		dff13	$⊢ F : I \underset{1-1}{⟶} \{x \in ℤ \| \exists i \in I x = i \cdot 2\} \leftrightarrow (F : I ⟶ \{x \in ℤ \| \exists i \in I x = i \cdot 2\} \land \forall y \in I \forall z \in I (F (y) = F (z) \to y = z))$
43	17 41 42	mpbir2an	$⊢ F : I \underset{1-1}{⟶} \{x \in ℤ \| \exists i \in I x = i \cdot 2\}$
44		oveq1	$⊢ j = i \to j \cdot 2 = i \cdot 2$
45	44	eqeq2d	$⊢ j = i \to (x = j \cdot 2 \leftrightarrow x = i \cdot 2)$
46	45	cbvrexvw	$⊢ \exists j \in I x = j \cdot 2 \leftrightarrow \exists i \in I x = i \cdot 2$
47		elfzelz	$⊢ i \in (A \dots B) \to i \in ℤ$
48	7	a1i	$⊢ i \in (A \dots B) \to 2 \in ℤ$
49	47 48	zmulcld	$⊢ i \in (A \dots B) \to i \cdot 2 \in ℤ$
50	49 1	eleq2s	$⊢ i \in I \to i \cdot 2 \in ℤ$
51		eleq1	$⊢ x = i \cdot 2 \to (x \in ℤ \leftrightarrow i \cdot 2 \in ℤ)$
52	50 51	syl5ibrcom	$⊢ i \in I \to (x = i \cdot 2 \to x \in ℤ)$
53	52	rexlimiv	$⊢ \exists i \in I x = i \cdot 2 \to x \in ℤ$
54	53	pm4.71ri	$⊢ \exists i \in I x = i \cdot 2 \leftrightarrow (x \in ℤ \land \exists i \in I x = i \cdot 2)$
55	46 54	bitri	$⊢ \exists j \in I x = j \cdot 2 \leftrightarrow (x \in ℤ \land \exists i \in I x = i \cdot 2)$
56	55	abbii	$⊢ \{x \| \exists j \in I x = j \cdot 2\} = \{x \| (x \in ℤ \land \exists i \in I x = i \cdot 2)\}$
57	2	rnmpt	$⊢ ran F = \{x \| \exists j \in I x = j \cdot 2\}$
58		df-rab	$⊢ \{x \in ℤ \| \exists i \in I x = i \cdot 2\} = \{x \| (x \in ℤ \land \exists i \in I x = i \cdot 2)\}$
59	56 57 58	3eqtr4i	$⊢ ran F = \{x \in ℤ \| \exists i \in I x = i \cdot 2\}$
60		dff1o5	$⊢ F : I \underset{1-1 onto}{⟶} \{x \in ℤ \| \exists i \in I x = i \cdot 2\} \leftrightarrow (F : I \underset{1-1}{⟶} \{x \in ℤ \| \exists i \in I x = i \cdot 2\} \land ran F = \{x \in ℤ \| \exists i \in I x = i \cdot 2\})$
61	43 59 60	mpbir2an	$⊢ F : I \underset{1-1 onto}{⟶} \{x \in ℤ \| \exists i \in I x = i \cdot 2\}$

Metamath Proof Explorer

Theorem 2lgslem1b

Proof