Theorem i1fd 25589

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 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → 𝐹:ℝ⟶ℝ)
3		ffun 6694	. . . . . . . 8 ⊢ (𝐹:ℝ⟶ℝ → Fun 𝐹)
4		funcnvcnv 6586	. . . . . . . 8 ⊢ (Fun 𝐹 → Fun ◡◡𝐹)
5		imadif 6603	. . . . . . . 8 ⊢ (Fun ◡◡𝐹 → (◡𝐹 “ (ℝ ∖ (ℝ ∖ 𝑥))) = ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥))))
6	2, 3, 4, 5	4syl 19	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ (ℝ ∖ (ℝ ∖ 𝑥))) = ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥))))
7		ioof 13415	. . . . . . . . . . . . 13 ⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ
8		frn 6698	. . . . . . . . . . . . 13 ⊢ ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → ran (,) ⊆ 𝒫 ℝ)
9	7, 8	ax-mp 5	. . . . . . . . . . . 12 ⊢ ran (,) ⊆ 𝒫 ℝ
10	9	sseli 3945	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ran (,) → 𝑥 ∈ 𝒫 ℝ)
11	10	elpwid 4575	. . . . . . . . . 10 ⊢ (𝑥 ∈ ran (,) → 𝑥 ⊆ ℝ)
12	11	ad2antlr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → 𝑥 ⊆ ℝ)
13		dfss4 4235	. . . . . . . . 9 ⊢ (𝑥 ⊆ ℝ ↔ (ℝ ∖ (ℝ ∖ 𝑥)) = 𝑥)
14	12, 13	sylib 218	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (ℝ ∖ (ℝ ∖ 𝑥)) = 𝑥)
15	14	imaeq2d 6034	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ (ℝ ∖ (ℝ ∖ 𝑥))) = (◡𝐹 “ 𝑥))
16	6, 15	eqtr3d 2767	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥))) = (◡𝐹 “ 𝑥))
17		fimacnv 6713	. . . . . . . . 9 ⊢ (𝐹:ℝ⟶ℝ → (◡𝐹 “ ℝ) = ℝ)
18	2, 17	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ ℝ) = ℝ)
19		rembl 25448	. . . . . . . 8 ⊢ ℝ ∈ dom vol
20	18, 19	eqeltrdi 2837	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ ℝ) ∈ dom vol)
21	1	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → 𝐹:ℝ⟶ℝ)
22		inpreima 7039	. . . . . . . . . . . . . 14 ⊢ (Fun 𝐹 → (◡𝐹 “ (𝑦 ∩ ran 𝐹)) = ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ ran 𝐹)))
23		iunid 5027	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹){𝑥} = (𝑦 ∩ ran 𝐹)
24	23	imaeq2i 6032	. . . . . . . . . . . . . . 15 ⊢ (◡𝐹 “ ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹){𝑥}) = (◡𝐹 “ (𝑦 ∩ ran 𝐹))
25		imaiun 7222	. . . . . . . . . . . . . . 15 ⊢ (◡𝐹 “ ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹){𝑥}) = ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥})
26	24, 25	eqtr3i 2755	. . . . . . . . . . . . . 14 ⊢ (◡𝐹 “ (𝑦 ∩ ran 𝐹)) = ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥})
27		cnvimass 6056	. . . . . . . . . . . . . . . 16 ⊢ (◡𝐹 “ 𝑦) ⊆ dom 𝐹
28		cnvimarndm 6057	. . . . . . . . . . . . . . . 16 ⊢ (◡𝐹 “ ran 𝐹) = dom 𝐹
29	27, 28	sseqtrri 3999	. . . . . . . . . . . . . . 15 ⊢ (◡𝐹 “ 𝑦) ⊆ (◡𝐹 “ ran 𝐹)
30		dfss2 3935	. . . . . . . . . . . . . . 15 ⊢ ((◡𝐹 “ 𝑦) ⊆ (◡𝐹 “ ran 𝐹) ↔ ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ ran 𝐹)) = (◡𝐹 “ 𝑦))
31	29, 30	mpbi 230	. . . . . . . . . . . . . 14 ⊢ ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ ran 𝐹)) = (◡𝐹 “ 𝑦)
32	22, 26, 31	3eqtr3g 2788	. . . . . . . . . . . . 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 4204	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∩ ran 𝐹) ⊆ ran 𝐹
37		ssfi 9143	. . . . . . . . . . . . . 14 ⊢ ((ran 𝐹 ∈ Fin ∧ (𝑦 ∩ ran 𝐹) ⊆ ran 𝐹) → (𝑦 ∩ ran 𝐹) ∈ Fin)
38	35, 36, 37	sylancl 586	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (𝑦 ∩ ran 𝐹) ∈ Fin)
39		simpll 766	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → 𝜑)
40		elinel1 4167	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ (𝑦 ∩ ran 𝐹) → 0 ∈ 𝑦)
41	40	con3i 154	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 0 ∈ 𝑦 → ¬ 0 ∈ (𝑦 ∩ ran 𝐹))
42	41	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ¬ 0 ∈ (𝑦 ∩ ran 𝐹))
43		disjsn 4678	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∩ ran 𝐹) ∩ {0}) = ∅ ↔ ¬ 0 ∈ (𝑦 ∩ ran 𝐹))
44	42, 43	sylibr 234	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ((𝑦 ∩ ran 𝐹) ∩ {0}) = ∅)
45		reldisj 4419	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∩ ran 𝐹) ⊆ ran 𝐹 → (((𝑦 ∩ ran 𝐹) ∩ {0}) = ∅ ↔ (𝑦 ∩ ran 𝐹) ⊆ (ran 𝐹 ∖ {0})))
46	36, 45	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∩ ran 𝐹) ∩ {0}) = ∅ ↔ (𝑦 ∩ ran 𝐹) ⊆ (ran 𝐹 ∖ {0}))
47	44, 46	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (𝑦 ∩ ran 𝐹) ⊆ (ran 𝐹 ∖ {0}))
48	47	sselda 3949	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → 𝑥 ∈ (ran 𝐹 ∖ {0}))
49		i1fd.3	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ {0})) → (◡𝐹 “ {𝑥}) ∈ dom vol)
50	39, 48, 49	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → (◡𝐹 “ {𝑥}) ∈ dom vol)
51	50	ralrimiva 3126	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ∀𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) ∈ dom vol)
52		finiunmbl 25452	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∩ ran 𝐹) ∈ Fin ∧ ∀𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) ∈ dom vol) → ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) ∈ dom vol)
53	38, 51, 52	syl2anc 584	. . . . . . . . . . . 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 1927	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑦(¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol))
57	56	ad2antrr 726	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → ∀𝑦(¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol))
58		elndif 4099	. . . . . . . . 9 ⊢ (0 ∈ 𝑥 → ¬ 0 ∈ (ℝ ∖ 𝑥))
59	58	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → ¬ 0 ∈ (ℝ ∖ 𝑥))
60		reex 11166	. . . . . . . . . 10 ⊢ ℝ ∈ V
61	60	difexi 5288	. . . . . . . . 9 ⊢ (ℝ ∖ 𝑥) ∈ V
62		eleq2 2818	. . . . . . . . . . 11 ⊢ (𝑦 = (ℝ ∖ 𝑥) → (0 ∈ 𝑦 ↔ 0 ∈ (ℝ ∖ 𝑥)))
63	62	notbid 318	. . . . . . . . . 10 ⊢ (𝑦 = (ℝ ∖ 𝑥) → (¬ 0 ∈ 𝑦 ↔ ¬ 0 ∈ (ℝ ∖ 𝑥)))
64		imaeq2 6030	. . . . . . . . . . 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 3574	. . . . . . . 8 ⊢ (∀𝑦(¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol) → (¬ 0 ∈ (ℝ ∖ 𝑥) → (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol))
68	57, 59, 67	sylc 65	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol)
69		difmbl 25451	. . . . . . 7 ⊢ (((◡𝐹 “ ℝ) ∈ dom vol ∧ (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol) → ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥))) ∈ dom vol)
70	20, 68, 69	syl2anc 584	. . . . . 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 6030	. . . . . . . . . . 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 1988	. . . . . . . 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 715	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ ¬ 0 ∈ 𝑥) → (◡𝐹 “ 𝑥) ∈ dom vol)
81	71, 80	pm2.61dan 812	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ran (,)) → (◡𝐹 “ 𝑥) ∈ dom vol)
82	81	ralrimiva 3126	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol)
83		ismbf 25536	. . . 4 ⊢ (𝐹:ℝ⟶ℝ → (𝐹 ∈ MblFn ↔ ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol))
84	1, 83	syl 17	. . 3 ⊢ (𝜑 → (𝐹 ∈ MblFn ↔ ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol))
85	82, 84	mpbird 257	. 2 ⊢ (𝜑 → 𝐹 ∈ MblFn)
86		mblvol 25438	. . . . . . . 8 ⊢ ((◡𝐹 “ 𝑦) ∈ dom vol → (vol‘(◡𝐹 “ 𝑦)) = (vol*‘(◡𝐹 “ 𝑦)))
87	54, 86	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol‘(◡𝐹 “ 𝑦)) = (vol*‘(◡𝐹 “ 𝑦)))
88		mblss 25439	. . . . . . . . 9 ⊢ ((◡𝐹 “ 𝑦) ∈ dom vol → (◡𝐹 “ 𝑦) ⊆ ℝ)
89	54, 88	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (◡𝐹 “ 𝑦) ⊆ ℝ)
90		mblvol 25438	. . . . . . . . . . 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 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → (vol‘(◡𝐹 “ {𝑥})) ∈ ℝ)
94	91, 93	eqeltrrd 2830	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → (vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ)
95	38, 94	fsumrecl 15707	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ)
96	33	fveq2d 6865	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol*‘∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥})) = (vol*‘(◡𝐹 “ 𝑦)))
97		mblss 25439	. . . . . . . . . . . . 13 ⊢ ((◡𝐹 “ {𝑥}) ∈ dom vol → (◡𝐹 “ {𝑥}) ⊆ ℝ)
98	50, 97	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → (◡𝐹 “ {𝑥}) ⊆ ℝ)
99	98, 94	jca 511	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → ((◡𝐹 “ {𝑥}) ⊆ ℝ ∧ (vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ))
100	99	ralrimiva 3126	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ∀𝑥 ∈ (𝑦 ∩ ran 𝐹)((◡𝐹 “ {𝑥}) ⊆ ℝ ∧ (vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ))
101		ovolfiniun 25409	. . . . . . . . . 10 ⊢ (((𝑦 ∩ ran 𝐹) ∈ Fin ∧ ∀𝑥 ∈ (𝑦 ∩ ran 𝐹)((◡𝐹 “ {𝑥}) ⊆ ℝ ∧ (vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ)) → (vol*‘∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥})) ≤ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥})))
102	38, 100, 101	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol*‘∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥})) ≤ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥})))
103	96, 102	eqbrtrrd 5134	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol*‘(◡𝐹 “ 𝑦)) ≤ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥})))
104		ovollecl 25391	. . . . . . . 8 ⊢ (((◡𝐹 “ 𝑦) ⊆ ℝ ∧ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ ∧ (vol*‘(◡𝐹 “ 𝑦)) ≤ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥}))) → (vol*‘(◡𝐹 “ 𝑦)) ∈ ℝ)
105	89, 95, 103, 104	syl3anc 1373	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol*‘(◡𝐹 “ 𝑦)) ∈ ℝ)
106	87, 105	eqeltrd 2829	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol‘(◡𝐹 “ 𝑦)) ∈ ℝ)
107	106	ex 412	. . . . 5 ⊢ (𝜑 → (¬ 0 ∈ 𝑦 → (vol‘(◡𝐹 “ 𝑦)) ∈ ℝ))
108	107	alrimiv 1927	. . . 4 ⊢ (𝜑 → ∀𝑦(¬ 0 ∈ 𝑦 → (vol‘(◡𝐹 “ 𝑦)) ∈ ℝ))
109		neldifsn 4759	. . . 4 ⊢ ¬ 0 ∈ (ℝ ∖ {0})
110	60	difexi 5288	. . . . 5 ⊢ (ℝ ∖ {0}) ∈ V
111		eleq2 2818	. . . . . . 7 ⊢ (𝑦 = (ℝ ∖ {0}) → (0 ∈ 𝑦 ↔ 0 ∈ (ℝ ∖ {0})))
112	111	notbid 318	. . . . . 6 ⊢ (𝑦 = (ℝ ∖ {0}) → (¬ 0 ∈ 𝑦 ↔ ¬ 0 ∈ (ℝ ∖ {0})))
113		imaeq2 6030	. . . . . . . 8 ⊢ (𝑦 = (ℝ ∖ {0}) → (◡𝐹 “ 𝑦) = (◡𝐹 “ (ℝ ∖ {0})))
114	113	fveq2d 6865	. . . . . . 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 3574	. . . 4 ⊢ (∀𝑦(¬ 0 ∈ 𝑦 → (vol‘(◡𝐹 “ 𝑦)) ∈ ℝ) → (¬ 0 ∈ (ℝ ∖ {0}) → (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ))
118	108, 109, 117	mpisyl 21	. . 3 ⊢ (𝜑 → (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ)
119	1, 34, 118	3jca 1128	. 2 ⊢ (𝜑 → (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ))
120		isi1f 25582	. 2 ⊢ (𝐹 ∈ dom ∫1 ↔ (𝐹 ∈ MblFn ∧ (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ)))
121	85, 119, 120	sylanbrc 583	1 ⊢ (𝜑 → 𝐹 ∈ dom ∫1)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086  ∀wal 1538   = wceq 1540   ∈ wcel 2109  ∀wral 3045   ∖ cdif 3914   ∩ cin 3916   ⊆ wss 3917  ∅c0 4299  𝒫 cpw 4566  {csn 4592  ∪ ciun 4958   class class class wbr 5110   × cxp 5639  ^◡ccnv 5640  dom cdm 5641  ran crn 5642   “ cima 5644  Fun wfun 6508  ⟶wf 6510  ‘cfv 6514  Fincfn 8921  ℝcr 11074  0cc0 11075  ℝ^*cxr 11214   ≤ cle 11216  (,)cioo 13313  Σcsu 15659  vol*covol 25370  volcvol 25371  MblFncmbf 25522  ∫₁citg1 25523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-inf2 9601  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152  ax-pre-sup 11153

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-int 4914  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-se 5595  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-isom 6523  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-of 7656  df-om 7846  df-1st 7971  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-1o 8437  df-2o 8438  df-er 8674  df-map 8804  df-pm 8805  df-en 8922  df-dom 8923  df-sdom 8924  df-fin 8925  df-sup 9400  df-inf 9401  df-oi 9470  df-dju 9861  df-card 9899  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221  df-sub 11414  df-neg 11415  df-div 11843  df-nn 12194  df-2 12256  df-3 12257  df-n0 12450  df-z 12537  df-uz 12801  df-q 12915  df-rp 12959  df-xadd 13080  df-ioo 13317  df-ico 13319  df-icc 13320  df-fz 13476  df-fzo 13623  df-fl 13761  df-seq 13974  df-exp 14034  df-hash 14303  df-cj 15072  df-re 15073  df-im 15074  df-sqrt 15208  df-abs 15209  df-clim 15461  df-sum 15660  df-xmet 21264  df-met 21265  df-ovol 25372  df-vol 25373  df-mbf 25527  df-itg1 25528

This theorem is referenced by:  i1f0  25595  i1f1  25598  i1fadd  25603  i1fmul  25604  i1fmulc  25611  i1fres  25613  mbfi1fseqlem4  25626  itg2addnclem2  37673  ftc1anclem3  37696