Theorem i1fd 24285

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 6490	. . . . . . . 8 ⊢ (𝐹:ℝ⟶ℝ → Fun 𝐹)
4		funcnvcnv 6391	. . . . . . . 8 ⊢ (Fun 𝐹 → Fun ◡◡𝐹)
5		imadif 6408	. . . . . . . 8 ⊢ (Fun ◡◡𝐹 → (◡𝐹 “ (ℝ ∖ (ℝ ∖ 𝑥))) = ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥))))
6	2, 3, 4, 5	4syl 19	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ (ℝ ∖ (ℝ ∖ 𝑥))) = ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥))))
7		ioof 12825	. . . . . . . . . . . . 13 ⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ
8		frn 6493	. . . . . . . . . . . . 13 ⊢ ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → ran (,) ⊆ 𝒫 ℝ)
9	7, 8	ax-mp 5	. . . . . . . . . . . 12 ⊢ ran (,) ⊆ 𝒫 ℝ
10	9	sseli 3911	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ran (,) → 𝑥 ∈ 𝒫 ℝ)
11	10	elpwid 4508	. . . . . . . . . 10 ⊢ (𝑥 ∈ ran (,) → 𝑥 ⊆ ℝ)
12	11	ad2antlr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → 𝑥 ⊆ ℝ)
13		dfss4 4185	. . . . . . . . 9 ⊢ (𝑥 ⊆ ℝ ↔ (ℝ ∖ (ℝ ∖ 𝑥)) = 𝑥)
14	12, 13	sylib 221	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (ℝ ∖ (ℝ ∖ 𝑥)) = 𝑥)
15	14	imaeq2d 5896	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ (ℝ ∖ (ℝ ∖ 𝑥))) = (◡𝐹 “ 𝑥))
16	6, 15	eqtr3d 2835	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥))) = (◡𝐹 “ 𝑥))
17		fimacnv 6816	. . . . . . . . 9 ⊢ (𝐹:ℝ⟶ℝ → (◡𝐹 “ ℝ) = ℝ)
18	2, 17	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ ℝ) = ℝ)
19		rembl 24144	. . . . . . . 8 ⊢ ℝ ∈ dom vol
20	18, 19	eqeltrdi 2898	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ ℝ) ∈ dom vol)
21	1	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → 𝐹:ℝ⟶ℝ)
22		inpreima 6811	. . . . . . . . . . . . . 14 ⊢ (Fun 𝐹 → (◡𝐹 “ (𝑦 ∩ ran 𝐹)) = ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ ran 𝐹)))
23		iunid 4947	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹){𝑥} = (𝑦 ∩ ran 𝐹)
24	23	imaeq2i 5894	. . . . . . . . . . . . . . 15 ⊢ (◡𝐹 “ ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹){𝑥}) = (◡𝐹 “ (𝑦 ∩ ran 𝐹))
25		imaiun 6982	. . . . . . . . . . . . . . 15 ⊢ (◡𝐹 “ ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹){𝑥}) = ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥})
26	24, 25	eqtr3i 2823	. . . . . . . . . . . . . 14 ⊢ (◡𝐹 “ (𝑦 ∩ ran 𝐹)) = ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥})
27		cnvimass 5916	. . . . . . . . . . . . . . . 16 ⊢ (◡𝐹 “ 𝑦) ⊆ dom 𝐹
28		cnvimarndm 5917	. . . . . . . . . . . . . . . 16 ⊢ (◡𝐹 “ ran 𝐹) = dom 𝐹
29	27, 28	sseqtrri 3952	. . . . . . . . . . . . . . 15 ⊢ (◡𝐹 “ 𝑦) ⊆ (◡𝐹 “ ran 𝐹)
30		df-ss 3898	. . . . . . . . . . . . . . 15 ⊢ ((◡𝐹 “ 𝑦) ⊆ (◡𝐹 “ ran 𝐹) ↔ ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ ran 𝐹)) = (◡𝐹 “ 𝑦))
31	29, 30	mpbi 233	. . . . . . . . . . . . . 14 ⊢ ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ ran 𝐹)) = (◡𝐹 “ 𝑦)
32	22, 26, 31	3eqtr3g 2856	. . . . . . . . . . . . 13 ⊢ (Fun 𝐹 → ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) = (◡𝐹 “ 𝑦))
33	21, 3, 32	3syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) = (◡𝐹 “ 𝑦))
34		i1fd.2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ran 𝐹 ∈ Fin)
35	34	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ran 𝐹 ∈ Fin)
36		inss2 4156	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∩ ran 𝐹) ⊆ ran 𝐹
37		ssfi 8722	. . . . . . . . . . . . . 14 ⊢ ((ran 𝐹 ∈ Fin ∧ (𝑦 ∩ ran 𝐹) ⊆ ran 𝐹) → (𝑦 ∩ ran 𝐹) ∈ Fin)
38	35, 36, 37	sylancl 589	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (𝑦 ∩ ran 𝐹) ∈ Fin)
39		simpll 766	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → 𝜑)
40		elinel1 4122	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ (𝑦 ∩ ran 𝐹) → 0 ∈ 𝑦)
41	40	con3i 157	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 0 ∈ 𝑦 → ¬ 0 ∈ (𝑦 ∩ ran 𝐹))
42	41	adantl 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ¬ 0 ∈ (𝑦 ∩ ran 𝐹))
43		disjsn 4607	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∩ ran 𝐹) ∩ {0}) = ∅ ↔ ¬ 0 ∈ (𝑦 ∩ ran 𝐹))
44	42, 43	sylibr 237	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ((𝑦 ∩ ran 𝐹) ∩ {0}) = ∅)
45		reldisj 4359	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∩ ran 𝐹) ⊆ ran 𝐹 → (((𝑦 ∩ ran 𝐹) ∩ {0}) = ∅ ↔ (𝑦 ∩ ran 𝐹) ⊆ (ran 𝐹 ∖ {0})))
46	36, 45	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∩ ran 𝐹) ∩ {0}) = ∅ ↔ (𝑦 ∩ ran 𝐹) ⊆ (ran 𝐹 ∖ {0}))
47	44, 46	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (𝑦 ∩ ran 𝐹) ⊆ (ran 𝐹 ∖ {0}))
48	47	sselda 3915	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → 𝑥 ∈ (ran 𝐹 ∖ {0}))
49		i1fd.3	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ {0})) → (◡𝐹 “ {𝑥}) ∈ dom vol)
50	39, 48, 49	syl2anc 587	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → (◡𝐹 “ {𝑥}) ∈ dom vol)
51	50	ralrimiva 3149	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ∀𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) ∈ dom vol)
52		finiunmbl 24148	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∩ ran 𝐹) ∈ Fin ∧ ∀𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) ∈ dom vol) → ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) ∈ dom vol)
53	38, 51, 52	syl2anc 587	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) ∈ dom vol)
54	33, 53	eqeltrrd 2891	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (◡𝐹 “ 𝑦) ∈ dom vol)
55	54	ex 416	. . . . . . . . . 10 ⊢ (𝜑 → (¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol))
56	55	alrimiv 1928	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑦(¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol))
57	56	ad2antrr 725	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → ∀𝑦(¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol))
58		elndif 4056	. . . . . . . . 9 ⊢ (0 ∈ 𝑥 → ¬ 0 ∈ (ℝ ∖ 𝑥))
59	58	adantl 485	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → ¬ 0 ∈ (ℝ ∖ 𝑥))
60		reex 10617	. . . . . . . . . 10 ⊢ ℝ ∈ V
61	60	difexi 5196	. . . . . . . . 9 ⊢ (ℝ ∖ 𝑥) ∈ V
62		eleq2 2878	. . . . . . . . . . 11 ⊢ (𝑦 = (ℝ ∖ 𝑥) → (0 ∈ 𝑦 ↔ 0 ∈ (ℝ ∖ 𝑥)))
63	62	notbid 321	. . . . . . . . . 10 ⊢ (𝑦 = (ℝ ∖ 𝑥) → (¬ 0 ∈ 𝑦 ↔ ¬ 0 ∈ (ℝ ∖ 𝑥)))
64		imaeq2 5892	. . . . . . . . . . 11 ⊢ (𝑦 = (ℝ ∖ 𝑥) → (◡𝐹 “ 𝑦) = (◡𝐹 “ (ℝ ∖ 𝑥)))
65	64	eleq1d 2874	. . . . . . . . . 10 ⊢ (𝑦 = (ℝ ∖ 𝑥) → ((◡𝐹 “ 𝑦) ∈ dom vol ↔ (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol))
66	63, 65	imbi12d 348	. . . . . . . . 9 ⊢ (𝑦 = (ℝ ∖ 𝑥) → ((¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol) ↔ (¬ 0 ∈ (ℝ ∖ 𝑥) → (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol)))
67	61, 66	spcv 3554	. . . . . . . 8 ⊢ (∀𝑦(¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol) → (¬ 0 ∈ (ℝ ∖ 𝑥) → (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol))
68	57, 59, 67	sylc 65	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol)
69		difmbl 24147	. . . . . . 7 ⊢ (((◡𝐹 “ ℝ) ∈ dom vol ∧ (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol) → ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥))) ∈ dom vol)
70	20, 68, 69	syl2anc 587	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥))) ∈ dom vol)
71	16, 70	eqeltrrd 2891	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ 𝑥) ∈ dom vol)
72		eleq2 2878	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → (0 ∈ 𝑦 ↔ 0 ∈ 𝑥))
73	72	notbid 321	. . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → (¬ 0 ∈ 𝑦 ↔ ¬ 0 ∈ 𝑥))
74		imaeq2 5892	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → (◡𝐹 “ 𝑦) = (◡𝐹 “ 𝑥))
75	74	eleq1d 2874	. . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → ((◡𝐹 “ 𝑦) ∈ dom vol ↔ (◡𝐹 “ 𝑥) ∈ dom vol))
76	73, 75	imbi12d 348	. . . . . . . . 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 410	. . . . . 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 3149	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol)
83		ismbf 24232	. . . 4 ⊢ (𝐹:ℝ⟶ℝ → (𝐹 ∈ MblFn ↔ ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol))
84	1, 83	syl 17	. . 3 ⊢ (𝜑 → (𝐹 ∈ MblFn ↔ ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol))
85	82, 84	mpbird 260	. 2 ⊢ (𝜑 → 𝐹 ∈ MblFn)
86		mblvol 24134	. . . . . . . 8 ⊢ ((◡𝐹 “ 𝑦) ∈ dom vol → (vol‘(◡𝐹 “ 𝑦)) = (vol*‘(◡𝐹 “ 𝑦)))
87	54, 86	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol‘(◡𝐹 “ 𝑦)) = (vol*‘(◡𝐹 “ 𝑦)))
88		mblss 24135	. . . . . . . . 9 ⊢ ((◡𝐹 “ 𝑦) ∈ dom vol → (◡𝐹 “ 𝑦) ⊆ ℝ)
89	54, 88	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (◡𝐹 “ 𝑦) ⊆ ℝ)
90		mblvol 24134	. . . . . . . . . . 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 587	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → (vol‘(◡𝐹 “ {𝑥})) ∈ ℝ)
94	91, 93	eqeltrrd 2891	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → (vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ)
95	38, 94	fsumrecl 15083	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ)
96	33	fveq2d 6649	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol*‘∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥})) = (vol*‘(◡𝐹 “ 𝑦)))
97		mblss 24135	. . . . . . . . . . . . 13 ⊢ ((◡𝐹 “ {𝑥}) ∈ dom vol → (◡𝐹 “ {𝑥}) ⊆ ℝ)
98	50, 97	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → (◡𝐹 “ {𝑥}) ⊆ ℝ)
99	98, 94	jca 515	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → ((◡𝐹 “ {𝑥}) ⊆ ℝ ∧ (vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ))
100	99	ralrimiva 3149	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ∀𝑥 ∈ (𝑦 ∩ ran 𝐹)((◡𝐹 “ {𝑥}) ⊆ ℝ ∧ (vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ))
101		ovolfiniun 24105	. . . . . . . . . 10 ⊢ (((𝑦 ∩ ran 𝐹) ∈ Fin ∧ ∀𝑥 ∈ (𝑦 ∩ ran 𝐹)((◡𝐹 “ {𝑥}) ⊆ ℝ ∧ (vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ)) → (vol*‘∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥})) ≤ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥})))
102	38, 100, 101	syl2anc 587	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol*‘∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥})) ≤ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥})))
103	96, 102	eqbrtrrd 5054	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol*‘(◡𝐹 “ 𝑦)) ≤ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥})))
104		ovollecl 24087	. . . . . . . 8 ⊢ (((◡𝐹 “ 𝑦) ⊆ ℝ ∧ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ ∧ (vol*‘(◡𝐹 “ 𝑦)) ≤ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥}))) → (vol*‘(◡𝐹 “ 𝑦)) ∈ ℝ)
105	89, 95, 103, 104	syl3anc 1368	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol*‘(◡𝐹 “ 𝑦)) ∈ ℝ)
106	87, 105	eqeltrd 2890	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol‘(◡𝐹 “ 𝑦)) ∈ ℝ)
107	106	ex 416	. . . . 5 ⊢ (𝜑 → (¬ 0 ∈ 𝑦 → (vol‘(◡𝐹 “ 𝑦)) ∈ ℝ))
108	107	alrimiv 1928	. . . 4 ⊢ (𝜑 → ∀𝑦(¬ 0 ∈ 𝑦 → (vol‘(◡𝐹 “ 𝑦)) ∈ ℝ))
109		neldifsn 4685	. . . 4 ⊢ ¬ 0 ∈ (ℝ ∖ {0})
110	60	difexi 5196	. . . . 5 ⊢ (ℝ ∖ {0}) ∈ V
111		eleq2 2878	. . . . . . 7 ⊢ (𝑦 = (ℝ ∖ {0}) → (0 ∈ 𝑦 ↔ 0 ∈ (ℝ ∖ {0})))
112	111	notbid 321	. . . . . 6 ⊢ (𝑦 = (ℝ ∖ {0}) → (¬ 0 ∈ 𝑦 ↔ ¬ 0 ∈ (ℝ ∖ {0})))
113		imaeq2 5892	. . . . . . . 8 ⊢ (𝑦 = (ℝ ∖ {0}) → (◡𝐹 “ 𝑦) = (◡𝐹 “ (ℝ ∖ {0})))
114	113	fveq2d 6649	. . . . . . 7 ⊢ (𝑦 = (ℝ ∖ {0}) → (vol‘(◡𝐹 “ 𝑦)) = (vol‘(◡𝐹 “ (ℝ ∖ {0}))))
115	114	eleq1d 2874	. . . . . 6 ⊢ (𝑦 = (ℝ ∖ {0}) → ((vol‘(◡𝐹 “ 𝑦)) ∈ ℝ ↔ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ))
116	112, 115	imbi12d 348	. . . . 5 ⊢ (𝑦 = (ℝ ∖ {0}) → ((¬ 0 ∈ 𝑦 → (vol‘(◡𝐹 “ 𝑦)) ∈ ℝ) ↔ (¬ 0 ∈ (ℝ ∖ {0}) → (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ)))
117	110, 116	spcv 3554	. . . 4 ⊢ (∀𝑦(¬ 0 ∈ 𝑦 → (vol‘(◡𝐹 “ 𝑦)) ∈ ℝ) → (¬ 0 ∈ (ℝ ∖ {0}) → (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ))
118	108, 109, 117	mpisyl 21	. . 3 ⊢ (𝜑 → (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ)
119	1, 34, 118	3jca 1125	. 2 ⊢ (𝜑 → (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ))
120		isi1f 24278	. 2 ⊢ (𝐹 ∈ dom ∫1 ↔ (𝐹 ∈ MblFn ∧ (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ)))
121	85, 119, 120	sylanbrc 586	1 ⊢ (𝜑 → 𝐹 ∈ dom ∫1)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084  ∀wal 1536   = wceq 1538   ∈ wcel 2111  ∀wral 3106   ∖ cdif 3878   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243  𝒫 cpw 4497  {csn 4525  ∪ ciun 4881   class class class wbr 5030   × cxp 5517  ^◡ccnv 5518  dom cdm 5519  ran crn 5520   “ cima 5522  Fun wfun 6318  ⟶wf 6320  ‘cfv 6324  Fincfn 8492  ℝcr 10525  0cc0 10526  ℝ^*cxr 10663   ≤ cle 10665  (,)cioo 12726  Σcsu 15034  vol*covol 24066  volcvol 24067  MblFncmbf 24218  ∫₁citg1 24219

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-inf2 9088  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-isom 6333  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-of 7389  df-om 7561  df-1st 7671  df-2nd 7672  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-1o 8085  df-2o 8086  df-oadd 8089  df-er 8272  df-map 8391  df-pm 8392  df-en 8493  df-dom 8494  df-sdom 8495  df-fin 8496  df-sup 8890  df-inf 8891  df-oi 8958  df-dju 9314  df-card 9352  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  df-2 11688  df-3 11689  df-n0 11886  df-z 11970  df-uz 12232  df-q 12337  df-rp 12378  df-xadd 12496  df-ioo 12730  df-ico 12732  df-icc 12733  df-fz 12886  df-fzo 13029  df-fl 13157  df-seq 13365  df-exp 13426  df-hash 13687  df-cj 14450  df-re 14451  df-im 14452  df-sqrt 14586  df-abs 14587  df-clim 14837  df-sum 15035  df-xmet 20084  df-met 20085  df-ovol 24068  df-vol 24069  df-mbf 24223  df-itg1 24224

This theorem is referenced by:  i1f0  24291  i1f1  24294  i1fadd  24299  i1fmul  24300  i1fmulc  24307  i1fres  24309  mbfi1fseqlem4  24322  itg2addnclem2  35109  ftc1anclem3  35132