Theorem prodeq2ii 16112

Description: Equality theorem for product, with the class expressions 𝐵 and 𝐶 guarded by I to be always sets. (Contributed by Scott Fenton, 4-Dec-2017.)

Assertion

Ref	Expression
prodeq2ii	⊢ (∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶)

Distinct variable group:   𝐴,𝑘

Allowed substitution hints:   𝐵(𝑘)   𝐶(𝑘)

Proof of Theorem prodeq2ii

Dummy variables 𝑓 𝑚 𝑛 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eluzelz 13005	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (ℤ≥‘𝑚) → 𝑛 ∈ ℤ)
2	1	adantl 487	. . . . . . . . . . . 12 ⊢ ((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑛 ∈ (ℤ≥‘𝑚)) → 𝑛 ∈ ℤ)
3		nfra1 3290	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶)
4		rsp 3254	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) → (𝑘 ∈ 𝐴 → ( I ‘𝐵) = ( I ‘𝐶)))
5	4	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑘 ∈ ℤ) → (𝑘 ∈ 𝐴 → ( I ‘𝐵) = ( I ‘𝐶)))
6		ifeq1 4489	. . . . . . . . . . . . . . . . . . . 20 ⊢ (( I ‘𝐵) = ( I ‘𝐶) → if(𝑘 ∈ 𝐴, ( I ‘𝐵), ( I ‘1)) = if(𝑘 ∈ 𝐴, ( I ‘𝐶), ( I ‘1)))
7	5, 6	syl6 36	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑘 ∈ ℤ) → (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, ( I ‘𝐵), ( I ‘1)) = if(𝑘 ∈ 𝐴, ( I ‘𝐶), ( I ‘1))))
8		iffalse 4494	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, ( I ‘𝐵), ( I ‘1)) = ( I ‘1))
9		iffalse 4494	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ 𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, ( I ‘𝐶), ( I ‘1)) = ( I ‘1))
10	8, 9	eqtr4d 2801	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, ( I ‘𝐵), ( I ‘1)) = if(𝑘 ∈ 𝐴, ( I ‘𝐶), ( I ‘1)))
11	7, 10	pm2.61d1 182	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑘 ∈ ℤ) → if(𝑘 ∈ 𝐴, ( I ‘𝐵), ( I ‘1)) = if(𝑘 ∈ 𝐴, ( I ‘𝐶), ( I ‘1)))
12		fvif 6927	. . . . . . . . . . . . . . . . . 18 ⊢ ( I ‘if(𝑘 ∈ 𝐴, 𝐵, 1)) = if(𝑘 ∈ 𝐴, ( I ‘𝐵), ( I ‘1))
13		fvif 6927	. . . . . . . . . . . . . . . . . 18 ⊢ ( I ‘if(𝑘 ∈ 𝐴, 𝐶, 1)) = if(𝑘 ∈ 𝐴, ( I ‘𝐶), ( I ‘1))
14	11, 12, 13	3eqtr4g 2823	. . . . . . . . . . . . . . . . 17 ⊢ ((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑘 ∈ ℤ) → ( I ‘if(𝑘 ∈ 𝐴, 𝐵, 1)) = ( I ‘if(𝑘 ∈ 𝐴, 𝐶, 1)))
15	3, 14	mpteq2da 5201	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) → (𝑘 ∈ ℤ ↦ ( I ‘if(𝑘 ∈ 𝐴, 𝐵, 1))) = (𝑘 ∈ ℤ ↦ ( I ‘if(𝑘 ∈ 𝐴, 𝐶, 1))))
16	15	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑥 ∈ (ℤ≥‘𝑛)) → (𝑘 ∈ ℤ ↦ ( I ‘if(𝑘 ∈ 𝐴, 𝐵, 1))) = (𝑘 ∈ ℤ ↦ ( I ‘if(𝑘 ∈ 𝐴, 𝐶, 1))))
17	16	fveq1d 6913	. . . . . . . . . . . . . 14 ⊢ ((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑥 ∈ (ℤ≥‘𝑛)) → ((𝑘 ∈ ℤ ↦ ( I ‘if(𝑘 ∈ 𝐴, 𝐵, 1)))‘𝑥) = ((𝑘 ∈ ℤ ↦ ( I ‘if(𝑘 ∈ 𝐴, 𝐶, 1)))‘𝑥))
18	17	adantlr 728	. . . . . . . . . . . . 13 ⊢ (((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑛 ∈ (ℤ≥‘𝑚)) ∧ 𝑥 ∈ (ℤ≥‘𝑛)) → ((𝑘 ∈ ℤ ↦ ( I ‘if(𝑘 ∈ 𝐴, 𝐵, 1)))‘𝑥) = ((𝑘 ∈ ℤ ↦ ( I ‘if(𝑘 ∈ 𝐴, 𝐶, 1)))‘𝑥))
19		eqid 2763	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1)) = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))
20		eqid 2763	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℤ ↦ ( I ‘if(𝑘 ∈ 𝐴, 𝐵, 1))) = (𝑘 ∈ ℤ ↦ ( I ‘if(𝑘 ∈ 𝐴, 𝐵, 1)))
21	19, 20	fvmptex 7034	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑥) = ((𝑘 ∈ ℤ ↦ ( I ‘if(𝑘 ∈ 𝐴, 𝐵, 1)))‘𝑥)
22		eqid 2763	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1)) = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))
23		eqid 2763	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℤ ↦ ( I ‘if(𝑘 ∈ 𝐴, 𝐶, 1))) = (𝑘 ∈ ℤ ↦ ( I ‘if(𝑘 ∈ 𝐴, 𝐶, 1)))
24	22, 23	fvmptex 7034	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))‘𝑥) = ((𝑘 ∈ ℤ ↦ ( I ‘if(𝑘 ∈ 𝐴, 𝐶, 1)))‘𝑥)
25	18, 21, 24	3eqtr4g 2823	. . . . . . . . . . . 12 ⊢ (((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑛 ∈ (ℤ≥‘𝑚)) ∧ 𝑥 ∈ (ℤ≥‘𝑛)) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑥) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))‘𝑥))
26	2, 25	seqfeq 14200	. . . . . . . . . . 11 ⊢ ((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑛 ∈ (ℤ≥‘𝑚)) → seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) = seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))))
27	26	breq1d 5116	. . . . . . . . . 10 ⊢ ((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑛 ∈ (ℤ≥‘𝑚)) → (seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦 ↔ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦))
28	27	anbi2d 642	. . . . . . . . 9 ⊢ ((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑛 ∈ (ℤ≥‘𝑚)) → ((𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ↔ (𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦)))
29	28	exbidv 1956	. . . . . . . 8 ⊢ ((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑛 ∈ (ℤ≥‘𝑚)) → (∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ↔ ∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦)))
30	29	rexbidva 3188	. . . . . . 7 ⊢ (∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) → (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ↔ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦)))
31	30	adantr 486	. . . . . 6 ⊢ ((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑚 ∈ ℤ) → (∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ↔ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦)))
32		simpr 490	. . . . . . . 8 ⊢ ((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑚 ∈ ℤ) → 𝑚 ∈ ℤ)
33	15	adantr 486	. . . . . . . . . . 11 ⊢ ((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑥 ∈ (ℤ≥‘𝑚)) → (𝑘 ∈ ℤ ↦ ( I ‘if(𝑘 ∈ 𝐴, 𝐵, 1))) = (𝑘 ∈ ℤ ↦ ( I ‘if(𝑘 ∈ 𝐴, 𝐶, 1))))
34	33	fveq1d 6913	. . . . . . . . . 10 ⊢ ((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑥 ∈ (ℤ≥‘𝑚)) → ((𝑘 ∈ ℤ ↦ ( I ‘if(𝑘 ∈ 𝐴, 𝐵, 1)))‘𝑥) = ((𝑘 ∈ ℤ ↦ ( I ‘if(𝑘 ∈ 𝐴, 𝐶, 1)))‘𝑥))
35	34, 21, 24	3eqtr4g 2823	. . . . . . . . 9 ⊢ ((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑥 ∈ (ℤ≥‘𝑚)) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑥) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))‘𝑥))
36	35	adantlr 728	. . . . . . . 8 ⊢ (((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑚 ∈ ℤ) ∧ 𝑥 ∈ (ℤ≥‘𝑚)) → ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))‘𝑥) = ((𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))‘𝑥))
37	32, 36	seqfeq 14200	. . . . . . 7 ⊢ ((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑚 ∈ ℤ) → seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) = seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))))
38	37	breq1d 5116	. . . . . 6 ⊢ ((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑚 ∈ ℤ) → (seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥 ↔ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥))
39	31, 38	3anbi23d 1468	. . . . 5 ⊢ ((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑚 ∈ ℤ) → ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥)))
40	39	rexbidva 3188	. . . 4 ⊢ (∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) → (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ↔ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥)))
41		simplr 781	. . . . . . . . . 10 ⊢ (((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)⟶1-1onto𝐴) → 𝑚 ∈ ℕ)
42		nnuz 13034	. . . . . . . . . 10 ⊢ ℕ = (ℤ≥‘1)
43	41, 42	eleqtrdi 2874	. . . . . . . . 9 ⊢ (((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)⟶1-1onto𝐴) → 𝑚 ∈ (ℤ≥‘1))
44		f1of 6849	. . . . . . . . . . . . . 14 ⊢ (𝑓:(1...𝑚)⟶1-1onto𝐴 → 𝑓:(1...𝑚)⟶𝐴)
45	44	ad2antlr 740	. . . . . . . . . . . . 13 ⊢ ((((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)⟶1-1onto𝐴) ∧ 𝑥 ∈ (1...𝑚)) → 𝑓:(1...𝑚)⟶𝐴)
46		ffvelcdm 7108	. . . . . . . . . . . . 13 ⊢ ((𝑓:(1...𝑚)⟶𝐴 ∧ 𝑥 ∈ (1...𝑚)) → (𝑓‘𝑥) ∈ 𝐴)
47	45, 46	sylancom 600	. . . . . . . . . . . 12 ⊢ ((((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)⟶1-1onto𝐴) ∧ 𝑥 ∈ (1...𝑚)) → (𝑓‘𝑥) ∈ 𝐴)
48		simplll 787	. . . . . . . . . . . 12 ⊢ ((((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)⟶1-1onto𝐴) ∧ 𝑥 ∈ (1...𝑚)) → ∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶))
49		nfcsb1v 3875	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘⦋(𝑓‘𝑥) / 𝑘⦌( I ‘𝐵)
50		nfcsb1v 3875	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑘⦋(𝑓‘𝑥) / 𝑘⦌( I ‘𝐶)
51	49, 50	nfeq 2939	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑘⦋(𝑓‘𝑥) / 𝑘⦌( I ‘𝐵) = ⦋(𝑓‘𝑥) / 𝑘⦌( I ‘𝐶)
52		csbeq1a 3865	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑓‘𝑥) → ( I ‘𝐵) = ⦋(𝑓‘𝑥) / 𝑘⦌( I ‘𝐵))
53		csbeq1a 3865	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑓‘𝑥) → ( I ‘𝐶) = ⦋(𝑓‘𝑥) / 𝑘⦌( I ‘𝐶))
54	52, 53	eqeq12d 2779	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑓‘𝑥) → (( I ‘𝐵) = ( I ‘𝐶) ↔ ⦋(𝑓‘𝑥) / 𝑘⦌( I ‘𝐵) = ⦋(𝑓‘𝑥) / 𝑘⦌( I ‘𝐶)))
55	51, 54	rspc 3568	. . . . . . . . . . . 12 ⊢ ((𝑓‘𝑥) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) → ⦋(𝑓‘𝑥) / 𝑘⦌( I ‘𝐵) = ⦋(𝑓‘𝑥) / 𝑘⦌( I ‘𝐶)))
56	47, 48, 55	sylc 66	. . . . . . . . . . 11 ⊢ ((((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)⟶1-1onto𝐴) ∧ 𝑥 ∈ (1...𝑚)) → ⦋(𝑓‘𝑥) / 𝑘⦌( I ‘𝐵) = ⦋(𝑓‘𝑥) / 𝑘⦌( I ‘𝐶))
57		fvex 6924	. . . . . . . . . . . 12 ⊢ (𝑓‘𝑥) ∈ V
58		csbfv2g 6957	. . . . . . . . . . . 12 ⊢ ((𝑓‘𝑥) ∈ V → ⦋(𝑓‘𝑥) / 𝑘⦌( I ‘𝐵) = ( I ‘⦋(𝑓‘𝑥) / 𝑘⦌𝐵))
59	57, 58	ax-mp 5	. . . . . . . . . . 11 ⊢ ⦋(𝑓‘𝑥) / 𝑘⦌( I ‘𝐵) = ( I ‘⦋(𝑓‘𝑥) / 𝑘⦌𝐵)
60		csbfv2g 6957	. . . . . . . . . . . 12 ⊢ ((𝑓‘𝑥) ∈ V → ⦋(𝑓‘𝑥) / 𝑘⦌( I ‘𝐶) = ( I ‘⦋(𝑓‘𝑥) / 𝑘⦌𝐶))
61	57, 60	ax-mp 5	. . . . . . . . . . 11 ⊢ ⦋(𝑓‘𝑥) / 𝑘⦌( I ‘𝐶) = ( I ‘⦋(𝑓‘𝑥) / 𝑘⦌𝐶)
62	56, 59, 61	3eqtr3g 2821	. . . . . . . . . 10 ⊢ ((((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)⟶1-1onto𝐴) ∧ 𝑥 ∈ (1...𝑚)) → ( I ‘⦋(𝑓‘𝑥) / 𝑘⦌𝐵) = ( I ‘⦋(𝑓‘𝑥) / 𝑘⦌𝐶))
63		elfznn 13717	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (1...𝑚) → 𝑥 ∈ ℕ)
64	63	adantl 487	. . . . . . . . . . 11 ⊢ ((((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)⟶1-1onto𝐴) ∧ 𝑥 ∈ (1...𝑚)) → 𝑥 ∈ ℕ)
65		fveq2 6911	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑥 → (𝑓‘𝑛) = (𝑓‘𝑥))
66	65	csbeq1d 3855	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑥 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐵 = ⦋(𝑓‘𝑥) / 𝑘⦌𝐵)
67		eqid 2763	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵) = (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵)
68	66, 67	fvmpti 7018	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵)‘𝑥) = ( I ‘⦋(𝑓‘𝑥) / 𝑘⦌𝐵))
69	64, 68	syl 18	. . . . . . . . . 10 ⊢ ((((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)⟶1-1onto𝐴) ∧ 𝑥 ∈ (1...𝑚)) → ((𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵)‘𝑥) = ( I ‘⦋(𝑓‘𝑥) / 𝑘⦌𝐵))
70	65	csbeq1d 3855	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑥 → ⦋(𝑓‘𝑛) / 𝑘⦌𝐶 = ⦋(𝑓‘𝑥) / 𝑘⦌𝐶)
71		eqid 2763	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶) = (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶)
72	70, 71	fvmpti 7018	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℕ → ((𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶)‘𝑥) = ( I ‘⦋(𝑓‘𝑥) / 𝑘⦌𝐶))
73	64, 72	syl 18	. . . . . . . . . 10 ⊢ ((((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)⟶1-1onto𝐴) ∧ 𝑥 ∈ (1...𝑚)) → ((𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶)‘𝑥) = ( I ‘⦋(𝑓‘𝑥) / 𝑘⦌𝐶))
74	62, 69, 73	3eqtr4d 2808	. . . . . . . . 9 ⊢ ((((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)⟶1-1onto𝐴) ∧ 𝑥 ∈ (1...𝑚)) → ((𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵)‘𝑥) = ((𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶)‘𝑥))
75	43, 74	seqfveq 14199	. . . . . . . 8 ⊢ (((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)⟶1-1onto𝐴) → (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚) = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))
76	75	eqeq2d 2774	. . . . . . 7 ⊢ (((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)⟶1-1onto𝐴) → (𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚) ↔ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚)))
77	76	pm5.32da 590	. . . . . 6 ⊢ ((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑚 ∈ ℕ) → ((𝑓:(1...𝑚)⟶1-1onto𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) ↔ (𝑓:(1...𝑚)⟶1-1onto𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))))
78	77	exbidv 1956	. . . . 5 ⊢ ((∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) ∧ 𝑚 ∈ ℕ) → (∃𝑓(𝑓:(1...𝑚)⟶1-1onto𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) ↔ ∃𝑓(𝑓:(1...𝑚)⟶1-1onto𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))))
79	78	rexbidva 3188	. . . 4 ⊢ (∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)⟶1-1onto𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)) ↔ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)⟶1-1onto𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))))
80	40, 79	orbi12d 932	. . 3 ⊢ (∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) → ((∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)⟶1-1onto𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))) ↔ (∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)⟶1-1onto𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚)))))
81	80	iotabidv 6544	. 2 ⊢ (∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) → (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)⟶1-1onto𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)⟶1-1onto𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚)))))
82		df-prod 16105	. 2 ⊢ ∏𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)⟶1-1onto𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))
83		df-prod 16105	. 2 ⊢ ∏𝑘 ∈ 𝐴 𝐶 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ ∃𝑛 ∈ (ℤ≥‘𝑚)∃𝑦(𝑦 ≠ 0 ∧ seq𝑛( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑦) ∧ seq𝑚( · , (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐶, 1))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)⟶1-1onto𝐴 ∧ 𝑥 = (seq1( · , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐶))‘𝑚))))
84	81, 82, 83	3eqtr4g 2823	1 ⊢ (∀𝑘 ∈ 𝐴 ( I ‘𝐵) = ( I ‘𝐶) → ∏𝑘 ∈ 𝐴 𝐵 = ∏𝑘 ∈ 𝐴 𝐶)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570  ∃wex 1812   ∈ wcel 2147   ≠ wne 2959  ∀wral 3080  ∃wrex 3090  Vcvv 3454  ⦋csb 3851   ⊆ wss 3900  ifcif 4485   class class class wbr 5106   ↦ cmpt 5190   I cid 5550  ℩cio 6513  ⟶wf 6557  ⟶1-1ontowf1o 6560  ‘cfv 6561  (class class class)co 7446  0cc0 11230  1c1 11231   · cmul 11235  ℕcn 12365  ℤcz 12723  ℤ_≥cuz 12995  ...cfz 13669  seqcseq 14174   ⇝ cli 15683  ∏cprod 16104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pow 5332  ax-pr 5396  ax-un 7778  ax-cnex 11286  ax-resscn 11287  ax-1cn 11288  ax-icn 11289  ax-addcl 11290  ax-addrcl 11291  ax-mulcl 11292  ax-mulrcl 11293  ax-mulcom 11294  ax-addass 11295  ax-mulass 11296  ax-distr 11297  ax-i2m1 11298  ax-1ne0 11299  ax-1rid 11300  ax-rnegex 11301  ax-rrecex 11302  ax-cnre 11303  ax-pre-lttri 11304  ax-pre-lttrn 11305  ax-pre-ltadd 11306  ax-pre-mulgt0 11307

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5551  df-eprel 5556  df-po 5564  df-so 5565  df-fr 5609  df-we 5611  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-pred 6325  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6515  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7403  df-ov 7449  df-oprab 7450  df-mpo 7451  df-om 7905  df-1st 8028  df-2nd 8029  df-frecs 8330  df-wrecs 8361  df-recs 8410  df-rdg 8449  df-er 8748  df-en 9005  df-dom 9006  df-sdom 9007  df-pnf 11375  df-mnf 11376  df-xr 11377  df-ltxr 11378  df-le 11379  df-sub 11573  df-neg 11574  df-nn 12366  df-n0 12637  df-z 12724  df-uz 12996  df-fz 13670  df-seq 14175  df-prod 16105

This theorem is used by:  prodeq2  16113  prod2id  16127