# Metamath Proof Explorer

## Theorem 2lgslem1b

Description: Lemma 2 for 2lgslem1 . (Contributed by AV, 18-Jun-2021)

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

### Proof

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