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 biimpi ⊢ ( 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → ∃ 𝑗 ∈ 𝐴 𝑘 ∈ 𝐵 )
80 79 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) → ∃ 𝑗 ∈ 𝐴 𝑘 ∈ 𝐵 )
81 76 77 80 r19.29af ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
82 81 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
83 13 14 15 16 17 18 19 23 27 73 82 esumf1o ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) → Σ* 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝐶 = Σ* 𝑧 ∈ ran 𝑓 ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
84 83 eqcomd ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) → Σ* 𝑧 ∈ ran 𝑓 ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 = Σ* 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝐶 )
85 vsnex ⊢ { 𝑗 } ∈ V
86 85 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → { 𝑗 } ∈ V )
87 86 2 xpexd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( { 𝑗 } × 𝐵 ) ∈ V )
88 87 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∈ V )
89 iunexg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∈ V ) → ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∈ V )
90 1 88 89 syl2anc ⊢ ( 𝜑 → ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∈ V )
91 90 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) → ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∈ V )
92 nfcv ⊢ Ⅎ 𝑗 𝑧
93 92 37 nfel ⊢ Ⅎ 𝑗 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 )
94 28 93 nfan ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
95 nfcv ⊢ Ⅎ 𝑗 ( 2nd ‘ 𝑧 )
96 nfcv ⊢ Ⅎ 𝑗 𝐶
97 95 96 nfcsbw ⊢ Ⅎ 𝑗 ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶
98 nfcv ⊢ Ⅎ 𝑗 ( 0 [,] +∞ )
99 97 98 nfel ⊢ Ⅎ 𝑗 ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 ∈ ( 0 [,] +∞ )
100 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( ( 1st ‘ 𝑧 ) = 𝑗 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝐵 ) ) → ( 2nd ‘ 𝑧 ) ∈ 𝐵 )
101 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( ( 1st ‘ 𝑧 ) = 𝑗 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝐵 ) ) → 𝜑 )
102 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( ( 1st ‘ 𝑧 ) = 𝑗 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝐵 ) ) → 𝑗 ∈ 𝐴 )
103 3 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ( 0 [,] +∞ ) )
104 101 102 103 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( ( 1st ‘ 𝑧 ) = 𝑗 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝐵 ) ) → ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ( 0 [,] +∞ ) )
105 rspcsbela ⊢ ( ( ( 2nd ‘ 𝑧 ) ∈ 𝐵 ∧ ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ( 0 [,] +∞ ) ) → ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 ∈ ( 0 [,] +∞ ) )
106 100 104 105 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( ( 1st ‘ 𝑧 ) = 𝑗 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝐵 ) ) → ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 ∈ ( 0 [,] +∞ ) )
107 xp1st ⊢ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) → ( 1st ‘ 𝑧 ) ∈ { 𝑗 } )
108 elsni ⊢ ( ( 1st ‘ 𝑧 ) ∈ { 𝑗 } → ( 1st ‘ 𝑧 ) = 𝑗 )
109 107 108 syl ⊢ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) → ( 1st ‘ 𝑧 ) = 𝑗 )
110 xp2nd ⊢ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) → ( 2nd ‘ 𝑧 ) ∈ 𝐵 )
111 109 110 jca ⊢ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) → ( ( 1st ‘ 𝑧 ) = 𝑗 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝐵 ) )
112 111 reximi ⊢ ( ∃ 𝑗 ∈ 𝐴 𝑧 ∈ ( { 𝑗 } × 𝐵 ) → ∃ 𝑗 ∈ 𝐴 ( ( 1st ‘ 𝑧 ) = 𝑗 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝐵 ) )
113 71 112 sylbi ⊢ ( 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) → ∃ 𝑗 ∈ 𝐴 ( ( 1st ‘ 𝑧 ) = 𝑗 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝐵 ) )
114 113 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) → ∃ 𝑗 ∈ 𝐴 ( ( 1st ‘ 𝑧 ) = 𝑗 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝐵 ) )
115 94 99 106 114 r19.29af2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) → ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 ∈ ( 0 [,] +∞ ) )
116 115 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) → ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 ∈ ( 0 [,] +∞ ) )
117 simprr ⊢ ( ( 𝜑 ∧ ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) → ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
118 117 adantrlr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) → ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
119 13 91 116 118 esummono ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) → Σ* 𝑧 ∈ ran 𝑓 ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 ≤ Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
120 84 119 eqbrtrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) → Σ* 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝐶 ≤ Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
121 vex ⊢ 𝑗 ∈ V
122 vex ⊢ 𝑘 ∈ V
123 121 122 op2ndd ⊢ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → ( 2nd ‘ 𝑧 ) = 𝑘 )
124 123 eqcomd ⊢ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → 𝑘 = ( 2nd ‘ 𝑧 ) )
125 124 19 syl ⊢ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → 𝐶 = ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
126 125 eqcomd ⊢ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 = 𝐶 )
127 3 anasss ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐶 ∈ ( 0 [,] +∞ ) )
128 15 126 1 2 127 esum2d ⊢ ( 𝜑 → Σ* 𝑗 ∈ 𝐴 Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
129 128 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) → Σ* 𝑗 ∈ 𝐴 Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
130 120 129 breqtrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) → Σ* 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝐶 ≤ Σ* 𝑗 ∈ 𝐴 Σ* 𝑘 ∈ 𝐵 𝐶 )
131 12 130 exlimddv ⊢ ( 𝜑 → Σ* 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝐶 ≤ Σ* 𝑗 ∈ 𝐴 Σ* 𝑘 ∈ 𝐵 𝐶 )