Theorem prodeq2w

Description: Equality theorem for product, when the class expressions B and C are equal everywhere. Proved using only Extensionality. (Contributed by Scott Fenton, 4-Dec-2017)

	Ref	Expression
Assertion	prodeq2w	⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ∏ 𝑘 ∈ 𝐴 𝐵 = ∏ 𝑘 ∈ 𝐴 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ℤ = ℤ
2		ifeq1	⊢ ( 𝐵 = 𝐶 → if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) = if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) )
3	2	alimi	⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ∀ 𝑘 if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) = if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) )
4		alral	⊢ ( ∀ 𝑘 if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) = if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) → ∀ 𝑘 ∈ ℤ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) = if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) )
5	3 4	syl	⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ∀ 𝑘 ∈ ℤ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) = if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) )
6		mpteq12	⊢ ( ( ℤ = ℤ ∧ ∀ 𝑘 ∈ ℤ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) = if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) → ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) = ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) )
7	1 5 6	sylancr	⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) = ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) )
8	7	seqeq3d	⊢ ( ∀ 𝑘 𝐵 = 𝐶 → seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) = seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) )
9	8	breq1d	⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ( seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ↔ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) )
10	9	anbi2d	⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ( ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ↔ ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ) )
11	10	exbidv	⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ( ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ↔ ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ) )
12	11	rexbidv	⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ( ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ↔ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ) )
13	7	seqeq3d	⊢ ( ∀ 𝑘 𝐵 = 𝐶 → seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) = seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) )
14	13	breq1d	⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ( seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ↔ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑥 ) )
15	12 14	3anbi23d	⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ( ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ↔ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑥 ) ) )
16	15	rexbidv	⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ↔ ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑥 ) ) )
17		csbeq2	⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 = ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 )
18	17	mpteq2dv	⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) = ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) )
19	18	seqeq3d	⊢ ( ∀ 𝑘 𝐵 = 𝐶 → seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) = seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) )
20	19	fveq1d	⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) )
21	20	eqeq2d	⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ( 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ↔ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) )
22	21	anbi2d	⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ( ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ↔ ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) )
23	22	exbidv	⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ( ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) )
24	23	rexbidv	⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ( ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ↔ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) )
25	16 24	orbi12d	⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ( ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 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 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) ) )
26	25	iotabidv	⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 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 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) ) )
27		df-prod	⊢ ∏ 𝑘 ∈ 𝐴 𝐵 = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐵 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐵 ) ) ‘ 𝑚 ) ) ) )
28		df-prod	⊢ ∏ 𝑘 ∈ 𝐴 𝐶 = ( ℩ 𝑥 ( ∃ 𝑚 ∈ ℤ ( 𝐴 ⊆ ( ℤ≥ ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑛 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑦 ) ∧ seq 𝑚 ( · , ( 𝑘 ∈ ℤ ↦ if ( 𝑘 ∈ 𝐴 , 𝐶 , 1 ) ) ) ⇝ 𝑥 ) ∨ ∃ 𝑚 ∈ ℕ ∃ 𝑓 ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ 𝐴 ∧ 𝑥 = ( seq 1 ( · , ( 𝑛 ∈ ℕ ↦ ⦋ ( 𝑓 ‘ 𝑛 ) / 𝑘 ⦌ 𝐶 ) ) ‘ 𝑚 ) ) ) )
29	26 27 28	3eqtr4g	⊢ ( ∀ 𝑘 𝐵 = 𝐶 → ∏ 𝑘 ∈ 𝐴 𝐵 = ∏ 𝑘 ∈ 𝐴 𝐶 )