Theorem prodeq2ii

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

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

Proof

Step	Hyp	Ref	Expression
1		eluzelz	⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) → 𝑛 ∈ ℤ )
2	1	adantl	⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ) → 𝑛 ∈ ℤ )
3		nfra1	⊢ Ⅎ 𝑘 ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 )
4		rsp	⊢ ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → ( 𝑘 ∈ 𝐴 → ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ) )
5	4	adantr	⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑘 ∈ ℤ ) → ( 𝑘 ∈ 𝐴 → ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ) )
6		ifeq1	⊢ ( ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → if ( 𝑘 ∈ 𝐴 , ( I ‘ 𝐵 ) , ( I ‘ 1 ) ) = if ( 𝑘 ∈ 𝐴 , ( I ‘ 𝐶 ) , ( I ‘ 1 ) ) )
7	5 6	syl6	⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑘 ∈ ℤ ) → ( 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , ( I ‘ 𝐵 ) , ( I ‘ 1 ) ) = if ( 𝑘 ∈ 𝐴 , ( I ‘ 𝐶 ) , ( I ‘ 1 ) ) ) )
8		iffalse	⊢ ( ¬ 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , ( I ‘ 𝐵 ) , ( I ‘ 1 ) ) = ( I ‘ 1 ) )
9		iffalse	⊢ ( ¬ 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , ( I ‘ 𝐶 ) , ( I ‘ 1 ) ) = ( I ‘ 1 ) )
10	8 9	eqtr4d	⊢ ( ¬ 𝑘 ∈ 𝐴 → if ( 𝑘 ∈ 𝐴 , ( I ‘ 𝐵 ) , ( I ‘ 1 ) ) = if ( 𝑘 ∈ 𝐴 , ( I ‘ 𝐶 ) , ( I ‘ 1 ) ) )
11	7 10	pm2.61d1	⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑘 ∈ ℤ ) → if ( 𝑘 ∈ 𝐴 , ( I ‘ 𝐵 ) , ( I ‘ 1 ) ) = if ( 𝑘 ∈ 𝐴 , ( I ‘ 𝐶 ) , ( I ‘ 1 ) ) )
12		fvif	⊢ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) = if ( 𝑘 ∈ 𝐴 , ( I ‘ 𝐵 ) , ( I ‘ 1 ) )
13		fvif	⊢ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) = if ( 𝑘 ∈ 𝐴 , ( I ‘ 𝐶 ) , ( I ‘ 1 ) )
14	11 12 13	3eqtr4g	⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑘 ∈ ℤ ) → ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) = ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) )
15	3 14	mpteq2da	⊢ ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) = ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) )
16	15	adantr	⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) = ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) )
17	16	fveq1d	⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ‘ 𝑥 ) = ( ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ‘ 𝑥 ) )
18	17	adantlr	⊢ ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ‘ 𝑥 ) = ( ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ‘ 𝑥 ) )
19		eqid	⊢ ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) = ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) )
20		eqid	⊢ ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) = ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) )
21	19 20	fvmptex	⊢ ( ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ‘ 𝑥 ) = ( ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ‘ 𝑥 )
22		eqid	⊢ ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) = ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) )
23		eqid	⊢ ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) = ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) )
24	22 23	fvmptex	⊢ ( ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ‘ 𝑥 ) = ( ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ‘ 𝑥 )
25	18 21 24	3eqtr4g	⊢ ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑛 ) ) → ( ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ‘ 𝑥 ) = ( ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ‘ 𝑥 ) )
26	2 25	seqfeq	⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ) → seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) = seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) )
27	26	breq1d	⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ↔ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) )
28	27	anbi2d	⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ↔ ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ) )
29	28	exbidv	⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ↔ ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ) )
30	29	rexbidva	⊢ ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → ( ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ↔ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ) )
31	30	adantr	⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) → ( ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ↔ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ) )
32		simpr	⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) → 𝑚 ∈ ℤ )
33	15	adantr	⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) = ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) )
34	33	fveq1d	⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ‘ 𝑥 ) = ( ( 𝑘 ∈ ℤ ↦ ( I ‘ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ‘ 𝑥 ) )
35	34 21 24	3eqtr4g	⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ‘ 𝑥 ) = ( ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ‘ 𝑥 ) )
36	35	adantlr	⊢ ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) ∧ 𝑥 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ‘ 𝑥 ) = ( ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ‘ 𝑥 ) )
37	32 36	seqfeq	⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) → seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) = seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) )
38	37	breq1d	⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) → ( seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ↔ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑥 ) )
39	31 38	3anbi23d	⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℤ ) → ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ↔ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑥 ) ) )
40	39	rexbidva	⊢ ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ↔ ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑥 ) ) )
41		simplr	⊢ ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) → 𝑚 ∈ ℕ )
42		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
43	41 42	eleqtrdi	⊢ ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) → 𝑚 ∈ ( ℤ≥ ‘ 1 ) )
44		f1of	⊢ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 → 𝑓 : ( 1 ... 𝑚 ) ⟶ 𝐴 )
45	44	ad2antlr	⊢ ( ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → 𝑓 : ( 1 ... 𝑚 ) ⟶ 𝐴 )
46		ffvelcdm	⊢ ( ( 𝑓 : ( 1 ... 𝑚 ) ⟶ 𝐴 ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝐴 )
47	45 46	sylancom	⊢ ( ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝐴 )
48		simplll	⊢ ( ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) )
49		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐵 )
50		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐶 )
51	49 50	nfeq	⊢ Ⅎ 𝑘 ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐵 ) = ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐶 )
52		csbeq1a	⊢ ( 𝑘 = ( 𝑓 ‘ 𝑥 ) → ( I ‘ 𝐵 ) = ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐵 ) )
53		csbeq1a	⊢ ( 𝑘 = ( 𝑓 ‘ 𝑥 ) → ( I ‘ 𝐶 ) = ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐶 ) )
54	52 53	eqeq12d	⊢ ( 𝑘 = ( 𝑓 ‘ 𝑥 ) → ( ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ↔ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐵 ) = ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐶 ) ) )
55	51 54	rspc	⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ 𝐴 → ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐵 ) = ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐶 ) ) )
56	47 48 55	sylc	⊢ ( ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐵 ) = ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐶 ) )
57		fvex	⊢ ( 𝑓 ‘ 𝑥 ) ∈ V
58		csbfv2g	⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ V → ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐵 ) = ( I ‘ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 ) )
59	57 58	ax-mp	⊢ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐵 ) = ( I ‘ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 )
60		csbfv2g	⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ V → ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐶 ) = ( I ‘ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐶 ) )
61	57 60	ax-mp	⊢ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ ( I ‘ 𝐶 ) = ( I ‘ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐶 )
62	56 59 61	3eqtr3g	⊢ ( ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → ( I ‘ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 ) = ( I ‘ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐶 ) )
63		elfznn	⊢ ( 𝑥 ∈ ( 1 ... 𝑚 ) → 𝑥 ∈ ℕ )
64	63	adantl	⊢ ( ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → 𝑥 ∈ ℕ )
65		fveq2	⊢ ( 𝑛 = 𝑥 → ( 𝑓 ‘ 𝑛 ) = ( 𝑓 ‘ 𝑥 ) )
66	65	csbeq1d	⊢ ( 𝑛 = 𝑥 → ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 = ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 )
67		eqid	⊢ ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) = ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 )
68	66 67	fvmpti	⊢ ( 𝑥 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ‘ 𝑥 ) = ( I ‘ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 ) )
69	64 68	syl	⊢ ( ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → ( ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ‘ 𝑥 ) = ( I ‘ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐵 ) )
70	65	csbeq1d	⊢ ( 𝑛 = 𝑥 → ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 = ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐶 )
71		eqid	⊢ ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) = ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 )
72	70 71	fvmpti	⊢ ( 𝑥 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ‘ 𝑥 ) = ( I ‘ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐶 ) )
73	64 72	syl	⊢ ( ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → ( ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ‘ 𝑥 ) = ( I ‘ ⦋ ( 𝑓 ‘ 𝑥 ) / 𝑘 ⦌ 𝐶 ) )
74	62 69 73	3eqtr4d	⊢ ( ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝑚 ) ) → ( ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ‘ 𝑥 ) = ( ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ‘ 𝑥 ) )
75	43 74	seqfveq	⊢ ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) )
76	75	eqeq2d	⊢ ( ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ) → ( 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ↔ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) )
77	76	pm5.32da	⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ↔ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) )
78	77	exbidv	⊢ ( ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ∧ 𝑚 ∈ ℕ ) → ( ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) )
79	78	rexbidva	⊢ ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ↔ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) )
80	40 79	orbi12d	⊢ ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) ↔ ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) ) )
81	80	iotabidv	⊢ ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) ) = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) ) )
82		df-prod	⊢ ∏ 𝑘 ∈ 𝐴 𝐵 = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) )
83		df-prod	⊢ ∏ 𝑘 ∈ 𝐴 𝐶 = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) )
84	81 82 83	3eqtr4g	⊢ ( ∀ 𝑘 ∈ 𝐴 ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) → ∏ 𝑘 ∈ 𝐴 𝐵 = ∏ 𝑘 ∈ 𝐴 𝐶 )