Metamath Proof Explorer

Theorem esum2dlem

Description: Lemma for esum2d (finite case). (Contributed by Thierry Arnoux, 17-May-2020) (Proof shortened by AV, 17-Sep-2021)

Ref Expression
Hypotheses esum2d.0 ⊢ Ⅎ 𝑘 𝐹
esum2d.1 ⊢ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → 𝐹 = 𝐶 )
esum2d.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
esum2d.3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
esum2d.4 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐶 ∈ ( 0 [,] +∞ ) )
esum2dlem.e ⊢ ( 𝜑 → 𝐴 ∈ Fin )
Assertion esum2dlem ( 𝜑 → Σ* 𝑗 ∈ 𝐴 Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 )

Proof

Step Hyp Ref Expression
1 esum2d.0 ⊢ Ⅎ 𝑘 𝐹
2 esum2d.1 ⊢ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → 𝐹 = 𝐶 )
3 esum2d.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4 esum2d.3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
5 esum2d.4 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐶 ∈ ( 0 [,] +∞ ) )
6 esum2dlem.e ⊢ ( 𝜑 → 𝐴 ∈ Fin )
7 esumeq1 ⊢ ( 𝑎 = ∅ → Σ* 𝑗 ∈ 𝑎 Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑗 ∈ ∅ Σ* 𝑘 ∈ 𝐵 𝐶 )
8 nfv ⊢ Ⅎ 𝑧 𝑎 = ∅
9 iuneq1 ⊢ ( 𝑎 = ∅ → ∪ 𝑗 ∈ 𝑎 ( { 𝑗 } × 𝐵 ) = ∪ 𝑗 ∈ ∅ ( { 𝑗 } × 𝐵 ) )
10 8 9 esumeq1d ⊢ ( 𝑎 = ∅ → Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝑎 ( { 𝑗 } × 𝐵 ) 𝐹 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ ∅ ( { 𝑗 } × 𝐵 ) 𝐹 )
11 7 10 eqeq12d ⊢ ( 𝑎 = ∅ → ( Σ* 𝑗 ∈ 𝑎 Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝑎 ( { 𝑗 } × 𝐵 ) 𝐹 ↔ Σ* 𝑗 ∈ ∅ Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ ∅ ( { 𝑗 } × 𝐵 ) 𝐹 ) )
12 esumeq1 ⊢ ( 𝑎 = 𝑏 → Σ* 𝑗 ∈ 𝑎 Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑗 ∈ 𝑏 Σ* 𝑘 ∈ 𝐵 𝐶 )
13 nfv ⊢ Ⅎ 𝑧 𝑎 = 𝑏
14 iuneq1 ⊢ ( 𝑎 = 𝑏 → ∪ 𝑗 ∈ 𝑎 ( { 𝑗 } × 𝐵 ) = ∪ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) )
15 13 14 esumeq1d ⊢ ( 𝑎 = 𝑏 → Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝑎 ( { 𝑗 } × 𝐵 ) 𝐹 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) 𝐹 )
16 12 15 eqeq12d ⊢ ( 𝑎 = 𝑏 → ( Σ* 𝑗 ∈ 𝑎 Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝑎 ( { 𝑗 } × 𝐵 ) 𝐹 ↔ Σ* 𝑗 ∈ 𝑏 Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) 𝐹 ) )
17 esumeq1 ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑙 } ) → Σ* 𝑗 ∈ 𝑎 Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑗 ∈ ( 𝑏 ∪ { 𝑙 } ) Σ* 𝑘 ∈ 𝐵 𝐶 )
18 nfv ⊢ Ⅎ 𝑧 𝑎 = ( 𝑏 ∪ { 𝑙 } )
19 iuneq1 ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑙 } ) → ∪ 𝑗 ∈ 𝑎 ( { 𝑗 } × 𝐵 ) = ∪ 𝑗 ∈ ( 𝑏 ∪ { 𝑙 } ) ( { 𝑗 } × 𝐵 ) )
20 18 19 esumeq1d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑙 } ) → Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝑎 ( { 𝑗 } × 𝐵 ) 𝐹 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ ( 𝑏 ∪ { 𝑙 } ) ( { 𝑗 } × 𝐵 ) 𝐹 )
21 17 20 eqeq12d ⊢ ( 𝑎 = ( 𝑏 ∪ { 𝑙 } ) → ( Σ* 𝑗 ∈ 𝑎 Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝑎 ( { 𝑗 } × 𝐵 ) 𝐹 ↔ Σ* 𝑗 ∈ ( 𝑏 ∪ { 𝑙 } ) Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ ( 𝑏 ∪ { 𝑙 } ) ( { 𝑗 } × 𝐵 ) 𝐹 ) )
22 esumeq1 ⊢ ( 𝑎 = 𝐴 → Σ* 𝑗 ∈ 𝑎 Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑗 ∈ 𝐴 Σ* 𝑘 ∈ 𝐵 𝐶 )
23 nfv ⊢ Ⅎ 𝑧 𝑎 = 𝐴
24 iuneq1 ⊢ ( 𝑎 = 𝐴 → ∪ 𝑗 ∈ 𝑎 ( { 𝑗 } × 𝐵 ) = ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
25 23 24 esumeq1d ⊢ ( 𝑎 = 𝐴 → Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝑎 ( { 𝑗 } × 𝐵 ) 𝐹 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 )
26 22 25 eqeq12d ⊢ ( 𝑎 = 𝐴 → ( Σ* 𝑗 ∈ 𝑎 Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝑎 ( { 𝑗 } × 𝐵 ) 𝐹 ↔ Σ* 𝑗 ∈ 𝐴 Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ) )
27 esumnul ⊢ Σ* 𝑧 ∈ ∅ 𝐹 = 0
28 0iun ⊢ ∪ 𝑗 ∈ ∅ ( { 𝑗 } × 𝐵 ) = ∅
29 esumeq1 ⊢ ( ∪ 𝑗 ∈ ∅ ( { 𝑗 } × 𝐵 ) = ∅ → Σ* 𝑧 ∈ ∪ 𝑗 ∈ ∅ ( { 𝑗 } × 𝐵 ) 𝐹 = Σ* 𝑧 ∈ ∅ 𝐹 )
30 28 29 ax-mp ⊢ Σ* 𝑧 ∈ ∪ 𝑗 ∈ ∅ ( { 𝑗 } × 𝐵 ) 𝐹 = Σ* 𝑧 ∈ ∅ 𝐹
31 esumnul ⊢ Σ* 𝑗 ∈ ∅ Σ* 𝑘 ∈ 𝐵 𝐶 = 0
32 27 30 31 3eqtr4ri ⊢ Σ* 𝑗 ∈ ∅ Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ ∅ ( { 𝑗 } × 𝐵 ) 𝐹
33 32 a1i ⊢ ( 𝜑 → Σ* 𝑗 ∈ ∅ Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ ∅ ( { 𝑗 } × 𝐵 ) 𝐹 )
34 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ Σ* 𝑗 ∈ 𝑏 Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) 𝐹 ) → Σ* 𝑗 ∈ 𝑏 Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) 𝐹 )
35 nfcsb1v ⊢ Ⅎ 𝑗 ⦋ 𝑙 / 𝑗 ⦌ 𝐵
36 nfcsb1v ⊢ Ⅎ 𝑗 ⦋ 𝑙 / 𝑗 ⦌ 𝐶
37 35 36 nfesum2 ⊢ Ⅎ 𝑗 Σ* 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ⦋ 𝑙 / 𝑗 ⦌ 𝐶
38 csbeq1a ⊢ ( 𝑗 = 𝑙 → 𝐵 = ⦋ 𝑙 / 𝑗 ⦌ 𝐵 )
39 csbeq1a ⊢ ( 𝑗 = 𝑙 → 𝐶 = ⦋ 𝑙 / 𝑗 ⦌ 𝐶 )
40 38 39 esumeq12d ⊢ ( 𝑗 = 𝑙 → Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ⦋ 𝑙 / 𝑗 ⦌ 𝐶 )
41 40 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑗 = 𝑙 ) → Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ⦋ 𝑙 / 𝑗 ⦌ 𝐶 )
42 simprr ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) )
43 42 eldifad ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → 𝑙 ∈ 𝐴 )
44 4 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
45 44 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ∀ 𝑗 ∈ 𝐴 𝐵 ∈ 𝑊 )
46 rspcsbela ⊢ ( ( 𝑙 ∈ 𝐴 ∧ ∀ 𝑗 ∈ 𝐴 𝐵 ∈ 𝑊 ) → ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ∈ 𝑊 )
47 43 45 46 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ∈ 𝑊 )
48 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) → 𝜑 )
49 43 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) → 𝑙 ∈ 𝐴 )
50 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) → 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 )
51 5 ex ⊢ ( 𝜑 → ( ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) ) )
52 51 sbcimdv ⊢ ( 𝜑 → ( [ 𝑙 / 𝑗 ] ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) → [ 𝑙 / 𝑗 ] 𝐶 ∈ ( 0 [,] +∞ ) ) )
53 sbcan ⊢ ( [ 𝑙 / 𝑗 ] ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ↔ ( [ 𝑙 / 𝑗 ] 𝑗 ∈ 𝐴 ∧ [ 𝑙 / 𝑗 ] 𝑘 ∈ 𝐵 ) )
54 sbcel1v ⊢ ( [ 𝑙 / 𝑗 ] 𝑗 ∈ 𝐴 ↔ 𝑙 ∈ 𝐴 )
55 sbcel2 ⊢ ( [ 𝑙 / 𝑗 ] 𝑘 ∈ 𝐵 ↔ 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 )
56 54 55 anbi12i ⊢ ( ( [ 𝑙 / 𝑗 ] 𝑗 ∈ 𝐴 ∧ [ 𝑙 / 𝑗 ] 𝑘 ∈ 𝐵 ) ↔ ( 𝑙 ∈ 𝐴 ∧ 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) )
57 53 56 bitri ⊢ ( [ 𝑙 / 𝑗 ] ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ↔ ( 𝑙 ∈ 𝐴 ∧ 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) )
58 vex ⊢ 𝑙 ∈ V
59 sbcel1g ⊢ ( 𝑙 ∈ V → ( [ 𝑙 / 𝑗 ] 𝐶 ∈ ( 0 [,] +∞ ) ↔ ⦋ 𝑙 / 𝑗 ⦌ 𝐶 ∈ ( 0 [,] +∞ ) ) )
60 58 59 ax-mp ⊢ ( [ 𝑙 / 𝑗 ] 𝐶 ∈ ( 0 [,] +∞ ) ↔ ⦋ 𝑙 / 𝑗 ⦌ 𝐶 ∈ ( 0 [,] +∞ ) )
61 52 57 60 3imtr3g ⊢ ( 𝜑 → ( ( 𝑙 ∈ 𝐴 ∧ 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) → ⦋ 𝑙 / 𝑗 ⦌ 𝐶 ∈ ( 0 [,] +∞ ) ) )
62 61 imp ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐴 ∧ 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) ) → ⦋ 𝑙 / 𝑗 ⦌ 𝐶 ∈ ( 0 [,] +∞ ) )
63 48 49 50 62 syl12anc ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) → ⦋ 𝑙 / 𝑗 ⦌ 𝐶 ∈ ( 0 [,] +∞ ) )
64 63 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ∀ 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ⦋ 𝑙 / 𝑗 ⦌ 𝐶 ∈ ( 0 [,] +∞ ) )
65 nfcv ⊢ Ⅎ 𝑘 ⦋ 𝑙 / 𝑗 ⦌ 𝐵
66 65 esumcl ⊢ ( ( ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ∈ 𝑊 ∧ ∀ 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ⦋ 𝑙 / 𝑗 ⦌ 𝐶 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ⦋ 𝑙 / 𝑗 ⦌ 𝐶 ∈ ( 0 [,] +∞ ) )
67 47 64 66 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → Σ* 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ⦋ 𝑙 / 𝑗 ⦌ 𝐶 ∈ ( 0 [,] +∞ ) )
68 37 41 42 67 esumsnf ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → Σ* 𝑗 ∈ { 𝑙 } Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ⦋ 𝑙 / 𝑗 ⦌ 𝐶 )
69 nfv ⊢ Ⅎ 𝑘 ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) )
70 nfv ⊢ Ⅎ 𝑗 𝑧 = ⟨ 𝑙 , 𝑘 ⟩
71 36 nfeq2 ⊢ Ⅎ 𝑗 𝐹 = ⦋ 𝑙 / 𝑗 ⦌ 𝐶
72 70 71 nfim ⊢ Ⅎ 𝑗 ( 𝑧 = ⟨ 𝑙 , 𝑘 ⟩ → 𝐹 = ⦋ 𝑙 / 𝑗 ⦌ 𝐶 )
73 opeq1 ⊢ ( 𝑗 = 𝑙 → ⟨ 𝑗 , 𝑘 ⟩ = ⟨ 𝑙 , 𝑘 ⟩ )
74 73 eqeq2d ⊢ ( 𝑗 = 𝑙 → ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ↔ 𝑧 = ⟨ 𝑙 , 𝑘 ⟩ ) )
75 39 eqeq2d ⊢ ( 𝑗 = 𝑙 → ( 𝐹 = 𝐶 ↔ 𝐹 = ⦋ 𝑙 / 𝑗 ⦌ 𝐶 ) )
76 74 75 imbi12d ⊢ ( 𝑗 = 𝑙 → ( ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → 𝐹 = 𝐶 ) ↔ ( 𝑧 = ⟨ 𝑙 , 𝑘 ⟩ → 𝐹 = ⦋ 𝑙 / 𝑗 ⦌ 𝐶 ) ) )
77 72 76 2 chvarfv ⊢ ( 𝑧 = ⟨ 𝑙 , 𝑘 ⟩ → 𝐹 = ⦋ 𝑙 / 𝑗 ⦌ 𝐶 )
78 vsnid ⊢ 𝑗 ∈ { 𝑗 }
79 78 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → 𝑗 ∈ { 𝑗 } )
80 simpr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → 𝑘 ∈ 𝐵 )
81 79 80 opelxpd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → ⟨ 𝑗 , 𝑘 ⟩ ∈ ( { 𝑗 } × 𝐵 ) )
82 xp2nd ⊢ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) → ( 2nd ‘ 𝑧 ) ∈ 𝐵 )
83 xp1st ⊢ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) → ( 1st ‘ 𝑧 ) ∈ { 𝑗 } )
84 fvex ⊢ ( 1st ‘ 𝑧 ) ∈ V
85 84 elsn ⊢ ( ( 1st ‘ 𝑧 ) ∈ { 𝑗 } ↔ ( 1st ‘ 𝑧 ) = 𝑗 )
86 83 85 sylib ⊢ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) → ( 1st ‘ 𝑧 ) = 𝑗 )
87 eqop ⊢ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) → ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ↔ ( ( 1st ‘ 𝑧 ) = 𝑗 ∧ ( 2nd ‘ 𝑧 ) = 𝑘 ) ) )
88 86 87 mpbirand ⊢ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) → ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ↔ ( 2nd ‘ 𝑧 ) = 𝑘 ) )
89 eqcom ⊢ ( ( 2nd ‘ 𝑧 ) = 𝑘 ↔ 𝑘 = ( 2nd ‘ 𝑧 ) )
90 88 89 bitrdi ⊢ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) → ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ↔ 𝑘 = ( 2nd ‘ 𝑧 ) ) )
91 90 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) ∧ 𝑘 ∈ 𝐵 ) → ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ↔ 𝑘 = ( 2nd ‘ 𝑧 ) ) )
92 91 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → ∀ 𝑘 ∈ 𝐵 ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ↔ 𝑘 = ( 2nd ‘ 𝑧 ) ) )
93 reu6i ⊢ ( ( ( 2nd ‘ 𝑧 ) ∈ 𝐵 ∧ ∀ 𝑘 ∈ 𝐵 ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ↔ 𝑘 = ( 2nd ‘ 𝑧 ) ) ) → ∃! 𝑘 ∈ 𝐵 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ )
94 82 92 93 syl2an2 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → ∃! 𝑘 ∈ 𝐵 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ )
95 81 94 f1mptrn ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → Fun ◡ ( 𝑘 ∈ 𝐵 ↦ ⟨ 𝑗 , 𝑘 ⟩ ) )
96 95 ex ⊢ ( 𝜑 → ( 𝑗 ∈ 𝐴 → Fun ◡ ( 𝑘 ∈ 𝐵 ↦ ⟨ 𝑗 , 𝑘 ⟩ ) ) )
97 96 sbcimdv ⊢ ( 𝜑 → ( [ 𝑙 / 𝑗 ] 𝑗 ∈ 𝐴 → [ 𝑙 / 𝑗 ] Fun ◡ ( 𝑘 ∈ 𝐵 ↦ ⟨ 𝑗 , 𝑘 ⟩ ) ) )
98 sbcfung ⊢ ( 𝑙 ∈ V → ( [ 𝑙 / 𝑗 ] Fun ◡ ( 𝑘 ∈ 𝐵 ↦ ⟨ 𝑗 , 𝑘 ⟩ ) ↔ Fun ⦋ 𝑙 / 𝑗 ⦌ ◡ ( 𝑘 ∈ 𝐵 ↦ ⟨ 𝑗 , 𝑘 ⟩ ) ) )
99 csbcnv ⊢ ◡ ⦋ 𝑙 / 𝑗 ⦌ ( 𝑘 ∈ 𝐵 ↦ ⟨ 𝑗 , 𝑘 ⟩ ) = ⦋ 𝑙 / 𝑗 ⦌ ◡ ( 𝑘 ∈ 𝐵 ↦ ⟨ 𝑗 , 𝑘 ⟩ )
100 csbmpt12 ⊢ ( 𝑙 ∈ V → ⦋ 𝑙 / 𝑗 ⦌ ( 𝑘 ∈ 𝐵 ↦ ⟨ 𝑗 , 𝑘 ⟩ ) = ( 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ↦ ⦋ 𝑙 / 𝑗 ⦌ ⟨ 𝑗 , 𝑘 ⟩ ) )
101 csbopg ⊢ ( 𝑙 ∈ V → ⦋ 𝑙 / 𝑗 ⦌ ⟨ 𝑗 , 𝑘 ⟩ = ⟨ ⦋ 𝑙 / 𝑗 ⦌ 𝑗 , ⦋ 𝑙 / 𝑗 ⦌ 𝑘 ⟩ )
102 csbvarg ⊢ ( 𝑙 ∈ V → ⦋ 𝑙 / 𝑗 ⦌ 𝑗 = 𝑙 )
103 csbconstg ⊢ ( 𝑙 ∈ V → ⦋ 𝑙 / 𝑗 ⦌ 𝑘 = 𝑘 )
104 102 103 opeq12d ⊢ ( 𝑙 ∈ V → ⟨ ⦋ 𝑙 / 𝑗 ⦌ 𝑗 , ⦋ 𝑙 / 𝑗 ⦌ 𝑘 ⟩ = ⟨ 𝑙 , 𝑘 ⟩ )
105 101 104 eqtrd ⊢ ( 𝑙 ∈ V → ⦋ 𝑙 / 𝑗 ⦌ ⟨ 𝑗 , 𝑘 ⟩ = ⟨ 𝑙 , 𝑘 ⟩ )
106 105 mpteq2dv ⊢ ( 𝑙 ∈ V → ( 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ↦ ⦋ 𝑙 / 𝑗 ⦌ ⟨ 𝑗 , 𝑘 ⟩ ) = ( 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ↦ ⟨ 𝑙 , 𝑘 ⟩ ) )
107 100 106 eqtrd ⊢ ( 𝑙 ∈ V → ⦋ 𝑙 / 𝑗 ⦌ ( 𝑘 ∈ 𝐵 ↦ ⟨ 𝑗 , 𝑘 ⟩ ) = ( 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ↦ ⟨ 𝑙 , 𝑘 ⟩ ) )
108 107 cnveqd ⊢ ( 𝑙 ∈ V → ◡ ⦋ 𝑙 / 𝑗 ⦌ ( 𝑘 ∈ 𝐵 ↦ ⟨ 𝑗 , 𝑘 ⟩ ) = ◡ ( 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ↦ ⟨ 𝑙 , 𝑘 ⟩ ) )
109 99 108 syl5eqr ⊢ ( 𝑙 ∈ V → ⦋ 𝑙 / 𝑗 ⦌ ◡ ( 𝑘 ∈ 𝐵 ↦ ⟨ 𝑗 , 𝑘 ⟩ ) = ◡ ( 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ↦ ⟨ 𝑙 , 𝑘 ⟩ ) )
110 109 funeqd ⊢ ( 𝑙 ∈ V → ( Fun ⦋ 𝑙 / 𝑗 ⦌ ◡ ( 𝑘 ∈ 𝐵 ↦ ⟨ 𝑗 , 𝑘 ⟩ ) ↔ Fun ◡ ( 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ↦ ⟨ 𝑙 , 𝑘 ⟩ ) ) )
111 98 110 bitrd ⊢ ( 𝑙 ∈ V → ( [ 𝑙 / 𝑗 ] Fun ◡ ( 𝑘 ∈ 𝐵 ↦ ⟨ 𝑗 , 𝑘 ⟩ ) ↔ Fun ◡ ( 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ↦ ⟨ 𝑙 , 𝑘 ⟩ ) ) )
112 58 111 ax-mp ⊢ ( [ 𝑙 / 𝑗 ] Fun ◡ ( 𝑘 ∈ 𝐵 ↦ ⟨ 𝑗 , 𝑘 ⟩ ) ↔ Fun ◡ ( 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ↦ ⟨ 𝑙 , 𝑘 ⟩ ) )
113 97 54 112 3imtr3g ⊢ ( 𝜑 → ( 𝑙 ∈ 𝐴 → Fun ◡ ( 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ↦ ⟨ 𝑙 , 𝑘 ⟩ ) ) )
114 113 imp ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝐴 ) → Fun ◡ ( 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ↦ ⟨ 𝑙 , 𝑘 ⟩ ) )
115 43 114 syldan ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → Fun ◡ ( 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ↦ ⟨ 𝑙 , 𝑘 ⟩ ) )
116 vsnid ⊢ 𝑙 ∈ { 𝑙 }
117 116 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) → 𝑙 ∈ { 𝑙 } )
118 117 50 opelxpd ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) → ⟨ 𝑙 , 𝑘 ⟩ ∈ ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) )
119 1 69 65 77 47 115 63 118 esumc ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → Σ* 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ⦋ 𝑙 / 𝑗 ⦌ 𝐶 = Σ* 𝑧 ∈ { 𝑡 ∣ ∃ 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 𝑡 = ⟨ 𝑙 , 𝑘 ⟩ } 𝐹 )
120 nfab1 ⊢ Ⅎ 𝑡 { 𝑡 ∣ ∃ 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 𝑡 = ⟨ 𝑙 , 𝑘 ⟩ }
121 nfcv ⊢ Ⅎ 𝑡 ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 )
122 opeq1 ⊢ ( 𝑖 = 𝑙 → ⟨ 𝑖 , 𝑘 ⟩ = ⟨ 𝑙 , 𝑘 ⟩ )
123 122 eqeq2d ⊢ ( 𝑖 = 𝑙 → ( 𝑡 = ⟨ 𝑖 , 𝑘 ⟩ ↔ 𝑡 = ⟨ 𝑙 , 𝑘 ⟩ ) )
124 123 rexbidv ⊢ ( 𝑖 = 𝑙 → ( ∃ 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 𝑡 = ⟨ 𝑖 , 𝑘 ⟩ ↔ ∃ 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 𝑡 = ⟨ 𝑙 , 𝑘 ⟩ ) )
125 58 124 rexsn ⊢ ( ∃ 𝑖 ∈ { 𝑙 } ∃ 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 𝑡 = ⟨ 𝑖 , 𝑘 ⟩ ↔ ∃ 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 𝑡 = ⟨ 𝑙 , 𝑘 ⟩ )
126 elxp2 ⊢ ( 𝑡 ∈ ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) ↔ ∃ 𝑖 ∈ { 𝑙 } ∃ 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 𝑡 = ⟨ 𝑖 , 𝑘 ⟩ )
127 abid ⊢ ( 𝑡 ∈ { 𝑡 ∣ ∃ 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 𝑡 = ⟨ 𝑙 , 𝑘 ⟩ } ↔ ∃ 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 𝑡 = ⟨ 𝑙 , 𝑘 ⟩ )
128 125 126 127 3bitr4ri ⊢ ( 𝑡 ∈ { 𝑡 ∣ ∃ 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 𝑡 = ⟨ 𝑙 , 𝑘 ⟩ } ↔ 𝑡 ∈ ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) )
129 120 121 128 eqri ⊢ { 𝑡 ∣ ∃ 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 𝑡 = ⟨ 𝑙 , 𝑘 ⟩ } = ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 )
130 esumeq1 ⊢ ( { 𝑡 ∣ ∃ 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 𝑡 = ⟨ 𝑙 , 𝑘 ⟩ } = ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) → Σ* 𝑧 ∈ { 𝑡 ∣ ∃ 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 𝑡 = ⟨ 𝑙 , 𝑘 ⟩ } 𝐹 = Σ* 𝑧 ∈ ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) 𝐹 )
131 129 130 ax-mp ⊢ Σ* 𝑧 ∈ { 𝑡 ∣ ∃ 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 𝑡 = ⟨ 𝑙 , 𝑘 ⟩ } 𝐹 = Σ* 𝑧 ∈ ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) 𝐹
132 119 131 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → Σ* 𝑘 ∈ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ⦋ 𝑙 / 𝑗 ⦌ 𝐶 = Σ* 𝑧 ∈ ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) 𝐹 )
133 68 132 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → Σ* 𝑗 ∈ { 𝑙 } Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑧 ∈ ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) 𝐹 )
134 133 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ Σ* 𝑗 ∈ 𝑏 Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) 𝐹 ) → Σ* 𝑗 ∈ { 𝑙 } Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑧 ∈ ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) 𝐹 )
135 34 134 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ Σ* 𝑗 ∈ 𝑏 Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) 𝐹 ) → ( Σ* 𝑗 ∈ 𝑏 Σ* 𝑘 ∈ 𝐵 𝐶 +𝑒 Σ* 𝑗 ∈ { 𝑙 } Σ* 𝑘 ∈ 𝐵 𝐶 ) = ( Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) 𝐹 +𝑒 Σ* 𝑧 ∈ ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) 𝐹 ) )
136 nfv ⊢ Ⅎ 𝑗 ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) )
137 nfcv ⊢ Ⅎ 𝑗 𝑏
138 nfcv ⊢ Ⅎ 𝑗 { 𝑙 }
139 vex ⊢ 𝑏 ∈ V
140 139 a1i ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → 𝑏 ∈ V )
141 snex ⊢ { 𝑙 } ∈ V
142 141 a1i ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → { 𝑙 } ∈ V )
143 42 eldifbd ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ¬ 𝑙 ∈ 𝑏 )
144 disjsn ⊢ ( ( 𝑏 ∩ { 𝑙 } ) = ∅ ↔ ¬ 𝑙 ∈ 𝑏 )
145 143 144 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( 𝑏 ∩ { 𝑙 } ) = ∅ )
146 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑗 ∈ 𝑏 ) → 𝜑 )
147 simprl ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → 𝑏 ⊆ 𝐴 )
148 147 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑗 ∈ 𝑏 ) → 𝑗 ∈ 𝐴 )
149 5 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
150 149 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ( 0 [,] +∞ ) )
151 nfcv ⊢ Ⅎ 𝑘 𝐵
152 151 esumcl ⊢ ( ( 𝐵 ∈ 𝑊 ∧ ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ 𝐵 𝐶 ∈ ( 0 [,] +∞ ) )
153 4 150 152 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → Σ* 𝑘 ∈ 𝐵 𝐶 ∈ ( 0 [,] +∞ ) )
154 146 148 153 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑗 ∈ 𝑏 ) → Σ* 𝑘 ∈ 𝐵 𝐶 ∈ ( 0 [,] +∞ ) )
155 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑗 ∈ { 𝑙 } ) → 𝜑 )
156 43 snssd ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → { 𝑙 } ⊆ 𝐴 )
157 156 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑗 ∈ { 𝑙 } ) → 𝑗 ∈ 𝐴 )
158 155 157 153 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑗 ∈ { 𝑙 } ) → Σ* 𝑘 ∈ 𝐵 𝐶 ∈ ( 0 [,] +∞ ) )
159 136 137 138 140 142 145 154 158 esumsplit ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → Σ* 𝑗 ∈ ( 𝑏 ∪ { 𝑙 } ) Σ* 𝑘 ∈ 𝐵 𝐶 = ( Σ* 𝑗 ∈ 𝑏 Σ* 𝑘 ∈ 𝐵 𝐶 +𝑒 Σ* 𝑗 ∈ { 𝑙 } Σ* 𝑘 ∈ 𝐵 𝐶 ) )
160 159 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ Σ* 𝑗 ∈ 𝑏 Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) 𝐹 ) → Σ* 𝑗 ∈ ( 𝑏 ∪ { 𝑙 } ) Σ* 𝑘 ∈ 𝐵 𝐶 = ( Σ* 𝑗 ∈ 𝑏 Σ* 𝑘 ∈ 𝐵 𝐶 +𝑒 Σ* 𝑗 ∈ { 𝑙 } Σ* 𝑘 ∈ 𝐵 𝐶 ) )
161 iunxun ⊢ ∪ 𝑗 ∈ ( 𝑏 ∪ { 𝑙 } ) ( { 𝑗 } × 𝐵 ) = ( ∪ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) ∪ ∪ 𝑗 ∈ { 𝑙 } ( { 𝑗 } × 𝐵 ) )
162 138 35 nfxp ⊢ Ⅎ 𝑗 ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 )
163 sneq ⊢ ( 𝑗 = 𝑙 → { 𝑗 } = { 𝑙 } )
164 163 38 xpeq12d ⊢ ( 𝑗 = 𝑙 → ( { 𝑗 } × 𝐵 ) = ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) )
165 162 164 iunxsngf ⊢ ( 𝑙 ∈ V → ∪ 𝑗 ∈ { 𝑙 } ( { 𝑗 } × 𝐵 ) = ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) )
166 58 165 ax-mp ⊢ ∪ 𝑗 ∈ { 𝑙 } ( { 𝑗 } × 𝐵 ) = ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 )
167 166 uneq2i ⊢ ( ∪ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) ∪ ∪ 𝑗 ∈ { 𝑙 } ( { 𝑗 } × 𝐵 ) ) = ( ∪ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) ∪ ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) )
168 161 167 eqtri ⊢ ∪ 𝑗 ∈ ( 𝑏 ∪ { 𝑙 } ) ( { 𝑗 } × 𝐵 ) = ( ∪ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) ∪ ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) )
169 esumeq1 ⊢ ( ∪ 𝑗 ∈ ( 𝑏 ∪ { 𝑙 } ) ( { 𝑗 } × 𝐵 ) = ( ∪ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) ∪ ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) ) → Σ* 𝑧 ∈ ∪ 𝑗 ∈ ( 𝑏 ∪ { 𝑙 } ) ( { 𝑗 } × 𝐵 ) 𝐹 = Σ* 𝑧 ∈ ( ∪ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) ∪ ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) ) 𝐹 )
170 168 169 ax-mp ⊢ Σ* 𝑧 ∈ ∪ 𝑗 ∈ ( 𝑏 ∪ { 𝑙 } ) ( { 𝑗 } × 𝐵 ) 𝐹 = Σ* 𝑧 ∈ ( ∪ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) ∪ ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) ) 𝐹
171 nfv ⊢ Ⅎ 𝑧 ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) )
172 nfcv ⊢ Ⅎ 𝑧 ∪ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 )
173 nfcv ⊢ Ⅎ 𝑧 ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 )
174 snex ⊢ { 𝑗 } ∈ V
175 148 44 syldan ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑗 ∈ 𝑏 ) → 𝐵 ∈ 𝑊 )
176 xpexg ⊢ ( ( { 𝑗 } ∈ V ∧ 𝐵 ∈ 𝑊 ) → ( { 𝑗 } × 𝐵 ) ∈ V )
177 174 175 176 sylancr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑗 ∈ 𝑏 ) → ( { 𝑗 } × 𝐵 ) ∈ V )
178 177 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ∀ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) ∈ V )
179 iunexg ⊢ ( ( 𝑏 ∈ V ∧ ∀ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) ∈ V ) → ∪ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) ∈ V )
180 139 178 179 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ∪ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) ∈ V )
181 xpexg ⊢ ( ( { 𝑙 } ∈ V ∧ ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ∈ 𝑊 ) → ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) ∈ V )
182 141 47 181 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) ∈ V )
183 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑗 ∈ 𝑏 ) → 𝑗 ∈ 𝑏 )
184 143 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑗 ∈ 𝑏 ) → ¬ 𝑙 ∈ 𝑏 )
185 nelne2 ⊢ ( ( 𝑗 ∈ 𝑏 ∧ ¬ 𝑙 ∈ 𝑏 ) → 𝑗 ≠ 𝑙 )
186 183 184 185 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑗 ∈ 𝑏 ) → 𝑗 ≠ 𝑙 )
187 disjsn2 ⊢ ( 𝑗 ≠ 𝑙 → ( { 𝑗 } ∩ { 𝑙 } ) = ∅ )
188 xpdisj1 ⊢ ( ( { 𝑗 } ∩ { 𝑙 } ) = ∅ → ( ( { 𝑗 } × 𝐵 ) ∩ ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) ) = ∅ )
189 186 187 188 3syl ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑗 ∈ 𝑏 ) → ( ( { 𝑗 } × 𝐵 ) ∩ ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) ) = ∅ )
190 189 iuneq2dv ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ∪ 𝑗 ∈ 𝑏 ( ( { 𝑗 } × 𝐵 ) ∩ ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) ) = ∪ 𝑗 ∈ 𝑏 ∅ )
191 162 iunin1f ⊢ ∪ 𝑗 ∈ 𝑏 ( ( { 𝑗 } × 𝐵 ) ∩ ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) ) = ( ∪ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) ∩ ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) )
192 iun0 ⊢ ∪ 𝑗 ∈ 𝑏 ∅ = ∅
193 190 191 192 3eqtr3g ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( ∪ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) ∩ ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) ) = ∅ )
194 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) ) → 𝜑 )
195 iunss1 ⊢ ( 𝑏 ⊆ 𝐴 → ∪ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
196 147 195 syl ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ∪ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
197 196 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) ) → 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
198 nfv ⊢ Ⅎ 𝑗 𝜑
199 nfiu1 ⊢ Ⅎ 𝑗 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 )
200 199 nfcri ⊢ Ⅎ 𝑗 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 )
201 198 200 nfan ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
202 nfv ⊢ Ⅎ 𝑘 ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) )
203 nfcv ⊢ Ⅎ 𝑘 ( 0 [,] +∞ )
204 1 203 nfel ⊢ Ⅎ 𝑘 𝐹 ∈ ( 0 [,] +∞ )
205 2 adantl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ) → 𝐹 = 𝐶 )
206 simp-5l ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ) → 𝜑 )
207 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ) → 𝑗 ∈ 𝐴 )
208 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ) → 𝑘 ∈ 𝐵 )
209 206 207 208 5 syl12anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ) → 𝐶 ∈ ( 0 [,] +∞ ) )
210 205 209 eqeltrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ) → 𝐹 ∈ ( 0 [,] +∞ ) )
211 elsnxp ⊢ ( 𝑗 ∈ 𝐴 → ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ↔ ∃ 𝑘 ∈ 𝐵 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ) )
212 211 biimpa ⊢ ( ( 𝑗 ∈ 𝐴 ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → ∃ 𝑘 ∈ 𝐵 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ )
213 212 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → ∃ 𝑘 ∈ 𝐵 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ )
214 202 204 210 213 r19.29af2 ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → 𝐹 ∈ ( 0 [,] +∞ ) )
215 simpr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) → 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
216 eliun ⊢ ( 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ↔ ∃ 𝑗 ∈ 𝐴 𝑧 ∈ ( { 𝑗 } × 𝐵 ) )
217 215 216 sylib ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) → ∃ 𝑗 ∈ 𝐴 𝑧 ∈ ( { 𝑗 } × 𝐵 ) )
218 201 214 217 r19.29af ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) → 𝐹 ∈ ( 0 [,] +∞ ) )
219 194 197 218 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) ) → 𝐹 ∈ ( 0 [,] +∞ ) )
220 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑧 ∈ ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) ) → 𝜑 )
221 nfcv ⊢ Ⅎ 𝑗 𝐴
222 nfcv ⊢ Ⅎ 𝑗 𝑙
223 221 222 162 164 ssiun2sf ⊢ ( 𝑙 ∈ 𝐴 → ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
224 43 223 syl ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
225 224 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑧 ∈ ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) ) → 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
226 220 225 218 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ 𝑧 ∈ ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) ) → 𝐹 ∈ ( 0 [,] +∞ ) )
227 171 172 173 180 182 193 219 226 esumsplit ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → Σ* 𝑧 ∈ ( ∪ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) ∪ ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) ) 𝐹 = ( Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) 𝐹 +𝑒 Σ* 𝑧 ∈ ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) 𝐹 ) )
228 170 227 syl5eq ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → Σ* 𝑧 ∈ ∪ 𝑗 ∈ ( 𝑏 ∪ { 𝑙 } ) ( { 𝑗 } × 𝐵 ) 𝐹 = ( Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) 𝐹 +𝑒 Σ* 𝑧 ∈ ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) 𝐹 ) )
229 228 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ Σ* 𝑗 ∈ 𝑏 Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) 𝐹 ) → Σ* 𝑧 ∈ ∪ 𝑗 ∈ ( 𝑏 ∪ { 𝑙 } ) ( { 𝑗 } × 𝐵 ) 𝐹 = ( Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) 𝐹 +𝑒 Σ* 𝑧 ∈ ( { 𝑙 } × ⦋ 𝑙 / 𝑗 ⦌ 𝐵 ) 𝐹 ) )
230 135 160 229 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) ∧ Σ* 𝑗 ∈ 𝑏 Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) 𝐹 ) → Σ* 𝑗 ∈ ( 𝑏 ∪ { 𝑙 } ) Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ ( 𝑏 ∪ { 𝑙 } ) ( { 𝑗 } × 𝐵 ) 𝐹 )
231 230 ex ⊢ ( ( 𝜑 ∧ ( 𝑏 ⊆ 𝐴 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑏 ) ) ) → ( Σ* 𝑗 ∈ 𝑏 Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝑏 ( { 𝑗 } × 𝐵 ) 𝐹 → Σ* 𝑗 ∈ ( 𝑏 ∪ { 𝑙 } ) Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ ( 𝑏 ∪ { 𝑙 } ) ( { 𝑗 } × 𝐵 ) 𝐹 ) )
232 11 16 21 26 33 231 6 findcard2d ⊢ ( 𝜑 → Σ* 𝑗 ∈ 𝐴 Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 )