Metamath Proof Explorer

Theorem i1fd

Description: A simplified set of assumptions to show that a given function is simple. (Contributed by Mario Carneiro, 26-Jun-2014)

Ref Expression
Hypotheses i1fd.1 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
i1fd.2 ⊢ ( 𝜑 → ran 𝐹 ∈ Fin )
i1fd.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ◡ 𝐹 “ { 𝑥 } ) ∈ dom vol )
i1fd.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ∈ ℝ )
Assertion i1fd ( 𝜑 → 𝐹 ∈ dom ∫1 )

Proof

Step Hyp Ref Expression
1 i1fd.1 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2 i1fd.2 ⊢ ( 𝜑 → ran 𝐹 ∈ Fin )
3 i1fd.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ◡ 𝐹 “ { 𝑥 } ) ∈ dom vol )
4 i1fd.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ∈ ℝ )
5 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) ∧ 0 ∈ 𝑥 ) → 𝐹 : ℝ ⟶ ℝ )
6 ffun ⊢ ( 𝐹 : ℝ ⟶ ℝ → Fun 𝐹 )
7 funcnvcnv ⊢ ( Fun 𝐹 → Fun ◡ ◡ 𝐹 )
8 imadif ⊢ ( Fun ◡ ◡ 𝐹 → ( ◡ 𝐹 “ ( ℝ ∖ ( ℝ ∖ 𝑥 ) ) ) = ( ( ◡ 𝐹 “ ℝ ) ∖ ( ◡ 𝐹 “ ( ℝ ∖ 𝑥 ) ) ) )
9 5 6 7 8 4syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) ∧ 0 ∈ 𝑥 ) → ( ◡ 𝐹 “ ( ℝ ∖ ( ℝ ∖ 𝑥 ) ) ) = ( ( ◡ 𝐹 “ ℝ ) ∖ ( ◡ 𝐹 “ ( ℝ ∖ 𝑥 ) ) ) )
10 ioof ⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
11 frn ⊢ ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ → ran (,) ⊆ 𝒫 ℝ )
12 10 11 ax-mp ⊢ ran (,) ⊆ 𝒫 ℝ
13 12 sseli ⊢ ( 𝑥 ∈ ran (,) → 𝑥 ∈ 𝒫 ℝ )
14 13 elpwid ⊢ ( 𝑥 ∈ ran (,) → 𝑥 ⊆ ℝ )
15 14 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) ∧ 0 ∈ 𝑥 ) → 𝑥 ⊆ ℝ )
16 dfss4 ⊢ ( 𝑥 ⊆ ℝ ↔ ( ℝ ∖ ( ℝ ∖ 𝑥 ) ) = 𝑥 )
17 15 16 sylib ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) ∧ 0 ∈ 𝑥 ) → ( ℝ ∖ ( ℝ ∖ 𝑥 ) ) = 𝑥 )
18 17 imaeq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) ∧ 0 ∈ 𝑥 ) → ( ◡ 𝐹 “ ( ℝ ∖ ( ℝ ∖ 𝑥 ) ) ) = ( ◡ 𝐹 “ 𝑥 ) )
19 9 18 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) ∧ 0 ∈ 𝑥 ) → ( ( ◡ 𝐹 “ ℝ ) ∖ ( ◡ 𝐹 “ ( ℝ ∖ 𝑥 ) ) ) = ( ◡ 𝐹 “ 𝑥 ) )
20 fimacnv ⊢ ( 𝐹 : ℝ ⟶ ℝ → ( ◡ 𝐹 “ ℝ ) = ℝ )
21 5 20 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) ∧ 0 ∈ 𝑥 ) → ( ◡ 𝐹 “ ℝ ) = ℝ )
22 rembl ⊢ ℝ ∈ dom vol
23 21 22 eqeltrdi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) ∧ 0 ∈ 𝑥 ) → ( ◡ 𝐹 “ ℝ ) ∈ dom vol )
24 1 adantr ⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → 𝐹 : ℝ ⟶ ℝ )
25 inpreima ⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ( 𝑦 ∩ ran 𝐹 ) ) = ( ( ◡ 𝐹 “ 𝑦 ) ∩ ( ◡ 𝐹 “ ran 𝐹 ) ) )
26 iunid ⊢ ∪ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) { 𝑥 } = ( 𝑦 ∩ ran 𝐹 )
27 26 imaeq2i ⊢ ( ◡ 𝐹 “ ∪ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) { 𝑥 } ) = ( ◡ 𝐹 “ ( 𝑦 ∩ ran 𝐹 ) )
28 imaiun ⊢ ( ◡ 𝐹 “ ∪ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) { 𝑥 } ) = ∪ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( ◡ 𝐹 “ { 𝑥 } )
29 27 28 eqtr3i ⊢ ( ◡ 𝐹 “ ( 𝑦 ∩ ran 𝐹 ) ) = ∪ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( ◡ 𝐹 “ { 𝑥 } )
30 cnvimass ⊢ ( ◡ 𝐹 “ 𝑦 ) ⊆ dom 𝐹
31 cnvimarndm ⊢ ( ◡ 𝐹 “ ran 𝐹 ) = dom 𝐹
32 30 31 sseqtrri ⊢ ( ◡ 𝐹 “ 𝑦 ) ⊆ ( ◡ 𝐹 “ ran 𝐹 )
33 df-ss ⊢ ( ( ◡ 𝐹 “ 𝑦 ) ⊆ ( ◡ 𝐹 “ ran 𝐹 ) ↔ ( ( ◡ 𝐹 “ 𝑦 ) ∩ ( ◡ 𝐹 “ ran 𝐹 ) ) = ( ◡ 𝐹 “ 𝑦 ) )
34 32 33 mpbi ⊢ ( ( ◡ 𝐹 “ 𝑦 ) ∩ ( ◡ 𝐹 “ ran 𝐹 ) ) = ( ◡ 𝐹 “ 𝑦 )
35 25 29 34 3eqtr3g ⊢ ( Fun 𝐹 → ∪ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( ◡ 𝐹 “ { 𝑥 } ) = ( ◡ 𝐹 “ 𝑦 ) )
36 24 6 35 3syl ⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ∪ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( ◡ 𝐹 “ { 𝑥 } ) = ( ◡ 𝐹 “ 𝑦 ) )
37 2 adantr ⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ran 𝐹 ∈ Fin )
38 inss2 ⊢ ( 𝑦 ∩ ran 𝐹 ) ⊆ ran 𝐹
39 ssfi ⊢ ( ( ran 𝐹 ∈ Fin ∧ ( 𝑦 ∩ ran 𝐹 ) ⊆ ran 𝐹 ) → ( 𝑦 ∩ ran 𝐹 ) ∈ Fin )
40 37 38 39 sylancl ⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ( 𝑦 ∩ ran 𝐹 ) ∈ Fin )
41 simpll ⊢ ( ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) ∧ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ) → 𝜑 )
42 elinel1 ⊢ ( 0 ∈ ( 𝑦 ∩ ran 𝐹 ) → 0 ∈ 𝑦 )
43 42 con3i ⊢ ( ¬ 0 ∈ 𝑦 → ¬ 0 ∈ ( 𝑦 ∩ ran 𝐹 ) )
44 43 adantl ⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ¬ 0 ∈ ( 𝑦 ∩ ran 𝐹 ) )
45 disjsn ⊢ ( ( ( 𝑦 ∩ ran 𝐹 ) ∩ { 0 } ) = ∅ ↔ ¬ 0 ∈ ( 𝑦 ∩ ran 𝐹 ) )
46 44 45 sylibr ⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ( ( 𝑦 ∩ ran 𝐹 ) ∩ { 0 } ) = ∅ )
47 reldisj ⊢ ( ( 𝑦 ∩ ran 𝐹 ) ⊆ ran 𝐹 → ( ( ( 𝑦 ∩ ran 𝐹 ) ∩ { 0 } ) = ∅ ↔ ( 𝑦 ∩ ran 𝐹 ) ⊆ ( ran 𝐹 ∖ { 0 } ) ) )
48 38 47 ax-mp ⊢ ( ( ( 𝑦 ∩ ran 𝐹 ) ∩ { 0 } ) = ∅ ↔ ( 𝑦 ∩ ran 𝐹 ) ⊆ ( ran 𝐹 ∖ { 0 } ) )
49 46 48 sylib ⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ( 𝑦 ∩ ran 𝐹 ) ⊆ ( ran 𝐹 ∖ { 0 } ) )
50 49 sselda ⊢ ( ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) ∧ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ) → 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) )
51 41 50 3 syl2anc ⊢ ( ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) ∧ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ) → ( ◡ 𝐹 “ { 𝑥 } ) ∈ dom vol )
52 51 ralrimiva ⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ∀ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( ◡ 𝐹 “ { 𝑥 } ) ∈ dom vol )
53 finiunmbl ⊢ ( ( ( 𝑦 ∩ ran 𝐹 ) ∈ Fin ∧ ∀ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( ◡ 𝐹 “ { 𝑥 } ) ∈ dom vol ) → ∪ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( ◡ 𝐹 “ { 𝑥 } ) ∈ dom vol )
54 40 52 53 syl2anc ⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ∪ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( ◡ 𝐹 “ { 𝑥 } ) ∈ dom vol )
55 36 54 eqeltrrd ⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ( ◡ 𝐹 “ 𝑦 ) ∈ dom vol )
56 55 ex ⊢ ( 𝜑 → ( ¬ 0 ∈ 𝑦 → ( ◡ 𝐹 “ 𝑦 ) ∈ dom vol ) )
57 56 alrimiv ⊢ ( 𝜑 → ∀ 𝑦 ( ¬ 0 ∈ 𝑦 → ( ◡ 𝐹 “ 𝑦 ) ∈ dom vol ) )
58 57 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) ∧ 0 ∈ 𝑥 ) → ∀ 𝑦 ( ¬ 0 ∈ 𝑦 → ( ◡ 𝐹 “ 𝑦 ) ∈ dom vol ) )
59 elndif ⊢ ( 0 ∈ 𝑥 → ¬ 0 ∈ ( ℝ ∖ 𝑥 ) )
60 59 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) ∧ 0 ∈ 𝑥 ) → ¬ 0 ∈ ( ℝ ∖ 𝑥 ) )
61 reex ⊢ ℝ ∈ V
62 61 difexi ⊢ ( ℝ ∖ 𝑥 ) ∈ V
63 eleq2 ⊢ ( 𝑦 = ( ℝ ∖ 𝑥 ) → ( 0 ∈ 𝑦 ↔ 0 ∈ ( ℝ ∖ 𝑥 ) ) )
64 63 notbid ⊢ ( 𝑦 = ( ℝ ∖ 𝑥 ) → ( ¬ 0 ∈ 𝑦 ↔ ¬ 0 ∈ ( ℝ ∖ 𝑥 ) ) )
65 imaeq2 ⊢ ( 𝑦 = ( ℝ ∖ 𝑥 ) → ( ◡ 𝐹 “ 𝑦 ) = ( ◡ 𝐹 “ ( ℝ ∖ 𝑥 ) ) )
66 65 eleq1d ⊢ ( 𝑦 = ( ℝ ∖ 𝑥 ) → ( ( ◡ 𝐹 “ 𝑦 ) ∈ dom vol ↔ ( ◡ 𝐹 “ ( ℝ ∖ 𝑥 ) ) ∈ dom vol ) )
67 64 66 imbi12d ⊢ ( 𝑦 = ( ℝ ∖ 𝑥 ) → ( ( ¬ 0 ∈ 𝑦 → ( ◡ 𝐹 “ 𝑦 ) ∈ dom vol ) ↔ ( ¬ 0 ∈ ( ℝ ∖ 𝑥 ) → ( ◡ 𝐹 “ ( ℝ ∖ 𝑥 ) ) ∈ dom vol ) ) )
68 62 67 spcv ⊢ ( ∀ 𝑦 ( ¬ 0 ∈ 𝑦 → ( ◡ 𝐹 “ 𝑦 ) ∈ dom vol ) → ( ¬ 0 ∈ ( ℝ ∖ 𝑥 ) → ( ◡ 𝐹 “ ( ℝ ∖ 𝑥 ) ) ∈ dom vol ) )
69 58 60 68 sylc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) ∧ 0 ∈ 𝑥 ) → ( ◡ 𝐹 “ ( ℝ ∖ 𝑥 ) ) ∈ dom vol )
70 difmbl ⊢ ( ( ( ◡ 𝐹 “ ℝ ) ∈ dom vol ∧ ( ◡ 𝐹 “ ( ℝ ∖ 𝑥 ) ) ∈ dom vol ) → ( ( ◡ 𝐹 “ ℝ ) ∖ ( ◡ 𝐹 “ ( ℝ ∖ 𝑥 ) ) ) ∈ dom vol )
71 23 69 70 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) ∧ 0 ∈ 𝑥 ) → ( ( ◡ 𝐹 “ ℝ ) ∖ ( ◡ 𝐹 “ ( ℝ ∖ 𝑥 ) ) ) ∈ dom vol )
72 19 71 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) ∧ 0 ∈ 𝑥 ) → ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol )
73 eleq2 ⊢ ( 𝑦 = 𝑥 → ( 0 ∈ 𝑦 ↔ 0 ∈ 𝑥 ) )
74 73 notbid ⊢ ( 𝑦 = 𝑥 → ( ¬ 0 ∈ 𝑦 ↔ ¬ 0 ∈ 𝑥 ) )
75 imaeq2 ⊢ ( 𝑦 = 𝑥 → ( ◡ 𝐹 “ 𝑦 ) = ( ◡ 𝐹 “ 𝑥 ) )
76 75 eleq1d ⊢ ( 𝑦 = 𝑥 → ( ( ◡ 𝐹 “ 𝑦 ) ∈ dom vol ↔ ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol ) )
77 74 76 imbi12d ⊢ ( 𝑦 = 𝑥 → ( ( ¬ 0 ∈ 𝑦 → ( ◡ 𝐹 “ 𝑦 ) ∈ dom vol ) ↔ ( ¬ 0 ∈ 𝑥 → ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol ) ) )
78 77 spvv ⊢ ( ∀ 𝑦 ( ¬ 0 ∈ 𝑦 → ( ◡ 𝐹 “ 𝑦 ) ∈ dom vol ) → ( ¬ 0 ∈ 𝑥 → ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol ) )
79 57 78 syl ⊢ ( 𝜑 → ( ¬ 0 ∈ 𝑥 → ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol ) )
80 79 imp ⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑥 ) → ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol )
81 80 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) ∧ ¬ 0 ∈ 𝑥 ) → ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol )
82 72 81 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) → ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol )
83 82 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ran (,) ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol )
84 ismbf ⊢ ( 𝐹 : ℝ ⟶ ℝ → ( 𝐹 ∈ MblFn ↔ ∀ 𝑥 ∈ ran (,) ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol ) )
85 1 84 syl ⊢ ( 𝜑 → ( 𝐹 ∈ MblFn ↔ ∀ 𝑥 ∈ ran (,) ( ◡ 𝐹 “ 𝑥 ) ∈ dom vol ) )
86 83 85 mpbird ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
87 mblvol ⊢ ( ( ◡ 𝐹 “ 𝑦 ) ∈ dom vol → ( vol ‘ ( ◡ 𝐹 “ 𝑦 ) ) = ( vol* ‘ ( ◡ 𝐹 “ 𝑦 ) ) )
88 55 87 syl ⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ( vol ‘ ( ◡ 𝐹 “ 𝑦 ) ) = ( vol* ‘ ( ◡ 𝐹 “ 𝑦 ) ) )
89 mblss ⊢ ( ( ◡ 𝐹 “ 𝑦 ) ∈ dom vol → ( ◡ 𝐹 “ 𝑦 ) ⊆ ℝ )
90 55 89 syl ⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ( ◡ 𝐹 “ 𝑦 ) ⊆ ℝ )
91 mblvol ⊢ ( ( ◡ 𝐹 “ { 𝑥 } ) ∈ dom vol → ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) = ( vol* ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) )
92 51 91 syl ⊢ ( ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) ∧ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) = ( vol* ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) )
93 41 50 4 syl2anc ⊢ ( ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) ∧ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ) → ( vol ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ∈ ℝ )
94 92 93 eqeltrrd ⊢ ( ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) ∧ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ) → ( vol* ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ∈ ℝ )
95 40 94 fsumrecl ⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → Σ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( vol* ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ∈ ℝ )
96 36 fveq2d ⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ( vol* ‘ ∪ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( ◡ 𝐹 “ { 𝑥 } ) ) = ( vol* ‘ ( ◡ 𝐹 “ 𝑦 ) ) )
97 mblss ⊢ ( ( ◡ 𝐹 “ { 𝑥 } ) ∈ dom vol → ( ◡ 𝐹 “ { 𝑥 } ) ⊆ ℝ )
98 51 97 syl ⊢ ( ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) ∧ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ) → ( ◡ 𝐹 “ { 𝑥 } ) ⊆ ℝ )
99 98 94 jca ⊢ ( ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) ∧ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ) → ( ( ◡ 𝐹 “ { 𝑥 } ) ⊆ ℝ ∧ ( vol* ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ∈ ℝ ) )
100 99 ralrimiva ⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ∀ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( ( ◡ 𝐹 “ { 𝑥 } ) ⊆ ℝ ∧ ( vol* ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ∈ ℝ ) )
101 ovolfiniun ⊢ ( ( ( 𝑦 ∩ ran 𝐹 ) ∈ Fin ∧ ∀ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( ( ◡ 𝐹 “ { 𝑥 } ) ⊆ ℝ ∧ ( vol* ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ∈ ℝ ) ) → ( vol* ‘ ∪ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( ◡ 𝐹 “ { 𝑥 } ) ) ≤ Σ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( vol* ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) )
102 40 100 101 syl2anc ⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ( vol* ‘ ∪ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( ◡ 𝐹 “ { 𝑥 } ) ) ≤ Σ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( vol* ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) )
103 96 102 eqbrtrrd ⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ( vol* ‘ ( ◡ 𝐹 “ 𝑦 ) ) ≤ Σ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( vol* ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) )
104 ovollecl ⊢ ( ( ( ◡ 𝐹 “ 𝑦 ) ⊆ ℝ ∧ Σ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( vol* ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ∈ ℝ ∧ ( vol* ‘ ( ◡ 𝐹 “ 𝑦 ) ) ≤ Σ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( vol* ‘ ( ◡ 𝐹 “ { 𝑥 } ) ) ) → ( vol* ‘ ( ◡ 𝐹 “ 𝑦 ) ) ∈ ℝ )
105 90 95 103 104 syl3anc ⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ( vol* ‘ ( ◡ 𝐹 “ 𝑦 ) ) ∈ ℝ )
106 88 105 eqeltrd ⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ( vol ‘ ( ◡ 𝐹 “ 𝑦 ) ) ∈ ℝ )
107 106 ex ⊢ ( 𝜑 → ( ¬ 0 ∈ 𝑦 → ( vol ‘ ( ◡ 𝐹 “ 𝑦 ) ) ∈ ℝ ) )
108 107 alrimiv ⊢ ( 𝜑 → ∀ 𝑦 ( ¬ 0 ∈ 𝑦 → ( vol ‘ ( ◡ 𝐹 “ 𝑦 ) ) ∈ ℝ ) )
109 neldifsn ⊢ ¬ 0 ∈ ( ℝ ∖ { 0 } )
110 61 difexi ⊢ ( ℝ ∖ { 0 } ) ∈ V
111 eleq2 ⊢ ( 𝑦 = ( ℝ ∖ { 0 } ) → ( 0 ∈ 𝑦 ↔ 0 ∈ ( ℝ ∖ { 0 } ) ) )
112 111 notbid ⊢ ( 𝑦 = ( ℝ ∖ { 0 } ) → ( ¬ 0 ∈ 𝑦 ↔ ¬ 0 ∈ ( ℝ ∖ { 0 } ) ) )
113 imaeq2 ⊢ ( 𝑦 = ( ℝ ∖ { 0 } ) → ( ◡ 𝐹 “ 𝑦 ) = ( ◡ 𝐹 “ ( ℝ ∖ { 0 } ) ) )
114 113 fveq2d ⊢ ( 𝑦 = ( ℝ ∖ { 0 } ) → ( vol ‘ ( ◡ 𝐹 “ 𝑦 ) ) = ( vol ‘ ( ◡ 𝐹 “ ( ℝ ∖ { 0 } ) ) ) )
115 114 eleq1d ⊢ ( 𝑦 = ( ℝ ∖ { 0 } ) → ( ( vol ‘ ( ◡ 𝐹 “ 𝑦 ) ) ∈ ℝ ↔ ( vol ‘ ( ◡ 𝐹 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) )
116 112 115 imbi12d ⊢ ( 𝑦 = ( ℝ ∖ { 0 } ) → ( ( ¬ 0 ∈ 𝑦 → ( vol ‘ ( ◡ 𝐹 “ 𝑦 ) ) ∈ ℝ ) ↔ ( ¬ 0 ∈ ( ℝ ∖ { 0 } ) → ( vol ‘ ( ◡ 𝐹 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) ) )
117 110 116 spcv ⊢ ( ∀ 𝑦 ( ¬ 0 ∈ 𝑦 → ( vol ‘ ( ◡ 𝐹 “ 𝑦 ) ) ∈ ℝ ) → ( ¬ 0 ∈ ( ℝ ∖ { 0 } ) → ( vol ‘ ( ◡ 𝐹 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) )
118 108 109 117 mpisyl ⊢ ( 𝜑 → ( vol ‘ ( ◡ 𝐹 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ )
119 1 2 118 3jca ⊢ ( 𝜑 → ( 𝐹 : ℝ ⟶ ℝ ∧ ran 𝐹 ∈ Fin ∧ ( vol ‘ ( ◡ 𝐹 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) )
120 isi1f ⊢ ( 𝐹 ∈ dom ∫1 ↔ ( 𝐹 ∈ MblFn ∧ ( 𝐹 : ℝ ⟶ ℝ ∧ ran 𝐹 ∈ Fin ∧ ( vol ‘ ( ◡ 𝐹 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) ) )
121 86 119 120 sylanbrc ⊢ ( 𝜑 → 𝐹 ∈ dom ∫1 )