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

Metamath Proof Explorer

Theorem fprod2dlem

Description: Lemma for fprod2d - induction step. (Contributed by Scott Fenton, 30-Jan-2018)

Ref Expression
Hypotheses fprod2d.1 ⊢ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → 𝐷 = 𝐶 )
fprod2d.2 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
fprod2d.3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ∈ Fin )
fprod2d.4 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐶 ∈ ℂ )
fprod2d.5 ⊢ ( 𝜑 → ¬ 𝑦 ∈ 𝑥 )
fprod2d.6 ⊢ ( 𝜑 → ( 𝑥 ∪ { 𝑦 } ) ⊆ 𝐴 )
fprod2d.7 ⊢ ( 𝜓 ↔ ∏ 𝑗 ∈ 𝑥 ∏ 𝑘 ∈ 𝐵 𝐶 = ∏ 𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) 𝐷 )
Assertion fprod2dlem ( ( 𝜑 ∧ 𝜓 ) → ∏ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ∏ 𝑘 ∈ 𝐵 𝐶 = ∏ 𝑧 ∈ ∪ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) 𝐷 )

Proof

Step Hyp Ref Expression
1 fprod2d.1 ⊢ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → 𝐷 = 𝐶 )
2 fprod2d.2 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
3 fprod2d.3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ∈ Fin )
4 fprod2d.4 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐶 ∈ ℂ )
5 fprod2d.5 ⊢ ( 𝜑 → ¬ 𝑦 ∈ 𝑥 )
6 fprod2d.6 ⊢ ( 𝜑 → ( 𝑥 ∪ { 𝑦 } ) ⊆ 𝐴 )
7 fprod2d.7 ⊢ ( 𝜓 ↔ ∏ 𝑗 ∈ 𝑥 ∏ 𝑘 ∈ 𝐵 𝐶 = ∏ 𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) 𝐷 )
8 simpr ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜓 )
9 8 7 sylib ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∏ 𝑗 ∈ 𝑥 ∏ 𝑘 ∈ 𝐵 𝐶 = ∏ 𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) 𝐷 )
10 nfcv ⊢ Ⅎ 𝑚 ∏ 𝑘 ∈ 𝐵 𝐶
11 nfcsb1v ⊢ Ⅎ 𝑗 ⦋ 𝑚 / 𝑗 ⦌ 𝐵
12 nfcsb1v ⊢ Ⅎ 𝑗 ⦋ 𝑚 / 𝑗 ⦌ 𝐶
13 11 12 nfcprod ⊢ Ⅎ 𝑗 ∏ 𝑘 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑚 / 𝑗 ⦌ 𝐶
14 csbeq1a ⊢ ( 𝑗 = 𝑚 → 𝐵 = ⦋ 𝑚 / 𝑗 ⦌ 𝐵 )
15 csbeq1a ⊢ ( 𝑗 = 𝑚 → 𝐶 = ⦋ 𝑚 / 𝑗 ⦌ 𝐶 )
16 15 adantr ⊢ ( ( 𝑗 = 𝑚 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 = ⦋ 𝑚 / 𝑗 ⦌ 𝐶 )
17 14 16 prodeq12dv ⊢ ( 𝑗 = 𝑚 → ∏ 𝑘 ∈ 𝐵 𝐶 = ∏ 𝑘 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑚 / 𝑗 ⦌ 𝐶 )
18 10 13 17 cbvprodi ⊢ ∏ 𝑗 ∈ { 𝑦 } ∏ 𝑘 ∈ 𝐵 𝐶 = ∏ 𝑚 ∈ { 𝑦 } ∏ 𝑘 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑚 / 𝑗 ⦌ 𝐶
19 6 unssbd ⊢ ( 𝜑 → { 𝑦 } ⊆ 𝐴 )
20 vex ⊢ 𝑦 ∈ V
21 20 snss ⊢ ( 𝑦 ∈ 𝐴 ↔ { 𝑦 } ⊆ 𝐴 )
22 19 21 sylibr ⊢ ( 𝜑 → 𝑦 ∈ 𝐴 )
23 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝐴 𝐵 ∈ Fin )
24 nfcsb1v ⊢ Ⅎ 𝑗 ⦋ 𝑦 / 𝑗 ⦌ 𝐵
25 24 nfel1 ⊢ Ⅎ 𝑗 ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ∈ Fin
26 csbeq1a ⊢ ( 𝑗 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑗 ⦌ 𝐵 )
27 26 eleq1d ⊢ ( 𝑗 = 𝑦 → ( 𝐵 ∈ Fin ↔ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ∈ Fin ) )
28 25 27 rspc ⊢ ( 𝑦 ∈ 𝐴 → ( ∀ 𝑗 ∈ 𝐴 𝐵 ∈ Fin → ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ∈ Fin ) )
29 22 23 28 sylc ⊢ ( 𝜑 → ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ∈ Fin )
30 4 ralrimivva ⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝐴 ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ℂ )
31 nfcsb1v ⊢ Ⅎ 𝑗 ⦋ 𝑦 / 𝑗 ⦌ 𝐶
32 31 nfel1 ⊢ Ⅎ 𝑗 ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ∈ ℂ
33 24 32 nfralw ⊢ Ⅎ 𝑗 ∀ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ∈ ℂ
34 csbeq1a ⊢ ( 𝑗 = 𝑦 → 𝐶 = ⦋ 𝑦 / 𝑗 ⦌ 𝐶 )
35 34 eleq1d ⊢ ( 𝑗 = 𝑦 → ( 𝐶 ∈ ℂ ↔ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ∈ ℂ ) )
36 26 35 raleqbidv ⊢ ( 𝑗 = 𝑦 → ( ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ℂ ↔ ∀ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ∈ ℂ ) )
37 33 36 rspc ⊢ ( 𝑦 ∈ 𝐴 → ( ∀ 𝑗 ∈ 𝐴 ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ℂ → ∀ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ∈ ℂ ) )
38 22 30 37 sylc ⊢ ( 𝜑 → ∀ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ∈ ℂ )
39 38 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) → ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ∈ ℂ )
40 29 39 fprodcl ⊢ ( 𝜑 → ∏ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ∈ ℂ )
41 csbeq1 ⊢ ( 𝑚 = 𝑦 → ⦋ 𝑚 / 𝑗 ⦌ 𝐵 = ⦋ 𝑦 / 𝑗 ⦌ 𝐵 )
42 csbeq1 ⊢ ( 𝑚 = 𝑦 → ⦋ 𝑚 / 𝑗 ⦌ 𝐶 = ⦋ 𝑦 / 𝑗 ⦌ 𝐶 )
43 42 adantr ⊢ ( ( 𝑚 = 𝑦 ∧ 𝑘 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ) → ⦋ 𝑚 / 𝑗 ⦌ 𝐶 = ⦋ 𝑦 / 𝑗 ⦌ 𝐶 )
44 41 43 prodeq12dv ⊢ ( 𝑚 = 𝑦 → ∏ 𝑘 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑚 / 𝑗 ⦌ 𝐶 = ∏ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑗 ⦌ 𝐶 )
45 44 prodsn ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ∏ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ∈ ℂ ) → ∏ 𝑚 ∈ { 𝑦 } ∏ 𝑘 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑚 / 𝑗 ⦌ 𝐶 = ∏ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑗 ⦌ 𝐶 )
46 22 40 45 syl2anc ⊢ ( 𝜑 → ∏ 𝑚 ∈ { 𝑦 } ∏ 𝑘 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑚 / 𝑗 ⦌ 𝐶 = ∏ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑗 ⦌ 𝐶 )
47 nfcv ⊢ Ⅎ 𝑚 ⦋ 𝑦 / 𝑗 ⦌ 𝐶
48 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑚 / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶
49 csbeq1a ⊢ ( 𝑘 = 𝑚 → ⦋ 𝑦 / 𝑗 ⦌ 𝐶 = ⦋ 𝑚 / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 )
50 47 48 49 cbvprodi ⊢ ∏ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑗 ⦌ 𝐶 = ∏ 𝑚 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ⦋ 𝑚 / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶
51 csbeq1 ⊢ ( 𝑚 = ( 2nd ‘ 𝑧 ) → ⦋ 𝑚 / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 = ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 )
52 snfi ⊢ { 𝑦 } ∈ Fin
53 xpfi ⊢ ( ( { 𝑦 } ∈ Fin ∧ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ∈ Fin ) → ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ∈ Fin )
54 52 29 53 sylancr ⊢ ( 𝜑 → ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ∈ Fin )
55 2ndconst ⊢ ( 𝑦 ∈ 𝐴 → ( 2nd ↾ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) : ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) –1-1-onto→ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 )
56 22 55 syl ⊢ ( 𝜑 → ( 2nd ↾ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) : ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) –1-1-onto→ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 )
57 fvres ⊢ ( 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) → ( ( 2nd ↾ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) ‘ 𝑧 ) = ( 2nd ‘ 𝑧 ) )
58 57 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) → ( ( 2nd ↾ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) ‘ 𝑧 ) = ( 2nd ‘ 𝑧 ) )
59 48 nfel1 ⊢ Ⅎ 𝑘 ⦋ 𝑚 / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ∈ ℂ
60 49 eleq1d ⊢ ( 𝑘 = 𝑚 → ( ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ∈ ℂ ↔ ⦋ 𝑚 / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ∈ ℂ ) )
61 59 60 rspc ⊢ ( 𝑚 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 → ( ∀ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ∈ ℂ → ⦋ 𝑚 / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ∈ ℂ ) )
62 38 61 mpan9 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) → ⦋ 𝑚 / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ∈ ℂ )
63 51 54 56 58 62 fprodf1o ⊢ ( 𝜑 → ∏ 𝑚 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ⦋ 𝑚 / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 = ∏ 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 )
64 elxp ⊢ ( 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ↔ ∃ 𝑚 ∃ 𝑘 ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑦 } ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) )
65 nfv ⊢ Ⅎ 𝑗 𝑧 = ⟨ 𝑚 , 𝑘 ⟩
66 nfv ⊢ Ⅎ 𝑗 𝑚 ∈ { 𝑦 }
67 24 nfcri ⊢ Ⅎ 𝑗 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵
68 66 67 nfan ⊢ Ⅎ 𝑗 ( 𝑚 ∈ { 𝑦 } ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 )
69 65 68 nfan ⊢ Ⅎ 𝑗 ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑦 } ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) )
70 69 nfex ⊢ Ⅎ 𝑗 ∃ 𝑘 ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑦 } ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) )
71 nfv ⊢ Ⅎ 𝑚 ∃ 𝑘 ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ∧ ( 𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵 ) )
72 opeq1 ⊢ ( 𝑚 = 𝑗 → ⟨ 𝑚 , 𝑘 ⟩ = ⟨ 𝑗 , 𝑘 ⟩ )
73 72 eqeq2d ⊢ ( 𝑚 = 𝑗 → ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ↔ 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ) )
74 eleq1w ⊢ ( 𝑚 = 𝑗 → ( 𝑚 ∈ { 𝑦 } ↔ 𝑗 ∈ { 𝑦 } ) )
75 velsn ⊢ ( 𝑗 ∈ { 𝑦 } ↔ 𝑗 = 𝑦 )
76 74 75 bitrdi ⊢ ( 𝑚 = 𝑗 → ( 𝑚 ∈ { 𝑦 } ↔ 𝑗 = 𝑦 ) )
77 76 anbi1d ⊢ ( 𝑚 = 𝑗 → ( ( 𝑚 ∈ { 𝑦 } ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ↔ ( 𝑗 = 𝑦 ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) )
78 26 eleq2d ⊢ ( 𝑗 = 𝑦 → ( 𝑘 ∈ 𝐵 ↔ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) )
79 78 pm5.32i ⊢ ( ( 𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵 ) ↔ ( 𝑗 = 𝑦 ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) )
80 77 79 bitr4di ⊢ ( 𝑚 = 𝑗 → ( ( 𝑚 ∈ { 𝑦 } ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ↔ ( 𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵 ) ) )
81 73 80 anbi12d ⊢ ( 𝑚 = 𝑗 → ( ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑦 } ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) ↔ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ∧ ( 𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵 ) ) ) )
82 81 exbidv ⊢ ( 𝑚 = 𝑗 → ( ∃ 𝑘 ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑦 } ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) ↔ ∃ 𝑘 ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ∧ ( 𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵 ) ) ) )
83 70 71 82 cbvexv1 ⊢ ( ∃ 𝑚 ∃ 𝑘 ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑦 } ∧ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) ↔ ∃ 𝑗 ∃ 𝑘 ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ∧ ( 𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵 ) ) )
84 64 83 bitri ⊢ ( 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ↔ ∃ 𝑗 ∃ 𝑘 ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ∧ ( 𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵 ) ) )
85 nfv ⊢ Ⅎ 𝑗 𝜑
86 nfcv ⊢ Ⅎ 𝑗 ( 2nd ‘ 𝑧 )
87 86 31 nfcsbw ⊢ Ⅎ 𝑗 ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶
88 87 nfeq2 ⊢ Ⅎ 𝑗 𝐷 = ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶
89 nfv ⊢ Ⅎ 𝑘 𝜑
90 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶
91 90 nfeq2 ⊢ Ⅎ 𝑘 𝐷 = ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶
92 1 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ) ∧ ( 𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐷 = 𝐶 )
93 34 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ) ∧ ( 𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐶 = ⦋ 𝑦 / 𝑗 ⦌ 𝐶 )
94 fveq2 ⊢ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → ( 2nd ‘ 𝑧 ) = ( 2nd ‘ ⟨ 𝑗 , 𝑘 ⟩ ) )
95 vex ⊢ 𝑗 ∈ V
96 vex ⊢ 𝑘 ∈ V
97 95 96 op2nd ⊢ ( 2nd ‘ ⟨ 𝑗 , 𝑘 ⟩ ) = 𝑘
98 94 97 eqtr2di ⊢ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → 𝑘 = ( 2nd ‘ 𝑧 ) )
99 98 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ) ∧ ( 𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵 ) ) → 𝑘 = ( 2nd ‘ 𝑧 ) )
100 csbeq1a ⊢ ( 𝑘 = ( 2nd ‘ 𝑧 ) → ⦋ 𝑦 / 𝑗 ⦌ 𝐶 = ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 )
101 99 100 syl ⊢ ( ( ( 𝜑 ∧ 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ) ∧ ( 𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵 ) ) → ⦋ 𝑦 / 𝑗 ⦌ 𝐶 = ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 )
102 92 93 101 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ) ∧ ( 𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐷 = ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 )
103 102 expl ⊢ ( 𝜑 → ( ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ∧ ( 𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐷 = ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ) )
104 89 91 103 exlimd ⊢ ( 𝜑 → ( ∃ 𝑘 ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ∧ ( 𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐷 = ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ) )
105 85 88 104 exlimd ⊢ ( 𝜑 → ( ∃ 𝑗 ∃ 𝑘 ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ∧ ( 𝑗 = 𝑦 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐷 = ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ) )
106 84 105 biimtrid ⊢ ( 𝜑 → ( 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) → 𝐷 = ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 ) )
107 106 imp ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) → 𝐷 = ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 )
108 107 prodeq2dv ⊢ ( 𝜑 → ∏ 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) 𝐷 = ∏ 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 )
109 63 108 eqtr4d ⊢ ( 𝜑 → ∏ 𝑚 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ⦋ 𝑚 / 𝑘 ⦌ ⦋ 𝑦 / 𝑗 ⦌ 𝐶 = ∏ 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) 𝐷 )
110 50 109 eqtrid ⊢ ( 𝜑 → ∏ 𝑘 ∈ ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ⦋ 𝑦 / 𝑗 ⦌ 𝐶 = ∏ 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) 𝐷 )
111 46 110 eqtrd ⊢ ( 𝜑 → ∏ 𝑚 ∈ { 𝑦 } ∏ 𝑘 ∈ ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ⦋ 𝑚 / 𝑗 ⦌ 𝐶 = ∏ 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) 𝐷 )
112 18 111 eqtrid ⊢ ( 𝜑 → ∏ 𝑗 ∈ { 𝑦 } ∏ 𝑘 ∈ 𝐵 𝐶 = ∏ 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) 𝐷 )
113 112 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∏ 𝑗 ∈ { 𝑦 } ∏ 𝑘 ∈ 𝐵 𝐶 = ∏ 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) 𝐷 )
114 9 113 oveq12d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ∏ 𝑗 ∈ 𝑥 ∏ 𝑘 ∈ 𝐵 𝐶 · ∏ 𝑗 ∈ { 𝑦 } ∏ 𝑘 ∈ 𝐵 𝐶 ) = ( ∏ 𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) 𝐷 · ∏ 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) 𝐷 ) )
115 disjsn ⊢ ( ( 𝑥 ∩ { 𝑦 } ) = ∅ ↔ ¬ 𝑦 ∈ 𝑥 )
116 5 115 sylibr ⊢ ( 𝜑 → ( 𝑥 ∩ { 𝑦 } ) = ∅ )
117 eqidd ⊢ ( 𝜑 → ( 𝑥 ∪ { 𝑦 } ) = ( 𝑥 ∪ { 𝑦 } ) )
118 2 6 ssfid ⊢ ( 𝜑 → ( 𝑥 ∪ { 𝑦 } ) ∈ Fin )
119 6 sselda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) → 𝑗 ∈ 𝐴 )
120 4 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ℂ )
121 3 120 fprodcl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ∏ 𝑘 ∈ 𝐵 𝐶 ∈ ℂ )
122 119 121 syldan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) → ∏ 𝑘 ∈ 𝐵 𝐶 ∈ ℂ )
123 116 117 118 122 fprodsplit ⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ∏ 𝑘 ∈ 𝐵 𝐶 = ( ∏ 𝑗 ∈ 𝑥 ∏ 𝑘 ∈ 𝐵 𝐶 · ∏ 𝑗 ∈ { 𝑦 } ∏ 𝑘 ∈ 𝐵 𝐶 ) )
124 123 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∏ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ∏ 𝑘 ∈ 𝐵 𝐶 = ( ∏ 𝑗 ∈ 𝑥 ∏ 𝑘 ∈ 𝐵 𝐶 · ∏ 𝑗 ∈ { 𝑦 } ∏ 𝑘 ∈ 𝐵 𝐶 ) )
125 eliun ⊢ ( 𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) ↔ ∃ 𝑗 ∈ 𝑥 𝑧 ∈ ( { 𝑗 } × 𝐵 ) )
126 xp1st ⊢ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) → ( 1st ‘ 𝑧 ) ∈ { 𝑗 } )
127 elsni ⊢ ( ( 1st ‘ 𝑧 ) ∈ { 𝑗 } → ( 1st ‘ 𝑧 ) = 𝑗 )
128 126 127 syl ⊢ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) → ( 1st ‘ 𝑧 ) = 𝑗 )
129 128 eleq1d ⊢ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) → ( ( 1st ‘ 𝑧 ) ∈ 𝑥 ↔ 𝑗 ∈ 𝑥 ) )
130 129 biimparc ⊢ ( ( 𝑗 ∈ 𝑥 ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → ( 1st ‘ 𝑧 ) ∈ 𝑥 )
131 130 rexlimiva ⊢ ( ∃ 𝑗 ∈ 𝑥 𝑧 ∈ ( { 𝑗 } × 𝐵 ) → ( 1st ‘ 𝑧 ) ∈ 𝑥 )
132 125 131 sylbi ⊢ ( 𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) → ( 1st ‘ 𝑧 ) ∈ 𝑥 )
133 xp1st ⊢ ( 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) → ( 1st ‘ 𝑧 ) ∈ { 𝑦 } )
134 132 133 anim12i ⊢ ( ( 𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) ∧ 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) → ( ( 1st ‘ 𝑧 ) ∈ 𝑥 ∧ ( 1st ‘ 𝑧 ) ∈ { 𝑦 } ) )
135 elin ⊢ ( 𝑧 ∈ ( ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) ∩ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) ↔ ( 𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) ∧ 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) )
136 elin ⊢ ( ( 1st ‘ 𝑧 ) ∈ ( 𝑥 ∩ { 𝑦 } ) ↔ ( ( 1st ‘ 𝑧 ) ∈ 𝑥 ∧ ( 1st ‘ 𝑧 ) ∈ { 𝑦 } ) )
137 134 135 136 3imtr4i ⊢ ( 𝑧 ∈ ( ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) ∩ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) → ( 1st ‘ 𝑧 ) ∈ ( 𝑥 ∩ { 𝑦 } ) )
138 116 eleq2d ⊢ ( 𝜑 → ( ( 1st ‘ 𝑧 ) ∈ ( 𝑥 ∩ { 𝑦 } ) ↔ ( 1st ‘ 𝑧 ) ∈ ∅ ) )
139 noel ⊢ ¬ ( 1st ‘ 𝑧 ) ∈ ∅
140 139 pm2.21i ⊢ ( ( 1st ‘ 𝑧 ) ∈ ∅ → 𝑧 ∈ ∅ )
141 138 140 biimtrdi ⊢ ( 𝜑 → ( ( 1st ‘ 𝑧 ) ∈ ( 𝑥 ∩ { 𝑦 } ) → 𝑧 ∈ ∅ ) )
142 137 141 syl5 ⊢ ( 𝜑 → ( 𝑧 ∈ ( ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) ∩ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) → 𝑧 ∈ ∅ ) )
143 142 ssrdv ⊢ ( 𝜑 → ( ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) ∩ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) ⊆ ∅ )
144 ss0 ⊢ ( ( ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) ∩ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) ⊆ ∅ → ( ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) ∩ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) = ∅ )
145 143 144 syl ⊢ ( 𝜑 → ( ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) ∩ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) = ∅ )
146 iunxun ⊢ ∪ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) = ( ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) ∪ ∪ 𝑗 ∈ { 𝑦 } ( { 𝑗 } × 𝐵 ) )
147 nfcv ⊢ Ⅎ 𝑚 ( { 𝑗 } × 𝐵 )
148 nfcv ⊢ Ⅎ 𝑗 { 𝑚 }
149 148 11 nfxp ⊢ Ⅎ 𝑗 ( { 𝑚 } × ⦋ 𝑚 / 𝑗 ⦌ 𝐵 )
150 sneq ⊢ ( 𝑗 = 𝑚 → { 𝑗 } = { 𝑚 } )
151 150 14 xpeq12d ⊢ ( 𝑗 = 𝑚 → ( { 𝑗 } × 𝐵 ) = ( { 𝑚 } × ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ) )
152 147 149 151 cbviun ⊢ ∪ 𝑗 ∈ { 𝑦 } ( { 𝑗 } × 𝐵 ) = ∪ 𝑚 ∈ { 𝑦 } ( { 𝑚 } × ⦋ 𝑚 / 𝑗 ⦌ 𝐵 )
153 sneq ⊢ ( 𝑚 = 𝑦 → { 𝑚 } = { 𝑦 } )
154 153 41 xpeq12d ⊢ ( 𝑚 = 𝑦 → ( { 𝑚 } × ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ) = ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) )
155 20 154 iunxsn ⊢ ∪ 𝑚 ∈ { 𝑦 } ( { 𝑚 } × ⦋ 𝑚 / 𝑗 ⦌ 𝐵 ) = ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 )
156 152 155 eqtri ⊢ ∪ 𝑗 ∈ { 𝑦 } ( { 𝑗 } × 𝐵 ) = ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 )
157 156 uneq2i ⊢ ( ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) ∪ ∪ 𝑗 ∈ { 𝑦 } ( { 𝑗 } × 𝐵 ) ) = ( ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) ∪ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) )
158 146 157 eqtri ⊢ ∪ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) = ( ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) ∪ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) )
159 158 a1i ⊢ ( 𝜑 → ∪ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) = ( ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) ∪ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) ) )
160 snfi ⊢ { 𝑗 } ∈ Fin
161 119 3 syldan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) → 𝐵 ∈ Fin )
162 xpfi ⊢ ( ( { 𝑗 } ∈ Fin ∧ 𝐵 ∈ Fin ) → ( { 𝑗 } × 𝐵 ) ∈ Fin )
163 160 161 162 sylancr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) → ( { 𝑗 } × 𝐵 ) ∈ Fin )
164 163 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) ∈ Fin )
165 iunfi ⊢ ( ( ( 𝑥 ∪ { 𝑦 } ) ∈ Fin ∧ ∀ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) ∈ Fin ) → ∪ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) ∈ Fin )
166 118 164 165 syl2anc ⊢ ( 𝜑 → ∪ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) ∈ Fin )
167 eliun ⊢ ( 𝑧 ∈ ∪ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) ↔ ∃ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) 𝑧 ∈ ( { 𝑗 } × 𝐵 ) )
168 elxp ⊢ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ↔ ∃ 𝑚 ∃ 𝑘 ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑗 } ∧ 𝑘 ∈ 𝐵 ) ) )
169 simprl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) ∧ ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑗 } ∧ 𝑘 ∈ 𝐵 ) ) ) → 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ )
170 simprrl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) ∧ ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑗 } ∧ 𝑘 ∈ 𝐵 ) ) ) → 𝑚 ∈ { 𝑗 } )
171 elsni ⊢ ( 𝑚 ∈ { 𝑗 } → 𝑚 = 𝑗 )
172 170 171 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) ∧ ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑗 } ∧ 𝑘 ∈ 𝐵 ) ) ) → 𝑚 = 𝑗 )
173 172 opeq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) ∧ ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑗 } ∧ 𝑘 ∈ 𝐵 ) ) ) → ⟨ 𝑚 , 𝑘 ⟩ = ⟨ 𝑗 , 𝑘 ⟩ )
174 169 173 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) ∧ ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑗 } ∧ 𝑘 ∈ 𝐵 ) ) ) → 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ )
175 174 1 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) ∧ ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑗 } ∧ 𝑘 ∈ 𝐵 ) ) ) → 𝐷 = 𝐶 )
176 simpll ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) ∧ ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑗 } ∧ 𝑘 ∈ 𝐵 ) ) ) → 𝜑 )
177 119 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) ∧ ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑗 } ∧ 𝑘 ∈ 𝐵 ) ) ) → 𝑗 ∈ 𝐴 )
178 simprrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) ∧ ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑗 } ∧ 𝑘 ∈ 𝐵 ) ) ) → 𝑘 ∈ 𝐵 )
179 176 177 178 4 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) ∧ ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑗 } ∧ 𝑘 ∈ 𝐵 ) ) ) → 𝐶 ∈ ℂ )
180 175 179 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) ∧ ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑗 } ∧ 𝑘 ∈ 𝐵 ) ) ) → 𝐷 ∈ ℂ )
181 180 ex ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) → ( ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑗 } ∧ 𝑘 ∈ 𝐵 ) ) → 𝐷 ∈ ℂ ) )
182 181 exlimdvv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) → ( ∃ 𝑚 ∃ 𝑘 ( 𝑧 = ⟨ 𝑚 , 𝑘 ⟩ ∧ ( 𝑚 ∈ { 𝑗 } ∧ 𝑘 ∈ 𝐵 ) ) → 𝐷 ∈ ℂ ) )
183 168 182 biimtrid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ) → ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) → 𝐷 ∈ ℂ ) )
184 183 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) 𝑧 ∈ ( { 𝑗 } × 𝐵 ) → 𝐷 ∈ ℂ ) )
185 167 184 biimtrid ⊢ ( 𝜑 → ( 𝑧 ∈ ∪ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) → 𝐷 ∈ ℂ ) )
186 185 imp ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) ) → 𝐷 ∈ ℂ )
187 145 159 166 186 fprodsplit ⊢ ( 𝜑 → ∏ 𝑧 ∈ ∪ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) 𝐷 = ( ∏ 𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) 𝐷 · ∏ 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) 𝐷 ) )
188 187 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∏ 𝑧 ∈ ∪ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) 𝐷 = ( ∏ 𝑧 ∈ ∪ 𝑗 ∈ 𝑥 ( { 𝑗 } × 𝐵 ) 𝐷 · ∏ 𝑧 ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑗 ⦌ 𝐵 ) 𝐷 ) )
189 114 124 188 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ∏ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ∏ 𝑘 ∈ 𝐵 𝐶 = ∏ 𝑧 ∈ ∪ 𝑗 ∈ ( 𝑥 ∪ { 𝑦 } ) ( { 𝑗 } × 𝐵 ) 𝐷 )