Theorem fprodss

Description: Change the index set to a subset in a finite product. (Contributed by Scott Fenton, 16-Dec-2017)

	Ref	Expression
Hypotheses	fprodss.1	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
	fprodss.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
	fprodss.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐶 = 1 )
	fprodss.4	⊢ ( 𝜑 → 𝐵 ∈ Fin )
Assertion	fprodss	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐶 = ∏ 𝑘 ∈ 𝐵 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		fprodss.1	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
2		fprodss.2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
3		fprodss.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐶 = 1 )
4		fprodss.4	⊢ ( 𝜑 → 𝐵 ∈ Fin )
5		sseq2	⊢ ( 𝐵 = ∅ → ( 𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ ∅ ) )
6		ss0	⊢ ( 𝐴 ⊆ ∅ → 𝐴 = ∅ )
7	5 6	syl6bi	⊢ ( 𝐵 = ∅ → ( 𝐴 ⊆ 𝐵 → 𝐴 = ∅ ) )
8		prodeq1	⊢ ( 𝐴 = ∅ → ∏ 𝑘 ∈ 𝐴 𝐶 = ∏ 𝑘 ∈ ∅ 𝐶 )
9		prodeq1	⊢ ( 𝐵 = ∅ → ∏ 𝑘 ∈ 𝐵 𝐶 = ∏ 𝑘 ∈ ∅ 𝐶 )
10	9	eqcomd	⊢ ( 𝐵 = ∅ → ∏ 𝑘 ∈ ∅ 𝐶 = ∏ 𝑘 ∈ 𝐵 𝐶 )
11	8 10	sylan9eq	⊢ ( ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) → ∏ 𝑘 ∈ 𝐴 𝐶 = ∏ 𝑘 ∈ 𝐵 𝐶 )
12	11	expcom	⊢ ( 𝐵 = ∅ → ( 𝐴 = ∅ → ∏ 𝑘 ∈ 𝐴 𝐶 = ∏ 𝑘 ∈ 𝐵 𝐶 ) )
13	7 12	syld	⊢ ( 𝐵 = ∅ → ( 𝐴 ⊆ 𝐵 → ∏ 𝑘 ∈ 𝐴 𝐶 = ∏ 𝑘 ∈ 𝐵 𝐶 ) )
14	1 13	syl5com	⊢ ( 𝜑 → ( 𝐵 = ∅ → ∏ 𝑘 ∈ 𝐴 𝐶 = ∏ 𝑘 ∈ 𝐵 𝐶 ) )
15		cnvimass	⊢ ( ◡ 𝑓 “ 𝐴 ) ⊆ dom 𝑓
16		simprr	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 )
17		f1of	⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 → 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) ⟶ 𝐵 )
18	16 17	syl	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) ⟶ 𝐵 )
19	15 18	fssdm	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) → ( ◡ 𝑓 “ 𝐴 ) ⊆ ( 1 ... ( ♯ ‘ 𝐵 ) ) )
20		f1ofn	⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 → 𝑓 Fn ( 1 ... ( ♯ ‘ 𝐵 ) ) )
21		elpreima	⊢ ( 𝑓 Fn ( 1 ... ( ♯ ‘ 𝐵 ) ) → ( 𝑛 ∈ ( ◡ 𝑓 “ 𝐴 ) ↔ ( 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ ( 𝑓 ‘ 𝑛 ) ∈ 𝐴 ) ) )
22	16 20 21	3syl	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) → ( 𝑛 ∈ ( ◡ 𝑓 “ 𝐴 ) ↔ ( 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ ( 𝑓 ‘ 𝑛 ) ∈ 𝐴 ) ) )
23	18	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ) → ( 𝑓 ‘ 𝑛 ) ∈ 𝐵 )
24	23	ex	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) → ( 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) → ( 𝑓 ‘ 𝑛 ) ∈ 𝐵 ) )
25	24	adantrd	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) → ( ( 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ ( 𝑓 ‘ 𝑛 ) ∈ 𝐴 ) → ( 𝑓 ‘ 𝑛 ) ∈ 𝐵 ) )
26	22 25	sylbid	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) → ( 𝑛 ∈ ( ◡ 𝑓 “ 𝐴 ) → ( 𝑓 ‘ 𝑛 ) ∈ 𝐵 ) )
27	26	imp	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) ∧ 𝑛 ∈ ( ◡ 𝑓 “ 𝐴 ) ) → ( 𝑓 ‘ 𝑛 ) ∈ 𝐵 )
28	2	ex	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 → 𝐶 ∈ ℂ ) )
29	28	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑘 ∈ 𝐴 → 𝐶 ∈ ℂ ) )
30		eldif	⊢ ( 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ↔ ( 𝑘 ∈ 𝐵 ∧ ¬ 𝑘 ∈ 𝐴 ) )
31		ax-1cn	⊢ 1 ∈ ℂ
32	3 31	eqeltrdi	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐶 ∈ ℂ )
33	30 32	sylan2br	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐵 ∧ ¬ 𝑘 ∈ 𝐴 ) ) → 𝐶 ∈ ℂ )
34	33	expr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( ¬ 𝑘 ∈ 𝐴 → 𝐶 ∈ ℂ ) )
35	29 34	pm2.61d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ℂ )
36	35	adantlr	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ℂ )
37	36	fmpttd	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) → ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) : 𝐵 ⟶ ℂ )
38	37	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) ∧ ( 𝑓 ‘ 𝑛 ) ∈ 𝐵 ) → ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℂ )
39	27 38	syldan	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) ∧ 𝑛 ∈ ( ◡ 𝑓 “ 𝐴 ) ) → ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ ℂ )
40		eqid	⊢ ( ℤ≥ ‘ 1 ) = ( ℤ≥ ‘ 1 )
41		simprl	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) → ( ♯ ‘ 𝐵 ) ∈ ℕ )
42		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
43	41 42	eleqtrdi	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) → ( ♯ ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 1 ) )
44		ssidd	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) → ( 1 ... ( ♯ ‘ 𝐵 ) ) ⊆ ( 1 ... ( ♯ ‘ 𝐵 ) ) )
45	40 43 44	fprodntriv	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) → ∃ 𝑚 ∈ ( ℤ≥ ‘ 1 ) ∃ 𝑦 ( 𝑦 ≠ 0 ∧ seq 𝑚 ( · , ( 𝑛 ∈ ( ℤ≥ ‘ 1 ) ↦ if ( 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) , ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) , 1 ) ) ) ⇝ 𝑦 ) )
46		eldifi	⊢ ( 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( ◡ 𝑓 “ 𝐴 ) ) → 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) )
47	46 23	sylan2	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( ◡ 𝑓 “ 𝐴 ) ) ) → ( 𝑓 ‘ 𝑛 ) ∈ 𝐵 )
48		eldifn	⊢ ( 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( ◡ 𝑓 “ 𝐴 ) ) → ¬ 𝑛 ∈ ( ◡ 𝑓 “ 𝐴 ) )
49	48	adantl	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( ◡ 𝑓 “ 𝐴 ) ) ) → ¬ 𝑛 ∈ ( ◡ 𝑓 “ 𝐴 ) )
50	46	adantl	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( ◡ 𝑓 “ 𝐴 ) ) ) → 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) )
51	22	adantr	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( ◡ 𝑓 “ 𝐴 ) ) ) → ( 𝑛 ∈ ( ◡ 𝑓 “ 𝐴 ) ↔ ( 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ∧ ( 𝑓 ‘ 𝑛 ) ∈ 𝐴 ) ) )
52	50 51	mpbirand	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( ◡ 𝑓 “ 𝐴 ) ) ) → ( 𝑛 ∈ ( ◡ 𝑓 “ 𝐴 ) ↔ ( 𝑓 ‘ 𝑛 ) ∈ 𝐴 ) )
53	49 52	mtbid	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( ◡ 𝑓 “ 𝐴 ) ) ) → ¬ ( 𝑓 ‘ 𝑛 ) ∈ 𝐴 )
54	47 53	eldifd	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( ◡ 𝑓 “ 𝐴 ) ) ) → ( 𝑓 ‘ 𝑛 ) ∈ ( 𝐵 ∖ 𝐴 ) )
55		difss	⊢ ( 𝐵 ∖ 𝐴 ) ⊆ 𝐵
56		resmpt	⊢ ( ( 𝐵 ∖ 𝐴 ) ⊆ 𝐵 → ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ↾ ( 𝐵 ∖ 𝐴 ) ) = ( 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 𝐶 ) )
57	55 56	ax-mp	⊢ ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ↾ ( 𝐵 ∖ 𝐴 ) ) = ( 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 𝐶 )
58	57	fveq1i	⊢ ( ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ↾ ( 𝐵 ∖ 𝐴 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) = ( ( 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) )
59		fvres	⊢ ( ( 𝑓 ‘ 𝑛 ) ∈ ( 𝐵 ∖ 𝐴 ) → ( ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ↾ ( 𝐵 ∖ 𝐴 ) ) ‘ ( 𝑓 ‘ 𝑛 ) ) = ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
60	58 59	eqtr3id	⊢ ( ( 𝑓 ‘ 𝑛 ) ∈ ( 𝐵 ∖ 𝐴 ) → ( ( 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) = ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
61	54 60	syl	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( ◡ 𝑓 “ 𝐴 ) ) ) → ( ( 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) = ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
62		1ex	⊢ 1 ∈ V
63	62	elsn2	⊢ ( 𝐶 ∈ { 1 } ↔ 𝐶 = 1 )
64	3 63	sylibr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐶 ∈ { 1 } )
65	64	fmpttd	⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 𝐶 ) : ( 𝐵 ∖ 𝐴 ) ⟶ { 1 } )
66	65	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( ◡ 𝑓 “ 𝐴 ) ) ) → ( 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 𝐶 ) : ( 𝐵 ∖ 𝐴 ) ⟶ { 1 } )
67	66 54	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( ◡ 𝑓 “ 𝐴 ) ) ) → ( ( 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ { 1 } )
68		elsni	⊢ ( ( ( 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) ∈ { 1 } → ( ( 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) = 1 )
69	67 68	syl	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( ◡ 𝑓 “ 𝐴 ) ) ) → ( ( 𝑘 ∈ ( 𝐵 ∖ 𝐴 ) ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) = 1 )
70	61 69	eqtr3d	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) ∧ 𝑛 ∈ ( ( 1 ... ( ♯ ‘ 𝐵 ) ) ∖ ( ◡ 𝑓 “ 𝐴 ) ) ) → ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) = 1 )
71		fzssuz	⊢ ( 1 ... ( ♯ ‘ 𝐵 ) ) ⊆ ( ℤ≥ ‘ 1 )
72	71	a1i	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) → ( 1 ... ( ♯ ‘ 𝐵 ) ) ⊆ ( ℤ≥ ‘ 1 ) )
73	19 39 45 70 72	prodss	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) → ∏ 𝑛 ∈ ( ◡ 𝑓 “ 𝐴 ) ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) = ∏ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
74	1	adantr	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) → 𝐴 ⊆ 𝐵 )
75	74	resmptd	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) → ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ↾ 𝐴 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) )
76	75	fveq1d	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) → ( ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ↾ 𝐴 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑚 ) )
77		fvres	⊢ ( 𝑚 ∈ 𝐴 → ( ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ↾ 𝐴 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑚 ) )
78	76 77	sylan9req	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) ∧ 𝑚 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑚 ) )
79	78	prodeq2dv	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) → ∏ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑚 ) = ∏ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑚 ) )
80		fveq2	⊢ ( 𝑚 = ( 𝑓 ‘ 𝑛 ) → ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑚 ) = ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
81		fzfid	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) → ( 1 ... ( ♯ ‘ 𝐵 ) ) ∈ Fin )
82	81 18	fisuppfi	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) → ( ◡ 𝑓 “ 𝐴 ) ∈ Fin )
83		f1of1	⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 → 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1→ 𝐵 )
84	16 83	syl	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1→ 𝐵 )
85		f1ores	⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1→ 𝐵 ∧ ( ◡ 𝑓 “ 𝐴 ) ⊆ ( 1 ... ( ♯ ‘ 𝐵 ) ) ) → ( 𝑓 ↾ ( ◡ 𝑓 “ 𝐴 ) ) : ( ◡ 𝑓 “ 𝐴 ) –1-1-onto→ ( 𝑓 “ ( ◡ 𝑓 “ 𝐴 ) ) )
86	84 19 85	syl2anc	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) → ( 𝑓 ↾ ( ◡ 𝑓 “ 𝐴 ) ) : ( ◡ 𝑓 “ 𝐴 ) –1-1-onto→ ( 𝑓 “ ( ◡ 𝑓 “ 𝐴 ) ) )
87		f1ofo	⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 → 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –onto→ 𝐵 )
88	16 87	syl	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –onto→ 𝐵 )
89		foimacnv	⊢ ( ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –onto→ 𝐵 ∧ 𝐴 ⊆ 𝐵 ) → ( 𝑓 “ ( ◡ 𝑓 “ 𝐴 ) ) = 𝐴 )
90	88 74 89	syl2anc	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) → ( 𝑓 “ ( ◡ 𝑓 “ 𝐴 ) ) = 𝐴 )
91	90	f1oeq3d	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) → ( ( 𝑓 ↾ ( ◡ 𝑓 “ 𝐴 ) ) : ( ◡ 𝑓 “ 𝐴 ) –1-1-onto→ ( 𝑓 “ ( ◡ 𝑓 “ 𝐴 ) ) ↔ ( 𝑓 ↾ ( ◡ 𝑓 “ 𝐴 ) ) : ( ◡ 𝑓 “ 𝐴 ) –1-1-onto→ 𝐴 ) )
92	86 91	mpbid	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) → ( 𝑓 ↾ ( ◡ 𝑓 “ 𝐴 ) ) : ( ◡ 𝑓 “ 𝐴 ) –1-1-onto→ 𝐴 )
93		fvres	⊢ ( 𝑛 ∈ ( ◡ 𝑓 “ 𝐴 ) → ( ( 𝑓 ↾ ( ◡ 𝑓 “ 𝐴 ) ) ‘ 𝑛 ) = ( 𝑓 ‘ 𝑛 ) )
94	93	adantl	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) ∧ 𝑛 ∈ ( ◡ 𝑓 “ 𝐴 ) ) → ( ( 𝑓 ↾ ( ◡ 𝑓 “ 𝐴 ) ) ‘ 𝑛 ) = ( 𝑓 ‘ 𝑛 ) )
95	74	sselda	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) ∧ 𝑚 ∈ 𝐴 ) → 𝑚 ∈ 𝐵 )
96	37	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) ∧ 𝑚 ∈ 𝐵 ) → ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑚 ) ∈ ℂ )
97	95 96	syldan	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) ∧ 𝑚 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑚 ) ∈ ℂ )
98	80 82 92 94 97	fprodf1o	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) → ∏ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑚 ) = ∏ 𝑛 ∈ ( ◡ 𝑓 “ 𝐴 ) ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
99	79 98	eqtrd	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) → ∏ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑚 ) = ∏ 𝑛 ∈ ( ◡ 𝑓 “ 𝐴 ) ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
100		eqidd	⊢ ( ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ) → ( 𝑓 ‘ 𝑛 ) = ( 𝑓 ‘ 𝑛 ) )
101	80 81 16 100 96	fprodf1o	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) → ∏ 𝑚 ∈ 𝐵 ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑚 ) = ∏ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ ( 𝑓 ‘ 𝑛 ) ) )
102	73 99 101	3eqtr4d	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) → ∏ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑚 ) = ∏ 𝑚 ∈ 𝐵 ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑚 ) )
103		prodfc	⊢ ∏ 𝑚 ∈ 𝐴 ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑚 ) = ∏ 𝑘 ∈ 𝐴 𝐶
104		prodfc	⊢ ∏ 𝑚 ∈ 𝐵 ( ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ‘ 𝑚 ) = ∏ 𝑘 ∈ 𝐵 𝐶
105	102 103 104	3eqtr3g	⊢ ( ( 𝜑 ∧ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) → ∏ 𝑘 ∈ 𝐴 𝐶 = ∏ 𝑘 ∈ 𝐵 𝐶 )
106	105	expr	⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ ) → ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 → ∏ 𝑘 ∈ 𝐴 𝐶 = ∏ 𝑘 ∈ 𝐵 𝐶 ) )
107	106	exlimdv	⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ ) → ( ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 → ∏ 𝑘 ∈ 𝐴 𝐶 = ∏ 𝑘 ∈ 𝐵 𝐶 ) )
108	107	expimpd	⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) → ∏ 𝑘 ∈ 𝐴 𝐶 = ∏ 𝑘 ∈ 𝐵 𝐶 ) )
109		fz1f1o	⊢ ( 𝐵 ∈ Fin → ( 𝐵 = ∅ ∨ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) )
110	4 109	syl	⊢ ( 𝜑 → ( 𝐵 = ∅ ∨ ( ( ♯ ‘ 𝐵 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐵 ) ) –1-1-onto→ 𝐵 ) ) )
111	14 108 110	mpjaod	⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐶 = ∏ 𝑘 ∈ 𝐵 𝐶 )