This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrdi ⊢ ( 𝐵 = ∅ → ( 𝐴 ⊆ 𝐵 → 𝐴 = ∅ ) )
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 ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐶 = ∏ 𝑘 ∈ 𝐵 𝐶 )