Step | Hyp | Ref
| Expression |
1 | | 2lgslem1b.f |
. . . 4
⊢ 𝐹 = (𝑗 ∈ 𝐼 ↦ (𝑗 · 2)) |
2 | | elfzelz 12213 |
. . . . . . 7
⊢ (𝑗 ∈ (𝐴...𝐵) → 𝑗 ∈ ℤ) |
3 | | 2lgslem1b.i |
. . . . . . 7
⊢ 𝐼 = (𝐴...𝐵) |
4 | 2, 3 | eleq2s 2706 |
. . . . . 6
⊢ (𝑗 ∈ 𝐼 → 𝑗 ∈ ℤ) |
5 | | 2z 11286 |
. . . . . . 7
⊢ 2 ∈
ℤ |
6 | 5 | a1i 11 |
. . . . . 6
⊢ (𝑗 ∈ 𝐼 → 2 ∈ ℤ) |
7 | 4, 6 | zmulcld 11364 |
. . . . 5
⊢ (𝑗 ∈ 𝐼 → (𝑗 · 2) ∈ ℤ) |
8 | | id 22 |
. . . . . 6
⊢ (𝑗 ∈ 𝐼 → 𝑗 ∈ 𝐼) |
9 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑖 = 𝑗 → (𝑖 · 2) = (𝑗 · 2)) |
10 | 9 | eqeq2d 2620 |
. . . . . . 7
⊢ (𝑖 = 𝑗 → ((𝑗 · 2) = (𝑖 · 2) ↔ (𝑗 · 2) = (𝑗 · 2))) |
11 | 10 | adantl 481 |
. . . . . 6
⊢ ((𝑗 ∈ 𝐼 ∧ 𝑖 = 𝑗) → ((𝑗 · 2) = (𝑖 · 2) ↔ (𝑗 · 2) = (𝑗 · 2))) |
12 | | eqidd 2611 |
. . . . . 6
⊢ (𝑗 ∈ 𝐼 → (𝑗 · 2) = (𝑗 · 2)) |
13 | 8, 11, 12 | rspcedvd 3289 |
. . . . 5
⊢ (𝑗 ∈ 𝐼 → ∃𝑖 ∈ 𝐼 (𝑗 · 2) = (𝑖 · 2)) |
14 | | eqeq1 2614 |
. . . . . . 7
⊢ (𝑥 = (𝑗 · 2) → (𝑥 = (𝑖 · 2) ↔ (𝑗 · 2) = (𝑖 · 2))) |
15 | 14 | rexbidv 3034 |
. . . . . 6
⊢ (𝑥 = (𝑗 · 2) → (∃𝑖 ∈ 𝐼 𝑥 = (𝑖 · 2) ↔ ∃𝑖 ∈ 𝐼 (𝑗 · 2) = (𝑖 · 2))) |
16 | 15 | elrab 3331 |
. . . . 5
⊢ ((𝑗 · 2) ∈ {𝑥 ∈ ℤ ∣
∃𝑖 ∈ 𝐼 𝑥 = (𝑖 · 2)} ↔ ((𝑗 · 2) ∈ ℤ ∧
∃𝑖 ∈ 𝐼 (𝑗 · 2) = (𝑖 · 2))) |
17 | 7, 13, 16 | sylanbrc 695 |
. . . 4
⊢ (𝑗 ∈ 𝐼 → (𝑗 · 2) ∈ {𝑥 ∈ ℤ ∣ ∃𝑖 ∈ 𝐼 𝑥 = (𝑖 · 2)}) |
18 | 1, 17 | fmpti 6291 |
. . 3
⊢ 𝐹:𝐼⟶{𝑥 ∈ ℤ ∣ ∃𝑖 ∈ 𝐼 𝑥 = (𝑖 · 2)} |
19 | 1 | a1i 11 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼) → 𝐹 = (𝑗 ∈ 𝐼 ↦ (𝑗 · 2))) |
20 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑗 = 𝑦 → (𝑗 · 2) = (𝑦 · 2)) |
21 | 20 | adantl 481 |
. . . . . . 7
⊢ (((𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼) ∧ 𝑗 = 𝑦) → (𝑗 · 2) = (𝑦 · 2)) |
22 | | simpl 472 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼) → 𝑦 ∈ 𝐼) |
23 | | ovex 6577 |
. . . . . . . 8
⊢ (𝑦 · 2) ∈
V |
24 | 23 | a1i 11 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼) → (𝑦 · 2) ∈ V) |
25 | 19, 21, 22, 24 | fvmptd 6197 |
. . . . . 6
⊢ ((𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑦) = (𝑦 · 2)) |
26 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑗 = 𝑧 → (𝑗 · 2) = (𝑧 · 2)) |
27 | 26 | adantl 481 |
. . . . . . 7
⊢ (((𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼) ∧ 𝑗 = 𝑧) → (𝑗 · 2) = (𝑧 · 2)) |
28 | | simpr 476 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼) → 𝑧 ∈ 𝐼) |
29 | | ovex 6577 |
. . . . . . . 8
⊢ (𝑧 · 2) ∈
V |
30 | 29 | a1i 11 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼) → (𝑧 · 2) ∈ V) |
31 | 19, 27, 28, 30 | fvmptd 6197 |
. . . . . 6
⊢ ((𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) = (𝑧 · 2)) |
32 | 25, 31 | eqeq12d 2625 |
. . . . 5
⊢ ((𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼) → ((𝐹‘𝑦) = (𝐹‘𝑧) ↔ (𝑦 · 2) = (𝑧 · 2))) |
33 | | elfzelz 12213 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (𝐴...𝐵) → 𝑦 ∈ ℤ) |
34 | 33, 3 | eleq2s 2706 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐼 → 𝑦 ∈ ℤ) |
35 | 34 | zcnd 11359 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐼 → 𝑦 ∈ ℂ) |
36 | 35 | adantr 480 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼) → 𝑦 ∈ ℂ) |
37 | | elfzelz 12213 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝐴...𝐵) → 𝑧 ∈ ℤ) |
38 | 37, 3 | eleq2s 2706 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝐼 → 𝑧 ∈ ℤ) |
39 | 38 | zcnd 11359 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝐼 → 𝑧 ∈ ℂ) |
40 | 39 | adantl 481 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼) → 𝑧 ∈ ℂ) |
41 | | 2cnd 10970 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼) → 2 ∈ ℂ) |
42 | | 2ne0 10990 |
. . . . . . . 8
⊢ 2 ≠
0 |
43 | 42 | a1i 11 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼) → 2 ≠ 0) |
44 | 36, 40, 41, 43 | mulcan2d 10540 |
. . . . . 6
⊢ ((𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼) → ((𝑦 · 2) = (𝑧 · 2) ↔ 𝑦 = 𝑧)) |
45 | 44 | biimpd 218 |
. . . . 5
⊢ ((𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼) → ((𝑦 · 2) = (𝑧 · 2) → 𝑦 = 𝑧)) |
46 | 32, 45 | sylbid 229 |
. . . 4
⊢ ((𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼) → ((𝐹‘𝑦) = (𝐹‘𝑧) → 𝑦 = 𝑧)) |
47 | 46 | rgen2 2958 |
. . 3
⊢
∀𝑦 ∈
𝐼 ∀𝑧 ∈ 𝐼 ((𝐹‘𝑦) = (𝐹‘𝑧) → 𝑦 = 𝑧) |
48 | | dff13 6416 |
. . 3
⊢ (𝐹:𝐼–1-1→{𝑥 ∈ ℤ ∣ ∃𝑖 ∈ 𝐼 𝑥 = (𝑖 · 2)} ↔ (𝐹:𝐼⟶{𝑥 ∈ ℤ ∣ ∃𝑖 ∈ 𝐼 𝑥 = (𝑖 · 2)} ∧ ∀𝑦 ∈ 𝐼 ∀𝑧 ∈ 𝐼 ((𝐹‘𝑦) = (𝐹‘𝑧) → 𝑦 = 𝑧))) |
49 | 18, 47, 48 | mpbir2an 957 |
. 2
⊢ 𝐹:𝐼–1-1→{𝑥 ∈ ℤ ∣ ∃𝑖 ∈ 𝐼 𝑥 = (𝑖 · 2)} |
50 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑗 = 𝑖 → (𝑗 · 2) = (𝑖 · 2)) |
51 | 50 | eqeq2d 2620 |
. . . . . 6
⊢ (𝑗 = 𝑖 → (𝑥 = (𝑗 · 2) ↔ 𝑥 = (𝑖 · 2))) |
52 | 51 | cbvrexv 3148 |
. . . . 5
⊢
(∃𝑗 ∈
𝐼 𝑥 = (𝑗 · 2) ↔ ∃𝑖 ∈ 𝐼 𝑥 = (𝑖 · 2)) |
53 | | elfzelz 12213 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (𝐴...𝐵) → 𝑖 ∈ ℤ) |
54 | 5 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (𝐴...𝐵) → 2 ∈ ℤ) |
55 | 53, 54 | zmulcld 11364 |
. . . . . . . . 9
⊢ (𝑖 ∈ (𝐴...𝐵) → (𝑖 · 2) ∈ ℤ) |
56 | 55, 3 | eleq2s 2706 |
. . . . . . . 8
⊢ (𝑖 ∈ 𝐼 → (𝑖 · 2) ∈ ℤ) |
57 | | eleq1 2676 |
. . . . . . . 8
⊢ (𝑥 = (𝑖 · 2) → (𝑥 ∈ ℤ ↔ (𝑖 · 2) ∈
ℤ)) |
58 | 56, 57 | syl5ibrcom 236 |
. . . . . . 7
⊢ (𝑖 ∈ 𝐼 → (𝑥 = (𝑖 · 2) → 𝑥 ∈ ℤ)) |
59 | 58 | rexlimiv 3009 |
. . . . . 6
⊢
(∃𝑖 ∈
𝐼 𝑥 = (𝑖 · 2) → 𝑥 ∈ ℤ) |
60 | 59 | pm4.71ri 663 |
. . . . 5
⊢
(∃𝑖 ∈
𝐼 𝑥 = (𝑖 · 2) ↔ (𝑥 ∈ ℤ ∧ ∃𝑖 ∈ 𝐼 𝑥 = (𝑖 · 2))) |
61 | 52, 60 | bitri 263 |
. . . 4
⊢
(∃𝑗 ∈
𝐼 𝑥 = (𝑗 · 2) ↔ (𝑥 ∈ ℤ ∧ ∃𝑖 ∈ 𝐼 𝑥 = (𝑖 · 2))) |
62 | 61 | abbii 2726 |
. . 3
⊢ {𝑥 ∣ ∃𝑗 ∈ 𝐼 𝑥 = (𝑗 · 2)} = {𝑥 ∣ (𝑥 ∈ ℤ ∧ ∃𝑖 ∈ 𝐼 𝑥 = (𝑖 · 2))} |
63 | 1 | rnmpt 5292 |
. . 3
⊢ ran 𝐹 = {𝑥 ∣ ∃𝑗 ∈ 𝐼 𝑥 = (𝑗 · 2)} |
64 | | df-rab 2905 |
. . 3
⊢ {𝑥 ∈ ℤ ∣
∃𝑖 ∈ 𝐼 𝑥 = (𝑖 · 2)} = {𝑥 ∣ (𝑥 ∈ ℤ ∧ ∃𝑖 ∈ 𝐼 𝑥 = (𝑖 · 2))} |
65 | 62, 63, 64 | 3eqtr4i 2642 |
. 2
⊢ ran 𝐹 = {𝑥 ∈ ℤ ∣ ∃𝑖 ∈ 𝐼 𝑥 = (𝑖 · 2)} |
66 | | dff1o5 6059 |
. 2
⊢ (𝐹:𝐼–1-1-onto→{𝑥 ∈ ℤ ∣ ∃𝑖 ∈ 𝐼 𝑥 = (𝑖 · 2)} ↔ (𝐹:𝐼–1-1→{𝑥 ∈ ℤ ∣ ∃𝑖 ∈ 𝐼 𝑥 = (𝑖 · 2)} ∧ ran 𝐹 = {𝑥 ∈ ℤ ∣ ∃𝑖 ∈ 𝐼 𝑥 = (𝑖 · 2)})) |
67 | 49, 65, 66 | mpbir2an 957 |
1
⊢ 𝐹:𝐼–1-1-onto→{𝑥 ∈ ℤ ∣ ∃𝑖 ∈ 𝐼 𝑥 = (𝑖 · 2)} |