Theorem i1fd 25609

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

Hypotheses

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

Assertion

Ref	Expression
i1fd	⊢ (𝜑 → 𝐹 ∈ dom ∫1)

Distinct variable groups:   𝑥,𝐹   𝜑,𝑥

Proof of Theorem i1fd

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		i1fd.1	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
2	1	ad2antrr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → 𝐹:ℝ⟶ℝ)
3		ffun 6725	. . . . . . . 8 ⊢ (𝐹:ℝ⟶ℝ → Fun 𝐹)
4		funcnvcnv 6620	. . . . . . . 8 ⊢ (Fun 𝐹 → Fun ◡◡𝐹)
5		imadif 6637	. . . . . . . 8 ⊢ (Fun ◡◡𝐹 → (◡𝐹 “ (ℝ ∖ (ℝ ∖ 𝑥))) = ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥))))
6	2, 3, 4, 5	4syl 19	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ (ℝ ∖ (ℝ ∖ 𝑥))) = ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥))))
7		ioof 13456	. . . . . . . . . . . . 13 ⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ
8		frn 6729	. . . . . . . . . . . . 13 ⊢ ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → ran (,) ⊆ 𝒫 ℝ)
9	7, 8	ax-mp 5	. . . . . . . . . . . 12 ⊢ ran (,) ⊆ 𝒫 ℝ
10	9	sseli 3976	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ran (,) → 𝑥 ∈ 𝒫 ℝ)
11	10	elpwid 4612	. . . . . . . . . 10 ⊢ (𝑥 ∈ ran (,) → 𝑥 ⊆ ℝ)
12	11	ad2antlr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → 𝑥 ⊆ ℝ)
13		dfss4 4259	. . . . . . . . 9 ⊢ (𝑥 ⊆ ℝ ↔ (ℝ ∖ (ℝ ∖ 𝑥)) = 𝑥)
14	12, 13	sylib 217	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (ℝ ∖ (ℝ ∖ 𝑥)) = 𝑥)
15	14	imaeq2d 6063	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ (ℝ ∖ (ℝ ∖ 𝑥))) = (◡𝐹 “ 𝑥))
16	6, 15	eqtr3d 2770	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥))) = (◡𝐹 “ 𝑥))
17		fimacnv 6745	. . . . . . . . 9 ⊢ (𝐹:ℝ⟶ℝ → (◡𝐹 “ ℝ) = ℝ)
18	2, 17	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ ℝ) = ℝ)
19		rembl 25468	. . . . . . . 8 ⊢ ℝ ∈ dom vol
20	18, 19	eqeltrdi 2837	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ ℝ) ∈ dom vol)
21	1	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → 𝐹:ℝ⟶ℝ)
22		inpreima 7073	. . . . . . . . . . . . . 14 ⊢ (Fun 𝐹 → (◡𝐹 “ (𝑦 ∩ ran 𝐹)) = ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ ran 𝐹)))
23		iunid 5063	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹){𝑥} = (𝑦 ∩ ran 𝐹)
24	23	imaeq2i 6061	. . . . . . . . . . . . . . 15 ⊢ (◡𝐹 “ ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹){𝑥}) = (◡𝐹 “ (𝑦 ∩ ran 𝐹))
25		imaiun 7255	. . . . . . . . . . . . . . 15 ⊢ (◡𝐹 “ ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹){𝑥}) = ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥})
26	24, 25	eqtr3i 2758	. . . . . . . . . . . . . 14 ⊢ (◡𝐹 “ (𝑦 ∩ ran 𝐹)) = ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥})
27		cnvimass 6085	. . . . . . . . . . . . . . . 16 ⊢ (◡𝐹 “ 𝑦) ⊆ dom 𝐹
28		cnvimarndm 6086	. . . . . . . . . . . . . . . 16 ⊢ (◡𝐹 “ ran 𝐹) = dom 𝐹
29	27, 28	sseqtrri 4017	. . . . . . . . . . . . . . 15 ⊢ (◡𝐹 “ 𝑦) ⊆ (◡𝐹 “ ran 𝐹)
30		df-ss 3964	. . . . . . . . . . . . . . 15 ⊢ ((◡𝐹 “ 𝑦) ⊆ (◡𝐹 “ ran 𝐹) ↔ ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ ran 𝐹)) = (◡𝐹 “ 𝑦))
31	29, 30	mpbi 229	. . . . . . . . . . . . . 14 ⊢ ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ ran 𝐹)) = (◡𝐹 “ 𝑦)
32	22, 26, 31	3eqtr3g 2791	. . . . . . . . . . . . 13 ⊢ (Fun 𝐹 → ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) = (◡𝐹 “ 𝑦))
33	21, 3, 32	3syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) = (◡𝐹 “ 𝑦))
34		i1fd.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ran 𝐹 ∈ Fin)
35	34	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ran 𝐹 ∈ Fin)
36		inss2 4230	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∩ ran 𝐹) ⊆ ran 𝐹
37		ssfi 9197	. . . . . . . . . . . . . 14 ⊢ ((ran 𝐹 ∈ Fin ∧ (𝑦 ∩ ran 𝐹) ⊆ ran 𝐹) → (𝑦 ∩ ran 𝐹) ∈ Fin)
38	35, 36, 37	sylancl 585	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (𝑦 ∩ ran 𝐹) ∈ Fin)
39		simpll 766	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → 𝜑)
40		elinel1 4195	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ (𝑦 ∩ ran 𝐹) → 0 ∈ 𝑦)
41	40	con3i 154	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 0 ∈ 𝑦 → ¬ 0 ∈ (𝑦 ∩ ran 𝐹))
42	41	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ¬ 0 ∈ (𝑦 ∩ ran 𝐹))
43		disjsn 4716	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∩ ran 𝐹) ∩ {0}) = ∅ ↔ ¬ 0 ∈ (𝑦 ∩ ran 𝐹))
44	42, 43	sylibr 233	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ((𝑦 ∩ ran 𝐹) ∩ {0}) = ∅)
45		reldisj 4452	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∩ ran 𝐹) ⊆ ran 𝐹 → (((𝑦 ∩ ran 𝐹) ∩ {0}) = ∅ ↔ (𝑦 ∩ ran 𝐹) ⊆ (ran 𝐹 ∖ {0})))
46	36, 45	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∩ ran 𝐹) ∩ {0}) = ∅ ↔ (𝑦 ∩ ran 𝐹) ⊆ (ran 𝐹 ∖ {0}))
47	44, 46	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (𝑦 ∩ ran 𝐹) ⊆ (ran 𝐹 ∖ {0}))
48	47	sselda 3980	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → 𝑥 ∈ (ran 𝐹 ∖ {0}))
49		i1fd.3	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ {0})) → (◡𝐹 “ {𝑥}) ∈ dom vol)
50	39, 48, 49	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → (◡𝐹 “ {𝑥}) ∈ dom vol)
51	50	ralrimiva 3143	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ∀𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) ∈ dom vol)
52		finiunmbl 25472	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∩ ran 𝐹) ∈ Fin ∧ ∀𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) ∈ dom vol) → ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) ∈ dom vol)
53	38, 51, 52	syl2anc 583	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) ∈ dom vol)
54	33, 53	eqeltrrd 2830	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (◡𝐹 “ 𝑦) ∈ dom vol)
55	54	ex 412	. . . . . . . . . 10 ⊢ (𝜑 → (¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol))
56	55	alrimiv 1923	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑦(¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol))
57	56	ad2antrr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → ∀𝑦(¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol))
58		elndif 4127	. . . . . . . . 9 ⊢ (0 ∈ 𝑥 → ¬ 0 ∈ (ℝ ∖ 𝑥))
59	58	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → ¬ 0 ∈ (ℝ ∖ 𝑥))
60		reex 11229	. . . . . . . . . 10 ⊢ ℝ ∈ V
61	60	difexi 5330	. . . . . . . . 9 ⊢ (ℝ ∖ 𝑥) ∈ V
62		eleq2 2818	. . . . . . . . . . 11 ⊢ (𝑦 = (ℝ ∖ 𝑥) → (0 ∈ 𝑦 ↔ 0 ∈ (ℝ ∖ 𝑥)))
63	62	notbid 318	. . . . . . . . . 10 ⊢ (𝑦 = (ℝ ∖ 𝑥) → (¬ 0 ∈ 𝑦 ↔ ¬ 0 ∈ (ℝ ∖ 𝑥)))
64		imaeq2 6059	. . . . . . . . . . 11 ⊢ (𝑦 = (ℝ ∖ 𝑥) → (◡𝐹 “ 𝑦) = (◡𝐹 “ (ℝ ∖ 𝑥)))
65	64	eleq1d 2814	. . . . . . . . . 10 ⊢ (𝑦 = (ℝ ∖ 𝑥) → ((◡𝐹 “ 𝑦) ∈ dom vol ↔ (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol))
66	63, 65	imbi12d 344	. . . . . . . . 9 ⊢ (𝑦 = (ℝ ∖ 𝑥) → ((¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol) ↔ (¬ 0 ∈ (ℝ ∖ 𝑥) → (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol)))
67	61, 66	spcv 3592	. . . . . . . 8 ⊢ (∀𝑦(¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol) → (¬ 0 ∈ (ℝ ∖ 𝑥) → (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol))
68	57, 59, 67	sylc 65	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol)
69		difmbl 25471	. . . . . . 7 ⊢ (((◡𝐹 “ ℝ) ∈ dom vol ∧ (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol) → ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥))) ∈ dom vol)
70	20, 68, 69	syl2anc 583	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥))) ∈ dom vol)
71	16, 70	eqeltrrd 2830	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ 𝑥) ∈ dom vol)
72		eleq2 2818	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → (0 ∈ 𝑦 ↔ 0 ∈ 𝑥))
73	72	notbid 318	. . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → (¬ 0 ∈ 𝑦 ↔ ¬ 0 ∈ 𝑥))
74		imaeq2 6059	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → (◡𝐹 “ 𝑦) = (◡𝐹 “ 𝑥))
75	74	eleq1d 2814	. . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → ((◡𝐹 “ 𝑦) ∈ dom vol ↔ (◡𝐹 “ 𝑥) ∈ dom vol))
76	73, 75	imbi12d 344	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → ((¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol) ↔ (¬ 0 ∈ 𝑥 → (◡𝐹 “ 𝑥) ∈ dom vol)))
77	76	spvv 1993	. . . . . . . 8 ⊢ (∀𝑦(¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol) → (¬ 0 ∈ 𝑥 → (◡𝐹 “ 𝑥) ∈ dom vol))
78	56, 77	syl 17	. . . . . . 7 ⊢ (𝜑 → (¬ 0 ∈ 𝑥 → (◡𝐹 “ 𝑥) ∈ dom vol))
79	78	imp 406	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑥) → (◡𝐹 “ 𝑥) ∈ dom vol)
80	79	adantlr 714	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ ¬ 0 ∈ 𝑥) → (◡𝐹 “ 𝑥) ∈ dom vol)
81	71, 80	pm2.61dan 812	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ran (,)) → (◡𝐹 “ 𝑥) ∈ dom vol)
82	81	ralrimiva 3143	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol)
83		ismbf 25556	. . . 4 ⊢ (𝐹:ℝ⟶ℝ → (𝐹 ∈ MblFn ↔ ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol))
84	1, 83	syl 17	. . 3 ⊢ (𝜑 → (𝐹 ∈ MblFn ↔ ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol))
85	82, 84	mpbird 257	. 2 ⊢ (𝜑 → 𝐹 ∈ MblFn)
86		mblvol 25458	. . . . . . . 8 ⊢ ((◡𝐹 “ 𝑦) ∈ dom vol → (vol‘(◡𝐹 “ 𝑦)) = (vol*‘(◡𝐹 “ 𝑦)))
87	54, 86	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol‘(◡𝐹 “ 𝑦)) = (vol*‘(◡𝐹 “ 𝑦)))
88		mblss 25459	. . . . . . . . 9 ⊢ ((◡𝐹 “ 𝑦) ∈ dom vol → (◡𝐹 “ 𝑦) ⊆ ℝ)
89	54, 88	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (◡𝐹 “ 𝑦) ⊆ ℝ)
90		mblvol 25458	. . . . . . . . . . 11 ⊢ ((◡𝐹 “ {𝑥}) ∈ dom vol → (vol‘(◡𝐹 “ {𝑥})) = (vol*‘(◡𝐹 “ {𝑥})))
91	50, 90	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → (vol‘(◡𝐹 “ {𝑥})) = (vol*‘(◡𝐹 “ {𝑥})))
92		i1fd.4	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ {0})) → (vol‘(◡𝐹 “ {𝑥})) ∈ ℝ)
93	39, 48, 92	syl2anc 583	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → (vol‘(◡𝐹 “ {𝑥})) ∈ ℝ)
94	91, 93	eqeltrrd 2830	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → (vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ)
95	38, 94	fsumrecl 15712	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ)
96	33	fveq2d 6901	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol*‘∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥})) = (vol*‘(◡𝐹 “ 𝑦)))
97		mblss 25459	. . . . . . . . . . . . 13 ⊢ ((◡𝐹 “ {𝑥}) ∈ dom vol → (◡𝐹 “ {𝑥}) ⊆ ℝ)
98	50, 97	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → (◡𝐹 “ {𝑥}) ⊆ ℝ)
99	98, 94	jca 511	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → ((◡𝐹 “ {𝑥}) ⊆ ℝ ∧ (vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ))
100	99	ralrimiva 3143	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ∀𝑥 ∈ (𝑦 ∩ ran 𝐹)((◡𝐹 “ {𝑥}) ⊆ ℝ ∧ (vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ))
101		ovolfiniun 25429	. . . . . . . . . 10 ⊢ (((𝑦 ∩ ran 𝐹) ∈ Fin ∧ ∀𝑥 ∈ (𝑦 ∩ ran 𝐹)((◡𝐹 “ {𝑥}) ⊆ ℝ ∧ (vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ)) → (vol*‘∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥})) ≤ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥})))
102	38, 100, 101	syl2anc 583	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol*‘∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥})) ≤ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥})))
103	96, 102	eqbrtrrd 5172	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol*‘(◡𝐹 “ 𝑦)) ≤ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥})))
104		ovollecl 25411	. . . . . . . 8 ⊢ (((◡𝐹 “ 𝑦) ⊆ ℝ ∧ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ ∧ (vol*‘(◡𝐹 “ 𝑦)) ≤ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥}))) → (vol*‘(◡𝐹 “ 𝑦)) ∈ ℝ)
105	89, 95, 103, 104	syl3anc 1369	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol*‘(◡𝐹 “ 𝑦)) ∈ ℝ)
106	87, 105	eqeltrd 2829	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol‘(◡𝐹 “ 𝑦)) ∈ ℝ)
107	106	ex 412	. . . . 5 ⊢ (𝜑 → (¬ 0 ∈ 𝑦 → (vol‘(◡𝐹 “ 𝑦)) ∈ ℝ))
108	107	alrimiv 1923	. . . 4 ⊢ (𝜑 → ∀𝑦(¬ 0 ∈ 𝑦 → (vol‘(◡𝐹 “ 𝑦)) ∈ ℝ))
109		neldifsn 4796	. . . 4 ⊢ ¬ 0 ∈ (ℝ ∖ {0})
110	60	difexi 5330	. . . . 5 ⊢ (ℝ ∖ {0}) ∈ V
111		eleq2 2818	. . . . . . 7 ⊢ (𝑦 = (ℝ ∖ {0}) → (0 ∈ 𝑦 ↔ 0 ∈ (ℝ ∖ {0})))
112	111	notbid 318	. . . . . 6 ⊢ (𝑦 = (ℝ ∖ {0}) → (¬ 0 ∈ 𝑦 ↔ ¬ 0 ∈ (ℝ ∖ {0})))
113		imaeq2 6059	. . . . . . . 8 ⊢ (𝑦 = (ℝ ∖ {0}) → (◡𝐹 “ 𝑦) = (◡𝐹 “ (ℝ ∖ {0})))
114	113	fveq2d 6901	. . . . . . 7 ⊢ (𝑦 = (ℝ ∖ {0}) → (vol‘(◡𝐹 “ 𝑦)) = (vol‘(◡𝐹 “ (ℝ ∖ {0}))))
115	114	eleq1d 2814	. . . . . 6 ⊢ (𝑦 = (ℝ ∖ {0}) → ((vol‘(◡𝐹 “ 𝑦)) ∈ ℝ ↔ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ))
116	112, 115	imbi12d 344	. . . . 5 ⊢ (𝑦 = (ℝ ∖ {0}) → ((¬ 0 ∈ 𝑦 → (vol‘(◡𝐹 “ 𝑦)) ∈ ℝ) ↔ (¬ 0 ∈ (ℝ ∖ {0}) → (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ)))
117	110, 116	spcv 3592	. . . 4 ⊢ (∀𝑦(¬ 0 ∈ 𝑦 → (vol‘(◡𝐹 “ 𝑦)) ∈ ℝ) → (¬ 0 ∈ (ℝ ∖ {0}) → (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ))
118	108, 109, 117	mpisyl 21	. . 3 ⊢ (𝜑 → (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ)
119	1, 34, 118	3jca 1126	. 2 ⊢ (𝜑 → (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ))
120		isi1f 25602	. 2 ⊢ (𝐹 ∈ dom ∫1 ↔ (𝐹 ∈ MblFn ∧ (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ)))
121	85, 119, 120	sylanbrc 582	1 ⊢ (𝜑 → 𝐹 ∈ dom ∫1)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085  ∀wal 1532   = wceq 1534   ∈ wcel 2099  ∀wral 3058   ∖ cdif 3944   ∩ cin 3946   ⊆ wss 3947  ∅c0 4323  𝒫 cpw 4603  {csn 4629  ∪ ciun 4996   class class class wbr 5148   × cxp 5676  ^◡ccnv 5677  dom cdm 5678  ran crn 5679   “ cima 5681  Fun wfun 6542  ⟶wf 6544  ‘cfv 6548  Fincfn 8963  ℝcr 11137  0cc0 11138  ℝ^*cxr 11277   ≤ cle 11279  (,)cioo 13356  Σcsu 15664  vol*covol 25390  volcvol 25391  MblFncmbf 25542  ∫₁citg1 25543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740  ax-inf2 9664  ax-cnex 11194  ax-resscn 11195  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-addrcl 11199  ax-mulcl 11200  ax-mulrcl 11201  ax-mulcom 11202  ax-addass 11203  ax-mulass 11204  ax-distr 11205  ax-i2m1 11206  ax-1ne0 11207  ax-1rid 11208  ax-rnegex 11209  ax-rrecex 11210  ax-cnre 11211  ax-pre-lttri 11212  ax-pre-lttrn 11213  ax-pre-ltadd 11214  ax-pre-mulgt0 11215  ax-pre-sup 11216

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3373  df-reu 3374  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-int 4950  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-se 5634  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6305  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-isom 6557  df-riota 7376  df-ov 7423  df-oprab 7424  df-mpo 7425  df-of 7685  df-om 7871  df-1st 7993  df-2nd 7994  df-frecs 8286  df-wrecs 8317  df-recs 8391  df-rdg 8430  df-1o 8486  df-2o 8487  df-er 8724  df-map 8846  df-pm 8847  df-en 8964  df-dom 8965  df-sdom 8966  df-fin 8967  df-sup 9465  df-inf 9466  df-oi 9533  df-dju 9924  df-card 9962  df-pnf 11280  df-mnf 11281  df-xr 11282  df-ltxr 11283  df-le 11284  df-sub 11476  df-neg 11477  df-div 11902  df-nn 12243  df-2 12305  df-3 12306  df-n0 12503  df-z 12589  df-uz 12853  df-q 12963  df-rp 13007  df-xadd 13125  df-ioo 13360  df-ico 13362  df-icc 13363  df-fz 13517  df-fzo 13660  df-fl 13789  df-seq 13999  df-exp 14059  df-hash 14322  df-cj 15078  df-re 15079  df-im 15080  df-sqrt 15214  df-abs 15215  df-clim 15464  df-sum 15665  df-xmet 21271  df-met 21272  df-ovol 25392  df-vol 25393  df-mbf 25547  df-itg1 25548

This theorem is referenced by:  i1f0  25615  i1f1  25618  i1fadd  25623  i1fmul  25624  i1fmulc  25632  i1fres  25634  mbfi1fseqlem4  25647  itg2addnclem2  37145  ftc1anclem3  37168