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 opelxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝑗 } × 𝐵 ) ↔ ( 𝑥 ∈ { 𝑗 } ∧ 𝑦 ∈ 𝐵 ) )
68 67 bilani ⊢ ( ( 𝑗 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝑗 } × 𝐵 ) ) → ( 𝑥 ∈ { 𝑗 } ∧ 𝑦 ∈ 𝐵 ) )
69 68 simpld ⊢ ( ( 𝑗 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝑗 } × 𝐵 ) ) → 𝑥 ∈ { 𝑗 } )
70 elsni ⊢ ( 𝑥 ∈ { 𝑗 } → 𝑥 = 𝑗 )
71 69 70 syl ⊢ ( ( 𝑗 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝑗 } × 𝐵 ) ) → 𝑥 = 𝑗 )
72 simpl ⊢ ( ( 𝑗 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝑗 } × 𝐵 ) ) → 𝑗 ∈ 𝐴 )
73 71 72 eqeltrd ⊢ ( ( 𝑗 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝑗 } × 𝐵 ) ) → 𝑥 ∈ 𝐴 )
74 73 rexlimiva ⊢ ( ∃ 𝑗 ∈ 𝐴 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝑗 } × 𝐵 ) → 𝑥 ∈ 𝐴 )
75 66 74 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → 𝑥 ∈ 𝐴 )
76 75 expr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 → 𝑥 ∈ 𝐴 ) )
77 76 ssrdv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ⊆ 𝐴 )
78 59 77 ssfid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ∈ Fin )
79 xpfi ⊢ ( ( { 𝑦 } ∈ Fin ∧ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ∈ Fin ) → ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ∈ Fin )
80 58 78 79 sylancr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ∈ Fin )
81 80 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ∈ Fin )
82 iunfi ⊢ ( ( 𝐶 ∈ Fin ∧ ∀ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ∈ Fin ) → ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ∈ Fin )
83 2 81 82 syl2anc ⊢ ( 𝜑 → ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ∈ Fin )
84 reliun ⊢ ( Rel ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ↔ ∀ 𝑦 ∈ 𝐶 Rel ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) )
85 relxp ⊢ Rel ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 )
86 85 a1i ⊢ ( 𝑦 ∈ 𝐶 → Rel ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) )
87 84 86 mprgbir ⊢ Rel ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 )
88 87 a1i ⊢ ( 𝜑 → Rel ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) )
89 csbeq1 ⊢ ( 𝑥 = ( 2nd ‘ 𝑤 ) → ⦋ 𝑥 / 𝑗 ⦌ 𝐸 = ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 )
90 89 csbeq2dv ⊢ ( 𝑥 = ( 2nd ‘ 𝑤 ) → ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 = ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 )
91 90 eleq1d ⊢ ( 𝑥 = ( 2nd ‘ 𝑤 ) → ( ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ ↔ ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
92 csbeq1 ⊢ ( 𝑦 = ( 1st ‘ 𝑤 ) → ⦋ 𝑦 / 𝑘 ⦌ 𝐷 = ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ 𝐷 )
93 csbeq1 ⊢ ( 𝑦 = ( 1st ‘ 𝑤 ) → ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 = ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 )
94 93 eleq1d ⊢ ( 𝑦 = ( 1st ‘ 𝑤 ) → ( ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ ↔ ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
95 92 94 raleqbidv ⊢ ( 𝑦 = ( 1st ‘ 𝑤 ) → ( ∀ 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ ↔ ∀ 𝑥 ∈ ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ 𝐷 ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
96 simpl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → 𝜑 )
97 29 nfcri ⊢ Ⅎ 𝑗 𝑦 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵
98 70 equcomd ⊢ ( 𝑥 ∈ { 𝑗 } → 𝑗 = 𝑥 )
99 98 32 syl ⊢ ( 𝑥 ∈ { 𝑗 } → 𝐵 = ⦋ 𝑥 / 𝑗 ⦌ 𝐵 )
100 99 eleq2d ⊢ ( 𝑥 ∈ { 𝑗 } → ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ) )
101 100 biimpa ⊢ ( ( 𝑥 ∈ { 𝑗 } ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 )
102 67 101 sylbi ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝑗 } × 𝐵 ) → 𝑦 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 )
103 102 a1i ⊢ ( 𝑗 ∈ 𝐴 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝑗 } × 𝐵 ) → 𝑦 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ) )
104 97 103 rexlimi ⊢ ( ∃ 𝑗 ∈ 𝐴 ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝑗 } × 𝐵 ) → 𝑦 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 )
105 66 104 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → 𝑦 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 )
106 5 ralrimivva ⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝐴 ∀ 𝑘 ∈ 𝐵 𝐸 ∈ ℂ )
107 nfcsb1v ⊢ Ⅎ 𝑗 ⦋ 𝑥 / 𝑗 ⦌ 𝐸
108 107 nfel1 ⊢ Ⅎ 𝑗 ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ
109 29 108 nfralw ⊢ Ⅎ 𝑗 ∀ 𝑘 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ
110 csbeq1a ⊢ ( 𝑗 = 𝑥 → 𝐸 = ⦋ 𝑥 / 𝑗 ⦌ 𝐸 )
111 110 eleq1d ⊢ ( 𝑗 = 𝑥 → ( 𝐸 ∈ ℂ ↔ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
112 32 111 raleqbidv ⊢ ( 𝑗 = 𝑥 → ( ∀ 𝑘 ∈ 𝐵 𝐸 ∈ ℂ ↔ ∀ 𝑘 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
113 109 112 rspc ⊢ ( 𝑥 ∈ 𝐴 → ( ∀ 𝑗 ∈ 𝐴 ∀ 𝑘 ∈ 𝐵 𝐸 ∈ ℂ → ∀ 𝑘 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
114 106 113 mpan9 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑘 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ )
115 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸
116 115 nfel1 ⊢ Ⅎ 𝑘 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ
117 csbeq1a ⊢ ( 𝑘 = 𝑦 → ⦋ 𝑥 / 𝑗 ⦌ 𝐸 = ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 )
118 117 eleq1d ⊢ ( 𝑘 = 𝑦 → ( ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ ↔ ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
119 116 118 rspc ⊢ ( 𝑦 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 → ( ∀ 𝑘 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ → ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
120 114 119 syl5com ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 → ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ ) )
121 120 impr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ) ) → ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ )
122 96 75 105 121 syl12anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ )
123 122 ralrimivva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐶 ∀ 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ )
124 123 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → ∀ 𝑦 ∈ 𝐶 ∀ 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ )
125 eliun ⊢ ( 𝑤 ∈ ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ↔ ∃ 𝑦 ∈ 𝐶 𝑤 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) )
126 125 bilani ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → ∃ 𝑦 ∈ 𝐶 𝑤 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) )
127 xp1st ⊢ ( 𝑤 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) → ( 1st ‘ 𝑤 ) ∈ { 𝑦 } )
128 127 adantl ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑤 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → ( 1st ‘ 𝑤 ) ∈ { 𝑦 } )
129 elsni ⊢ ( ( 1st ‘ 𝑤 ) ∈ { 𝑦 } → ( 1st ‘ 𝑤 ) = 𝑦 )
130 128 129 syl ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑤 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → ( 1st ‘ 𝑤 ) = 𝑦 )
131 simpl ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑤 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → 𝑦 ∈ 𝐶 )
132 130 131 eqeltrd ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑤 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → ( 1st ‘ 𝑤 ) ∈ 𝐶 )
133 132 rexlimiva ⊢ ( ∃ 𝑦 ∈ 𝐶 𝑤 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) → ( 1st ‘ 𝑤 ) ∈ 𝐶 )
134 126 133 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → ( 1st ‘ 𝑤 ) ∈ 𝐶 )
135 95 124 134 rspcdva ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → ∀ 𝑥 ∈ ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ 𝐷 ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 ∈ ℂ )
136 xp2nd ⊢ ( 𝑤 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) → ( 2nd ‘ 𝑤 ) ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 )
137 136 adantl ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑤 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → ( 2nd ‘ 𝑤 ) ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 )
138 130 csbeq1d ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑤 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ 𝐷 = ⦋ 𝑦 / 𝑘 ⦌ 𝐷 )
139 137 138 eleqtrrd ⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑤 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → ( 2nd ‘ 𝑤 ) ∈ ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ 𝐷 )
140 139 rexlimiva ⊢ ( ∃ 𝑦 ∈ 𝐶 𝑤 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) → ( 2nd ‘ 𝑤 ) ∈ ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ 𝐷 )
141 126 140 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → ( 2nd ‘ 𝑤 ) ∈ ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ 𝐷 )
142 91 135 141 rspcdva ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ) → ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 ∈ ℂ )
143 51 57 83 88 142 fprodcnv ⊢ ( 𝜑 → ∏ 𝑤 ∈ ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 = ∏ 𝑧 ∈ ◡ ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ ( 1st ‘ 𝑧 ) / 𝑗 ⦌ 𝐸 )
144 45 143 eqtr4d ⊢ ( 𝜑 → ∏ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ ( 1st ‘ 𝑧 ) / 𝑗 ⦌ 𝐸 = ∏ 𝑤 ∈ ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 )
145 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝐴 𝐵 ∈ Fin )
146 29 nfel1 ⊢ Ⅎ 𝑗 ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ∈ Fin
147 32 eleq1d ⊢ ( 𝑗 = 𝑥 → ( 𝐵 ∈ Fin ↔ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ∈ Fin ) )
148 146 147 rspc ⊢ ( 𝑥 ∈ 𝐴 → ( ∀ 𝑗 ∈ 𝐴 𝐵 ∈ Fin → ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ∈ Fin ) )
149 145 148 mpan9 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ∈ Fin )
150 57 1 149 121 fprod2d ⊢ ( 𝜑 → ∏ 𝑥 ∈ 𝐴 ∏ 𝑦 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 = ∏ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ ( 1st ‘ 𝑧 ) / 𝑗 ⦌ 𝐸 )
151 51 2 78 122 fprod2d ⊢ ( 𝜑 → ∏ 𝑦 ∈ 𝐶 ∏ 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 = ∏ 𝑤 ∈ ∪ 𝑦 ∈ 𝐶 ( { 𝑦 } × ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ) ⦋ ( 1st ‘ 𝑤 ) / 𝑘 ⦌ ⦋ ( 2nd ‘ 𝑤 ) / 𝑗 ⦌ 𝐸 )
152 144 150 151 3eqtr4d ⊢ ( 𝜑 → ∏ 𝑥 ∈ 𝐴 ∏ 𝑦 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 = ∏ 𝑦 ∈ 𝐶 ∏ 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 )
153 nfcv ⊢ Ⅎ 𝑥 ∏ 𝑘 ∈ 𝐵 𝐸
154 nfcv ⊢ Ⅎ 𝑗 𝑦
155 154 107 nfcsbw ⊢ Ⅎ 𝑗 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸
156 29 155 nfcprod ⊢ Ⅎ 𝑗 ∏ 𝑦 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸
157 nfcv ⊢ Ⅎ 𝑦 𝐸
158 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑦 / 𝑘 ⦌ 𝐸
159 csbeq1a ⊢ ( 𝑘 = 𝑦 → 𝐸 = ⦋ 𝑦 / 𝑘 ⦌ 𝐸 )
160 157 158 159 cbvprodi ⊢ ∏ 𝑘 ∈ 𝐵 𝐸 = ∏ 𝑦 ∈ 𝐵 ⦋ 𝑦 / 𝑘 ⦌ 𝐸
161 110 csbeq2dv ⊢ ( 𝑗 = 𝑥 → ⦋ 𝑦 / 𝑘 ⦌ 𝐸 = ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 )
162 161 adantr ⊢ ( ( 𝑗 = 𝑥 ∧ 𝑦 ∈ 𝐵 ) → ⦋ 𝑦 / 𝑘 ⦌ 𝐸 = ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 )
163 32 162 prodeq12dv ⊢ ( 𝑗 = 𝑥 → ∏ 𝑦 ∈ 𝐵 ⦋ 𝑦 / 𝑘 ⦌ 𝐸 = ∏ 𝑦 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 )
164 160 163 eqtrid ⊢ ( 𝑗 = 𝑥 → ∏ 𝑘 ∈ 𝐵 𝐸 = ∏ 𝑦 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 )
165 153 156 164 cbvprodi ⊢ ∏ 𝑗 ∈ 𝐴 ∏ 𝑘 ∈ 𝐵 𝐸 = ∏ 𝑥 ∈ 𝐴 ∏ 𝑦 ∈ ⦋ 𝑥 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸
166 nfcv ⊢ Ⅎ 𝑦 ∏ 𝑗 ∈ 𝐷 𝐸
167 37 115 nfcprod ⊢ Ⅎ 𝑘 ∏ 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸
168 nfcv ⊢ Ⅎ 𝑥 𝐸
169 168 107 110 cbvprodi ⊢ ∏ 𝑗 ∈ 𝐷 𝐸 = ∏ 𝑥 ∈ 𝐷 ⦋ 𝑥 / 𝑗 ⦌ 𝐸
170 117 adantr ⊢ ( ( 𝑘 = 𝑦 ∧ 𝑥 ∈ 𝐷 ) → ⦋ 𝑥 / 𝑗 ⦌ 𝐸 = ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 )
171 40 170 prodeq12dv ⊢ ( 𝑘 = 𝑦 → ∏ 𝑥 ∈ 𝐷 ⦋ 𝑥 / 𝑗 ⦌ 𝐸 = ∏ 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 )
172 169 171 eqtrid ⊢ ( 𝑘 = 𝑦 → ∏ 𝑗 ∈ 𝐷 𝐸 = ∏ 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸 )
173 166 167 172 cbvprodi ⊢ ∏ 𝑘 ∈ 𝐶 ∏ 𝑗 ∈ 𝐷 𝐸 = ∏ 𝑦 ∈ 𝐶 ∏ 𝑥 ∈ ⦋ 𝑦 / 𝑘 ⦌ 𝐷 ⦋ 𝑦 / 𝑘 ⦌ ⦋ 𝑥 / 𝑗 ⦌ 𝐸
174 152 165 173 3eqtr4g ⊢ ( 𝜑 → ∏ 𝑗 ∈ 𝐴 ∏ 𝑘 ∈ 𝐵 𝐸 = ∏ 𝑘 ∈ 𝐶 ∏ 𝑗 ∈ 𝐷 𝐸 )