Metamath Proof Explorer

Theorem esumiun

Description: Sum over a nonnecessarily disjoint indexed union. The inequality is strict in the case where the sets B(x) overlap. (Contributed by Thierry Arnoux, 21-Sep-2019)

Ref Expression
Hypotheses esumiun.0 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
esumiun.1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
esumiun.2 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
Assertion esumiun ( 𝜑 → Σ* 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝐶 ≤ Σ* 𝑗 ∈ 𝐴 Σ* 𝑘 ∈ 𝐵 𝐶 )

Proof

Step Hyp Ref Expression
1 esumiun.0 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 esumiun.1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
3 esumiun.2 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
4 1 2 aciunf1 ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) )
5 f1f1orn ⊢ ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) → 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 )
6 5 anim1i ⊢ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) → ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) )
7 f1f ⊢ ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) → 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
8 7 frnd ⊢ ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) → ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
9 8 adantr ⊢ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) → ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
10 6 9 jca ⊢ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) → ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) )
11 10 eximi ⊢ ( ∃ 𝑓 ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) → ∃ 𝑓 ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) )
12 4 11 syl ⊢ ( 𝜑 → ∃ 𝑓 ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) )
13 nfv ⊢ Ⅎ 𝑧 ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) )
14 nfcv ⊢ Ⅎ 𝑧 𝐶
15 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶
16 nfcv ⊢ Ⅎ 𝑧 ∪ 𝑗 ∈ 𝐴 𝐵
17 nfcv ⊢ Ⅎ 𝑧 ran 𝑓
18 nfcv ⊢ Ⅎ 𝑧 ◡ 𝑓
19 csbeq1a ⊢ ( 𝑘 = ( 2nd ‘ 𝑧 ) → 𝐶 = ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
20 2 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝐴 𝐵 ∈ 𝑊 )
21 iunexg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑗 ∈ 𝐴 𝐵 ∈ 𝑊 ) → ∪ 𝑗 ∈ 𝐴 𝐵 ∈ V )
22 1 20 21 syl2anc ⊢ ( 𝜑 → ∪ 𝑗 ∈ 𝐴 𝐵 ∈ V )
23 22 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) → ∪ 𝑗 ∈ 𝐴 𝐵 ∈ V )
24 simprl ⊢ ( ( 𝜑 ∧ ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) → 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 )
25 f1ocnv ⊢ ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 → ◡ 𝑓 : ran 𝑓 –1-1-onto→ ∪ 𝑗 ∈ 𝐴 𝐵 )
26 24 25 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) → ◡ 𝑓 : ran 𝑓 –1-1-onto→ ∪ 𝑗 ∈ 𝐴 𝐵 )
27 26 adantrlr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) → ◡ 𝑓 : ran 𝑓 –1-1-onto→ ∪ 𝑗 ∈ 𝐴 𝐵 )
28 nfv ⊢ Ⅎ 𝑗 𝜑
29 nfcv ⊢ Ⅎ 𝑗 𝑓
30 nfiu1 ⊢ Ⅎ 𝑗 ∪ 𝑗 ∈ 𝐴 𝐵
31 29 nfrn ⊢ Ⅎ 𝑗 ran 𝑓
32 29 30 31 nff1o ⊢ Ⅎ 𝑗 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓
33 nfv ⊢ Ⅎ 𝑗 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙
34 30 33 nfralw ⊢ Ⅎ 𝑗 ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙
35 32 34 nfan ⊢ Ⅎ 𝑗 ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 )
36 nfcv ⊢ Ⅎ 𝑗 ran 𝑓
37 nfiu1 ⊢ Ⅎ 𝑗 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 )
38 36 37 nfss ⊢ Ⅎ 𝑗 ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 )
39 35 38 nfan ⊢ Ⅎ 𝑗 ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
40 28 39 nfan ⊢ Ⅎ 𝑗 ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) )
41 nfv ⊢ Ⅎ 𝑗 𝑧 ∈ ran 𝑓
42 40 41 nfan ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 )
43 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) ∧ ( 𝑓 ‘ 𝑘 ) = 𝑧 ) → ( 𝑓 ‘ 𝑘 ) = 𝑧 )
44 43 fveq2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) ∧ ( 𝑓 ‘ 𝑘 ) = 𝑧 ) → ( 2nd ‘ ( 𝑓 ‘ 𝑘 ) ) = ( 2nd ‘ 𝑧 ) )
45 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) ∧ ( 𝑓 ‘ 𝑘 ) = 𝑧 ) → 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 )
46 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) )
47 46 simpld ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) )
48 47 simprd ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 )
49 48 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) ∧ ( 𝑓 ‘ 𝑘 ) = 𝑧 ) → ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 )
50 2fveq3 ⊢ ( 𝑙 = 𝑘 → ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = ( 2nd ‘ ( 𝑓 ‘ 𝑘 ) ) )
51 id ⊢ ( 𝑙 = 𝑘 → 𝑙 = 𝑘 )
52 50 51 eqeq12d ⊢ ( 𝑙 = 𝑘 → ( ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ↔ ( 2nd ‘ ( 𝑓 ‘ 𝑘 ) ) = 𝑘 ) )
53 52 rspcva ⊢ ( ( 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) → ( 2nd ‘ ( 𝑓 ‘ 𝑘 ) ) = 𝑘 )
54 45 49 53 syl2anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) ∧ ( 𝑓 ‘ 𝑘 ) = 𝑧 ) → ( 2nd ‘ ( 𝑓 ‘ 𝑘 ) ) = 𝑘 )
55 44 54 eqtr3d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) ∧ ( 𝑓 ‘ 𝑘 ) = 𝑧 ) → ( 2nd ‘ 𝑧 ) = 𝑘 )
56 47 simpld ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 )
57 56 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) ∧ ( 𝑓 ‘ 𝑘 ) = 𝑧 ) → 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 )
58 f1ocnvfv1 ⊢ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) → ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑘 ) ) = 𝑘 )
59 57 45 58 syl2anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) ∧ ( 𝑓 ‘ 𝑘 ) = 𝑧 ) → ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑘 ) ) = 𝑘 )
60 43 fveq2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) ∧ ( 𝑓 ‘ 𝑘 ) = 𝑧 ) → ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑘 ) ) = ( ◡ 𝑓 ‘ 𝑧 ) )
61 55 59 60 3eqtr2rd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) ∧ ( 𝑓 ‘ 𝑘 ) = 𝑧 ) → ( ◡ 𝑓 ‘ 𝑧 ) = ( 2nd ‘ 𝑧 ) )
62 f1ofn ⊢ ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 → 𝑓 Fn ∪ 𝑗 ∈ 𝐴 𝐵 )
63 56 62 syl ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → 𝑓 Fn ∪ 𝑗 ∈ 𝐴 𝐵 )
64 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → 𝑧 ∈ ran 𝑓 )
65 fvelrnb ⊢ ( 𝑓 Fn ∪ 𝑗 ∈ 𝐴 𝐵 → ( 𝑧 ∈ ran 𝑓 ↔ ∃ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 𝑓 ‘ 𝑘 ) = 𝑧 ) )
66 65 biimpa ⊢ ( ( 𝑓 Fn ∪ 𝑗 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ran 𝑓 ) → ∃ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 𝑓 ‘ 𝑘 ) = 𝑧 )
67 63 64 66 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → ∃ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 𝑓 ‘ 𝑘 ) = 𝑧 )
68 61 67 r19.29a ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → ( ◡ 𝑓 ‘ 𝑧 ) = ( 2nd ‘ 𝑧 ) )
69 simprr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) → ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
70 69 sselda ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) → 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
71 eliun ⊢ ( 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ↔ ∃ 𝑗 ∈ 𝐴 𝑧 ∈ ( { 𝑗 } × 𝐵 ) )
72 70 71 sylib ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) → ∃ 𝑗 ∈ 𝐴 𝑧 ∈ ( { 𝑗 } × 𝐵 ) )
73 42 68 72 r19.29af ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) → ( ◡ 𝑓 ‘ 𝑧 ) = ( 2nd ‘ 𝑧 ) )
74 nfcv ⊢ Ⅎ 𝑗 𝑘
75 74 30 nfel ⊢ Ⅎ 𝑗 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵
76 28 75 nfan ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 )
77 3 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
78 eliun ⊢ ( 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↔ ∃ 𝑗 ∈ 𝐴 𝑘 ∈ 𝐵 )
79 78 bilani ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) → ∃ 𝑗 ∈ 𝐴 𝑘 ∈ 𝐵 )
80 76 77 79 r19.29af ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
81 80 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
82 13 14 15 16 17 18 19 23 27 73 81 esumf1o ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) → Σ* 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝐶 = Σ* 𝑧 ∈ ran 𝑓 ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
83 82 eqcomd ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) → Σ* 𝑧 ∈ ran 𝑓 ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 = Σ* 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝐶 )
84 vsnex ⊢ { 𝑗 } ∈ V
85 84 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → { 𝑗 } ∈ V )
86 85 2 xpexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( { 𝑗 } × 𝐵 ) ∈ V )
87 86 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∈ V )
88 iunexg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∈ V ) → ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∈ V )
89 1 87 88 syl2anc ⊢ ( 𝜑 → ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∈ V )
90 89 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) → ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∈ V )
91 nfcv ⊢ Ⅎ 𝑗 𝑧
92 91 37 nfel ⊢ Ⅎ 𝑗 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 )
93 28 92 nfan ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
94 nfcv ⊢ Ⅎ 𝑗 ( 2nd ‘ 𝑧 )
95 nfcv ⊢ Ⅎ 𝑗 𝐶
96 94 95 nfcsbw ⊢ Ⅎ 𝑗 ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶
97 nfcv ⊢ Ⅎ 𝑗 ( 0 [,] +∞ )
98 96 97 nfel ⊢ Ⅎ 𝑗 ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 ∈ ( 0 [,] +∞ )
99 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( ( 1st ‘ 𝑧 ) = 𝑗 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝐵 ) ) → ( 2nd ‘ 𝑧 ) ∈ 𝐵 )
100 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( ( 1st ‘ 𝑧 ) = 𝑗 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝐵 ) ) → 𝜑 )
101 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( ( 1st ‘ 𝑧 ) = 𝑗 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝐵 ) ) → 𝑗 ∈ 𝐴 )
102 3 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ( 0 [,] +∞ ) )
103 100 101 102 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( ( 1st ‘ 𝑧 ) = 𝑗 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝐵 ) ) → ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ( 0 [,] +∞ ) )
104 rspcsbela ⊢ ( ( ( 2nd ‘ 𝑧 ) ∈ 𝐵 ∧ ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ( 0 [,] +∞ ) ) → ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 ∈ ( 0 [,] +∞ ) )
105 99 103 104 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( ( 1st ‘ 𝑧 ) = 𝑗 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝐵 ) ) → ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 ∈ ( 0 [,] +∞ ) )
106 xp1st ⊢ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) → ( 1st ‘ 𝑧 ) ∈ { 𝑗 } )
107 elsni ⊢ ( ( 1st ‘ 𝑧 ) ∈ { 𝑗 } → ( 1st ‘ 𝑧 ) = 𝑗 )
108 106 107 syl ⊢ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) → ( 1st ‘ 𝑧 ) = 𝑗 )
109 xp2nd ⊢ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) → ( 2nd ‘ 𝑧 ) ∈ 𝐵 )
110 108 109 jca ⊢ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) → ( ( 1st ‘ 𝑧 ) = 𝑗 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝐵 ) )
111 110 reximi ⊢ ( ∃ 𝑗 ∈ 𝐴 𝑧 ∈ ( { 𝑗 } × 𝐵 ) → ∃ 𝑗 ∈ 𝐴 ( ( 1st ‘ 𝑧 ) = 𝑗 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝐵 ) )
112 71 111 sylbi ⊢ ( 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) → ∃ 𝑗 ∈ 𝐴 ( ( 1st ‘ 𝑧 ) = 𝑗 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝐵 ) )
113 112 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) → ∃ 𝑗 ∈ 𝐴 ( ( 1st ‘ 𝑧 ) = 𝑗 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝐵 ) )
114 93 98 105 113 r19.29af2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) → ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 ∈ ( 0 [,] +∞ ) )
115 114 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) → ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 ∈ ( 0 [,] +∞ ) )
116 simprr ⊢ ( ( 𝜑 ∧ ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) → ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
117 116 adantrlr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) → ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
118 13 90 115 117 esummono ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) → Σ* 𝑧 ∈ ran 𝑓 ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 ≤ Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
119 83 118 eqbrtrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) → Σ* 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝐶 ≤ Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
120 vex ⊢ 𝑗 ∈ V
121 vex ⊢ 𝑘 ∈ V
122 120 121 op2ndd ⊢ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → ( 2nd ‘ 𝑧 ) = 𝑘 )
123 122 eqcomd ⊢ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → 𝑘 = ( 2nd ‘ 𝑧 ) )
124 123 19 syl ⊢ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → 𝐶 = ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
125 124 eqcomd ⊢ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 = 𝐶 )
126 3 anasss ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐶 ∈ ( 0 [,] +∞ ) )
127 15 125 1 2 126 esum2d ⊢ ( 𝜑 → Σ* 𝑗 ∈ 𝐴 Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
128 127 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) → Σ* 𝑗 ∈ 𝐴 Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
129 119 128 breqtrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) → Σ* 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝐶 ≤ Σ* 𝑗 ∈ 𝐴 Σ* 𝑘 ∈ 𝐵 𝐶 )
130 12 129 exlimddv ⊢ ( 𝜑 → Σ* 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝐶 ≤ Σ* 𝑗 ∈ 𝐴 Σ* 𝑘 ∈ 𝐵 𝐶 )