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