Theorem i1fd 25716

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 6739	. . . . . . . 8 ⊢ (𝐹:ℝ⟶ℝ → Fun 𝐹)
4		funcnvcnv 6633	. . . . . . . 8 ⊢ (Fun 𝐹 → Fun ◡◡𝐹)
5		imadif 6650	. . . . . . . 8 ⊢ (Fun ◡◡𝐹 → (◡𝐹 “ (ℝ ∖ (ℝ ∖ 𝑥))) = ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥))))
6	2, 3, 4, 5	4syl 19	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ (ℝ ∖ (ℝ ∖ 𝑥))) = ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥))))
7		ioof 13487	. . . . . . . . . . . . 13 ⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ
8		frn 6743	. . . . . . . . . . . . 13 ⊢ ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → ran (,) ⊆ 𝒫 ℝ)
9	7, 8	ax-mp 5	. . . . . . . . . . . 12 ⊢ ran (,) ⊆ 𝒫 ℝ
10	9	sseli 3979	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ran (,) → 𝑥 ∈ 𝒫 ℝ)
11	10	elpwid 4609	. . . . . . . . . 10 ⊢ (𝑥 ∈ ran (,) → 𝑥 ⊆ ℝ)
12	11	ad2antlr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → 𝑥 ⊆ ℝ)
13		dfss4 4269	. . . . . . . . 9 ⊢ (𝑥 ⊆ ℝ ↔ (ℝ ∖ (ℝ ∖ 𝑥)) = 𝑥)
14	12, 13	sylib 218	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (ℝ ∖ (ℝ ∖ 𝑥)) = 𝑥)
15	14	imaeq2d 6078	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ (ℝ ∖ (ℝ ∖ 𝑥))) = (◡𝐹 “ 𝑥))
16	6, 15	eqtr3d 2779	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥))) = (◡𝐹 “ 𝑥))
17		fimacnv 6758	. . . . . . . . 9 ⊢ (𝐹:ℝ⟶ℝ → (◡𝐹 “ ℝ) = ℝ)
18	2, 17	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ ℝ) = ℝ)
19		rembl 25575	. . . . . . . 8 ⊢ ℝ ∈ dom vol
20	18, 19	eqeltrdi 2849	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ ℝ) ∈ dom vol)
21	1	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → 𝐹:ℝ⟶ℝ)
22		inpreima 7084	. . . . . . . . . . . . . 14 ⊢ (Fun 𝐹 → (◡𝐹 “ (𝑦 ∩ ran 𝐹)) = ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ ran 𝐹)))
23		iunid 5060	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹){𝑥} = (𝑦 ∩ ran 𝐹)
24	23	imaeq2i 6076	. . . . . . . . . . . . . . 15 ⊢ (◡𝐹 “ ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹){𝑥}) = (◡𝐹 “ (𝑦 ∩ ran 𝐹))
25		imaiun 7265	. . . . . . . . . . . . . . 15 ⊢ (◡𝐹 “ ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹){𝑥}) = ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥})
26	24, 25	eqtr3i 2767	. . . . . . . . . . . . . 14 ⊢ (◡𝐹 “ (𝑦 ∩ ran 𝐹)) = ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥})
27		cnvimass 6100	. . . . . . . . . . . . . . . 16 ⊢ (◡𝐹 “ 𝑦) ⊆ dom 𝐹
28		cnvimarndm 6101	. . . . . . . . . . . . . . . 16 ⊢ (◡𝐹 “ ran 𝐹) = dom 𝐹
29	27, 28	sseqtrri 4033	. . . . . . . . . . . . . . 15 ⊢ (◡𝐹 “ 𝑦) ⊆ (◡𝐹 “ ran 𝐹)
30		dfss2 3969	. . . . . . . . . . . . . . 15 ⊢ ((◡𝐹 “ 𝑦) ⊆ (◡𝐹 “ ran 𝐹) ↔ ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ ran 𝐹)) = (◡𝐹 “ 𝑦))
31	29, 30	mpbi 230	. . . . . . . . . . . . . 14 ⊢ ((◡𝐹 “ 𝑦) ∩ (◡𝐹 “ ran 𝐹)) = (◡𝐹 “ 𝑦)
32	22, 26, 31	3eqtr3g 2800	. . . . . . . . . . . . 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 4238	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∩ ran 𝐹) ⊆ ran 𝐹
37		ssfi 9213	. . . . . . . . . . . . . 14 ⊢ ((ran 𝐹 ∈ Fin ∧ (𝑦 ∩ ran 𝐹) ⊆ ran 𝐹) → (𝑦 ∩ ran 𝐹) ∈ Fin)
38	35, 36, 37	sylancl 586	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (𝑦 ∩ ran 𝐹) ∈ Fin)
39		simpll 767	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → 𝜑)
40		elinel1 4201	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ (𝑦 ∩ ran 𝐹) → 0 ∈ 𝑦)
41	40	con3i 154	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 0 ∈ 𝑦 → ¬ 0 ∈ (𝑦 ∩ ran 𝐹))
42	41	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ¬ 0 ∈ (𝑦 ∩ ran 𝐹))
43		disjsn 4711	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∩ ran 𝐹) ∩ {0}) = ∅ ↔ ¬ 0 ∈ (𝑦 ∩ ran 𝐹))
44	42, 43	sylibr 234	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ((𝑦 ∩ ran 𝐹) ∩ {0}) = ∅)
45		reldisj 4453	. . . . . . . . . . . . . . . . . 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 3983	. . . . . . . . . . . . . . 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 3146	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ∀𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) ∈ dom vol)
52		finiunmbl 25579	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∩ ran 𝐹) ∈ Fin ∧ ∀𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) ∈ dom vol) → ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) ∈ dom vol)
53	38, 51, 52	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥}) ∈ dom vol)
54	33, 53	eqeltrrd 2842	. . . . . . . . . . 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 4133	. . . . . . . . 9 ⊢ (0 ∈ 𝑥 → ¬ 0 ∈ (ℝ ∖ 𝑥))
59	58	adantl 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → ¬ 0 ∈ (ℝ ∖ 𝑥))
60		reex 11246	. . . . . . . . . 10 ⊢ ℝ ∈ V
61	60	difexi 5330	. . . . . . . . 9 ⊢ (ℝ ∖ 𝑥) ∈ V
62		eleq2 2830	. . . . . . . . . . 11 ⊢ (𝑦 = (ℝ ∖ 𝑥) → (0 ∈ 𝑦 ↔ 0 ∈ (ℝ ∖ 𝑥)))
63	62	notbid 318	. . . . . . . . . 10 ⊢ (𝑦 = (ℝ ∖ 𝑥) → (¬ 0 ∈ 𝑦 ↔ ¬ 0 ∈ (ℝ ∖ 𝑥)))
64		imaeq2 6074	. . . . . . . . . . 11 ⊢ (𝑦 = (ℝ ∖ 𝑥) → (◡𝐹 “ 𝑦) = (◡𝐹 “ (ℝ ∖ 𝑥)))
65	64	eleq1d 2826	. . . . . . . . . 10 ⊢ (𝑦 = (ℝ ∖ 𝑥) → ((◡𝐹 “ 𝑦) ∈ dom vol ↔ (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol))
66	63, 65	imbi12d 344	. . . . . . . . 9 ⊢ (𝑦 = (ℝ ∖ 𝑥) → ((¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol) ↔ (¬ 0 ∈ (ℝ ∖ 𝑥) → (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol)))
67	61, 66	spcv 3605	. . . . . . . 8 ⊢ (∀𝑦(¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol) → (¬ 0 ∈ (ℝ ∖ 𝑥) → (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol))
68	57, 59, 67	sylc 65	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol)
69		difmbl 25578	. . . . . . 7 ⊢ (((◡𝐹 “ ℝ) ∈ dom vol ∧ (◡𝐹 “ (ℝ ∖ 𝑥)) ∈ dom vol) → ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥))) ∈ dom vol)
70	20, 68, 69	syl2anc 584	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → ((◡𝐹 “ ℝ) ∖ (◡𝐹 “ (ℝ ∖ 𝑥))) ∈ dom vol)
71	16, 70	eqeltrrd 2842	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ ran (,)) ∧ 0 ∈ 𝑥) → (◡𝐹 “ 𝑥) ∈ dom vol)
72		eleq2 2830	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → (0 ∈ 𝑦 ↔ 0 ∈ 𝑥))
73	72	notbid 318	. . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → (¬ 0 ∈ 𝑦 ↔ ¬ 0 ∈ 𝑥))
74		imaeq2 6074	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → (◡𝐹 “ 𝑦) = (◡𝐹 “ 𝑥))
75	74	eleq1d 2826	. . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → ((◡𝐹 “ 𝑦) ∈ dom vol ↔ (◡𝐹 “ 𝑥) ∈ dom vol))
76	73, 75	imbi12d 344	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → ((¬ 0 ∈ 𝑦 → (◡𝐹 “ 𝑦) ∈ dom vol) ↔ (¬ 0 ∈ 𝑥 → (◡𝐹 “ 𝑥) ∈ dom vol)))
77	76	spvv 1996	. . . . . . . 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 813	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ran (,)) → (◡𝐹 “ 𝑥) ∈ dom vol)
82	81	ralrimiva 3146	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol)
83		ismbf 25663	. . . 4 ⊢ (𝐹:ℝ⟶ℝ → (𝐹 ∈ MblFn ↔ ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol))
84	1, 83	syl 17	. . 3 ⊢ (𝜑 → (𝐹 ∈ MblFn ↔ ∀𝑥 ∈ ran (,)(◡𝐹 “ 𝑥) ∈ dom vol))
85	82, 84	mpbird 257	. 2 ⊢ (𝜑 → 𝐹 ∈ MblFn)
86		mblvol 25565	. . . . . . . 8 ⊢ ((◡𝐹 “ 𝑦) ∈ dom vol → (vol‘(◡𝐹 “ 𝑦)) = (vol*‘(◡𝐹 “ 𝑦)))
87	54, 86	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol‘(◡𝐹 “ 𝑦)) = (vol*‘(◡𝐹 “ 𝑦)))
88		mblss 25566	. . . . . . . . 9 ⊢ ((◡𝐹 “ 𝑦) ∈ dom vol → (◡𝐹 “ 𝑦) ⊆ ℝ)
89	54, 88	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (◡𝐹 “ 𝑦) ⊆ ℝ)
90		mblvol 25565	. . . . . . . . . . 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 2842	. . . . . . . . 9 ⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → (vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ)
95	38, 94	fsumrecl 15770	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ)
96	33	fveq2d 6910	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol*‘∪ 𝑥 ∈ (𝑦 ∩ ran 𝐹)(◡𝐹 “ {𝑥})) = (vol*‘(◡𝐹 “ 𝑦)))
97		mblss 25566	. . . . . . . . . . . . 13 ⊢ ((◡𝐹 “ {𝑥}) ∈ dom vol → (◡𝐹 “ {𝑥}) ⊆ ℝ)
98	50, 97	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → (◡𝐹 “ {𝑥}) ⊆ ℝ)
99	98, 94	jca 511	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ¬ 0 ∈ 𝑦) ∧ 𝑥 ∈ (𝑦 ∩ ran 𝐹)) → ((◡𝐹 “ {𝑥}) ⊆ ℝ ∧ (vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ))
100	99	ralrimiva 3146	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → ∀𝑥 ∈ (𝑦 ∩ ran 𝐹)((◡𝐹 “ {𝑥}) ⊆ ℝ ∧ (vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ))
101		ovolfiniun 25536	. . . . . . . . . 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 5167	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol*‘(◡𝐹 “ 𝑦)) ≤ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥})))
104		ovollecl 25518	. . . . . . . 8 ⊢ (((◡𝐹 “ 𝑦) ⊆ ℝ ∧ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥})) ∈ ℝ ∧ (vol*‘(◡𝐹 “ 𝑦)) ≤ Σ𝑥 ∈ (𝑦 ∩ ran 𝐹)(vol*‘(◡𝐹 “ {𝑥}))) → (vol*‘(◡𝐹 “ 𝑦)) ∈ ℝ)
105	89, 95, 103, 104	syl3anc 1373	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol*‘(◡𝐹 “ 𝑦)) ∈ ℝ)
106	87, 105	eqeltrd 2841	. . . . . 6 ⊢ ((𝜑 ∧ ¬ 0 ∈ 𝑦) → (vol‘(◡𝐹 “ 𝑦)) ∈ ℝ)
107	106	ex 412	. . . . 5 ⊢ (𝜑 → (¬ 0 ∈ 𝑦 → (vol‘(◡𝐹 “ 𝑦)) ∈ ℝ))
108	107	alrimiv 1927	. . . 4 ⊢ (𝜑 → ∀𝑦(¬ 0 ∈ 𝑦 → (vol‘(◡𝐹 “ 𝑦)) ∈ ℝ))
109		neldifsn 4792	. . . 4 ⊢ ¬ 0 ∈ (ℝ ∖ {0})
110	60	difexi 5330	. . . . 5 ⊢ (ℝ ∖ {0}) ∈ V
111		eleq2 2830	. . . . . . 7 ⊢ (𝑦 = (ℝ ∖ {0}) → (0 ∈ 𝑦 ↔ 0 ∈ (ℝ ∖ {0})))
112	111	notbid 318	. . . . . 6 ⊢ (𝑦 = (ℝ ∖ {0}) → (¬ 0 ∈ 𝑦 ↔ ¬ 0 ∈ (ℝ ∖ {0})))
113		imaeq2 6074	. . . . . . . 8 ⊢ (𝑦 = (ℝ ∖ {0}) → (◡𝐹 “ 𝑦) = (◡𝐹 “ (ℝ ∖ {0})))
114	113	fveq2d 6910	. . . . . . 7 ⊢ (𝑦 = (ℝ ∖ {0}) → (vol‘(◡𝐹 “ 𝑦)) = (vol‘(◡𝐹 “ (ℝ ∖ {0}))))
115	114	eleq1d 2826	. . . . . 6 ⊢ (𝑦 = (ℝ ∖ {0}) → ((vol‘(◡𝐹 “ 𝑦)) ∈ ℝ ↔ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ))
116	112, 115	imbi12d 344	. . . . 5 ⊢ (𝑦 = (ℝ ∖ {0}) → ((¬ 0 ∈ 𝑦 → (vol‘(◡𝐹 “ 𝑦)) ∈ ℝ) ↔ (¬ 0 ∈ (ℝ ∖ {0}) → (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ)))
117	110, 116	spcv 3605	. . . 4 ⊢ (∀𝑦(¬ 0 ∈ 𝑦 → (vol‘(◡𝐹 “ 𝑦)) ∈ ℝ) → (¬ 0 ∈ (ℝ ∖ {0}) → (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ))
118	108, 109, 117	mpisyl 21	. . 3 ⊢ (𝜑 → (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ)
119	1, 34, 118	3jca 1129	. 2 ⊢ (𝜑 → (𝐹:ℝ⟶ℝ ∧ ran 𝐹 ∈ Fin ∧ (vol‘(◡𝐹 “ (ℝ ∖ {0}))) ∈ ℝ))
120		isi1f 25709	. 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 1087  ∀wal 1538   = wceq 1540   ∈ wcel 2108  ∀wral 3061   ∖ cdif 3948   ∩ cin 3950   ⊆ wss 3951  ∅c0 4333  𝒫 cpw 4600  {csn 4626  ∪ ciun 4991   class class class wbr 5143   × cxp 5683  ^◡ccnv 5684  dom cdm 5685  ran crn 5686   “ cima 5688  Fun wfun 6555  ⟶wf 6557  ‘cfv 6561  Fincfn 8985  ℝcr 11154  0cc0 11155  ℝ^*cxr 11294   ≤ cle 11296  (,)cioo 13387  Σcsu 15722  vol*covol 25497  volcvol 25498  MblFncmbf 25649  ∫₁citg1 25650

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-er 8745  df-map 8868  df-pm 8869  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-sup 9482  df-inf 9483  df-oi 9550  df-dju 9941  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-n0 12527  df-z 12614  df-uz 12879  df-q 12991  df-rp 13035  df-xadd 13155  df-ioo 13391  df-ico 13393  df-icc 13394  df-fz 13548  df-fzo 13695  df-fl 13832  df-seq 14043  df-exp 14103  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-clim 15524  df-sum 15723  df-xmet 21357  df-met 21358  df-ovol 25499  df-vol 25500  df-mbf 25654  df-itg1 25655

This theorem is referenced by:  i1f0  25722  i1f1  25725  i1fadd  25730  i1fmul  25731  i1fmulc  25738  i1fres  25740  mbfi1fseqlem4  25753  itg2addnclem2  37679  ftc1anclem3  37702