Metamath Proof Explorer

Theorem fprodcom2

Description: Interchange order of multiplication. Note that B ( j ) and D ( k ) are not necessarily constant expressions. (Contributed by Scott Fenton, 1-Feb-2018) (Proof shortened by JJ, 2-Aug-2021)

Ref Expression
Hypotheses fprodcom2.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
fprodcom2.2 ⊢ ( 𝜑 → 𝐶 ∈ Fin )
fprodcom2.3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ∈ Fin )
fprodcom2.4 ⊢ ( 𝜑 → ( ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ↔ ( 𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷 ) ) )
fprodcom2.5 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐸 ∈ ℂ )
Assertion fprodcom2 ( 𝜑 → ∏ 𝑗 ∈ 𝐴 ∏ 𝑘 ∈ 𝐵 𝐸 = ∏ 𝑘 ∈ 𝐶 ∏ 𝑗 ∈ 𝐷 𝐸 )

Proof

Step Hyp Ref Expression
1 fprodcom2.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
2 fprodcom2.2 ⊢ ( 𝜑 → 𝐶 ∈ Fin )
3 fprodcom2.3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ∈ Fin )
4 fprodcom2.4 ⊢ ( 𝜑 → ( ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ↔ ( 𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷 ) ) )
5 fprodcom2.5 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐸 ∈ ℂ )
6 relxp ⊢ Rel ( { 𝑗 } × 𝐵 )
7 6 rgenw ⊢ ∀ 𝑗 ∈ 𝐴 Rel ( { 𝑗 } × 𝐵 )
8 reliun ⊢ ( Rel ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ↔ ∀ 𝑗 ∈ 𝐴 Rel ( { 𝑗 } × 𝐵 ) )
9 7 8 mpbir ⊢ Rel ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 )
10 relcnv ⊢ Rel ◡ ∪ 𝑘 ∈ 𝐶 ( { 𝑘 } × 𝐷 )
11 ancom ⊢ ( ( 𝑥 = 𝑗 ∧ 𝑦 = 𝑘 ) ↔ ( 𝑦 = 𝑘 ∧ 𝑥 = 𝑗 ) )
12 vex ⊢ 𝑥 ∈ V
13 vex ⊢ 𝑦 ∈ V
14 12 13 opth ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑗 , 𝑘 ⟩ ↔ ( 𝑥 = 𝑗 ∧ 𝑦 = 𝑘 ) )
15 13 12 opth ⊢ ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑘 , 𝑗 ⟩ ↔ ( 𝑦 = 𝑘 ∧ 𝑥 = 𝑗 ) )
16 11 14 15 3bitr4i ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑗 , 𝑘 ⟩ ↔ ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑘 , 𝑗 ⟩ )
17 16 a1i ⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑗 , 𝑘 ⟩ ↔ ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑘 , 𝑗 ⟩ ) )
18 17 4 anbi12d ⊢ ( 𝜑 → ( ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑗 , 𝑘 ⟩ ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) ↔ ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑘 , 𝑗 ⟩ ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷 ) ) ) )
19 18 2exbidv ⊢ ( 𝜑 → ( ∃ 𝑗 ∃ 𝑘 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑗 , 𝑘 ⟩ ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) ↔ ∃ 𝑗 ∃ 𝑘 ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑘 , 𝑗 ⟩ ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷 ) ) ) )
20 eliunxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ↔ ∃ 𝑗 ∃ 𝑘 ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑗 , 𝑘 ⟩ ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) )
21 12 13 opelcnv ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ ∪ 𝑘 ∈ 𝐶 ( { 𝑘 } × 𝐷 ) ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ ∪ 𝑘 ∈ 𝐶 ( { 𝑘 } × 𝐷 ) )
22 eliunxp ⊢ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ ∪ 𝑘 ∈ 𝐶 ( { 𝑘 } × 𝐷 ) ↔ ∃ 𝑘 ∃ 𝑗 ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑘 , 𝑗 ⟩ ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷 ) ) )
23 excom ⊢ ( ∃ 𝑘 ∃ 𝑗 ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑘 , 𝑗 ⟩ ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷 ) ) ↔ ∃ 𝑗 ∃ 𝑘 ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑘 , 𝑗 ⟩ ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷 ) ) )
24 21 22 23 3bitri ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ ∪ 𝑘 ∈ 𝐶 ( { 𝑘 } × 𝐷 ) ↔ ∃ 𝑗 ∃ 𝑘 ( ⟨ 𝑦 , 𝑥 ⟩ = ⟨ 𝑘 , 𝑗 ⟩ ∧ ( 𝑘 ∈ 𝐶 ∧ 𝑗 ∈ 𝐷 ) ) )
25 19 20 24 3bitr4g ⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ ∪ 𝑘 ∈ 𝐶 ( { 𝑘 } × 𝐷 ) ) )
26 9 10 25 eqrelrdv ⊢ ( 𝜑 → ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) = ◡ ∪ 𝑘 ∈ 𝐶 ( { 𝑘 } × 𝐷 ) )
27 nfcv ⊢ Ⅎ 𝑥 ( { 𝑗 } × 𝐵 )
28 nfcv ⊢ Ⅎ 𝑗 { 𝑥 }
29 nfcsb1v ⊢ Ⅎ 𝑗 ⦋ 𝑥 / 𝑗 ⦌ 𝐵
30 28 29 nfxp ⊢ Ⅎ 𝑗 ( { 𝑥 } × ⦋ 𝑥 / 𝑗 ⦌ 𝐵 )
31 sneq ⊢ ( 𝑗 = 𝑥 → { 𝑗 } = { 𝑥 } )
32 csbeq1a ⊢ ( 𝑗 = 𝑥 → 𝐵 = ⦋ 𝑥 / 𝑗 ⦌ 𝐵 )
33 31 32 xpeq12d ⊢ ( 𝑗 = 𝑥 → ( { 𝑗 } × 𝐵 ) = ( { 𝑥 } × ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ) )
34 27 30 33 cbviun ⊢ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) = ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ⦋ 𝑥 / 𝑗 ⦌ 𝐵 )
35 nfcv ⊢ Ⅎ 𝑦 ( { 𝑘 } × 𝐷 )
36 nfcv ⊢ Ⅎ 𝑘 { 𝑦 }
37 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑦 / 𝑘 ⦌ 𝐷
38 36 37 nfxp ⊢ Ⅎ 𝑘 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 )
39 sneq ⊢ ( 𝑘 = 𝑦 → { 𝑘 } = { 𝑦 } )
40 csbeq1a ⊢ ( 𝑘 = 𝑦 → 𝐷 = ⦋ 𝑦 / 𝑘 ⦌ 𝐷 )
41 39 40 xpeq12d ⊢ ( 𝑘 = 𝑦 → ( { 𝑘 } × 𝐷 ) = ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) )
42 35 38 41 cbviun ⊢ ∪ 𝑘 ∈ 𝐶 ( { 𝑘 } × 𝐷 ) = ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 )
43 42 cnveqi ⊢ ◡ ∪ 𝑘 ∈ 𝐶 ( { 𝑘 } × 𝐷 ) = ◡ ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 )
44 26 34 43 3eqtr3g ⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ) = ◡ ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) )
45 44 prodeq1d ⊢ ( 𝜑 → ∏ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ ( 1st ‘ 𝑧 ) / 𝑗 ⦌ 𝐸 = ∏ 𝑧 ∈ ◡ ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ ( 1st ‘ 𝑧 ) / 𝑗 ⦌ 𝐸 )
46 13 12 op1std ⊢ ( 𝑤 = ⟨ 𝑦 , 𝑥 ⟩ → ( 1st ‘ 𝑤 ) = 𝑦 )
47 46 csbeq1d ⊢ ( 𝑤 = ⟨ 𝑦 , 𝑥 ⟩ → ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 = ⦋ 𝑦 / 𝑘 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 )
48 13 12 op2ndd ⊢ ( 𝑤 = ⟨ 𝑦 , 𝑥 ⟩ → ( 2nd ‘ 𝑤 ) = 𝑥 )
49 48 csbeq1d ⊢ ( 𝑤 = ⟨ 𝑦 , 𝑥 ⟩ → ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 = ⦋ 𝑥 / 𝑗 ⦌ 𝐸 )
50 49 csbeq2dv ⊢ ( 𝑤 = ⟨ 𝑦 , 𝑥 ⟩ → ⦋ 𝑦 / 𝑘 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 = ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 )
51 47 50 eqtrd ⊢ ( 𝑤 = ⟨ 𝑦 , 𝑥 ⟩ → ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 = ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 )
52 12 13 op2ndd ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2nd ‘ 𝑧 ) = 𝑦 )
53 52 csbeq1d ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ ( 1st ‘ 𝑧 ) / 𝑗 ⦌ 𝐸 = ⦋ 𝑦 / 𝑘 ⦌ ⦋ ( 1st ‘ 𝑧 ) / 𝑗 ⦌ 𝐸 )
54 12 13 op1std ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 1st ‘ 𝑧 ) = 𝑥 )
55 54 csbeq1d ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ⦋ ( 1st ‘ 𝑧 ) / 𝑗 ⦌ 𝐸 = ⦋ 𝑥 / 𝑗 ⦌ 𝐸 )
56 55 csbeq2dv ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ⦋ 𝑦 / 𝑘 ⦌ ⦋ ( 1st ‘ 𝑧 ) / 𝑗 ⦌ 𝐸 = ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 )
57 53 56 eqtrd ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ ( 1st ‘ 𝑧 ) / 𝑗 ⦌ 𝐸 = ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 )
58 snfi ⊢ { 𝑦 } ∈ Fin
59 1 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → 𝐴 ∈ Fin )
60 37 40 opeliunxp2f ⊢ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ ∪ 𝑘 ∈ 𝐶 ( { 𝑘 } × 𝐷 ) ↔ ( 𝑦 ∈ 𝐶 ∧ 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) )
61 21 60 sylbbr ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ ∪ 𝑘 ∈ 𝐶 ( { 𝑘 } × 𝐷 ) )
62 61 adantl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ ∪ 𝑘 ∈ 𝐶 ( { 𝑘 } × 𝐷 ) )
63 26 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) = ◡ ∪ 𝑘 ∈ 𝐶 ( { 𝑘 } × 𝐷 ) )
64 62 63 eleqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
65 eliun ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ↔ ∃ 𝑗 ∈ 𝐴 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝑗 } × 𝐵 ) )
66 64 65 sylib ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → ∃ 𝑗 ∈ 𝐴 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝑗 } × 𝐵 ) )
67 simpr ⊢ ( ( 𝑗 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝑗 } × 𝐵 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝑗 } × 𝐵 ) )
68 opelxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝑗 } × 𝐵 ) ↔ ( 𝑥 ∈ { 𝑗 } ∧ 𝑦 ∈ 𝐵 ) )
69 67 68 sylib ⊢ ( ( 𝑗 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝑗 } × 𝐵 ) ) → ( 𝑥 ∈ { 𝑗 } ∧ 𝑦 ∈ 𝐵 ) )
70 69 simpld ⊢ ( ( 𝑗 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝑗 } × 𝐵 ) ) → 𝑥 ∈ { 𝑗 } )
71 elsni ⊢ ( 𝑥 ∈ { 𝑗 } → 𝑥 = 𝑗 )
72 70 71 syl ⊢ ( ( 𝑗 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝑗 } × 𝐵 ) ) → 𝑥 = 𝑗 )
73 simpl ⊢ ( ( 𝑗 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝑗 } × 𝐵 ) ) → 𝑗 ∈ 𝐴 )
74 72 73 eqeltrd ⊢ ( ( 𝑗 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝑗 } × 𝐵 ) ) → 𝑥 ∈ 𝐴 )
75 74 rexlimiva ⊢ ( ∃ 𝑗 ∈ 𝐴 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝑗 } × 𝐵 ) → 𝑥 ∈ 𝐴 )
76 66 75 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → 𝑥 ∈ 𝐴 )
77 76 expr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 → 𝑥 ∈ 𝐴 ) )
78 77 ssrdv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ⊆ 𝐴 )
79 59 78 ssfid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ∈ Fin )
80 xpfi ⊢ ( ( { 𝑦 } ∈ Fin ∧ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ∈ Fin ) → ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ∈ Fin )
81 58 79 80 sylancr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ∈ Fin )
82 81 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ∈ Fin )
83 iunfi ⊢ ( ( 𝐶 ∈ Fin ∧ ∀ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ∈ Fin ) → ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ∈ Fin )
84 2 82 83 syl2anc ⊢ ( 𝜑 → ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ∈ Fin )
85 reliun ⊢ ( Rel ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ↔ ∀ 𝑦 ∈ 𝐶 Rel ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) )
86 relxp ⊢ Rel ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 )
87 86 a1i ⊢ ( 𝑦 ∈ 𝐶 → Rel ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) )
88 85 87 mprgbir ⊢ Rel ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 )
89 88 a1i ⊢ ( 𝜑 → Rel ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) )
90 csbeq1 ⊢ ( 𝑥 = ( 2nd ‘ 𝑤 ) → ⦋ 𝑥 / 𝑗 ⦌ 𝐸 = ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 )
91 90 csbeq2dv ⊢ ( 𝑥 = ( 2nd ‘ 𝑤 ) → ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 = ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 )
92 91 eleq1d ⊢ ( 𝑥 = ( 2nd ‘ 𝑤 ) → ( ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ ↔ ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
93 csbeq1 ⊢ ( 𝑦 = ( 1st ‘ 𝑤 ) → ⦋ 𝑦 / 𝑘 ⦌ 𝐷 = ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ 𝐷 )
94 csbeq1 ⊢ ( 𝑦 = ( 1st ‘ 𝑤 ) → ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 = ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 )
95 94 eleq1d ⊢ ( 𝑦 = ( 1st ‘ 𝑤 ) → ( ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ ↔ ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
96 93 95 raleqbidv ⊢ ( 𝑦 = ( 1st ‘ 𝑤 ) → ( ∀ 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ ↔ ∀ 𝑥 ∈ ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ 𝐷 ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
97 simpl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → 𝜑 )
98 29 nfcri ⊢ Ⅎ 𝑗 𝑦 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵
99 71 equcomd ⊢ ( 𝑥 ∈ { 𝑗 } → 𝑗 = 𝑥 )
100 99 32 syl ⊢ ( 𝑥 ∈ { 𝑗 } → 𝐵 = ⦋ 𝑥 / 𝑗 ⦌ 𝐵 )
101 100 eleq2d ⊢ ( 𝑥 ∈ { 𝑗 } → ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ) )
102 101 biimpa ⊢ ( ( 𝑥 ∈ { 𝑗 } ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 )
103 68 102 sylbi ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝑗 } × 𝐵 ) → 𝑦 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 )
104 103 a1i ⊢ ( 𝑗 ∈ 𝐴 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝑗 } × 𝐵 ) → 𝑦 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ) )
105 98 104 rexlimi ⊢ ( ∃ 𝑗 ∈ 𝐴 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝑗 } × 𝐵 ) → 𝑦 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 )
106 66 105 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → 𝑦 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 )
107 5 ralrimivva ⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝐴 ∀ 𝑘 ∈ 𝐵 𝐸 ∈ ℂ )
108 nfcsb1v ⊢ Ⅎ 𝑗 ⦋ 𝑥 / 𝑗 ⦌ 𝐸
109 108 nfel1 ⊢ Ⅎ 𝑗 ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ
110 29 109 nfralw ⊢ Ⅎ 𝑗 ∀ 𝑘 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ
111 csbeq1a ⊢ ( 𝑗 = 𝑥 → 𝐸 = ⦋ 𝑥 / 𝑗 ⦌ 𝐸 )
112 111 eleq1d ⊢ ( 𝑗 = 𝑥 → ( 𝐸 ∈ ℂ ↔ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
113 32 112 raleqbidv ⊢ ( 𝑗 = 𝑥 → ( ∀ 𝑘 ∈ 𝐵 𝐸 ∈ ℂ ↔ ∀ 𝑘 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
114 110 113 rspc ⊢ ( 𝑥 ∈ 𝐴 → ( ∀ 𝑗 ∈ 𝐴 ∀ 𝑘 ∈ 𝐵 𝐸 ∈ ℂ → ∀ 𝑘 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
115 107 114 mpan9 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑘 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ )
116 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸
117 116 nfel1 ⊢ Ⅎ 𝑘 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ
118 csbeq1a ⊢ ( 𝑘 = 𝑦 → ⦋ 𝑥 / 𝑗 ⦌ 𝐸 = ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 )
119 118 eleq1d ⊢ ( 𝑘 = 𝑦 → ( ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ ↔ ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
120 117 119 rspc ⊢ ( 𝑦 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 → ( ∀ 𝑘 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ → ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
121 115 120 syl5com ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 → ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
122 121 impr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ) ) → ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ )
123 97 76 106 122 syl12anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ )
124 123 ralrimivva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐶 ∀ 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ )
125 124 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → ∀ 𝑦 ∈ 𝐶 ∀ 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ )
126 simpr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → 𝑤 ∈ ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) )
127 eliun ⊢ ( 𝑤 ∈ ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ↔ ∃ 𝑦 ∈ 𝐶 𝑤 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) )
128 126 127 sylib ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → ∃ 𝑦 ∈ 𝐶 𝑤 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) )
129 xp1st ⊢ ( 𝑤 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) → ( 1st ‘ 𝑤 ) ∈ { 𝑦 } )
130 129 adantl ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑤 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → ( 1st ‘ 𝑤 ) ∈ { 𝑦 } )
131 elsni ⊢ ( ( 1st ‘ 𝑤 ) ∈ { 𝑦 } → ( 1st ‘ 𝑤 ) = 𝑦 )
132 130 131 syl ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑤 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → ( 1st ‘ 𝑤 ) = 𝑦 )
133 simpl ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑤 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → 𝑦 ∈ 𝐶 )
134 132 133 eqeltrd ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑤 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → ( 1st ‘ 𝑤 ) ∈ 𝐶 )
135 134 rexlimiva ⊢ ( ∃ 𝑦 ∈ 𝐶 𝑤 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) → ( 1st ‘ 𝑤 ) ∈ 𝐶 )
136 128 135 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → ( 1st ‘ 𝑤 ) ∈ 𝐶 )
137 96 125 136 rspcdva ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → ∀ 𝑥 ∈ ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ 𝐷 ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ )
138 xp2nd ⊢ ( 𝑤 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) → ( 2nd ‘ 𝑤 ) ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 )
139 138 adantl ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑤 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → ( 2nd ‘ 𝑤 ) ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 )
140 132 csbeq1d ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑤 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ 𝐷 = ⦋ 𝑦 / 𝑘 ⦌ 𝐷 )
141 139 140 eleqtrrd ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑤 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → ( 2nd ‘ 𝑤 ) ∈ ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ 𝐷 )
142 141 rexlimiva ⊢ ( ∃ 𝑦 ∈ 𝐶 𝑤 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) → ( 2nd ‘ 𝑤 ) ∈ ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ 𝐷 )
143 128 142 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → ( 2nd ‘ 𝑤 ) ∈ ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ 𝐷 )
144 92 137 143 rspcdva ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 ∈ ℂ )
145 51 57 84 89 144 fprodcnv ⊢ ( 𝜑 → ∏ 𝑤 ∈ ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 = ∏ 𝑧 ∈ ◡ ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ ( 1st ‘ 𝑧 ) / 𝑗 ⦌ 𝐸 )
146 45 145 eqtr4d ⊢ ( 𝜑 → ∏ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ ( 1st ‘ 𝑧 ) / 𝑗 ⦌ 𝐸 = ∏ 𝑤 ∈ ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 )
147 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝐴 𝐵 ∈ Fin )
148 29 nfel1 ⊢ Ⅎ 𝑗 ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ∈ Fin
149 32 eleq1d ⊢ ( 𝑗 = 𝑥 → ( 𝐵 ∈ Fin ↔ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ∈ Fin ) )
150 148 149 rspc ⊢ ( 𝑥 ∈ 𝐴 → ( ∀ 𝑗 ∈ 𝐴 𝐵 ∈ Fin → ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ∈ Fin ) )
151 147 150 mpan9 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ∈ Fin )
152 57 1 151 122 fprod2d ⊢ ( 𝜑 → ∏ 𝑥 ∈ 𝐴 ∏ 𝑦 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 = ∏ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ ( 1st ‘ 𝑧 ) / 𝑗 ⦌ 𝐸 )
153 51 2 79 123 fprod2d ⊢ ( 𝜑 → ∏ 𝑦 ∈ 𝐶 ∏ 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 = ∏ 𝑤 ∈ ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 )
154 146 152 153 3eqtr4d ⊢ ( 𝜑 → ∏ 𝑥 ∈ 𝐴 ∏ 𝑦 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 = ∏ 𝑦 ∈ 𝐶 ∏ 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 )
155 nfcv ⊢ Ⅎ 𝑥 ∏ 𝑘 ∈ 𝐵 𝐸
156 nfcv ⊢ Ⅎ 𝑗 𝑦
157 156 108 nfcsbw ⊢ Ⅎ 𝑗 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸
158 29 157 nfcprod ⊢ Ⅎ 𝑗 ∏ 𝑦 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸
159 nfcv ⊢ Ⅎ 𝑦 𝐸
160 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑦 / 𝑘 ⦌ 𝐸
161 csbeq1a ⊢ ( 𝑘 = 𝑦 → 𝐸 = ⦋ 𝑦 / 𝑘 ⦌ 𝐸 )
162 159 160 161 cbvprodi ⊢ ∏ 𝑘 ∈ 𝐵 𝐸 = ∏ 𝑦 ∈ 𝐵 ⦋ 𝑦 / 𝑘 ⦌ 𝐸
163 111 csbeq2dv ⊢ ( 𝑗 = 𝑥 → ⦋ 𝑦 / 𝑘 ⦌ 𝐸 = ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 )
164 163 adantr ⊢ ( ( 𝑗 = 𝑥 ∧ 𝑦 ∈ 𝐵 ) → ⦋ 𝑦 / 𝑘 ⦌ 𝐸 = ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 )
165 32 164 prodeq12dv ⊢ ( 𝑗 = 𝑥 → ∏ 𝑦 ∈ 𝐵 ⦋ 𝑦 / 𝑘 ⦌ 𝐸 = ∏ 𝑦 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 )
166 162 165 syl5eq ⊢ ( 𝑗 = 𝑥 → ∏ 𝑘 ∈ 𝐵 𝐸 = ∏ 𝑦 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 )
167 155 158 166 cbvprodi ⊢ ∏ 𝑗 ∈ 𝐴 ∏ 𝑘 ∈ 𝐵 𝐸 = ∏ 𝑥 ∈ 𝐴 ∏ 𝑦 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸
168 nfcv ⊢ Ⅎ 𝑦 ∏ 𝑗 ∈ 𝐷 𝐸
169 37 116 nfcprod ⊢ Ⅎ 𝑘 ∏ 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸
170 nfcv ⊢ Ⅎ 𝑥 𝐸
171 170 108 111 cbvprodi ⊢ ∏ 𝑗 ∈ 𝐷 𝐸 = ∏ 𝑥 ∈ 𝐷 ⦋ 𝑥 / 𝑗 ⦌ 𝐸
172 118 adantr ⊢ ( ( 𝑘 = 𝑦 ∧ 𝑥 ∈ 𝐷 ) → ⦋ 𝑥 / 𝑗 ⦌ 𝐸 = ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 )
173 40 172 prodeq12dv ⊢ ( 𝑘 = 𝑦 → ∏ 𝑥 ∈ 𝐷 ⦋ 𝑥 / 𝑗 ⦌ 𝐸 = ∏ 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 )
174 171 173 syl5eq ⊢ ( 𝑘 = 𝑦 → ∏ 𝑗 ∈ 𝐷 𝐸 = ∏ 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 )
175 168 169 174 cbvprodi ⊢ ∏ 𝑘 ∈ 𝐶 ∏ 𝑗 ∈ 𝐷 𝐸 = ∏ 𝑦 ∈ 𝐶 ∏ 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸
176 154 167 175 3eqtr4g ⊢ ( 𝜑 → ∏ 𝑗 ∈ 𝐴 ∏ 𝑘 ∈ 𝐵 𝐸 = ∏ 𝑘 ∈ 𝐶 ∏ 𝑗 ∈ 𝐷 𝐸 )