Theorem i1fd 24284

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 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → 𝐹:ℝ⟶ℝ)
3		ffun 6519	. . . . . . . 8 ⊢ (𝐹:ℝ⟶ℝ → Fun 𝐹)
4		funcnvcnv 6423	. . . . . . . 8 ⊢ (Fun 𝐹 → Fun ◡◡𝐹)
5		imadif 6440	. . . . . . . 8 ⊢ (Fun ◡◡𝐹 → (◡𝐹 “ (ℝ ∖ (ℝ ∖ 𝑥))) = ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥))))
6	2, 3, 4, 5	4syl 19	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ (ℝ ∖ (ℝ ∖ 𝑥))) = ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥))))
7		ioof 12838	. . . . . . . . . . . . 13 ⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ
8		frn 6522	. . . . . . . . . . . . 13 ⊢ ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → ran (,) ⊆ 𝒫 ℝ)
9	7, 8	ax-mp 5	. . . . . . . . . . . 12 ⊢ ran (,) ⊆ 𝒫 ℝ
10	9	sseli 3965	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ran (,) → 𝑥 ∈ 𝒫 ℝ)
11	10	elpwid 4552	. . . . . . . . . 10 ⊢ (𝑥 ∈ ran (,) → 𝑥 ⊆ ℝ)
12	11	ad2antlr 725	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → 𝑥 ⊆ ℝ)
13		dfss4 4237	. . . . . . . . 9 ⊢ (𝑥 ⊆ ℝ ↔ (ℝ ∖ (ℝ ∖ 𝑥)) = 𝑥)
14	12, 13	sylib 220	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (ℝ ∖ (ℝ ∖ 𝑥)) = 𝑥)
15	14	imaeq2d 5931	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ (ℝ ∖ (ℝ ∖ 𝑥))) = (◡𝐹 “ 𝑥))
16	6, 15	eqtr3d 2860	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥))) = (◡𝐹 “ 𝑥))
17		fimacnv 6841	. . . . . . . . 9 ⊢ (𝐹:ℝ⟶ℝ → (◡𝐹 “ ℝ) = ℝ)
18	2, 17	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ ℝ) = ℝ)
19		rembl 24143	. . . . . . . 8 ⊢ ℝ ∈ dom vol
20	18, 19	eqeltrdi 2923	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ ℝ) ∈ dom vol)
21	1	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → 𝐹:ℝ⟶ℝ)
22		inpreima 6836	. . . . . . . . . . . . . 14 ⊢ (Fun 𝐹 → (◡𝐹 “ (𝑦 ∩ ran 𝐹)) = ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ ran 𝐹)))
23		iunid 4986	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹){𝑥} = (𝑦 ∩ ran 𝐹)
24	23	imaeq2i 5929	. . . . . . . . . . . . . . 15 ⊢ (◡𝐹 “ ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹){𝑥}) = (◡𝐹 “ (𝑦 ∩ ran 𝐹))
25		imaiun 7006	. . . . . . . . . . . . . . 15 ⊢ (◡𝐹 “ ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹){𝑥}) = ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥})
26	24, 25	eqtr3i 2848	. . . . . . . . . . . . . 14 ⊢ (◡𝐹 “ (𝑦 ∩ ran 𝐹)) = ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥})
27		cnvimass 5951	. . . . . . . . . . . . . . . 16 ⊢ (◡𝐹 “ 𝑦) ⊆ dom 𝐹
28		cnvimarndm 5952	. . . . . . . . . . . . . . . 16 ⊢ (◡𝐹 “ ran 𝐹) = dom 𝐹
29	27, 28	sseqtrri 4006	. . . . . . . . . . . . . . 15 ⊢ (◡𝐹 “ 𝑦) ⊆ (◡𝐹 “ ran 𝐹)
30		df-ss 3954	. . . . . . . . . . . . . . 15 ⊢ ((◡𝐹 “ 𝑦) ⊆ (◡𝐹 “ ran 𝐹) ↔ ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ ran 𝐹)) = (◡𝐹 “ 𝑦))
31	29, 30	mpbi 232	. . . . . . . . . . . . . 14 ⊢ ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ ran 𝐹)) = (◡𝐹 “ 𝑦)
32	22, 26, 31	3eqtr3g 2881	. . . . . . . . . . . . 13 ⊢ (Fun 𝐹 → ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) = (◡𝐹 “ 𝑦))
33	21, 3, 32	3syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) = (◡𝐹 “ 𝑦))
34		i1fd.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ran 𝐹 ∈ Fin)
35	34	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ran 𝐹 ∈ Fin)
36		inss2 4208	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∩ ran 𝐹) ⊆ ran 𝐹
37		ssfi 8740	. . . . . . . . . . . . . 14 ⊢ ((ran 𝐹 ∈ Fin ∧ (𝑦 ∩ ran 𝐹) ⊆ ran 𝐹) → (𝑦 ∩ ran 𝐹) ∈ Fin)
38	35, 36, 37	sylancl 588	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (𝑦 ∩ ran 𝐹) ∈ Fin)
39		simpll 765	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → 𝜑)
40		elinel1 4174	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ (𝑦 ∩ ran 𝐹) → 0 ∈ 𝑦)
41	40	con3i 157	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 0 ∈ 𝑦 → ¬ 0 ∈ (𝑦 ∩ ran 𝐹))
42	41	adantl 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ¬ 0 ∈ (𝑦 ∩ ran 𝐹))
43		disjsn 4649	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∩ ran 𝐹) ∩ {0}) = ∅ ↔ ¬ 0 ∈ (𝑦 ∩ ran 𝐹))
44	42, 43	sylibr 236	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ((𝑦 ∩ ran 𝐹) ∩ {0}) = ∅)
45		reldisj 4404	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∩ ran 𝐹) ⊆ ran 𝐹 → (((𝑦 ∩ ran 𝐹) ∩ {0}) = ∅ ↔ (𝑦 ∩ ran 𝐹) ⊆ (ran 𝐹 ∖ {0})))
46	36, 45	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∩ ran 𝐹) ∩ {0}) = ∅ ↔ (𝑦 ∩ ran 𝐹) ⊆ (ran 𝐹 ∖ {0}))
47	44, 46	sylib 220	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (𝑦 ∩ ran 𝐹) ⊆ (ran 𝐹 ∖ {0}))
48	47	sselda 3969	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → 𝑥 ∈ (ran 𝐹 ∖ {0}))
49		i1fd.3	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ {0})) → (◡𝐹 “ {𝑥}) ∈ dom vol)
50	39, 48, 49	syl2anc 586	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → (◡𝐹 “ {𝑥}) ∈ dom vol)
51	50	ralrimiva 3184	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ∀𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) ∈ dom vol)
52		finiunmbl 24147	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∩ ran 𝐹) ∈ Fin ∧ ∀𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) ∈ dom vol) → ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) ∈ dom vol)
53	38, 51, 52	syl2anc 586	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) ∈ dom vol)
54	33, 53	eqeltrrd 2916	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (◡𝐹 “ 𝑦) ∈ dom vol)
55	54	ex 415	. . . . . . . . . 10 ⊢ (𝜑 → (¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol))
56	55	alrimiv 1928	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑦(¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol))
57	56	ad2antrr 724	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → ∀𝑦(¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol))
58		elndif 4107	. . . . . . . . 9 ⊢ (0 ∈ 𝑥 → ¬ 0 ∈ (ℝ ∖ 𝑥))
59	58	adantl 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → ¬ 0 ∈ (ℝ ∖ 𝑥))
60		reex 10630	. . . . . . . . . 10 ⊢ ℝ ∈ V
61	60	difexi 5234	. . . . . . . . 9 ⊢ (ℝ ∖ 𝑥) ∈ V
62		eleq2 2903	. . . . . . . . . . 11 ⊢ (𝑦 = (ℝ ∖ 𝑥) → (0 ∈ 𝑦 ↔ 0 ∈ (ℝ ∖ 𝑥)))
63	62	notbid 320	. . . . . . . . . 10 ⊢ (𝑦 = (ℝ ∖ 𝑥) → (¬ 0 ∈ 𝑦 ↔ ¬ 0 ∈ (ℝ ∖ 𝑥)))
64		imaeq2 5927	. . . . . . . . . . 11 ⊢ (𝑦 = (ℝ ∖ 𝑥) → (◡𝐹 “ 𝑦) = (◡𝐹 “ (ℝ ∖ 𝑥)))
65	64	eleq1d 2899	. . . . . . . . . 10 ⊢ (𝑦 = (ℝ ∖ 𝑥) → ((◡𝐹 “ 𝑦) ∈ dom vol ↔ (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol))
66	63, 65	imbi12d 347	. . . . . . . . 9 ⊢ (𝑦 = (ℝ ∖ 𝑥) → ((¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol) ↔ (¬ 0 ∈ (ℝ ∖ 𝑥) → (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol)))
67	61, 66	spcv 3608	. . . . . . . 8 ⊢ (∀𝑦(¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol) → (¬ 0 ∈ (ℝ ∖ 𝑥) → (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol))
68	57, 59, 67	sylc 65	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol)
69		difmbl 24146	. . . . . . 7 ⊢ (((◡𝐹 “ ℝ) ∈ dom vol ∧ (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol) → ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥))) ∈ dom vol)
70	20, 68, 69	syl2anc 586	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥))) ∈ dom vol)
71	16, 70	eqeltrrd 2916	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ 𝑥) ∈ dom vol)
72		eleq2 2903	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → (0 ∈ 𝑦 ↔ 0 ∈ 𝑥))
73	72	notbid 320	. . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → (¬ 0 ∈ 𝑦 ↔ ¬ 0 ∈ 𝑥))
74		imaeq2 5927	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → (◡𝐹 “ 𝑦) = (◡𝐹 “ 𝑥))
75	74	eleq1d 2899	. . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → ((◡𝐹 “ 𝑦) ∈ dom vol ↔ (◡𝐹 “ 𝑥) ∈ dom vol))
76	73, 75	imbi12d 347	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → ((¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol) ↔ (¬ 0 ∈ 𝑥 → (◡𝐹 “ 𝑥) ∈ dom vol)))
77	76	spvv 2003	. . . . . . . 8 ⊢ (∀𝑦(¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol) → (¬ 0 ∈ 𝑥 → (◡𝐹 “ 𝑥) ∈ dom vol))
78	56, 77	syl 17	. . . . . . 7 ⊢ (𝜑 → (¬ 0 ∈ 𝑥 → (◡𝐹 “ 𝑥) ∈ dom vol))
79	78	imp 409	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑥) → (◡𝐹 “ 𝑥) ∈ dom vol)
80	79	adantlr 713	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ ¬ 0 ∈ 𝑥) → (◡𝐹 “ 𝑥) ∈ dom vol)
81	71, 80	pm2.61dan 811	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ran (,)) → (◡𝐹 “ 𝑥) ∈ dom vol)
82	81	ralrimiva 3184	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol)
83		ismbf 24231	. . . 4 ⊢ (𝐹:ℝ⟶ℝ → (𝐹 ∈ MblFn ↔ ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol))
84	1, 83	syl 17	. . 3 ⊢ (𝜑 → (𝐹 ∈ MblFn ↔ ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol))
85	82, 84	mpbird 259	. 2 ⊢ (𝜑 → 𝐹 ∈ MblFn)
86		mblvol 24133	. . . . . . . 8 ⊢ ((◡𝐹 “ 𝑦) ∈ dom vol → (vol‘(◡𝐹 “ 𝑦)) = (vol*‘(◡𝐹 “ 𝑦)))
87	54, 86	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol‘(◡𝐹 “ 𝑦)) = (vol*‘(◡𝐹 “ 𝑦)))
88		mblss 24134	. . . . . . . . 9 ⊢ ((◡𝐹 “ 𝑦) ∈ dom vol → (◡𝐹 “ 𝑦) ⊆ ℝ)
89	54, 88	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (◡𝐹 “ 𝑦) ⊆ ℝ)
90		mblvol 24133	. . . . . . . . . . 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 586	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → (vol‘(◡𝐹 “ {𝑥})) ∈ ℝ)
94	91, 93	eqeltrrd 2916	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → (vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ)
95	38, 94	fsumrecl 15093	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ)
96	33	fveq2d 6676	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol*‘∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥})) = (vol*‘(◡𝐹 “ 𝑦)))
97		mblss 24134	. . . . . . . . . . . . 13 ⊢ ((◡𝐹 “ {𝑥}) ∈ dom vol → (◡𝐹 “ {𝑥}) ⊆ ℝ)
98	50, 97	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → (◡𝐹 “ {𝑥}) ⊆ ℝ)
99	98, 94	jca 514	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → ((◡𝐹 “ {𝑥}) ⊆ ℝ ∧ (vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ))
100	99	ralrimiva 3184	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ∀𝑥 ∈ (𝑦 ∩ ran 𝐹)((◡𝐹 “ {𝑥}) ⊆ ℝ ∧ (vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ))
101		ovolfiniun 24104	. . . . . . . . . 10 ⊢ (((𝑦 ∩ ran 𝐹) ∈ Fin ∧ ∀𝑥 ∈ (𝑦 ∩ ran 𝐹)((◡𝐹 “ {𝑥}) ⊆ ℝ ∧ (vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ)) → (vol*‘∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥})) ≤ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥})))
102	38, 100, 101	syl2anc 586	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol*‘∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥})) ≤ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥})))
103	96, 102	eqbrtrrd 5092	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol*‘(◡𝐹 “ 𝑦)) ≤ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥})))
104		ovollecl 24086	. . . . . . . 8 ⊢ (((◡𝐹 “ 𝑦) ⊆ ℝ ∧ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ ∧ (vol*‘(◡𝐹 “ 𝑦)) ≤ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥}))) → (vol*‘(◡𝐹 “ 𝑦)) ∈ ℝ)
105	89, 95, 103, 104	syl3anc 1367	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol*‘(◡𝐹 “ 𝑦)) ∈ ℝ)
106	87, 105	eqeltrd 2915	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol‘(◡𝐹 “ 𝑦)) ∈ ℝ)
107	106	ex 415	. . . . 5 ⊢ (𝜑 → (¬ 0 ∈ 𝑦 → (vol‘(◡𝐹 “ 𝑦)) ∈ ℝ))
108	107	alrimiv 1928	. . . 4 ⊢ (𝜑 → ∀𝑦(¬ 0 ∈ 𝑦 → (vol‘(◡𝐹 “ 𝑦)) ∈ ℝ))
109		neldifsn 4727	. . . 4 ⊢ ¬ 0 ∈ (ℝ ∖ {0})
110	60	difexi 5234	. . . . 5 ⊢ (ℝ ∖ {0}) ∈ V
111		eleq2 2903	. . . . . . 7 ⊢ (𝑦 = (ℝ ∖ {0}) → (0 ∈ 𝑦 ↔ 0 ∈ (ℝ ∖ {0})))
112	111	notbid 320	. . . . . 6 ⊢ (𝑦 = (ℝ ∖ {0}) → (¬ 0 ∈ 𝑦 ↔ ¬ 0 ∈ (ℝ ∖ {0})))
113		imaeq2 5927	. . . . . . . 8 ⊢ (𝑦 = (ℝ ∖ {0}) → (◡𝐹 “ 𝑦) = (◡𝐹 “ (ℝ ∖ {0})))
114	113	fveq2d 6676	. . . . . . 7 ⊢ (𝑦 = (ℝ ∖ {0}) → (vol‘(◡𝐹 “ 𝑦)) = (vol‘(◡𝐹 “ (ℝ ∖ {0}))))
115	114	eleq1d 2899	. . . . . 6 ⊢ (𝑦 = (ℝ ∖ {0}) → ((vol‘(◡𝐹 “ 𝑦)) ∈ ℝ ↔ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ))
116	112, 115	imbi12d 347	. . . . 5 ⊢ (𝑦 = (ℝ ∖ {0}) → ((¬ 0 ∈ 𝑦 → (vol‘(◡𝐹 “ 𝑦)) ∈ ℝ) ↔ (¬ 0 ∈ (ℝ ∖ {0}) → (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ)))
117	110, 116	spcv 3608	. . . 4 ⊢ (∀𝑦(¬ 0 ∈ 𝑦 → (vol‘(◡𝐹 “ 𝑦)) ∈ ℝ) → (¬ 0 ∈ (ℝ ∖ {0}) → (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ))
118	108, 109, 117	mpisyl 21	. . 3 ⊢ (𝜑 → (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ)
119	1, 34, 118	3jca 1124	. 2 ⊢ (𝜑 → (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ))
120		isi1f 24277	. 2 ⊢ (𝐹 ∈ dom ∫1 ↔ (𝐹 ∈ MblFn ∧ (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ)))
121	85, 119, 120	sylanbrc 585	1 ⊢ (𝜑 → 𝐹 ∈ dom ∫1)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083  ∀wal 1535   = wceq 1537   ∈ wcel 2114  ∀wral 3140   ∖ cdif 3935   ∩ cin 3937   ⊆ wss 3938  ∅c0 4293  𝒫 cpw 4541  {csn 4569  ∪ ciun 4921   class class class wbr 5068   × cxp 5555  ^◡ccnv 5556  dom cdm 5557  ran crn 5558   “ cima 5560  Fun wfun 6351  ⟶wf 6353  ‘cfv 6357  Fincfn 8511  ℝcr 10538  0cc0 10539  ℝ^*cxr 10676   ≤ cle 10678  (,)cioo 12741  Σcsu 15044  vol*covol 24065  volcvol 24066  MblFncmbf 24217  ∫₁citg1 24218

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-rep 5192  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-inf2 9106  ax-cnex 10595  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-addrcl 10600  ax-mulcl 10601  ax-mulrcl 10602  ax-mulcom 10603  ax-addass 10604  ax-mulass 10605  ax-distr 10606  ax-i2m1 10607  ax-1ne0 10608  ax-1rid 10609  ax-rnegex 10610  ax-rrecex 10611  ax-cnre 10612  ax-pre-lttri 10613  ax-pre-lttrn 10614  ax-pre-ltadd 10615  ax-pre-mulgt0 10616  ax-pre-sup 10617

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-fal 1550  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-ral 3145  df-rex 3146  df-reu 3147  df-rmo 3148  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-int 4879  df-iun 4923  df-br 5069  df-opab 5131  df-mpt 5149  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-se 5517  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-pred 6150  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-isom 6366  df-riota 7116  df-ov 7161  df-oprab 7162  df-mpo 7163  df-of 7411  df-om 7583  df-1st 7691  df-2nd 7692  df-wrecs 7949  df-recs 8010  df-rdg 8048  df-1o 8104  df-2o 8105  df-oadd 8108  df-er 8291  df-map 8410  df-pm 8411  df-en 8512  df-dom 8513  df-sdom 8514  df-fin 8515  df-sup 8908  df-inf 8909  df-oi 8976  df-dju 9332  df-card 9370  df-pnf 10679  df-mnf 10680  df-xr 10681  df-ltxr 10682  df-le 10683  df-sub 10874  df-neg 10875  df-div 11300  df-nn 11641  df-2 11703  df-3 11704  df-n0 11901  df-z 11985  df-uz 12247  df-q 12352  df-rp 12393  df-xadd 12511  df-ioo 12745  df-ico 12747  df-icc 12748  df-fz 12896  df-fzo 13037  df-fl 13165  df-seq 13373  df-exp 13433  df-hash 13694  df-cj 14460  df-re 14461  df-im 14462  df-sqrt 14596  df-abs 14597  df-clim 14847  df-sum 15045  df-xmet 20540  df-met 20541  df-ovol 24067  df-vol 24068  df-mbf 24222  df-itg1 24223

This theorem is referenced by:  i1f0  24290  i1f1  24293  i1fadd  24298  i1fmul  24299  i1fmulc  24306  i1fres  24308  mbfi1fseqlem4  24321  itg2addnclem2  34946  ftc1anclem3  34971