Theorem 2lgslem1b

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

	Ref	Expression
Hypotheses	2lgslem1b.i	⊢ 𝐼 = ( 𝐴 ... 𝐵 )
	2lgslem1b.f	⊢ 𝐹 = ( 𝑗 ∈ 𝐼 ↦ ( 𝑗 · 2 ) )
Assertion	2lgslem1b	⊢ 𝐹 : 𝐼 –1-1-onto→ { 𝑥 ∈ ℤ ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = ( 𝑖 · 2 ) }

Proof

Step	Hyp	Ref	Expression
1		2lgslem1b.i	⊢ 𝐼 = ( 𝐴 ... 𝐵 )
2		2lgslem1b.f	⊢ 𝐹 = ( 𝑗 ∈ 𝐼 ↦ ( 𝑗 · 2 ) )
3		eqeq1	⊢ ( 𝑥 = ( 𝑗 · 2 ) → ( 𝑥 = ( 𝑖 · 2 ) ↔ ( 𝑗 · 2 ) = ( 𝑖 · 2 ) ) )
4	3	rexbidv	⊢ ( 𝑥 = ( 𝑗 · 2 ) → ( ∃ 𝑖 ∈ 𝐼 𝑥 = ( 𝑖 · 2 ) ↔ ∃ 𝑖 ∈ 𝐼 ( 𝑗 · 2 ) = ( 𝑖 · 2 ) ) )
5		elfzelz	⊢ ( 𝑗 ∈ ( 𝐴 ... 𝐵 ) → 𝑗 ∈ ℤ )
6	5 1	eleq2s	⊢ ( 𝑗 ∈ 𝐼 → 𝑗 ∈ ℤ )
7		2z	⊢ 2 ∈ ℤ
8	7	a1i	⊢ ( 𝑗 ∈ 𝐼 → 2 ∈ ℤ )
9	6 8	zmulcld	⊢ ( 𝑗 ∈ 𝐼 → ( 𝑗 · 2 ) ∈ ℤ )
10		id	⊢ ( 𝑗 ∈ 𝐼 → 𝑗 ∈ 𝐼 )
11		oveq1	⊢ ( 𝑖 = 𝑗 → ( 𝑖 · 2 ) = ( 𝑗 · 2 ) )
12	11	eqeq2d	⊢ ( 𝑖 = 𝑗 → ( ( 𝑗 · 2 ) = ( 𝑖 · 2 ) ↔ ( 𝑗 · 2 ) = ( 𝑗 · 2 ) ) )
13	12	adantl	⊢ ( ( 𝑗 ∈ 𝐼 ∧ 𝑖 = 𝑗 ) → ( ( 𝑗 · 2 ) = ( 𝑖 · 2 ) ↔ ( 𝑗 · 2 ) = ( 𝑗 · 2 ) ) )
14		eqidd	⊢ ( 𝑗 ∈ 𝐼 → ( 𝑗 · 2 ) = ( 𝑗 · 2 ) )
15	10 13 14	rspcedvd	⊢ ( 𝑗 ∈ 𝐼 → ∃ 𝑖 ∈ 𝐼 ( 𝑗 · 2 ) = ( 𝑖 · 2 ) )
16	4 9 15	elrabd	⊢ ( 𝑗 ∈ 𝐼 → ( 𝑗 · 2 ) ∈ { 𝑥 ∈ ℤ ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = ( 𝑖 · 2 ) } )
17	2 16	fmpti	⊢ 𝐹 : 𝐼 ⟶ { 𝑥 ∈ ℤ ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = ( 𝑖 · 2 ) }
18		oveq1	⊢ ( 𝑗 = 𝑦 → ( 𝑗 · 2 ) = ( 𝑦 · 2 ) )
19		simpl	⊢ ( ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼 ) → 𝑦 ∈ 𝐼 )
20		ovexd	⊢ ( ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼 ) → ( 𝑦 · 2 ) ∈ V )
21	2 18 19 20	fvmptd3	⊢ ( ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 · 2 ) )
22		oveq1	⊢ ( 𝑗 = 𝑧 → ( 𝑗 · 2 ) = ( 𝑧 · 2 ) )
23		simpr	⊢ ( ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼 ) → 𝑧 ∈ 𝐼 )
24		ovexd	⊢ ( ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼 ) → ( 𝑧 · 2 ) ∈ V )
25	2 22 23 24	fvmptd3	⊢ ( ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝑧 · 2 ) )
26	21 25	eqeq12d	⊢ ( ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ↔ ( 𝑦 · 2 ) = ( 𝑧 · 2 ) ) )
27		elfzelz	⊢ ( 𝑦 ∈ ( 𝐴 ... 𝐵 ) → 𝑦 ∈ ℤ )
28	27 1	eleq2s	⊢ ( 𝑦 ∈ 𝐼 → 𝑦 ∈ ℤ )
29	28	zcnd	⊢ ( 𝑦 ∈ 𝐼 → 𝑦 ∈ ℂ )
30	29	adantr	⊢ ( ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼 ) → 𝑦 ∈ ℂ )
31		elfzelz	⊢ ( 𝑧 ∈ ( 𝐴 ... 𝐵 ) → 𝑧 ∈ ℤ )
32	31 1	eleq2s	⊢ ( 𝑧 ∈ 𝐼 → 𝑧 ∈ ℤ )
33	32	zcnd	⊢ ( 𝑧 ∈ 𝐼 → 𝑧 ∈ ℂ )
34	33	adantl	⊢ ( ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼 ) → 𝑧 ∈ ℂ )
35		2cnd	⊢ ( ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼 ) → 2 ∈ ℂ )
36		2ne0	⊢ 2 ≠ 0
37	36	a1i	⊢ ( ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼 ) → 2 ≠ 0 )
38	30 34 35 37	mulcan2d	⊢ ( ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼 ) → ( ( 𝑦 · 2 ) = ( 𝑧 · 2 ) ↔ 𝑦 = 𝑧 ) )
39	38	biimpd	⊢ ( ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼 ) → ( ( 𝑦 · 2 ) = ( 𝑧 · 2 ) → 𝑦 = 𝑧 ) )
40	26 39	sylbid	⊢ ( ( 𝑦 ∈ 𝐼 ∧ 𝑧 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) → 𝑦 = 𝑧 ) )
41	40	rgen2	⊢ ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 𝐼 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) → 𝑦 = 𝑧 )
42		dff13	⊢ ( 𝐹 : 𝐼 –1-1→ { 𝑥 ∈ ℤ ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = ( 𝑖 · 2 ) } ↔ ( 𝐹 : 𝐼 ⟶ { 𝑥 ∈ ℤ ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = ( 𝑖 · 2 ) } ∧ ∀ 𝑦 ∈ 𝐼 ∀ 𝑧 ∈ 𝐼 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) → 𝑦 = 𝑧 ) ) )
43	17 41 42	mpbir2an	⊢ 𝐹 : 𝐼 –1-1→ { 𝑥 ∈ ℤ ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = ( 𝑖 · 2 ) }
44		oveq1	⊢ ( 𝑗 = 𝑖 → ( 𝑗 · 2 ) = ( 𝑖 · 2 ) )
45	44	eqeq2d	⊢ ( 𝑗 = 𝑖 → ( 𝑥 = ( 𝑗 · 2 ) ↔ 𝑥 = ( 𝑖 · 2 ) ) )
46	45	cbvrexvw	⊢ ( ∃ 𝑗 ∈ 𝐼 𝑥 = ( 𝑗 · 2 ) ↔ ∃ 𝑖 ∈ 𝐼 𝑥 = ( 𝑖 · 2 ) )
47		elfzelz	⊢ ( 𝑖 ∈ ( 𝐴 ... 𝐵 ) → 𝑖 ∈ ℤ )
48	7	a1i	⊢ ( 𝑖 ∈ ( 𝐴 ... 𝐵 ) → 2 ∈ ℤ )
49	47 48	zmulcld	⊢ ( 𝑖 ∈ ( 𝐴 ... 𝐵 ) → ( 𝑖 · 2 ) ∈ ℤ )
50	49 1	eleq2s	⊢ ( 𝑖 ∈ 𝐼 → ( 𝑖 · 2 ) ∈ ℤ )
51		eleq1	⊢ ( 𝑥 = ( 𝑖 · 2 ) → ( 𝑥 ∈ ℤ ↔ ( 𝑖 · 2 ) ∈ ℤ ) )
52	50 51	syl5ibrcom	⊢ ( 𝑖 ∈ 𝐼 → ( 𝑥 = ( 𝑖 · 2 ) → 𝑥 ∈ ℤ ) )
53	52	rexlimiv	⊢ ( ∃ 𝑖 ∈ 𝐼 𝑥 = ( 𝑖 · 2 ) → 𝑥 ∈ ℤ )
54	53	pm4.71ri	⊢ ( ∃ 𝑖 ∈ 𝐼 𝑥 = ( 𝑖 · 2 ) ↔ ( 𝑥 ∈ ℤ ∧ ∃ 𝑖 ∈ 𝐼 𝑥 = ( 𝑖 · 2 ) ) )
55	46 54	bitri	⊢ ( ∃ 𝑗 ∈ 𝐼 𝑥 = ( 𝑗 · 2 ) ↔ ( 𝑥 ∈ ℤ ∧ ∃ 𝑖 ∈ 𝐼 𝑥 = ( 𝑖 · 2 ) ) )
56	55	abbii	⊢ { 𝑥 ∣ ∃ 𝑗 ∈ 𝐼 𝑥 = ( 𝑗 · 2 ) } = { 𝑥 ∣ ( 𝑥 ∈ ℤ ∧ ∃ 𝑖 ∈ 𝐼 𝑥 = ( 𝑖 · 2 ) ) }
57	2	rnmpt	⊢ ran 𝐹 = { 𝑥 ∣ ∃ 𝑗 ∈ 𝐼 𝑥 = ( 𝑗 · 2 ) }
58		df-rab	⊢ { 𝑥 ∈ ℤ ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = ( 𝑖 · 2 ) } = { 𝑥 ∣ ( 𝑥 ∈ ℤ ∧ ∃ 𝑖 ∈ 𝐼 𝑥 = ( 𝑖 · 2 ) ) }
59	56 57 58	3eqtr4i	⊢ ran 𝐹 = { 𝑥 ∈ ℤ ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = ( 𝑖 · 2 ) }
60		dff1o5	⊢ ( 𝐹 : 𝐼 –1-1-onto→ { 𝑥 ∈ ℤ ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = ( 𝑖 · 2 ) } ↔ ( 𝐹 : 𝐼 –1-1→ { 𝑥 ∈ ℤ ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = ( 𝑖 · 2 ) } ∧ ran 𝐹 = { 𝑥 ∈ ℤ ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = ( 𝑖 · 2 ) } ) )
61	43 59 60	mpbir2an	⊢ 𝐹 : 𝐼 –1-1-onto→ { 𝑥 ∈ ℤ ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = ( 𝑖 · 2 ) }