i1fd

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

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

Proof

Step	Hyp	Ref	Expression
1		i1fd.1	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2		i1fd.2	⊢ ( 𝜑 → ran 𝐹 ∈ Fin )
3		i1fd.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( ^◡ 𝐹 “ { 𝑥 } ) ∈ dom vol )
4		i1fd.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( vol ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ∈ ℝ )
5	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) ∧ 0 ∈ 𝑥 ) → 𝐹 : ℝ ⟶ ℝ )
6		ffun	⊢ ( 𝐹 : ℝ ⟶ ℝ → Fun 𝐹 )
7		funcnvcnv	⊢ ( Fun 𝐹 → Fun ^◡ ^◡ 𝐹 )
8		imadif	⊢ ( Fun ^◡ ^◡ 𝐹 → ( ^◡ 𝐹 “ ( ℝ ∖ ( ℝ ∖ 𝑥 ) ) ) = ( ( ^◡ 𝐹 “ ℝ ) ∖ ( ^◡ 𝐹 “ ( ℝ ∖ 𝑥 ) ) ) )
9	5 6 7 8	4syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) ∧ 0 ∈ 𝑥 ) → ( ^◡ 𝐹 “ ( ℝ ∖ ( ℝ ∖ 𝑥 ) ) ) = ( ( ^◡ 𝐹 “ ℝ ) ∖ ( ^◡ 𝐹 “ ( ℝ ∖ 𝑥 ) ) ) )
10		ioof	⊢ (,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ
11		frn	⊢ ( (,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ → ran (,) ⊆ 𝒫 ℝ )
12	10 11	ax-mp	⊢ ran (,) ⊆ 𝒫 ℝ
13	12	sseli	⊢ ( 𝑥 ∈ ran (,) → 𝑥 ∈ 𝒫 ℝ )
14	13	elpwid	⊢ ( 𝑥 ∈ ran (,) → 𝑥 ⊆ ℝ )
15	14	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) ∧ 0 ∈ 𝑥 ) → 𝑥 ⊆ ℝ )
16		dfss4	⊢ ( 𝑥 ⊆ ℝ ↔ ( ℝ ∖ ( ℝ ∖ 𝑥 ) ) = 𝑥 )
17	15 16	sylib	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) ∧ 0 ∈ 𝑥 ) → ( ℝ ∖ ( ℝ ∖ 𝑥 ) ) = 𝑥 )
18	17	imaeq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) ∧ 0 ∈ 𝑥 ) → ( ^◡ 𝐹 “ ( ℝ ∖ ( ℝ ∖ 𝑥 ) ) ) = ( ^◡ 𝐹 “ 𝑥 ) )
19	9 18	eqtr3d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) ∧ 0 ∈ 𝑥 ) → ( ( ^◡ 𝐹 “ ℝ ) ∖ ( ^◡ 𝐹 “ ( ℝ ∖ 𝑥 ) ) ) = ( ^◡ 𝐹 “ 𝑥 ) )
20		fimacnv	⊢ ( 𝐹 : ℝ ⟶ ℝ → ( ^◡ 𝐹 “ ℝ ) = ℝ )
21	5 20	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) ∧ 0 ∈ 𝑥 ) → ( ^◡ 𝐹 “ ℝ ) = ℝ )
22		rembl	⊢ ℝ ∈ dom vol
23	21 22	eqeltrdi	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) ∧ 0 ∈ 𝑥 ) → ( ^◡ 𝐹 “ ℝ ) ∈ dom vol )
24	1	adantr	⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → 𝐹 : ℝ ⟶ ℝ )
25		inpreima	⊢ ( Fun 𝐹 → ( ^◡ 𝐹 “ ( 𝑦 ∩ ran 𝐹 ) ) = ( ( ^◡ 𝐹 “ 𝑦 ) ∩ ( ^◡ 𝐹 “ ran 𝐹 ) ) )
26		iunid	⊢ ∪ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) { 𝑥 } = ( 𝑦 ∩ ran 𝐹 )
27	26	imaeq2i	⊢ ( ^◡ 𝐹 “ ∪ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) { 𝑥 } ) = ( ^◡ 𝐹 “ ( 𝑦 ∩ ran 𝐹 ) )
28		imaiun	⊢ ( ^◡ 𝐹 “ ∪ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) { 𝑥 } ) = ∪ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( ^◡ 𝐹 “ { 𝑥 } )
29	27 28	eqtr3i	⊢ ( ^◡ 𝐹 “ ( 𝑦 ∩ ran 𝐹 ) ) = ∪ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( ^◡ 𝐹 “ { 𝑥 } )
30		cnvimass	⊢ ( ^◡ 𝐹 “ 𝑦 ) ⊆ dom 𝐹
31		cnvimarndm	⊢ ( ^◡ 𝐹 “ ran 𝐹 ) = dom 𝐹
32	30 31	sseqtrri	⊢ ( ^◡ 𝐹 “ 𝑦 ) ⊆ ( ^◡ 𝐹 “ ran 𝐹 )
33		dfss2	⊢ ( ( ^◡ 𝐹 “ 𝑦 ) ⊆ ( ^◡ 𝐹 “ ran 𝐹 ) ↔ ( ( ^◡ 𝐹 “ 𝑦 ) ∩ ( ^◡ 𝐹 “ ran 𝐹 ) ) = ( ^◡ 𝐹 “ 𝑦 ) )
34	32 33	mpbi	⊢ ( ( ^◡ 𝐹 “ 𝑦 ) ∩ ( ^◡ 𝐹 “ ran 𝐹 ) ) = ( ^◡ 𝐹 “ 𝑦 )
35	25 29 34	3eqtr3g	⊢ ( Fun 𝐹 → ∪ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( ^◡ 𝐹 “ { 𝑥 } ) = ( ^◡ 𝐹 “ 𝑦 ) )
36	24 6 35	3syl	⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ∪ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( ^◡ 𝐹 “ { 𝑥 } ) = ( ^◡ 𝐹 “ 𝑦 ) )
37	2	adantr	⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ran 𝐹 ∈ Fin )
38		inss2	⊢ ( 𝑦 ∩ ran 𝐹 ) ⊆ ran 𝐹
39		ssfi	⊢ ( ( ran 𝐹 ∈ Fin ∧ ( 𝑦 ∩ ran 𝐹 ) ⊆ ran 𝐹 ) → ( 𝑦 ∩ ran 𝐹 ) ∈ Fin )
40	37 38 39	sylancl	⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ( 𝑦 ∩ ran 𝐹 ) ∈ Fin )
41		simpll	⊢ ( ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) ∧ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ) → 𝜑 )
42		elinel1	⊢ ( 0 ∈ ( 𝑦 ∩ ran 𝐹 ) → 0 ∈ 𝑦 )
43	42	con3i	⊢ ( ¬ 0 ∈ 𝑦 → ¬ 0 ∈ ( 𝑦 ∩ ran 𝐹 ) )
44	43	adantl	⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ¬ 0 ∈ ( 𝑦 ∩ ran 𝐹 ) )
45		disjsn	⊢ ( ( ( 𝑦 ∩ ran 𝐹 ) ∩ { 0 } ) = ∅ ↔ ¬ 0 ∈ ( 𝑦 ∩ ran 𝐹 ) )
46	44 45	sylibr	⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ( ( 𝑦 ∩ ran 𝐹 ) ∩ { 0 } ) = ∅ )
47		reldisj	⊢ ( ( 𝑦 ∩ ran 𝐹 ) ⊆ ran 𝐹 → ( ( ( 𝑦 ∩ ran 𝐹 ) ∩ { 0 } ) = ∅ ↔ ( 𝑦 ∩ ran 𝐹 ) ⊆ ( ran 𝐹 ∖ { 0 } ) ) )
48	38 47	ax-mp	⊢ ( ( ( 𝑦 ∩ ran 𝐹 ) ∩ { 0 } ) = ∅ ↔ ( 𝑦 ∩ ran 𝐹 ) ⊆ ( ran 𝐹 ∖ { 0 } ) )
49	46 48	sylib	⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ( 𝑦 ∩ ran 𝐹 ) ⊆ ( ran 𝐹 ∖ { 0 } ) )
50	49	sselda	⊢ ( ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) ∧ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ) → 𝑥 ∈ ( ran 𝐹 ∖ { 0 } ) )
51	41 50 3	syl2anc	⊢ ( ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) ∧ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ) → ( ^◡ 𝐹 “ { 𝑥 } ) ∈ dom vol )
52	51	ralrimiva	⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ∀ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( ^◡ 𝐹 “ { 𝑥 } ) ∈ dom vol )
53		finiunmbl	⊢ ( ( ( 𝑦 ∩ ran 𝐹 ) ∈ Fin ∧ ∀ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( ^◡ 𝐹 “ { 𝑥 } ) ∈ dom vol ) → ∪ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( ^◡ 𝐹 “ { 𝑥 } ) ∈ dom vol )
54	40 52 53	syl2anc	⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ∪ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( ^◡ 𝐹 “ { 𝑥 } ) ∈ dom vol )
55	36 54	eqeltrrd	⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ( ^◡ 𝐹 “ 𝑦 ) ∈ dom vol )
56	55	ex	⊢ ( 𝜑 → ( ¬ 0 ∈ 𝑦 → ( ^◡ 𝐹 “ 𝑦 ) ∈ dom vol ) )
57	56	alrimiv	⊢ ( 𝜑 → ∀ 𝑦 ( ¬ 0 ∈ 𝑦 → ( ^◡ 𝐹 “ 𝑦 ) ∈ dom vol ) )
58	57	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) ∧ 0 ∈ 𝑥 ) → ∀ 𝑦 ( ¬ 0 ∈ 𝑦 → ( ^◡ 𝐹 “ 𝑦 ) ∈ dom vol ) )
59		elndif	⊢ ( 0 ∈ 𝑥 → ¬ 0 ∈ ( ℝ ∖ 𝑥 ) )
60	59	adantl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) ∧ 0 ∈ 𝑥 ) → ¬ 0 ∈ ( ℝ ∖ 𝑥 ) )
61		reex	⊢ ℝ ∈ V
62	61	difexi	⊢ ( ℝ ∖ 𝑥 ) ∈ V
63		eleq2	⊢ ( 𝑦 = ( ℝ ∖ 𝑥 ) → ( 0 ∈ 𝑦 ↔ 0 ∈ ( ℝ ∖ 𝑥 ) ) )
64	63	notbid	⊢ ( 𝑦 = ( ℝ ∖ 𝑥 ) → ( ¬ 0 ∈ 𝑦 ↔ ¬ 0 ∈ ( ℝ ∖ 𝑥 ) ) )
65		imaeq2	⊢ ( 𝑦 = ( ℝ ∖ 𝑥 ) → ( ^◡ 𝐹 “ 𝑦 ) = ( ^◡ 𝐹 “ ( ℝ ∖ 𝑥 ) ) )
66	65	eleq1d	⊢ ( 𝑦 = ( ℝ ∖ 𝑥 ) → ( ( ^◡ 𝐹 “ 𝑦 ) ∈ dom vol ↔ ( ^◡ 𝐹 “ ( ℝ ∖ 𝑥 ) ) ∈ dom vol ) )
67	64 66	imbi12d	⊢ ( 𝑦 = ( ℝ ∖ 𝑥 ) → ( ( ¬ 0 ∈ 𝑦 → ( ^◡ 𝐹 “ 𝑦 ) ∈ dom vol ) ↔ ( ¬ 0 ∈ ( ℝ ∖ 𝑥 ) → ( ^◡ 𝐹 “ ( ℝ ∖ 𝑥 ) ) ∈ dom vol ) ) )
68	62 67	spcv	⊢ ( ∀ 𝑦 ( ¬ 0 ∈ 𝑦 → ( ^◡ 𝐹 “ 𝑦 ) ∈ dom vol ) → ( ¬ 0 ∈ ( ℝ ∖ 𝑥 ) → ( ^◡ 𝐹 “ ( ℝ ∖ 𝑥 ) ) ∈ dom vol ) )
69	58 60 68	sylc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) ∧ 0 ∈ 𝑥 ) → ( ^◡ 𝐹 “ ( ℝ ∖ 𝑥 ) ) ∈ dom vol )
70		difmbl	⊢ ( ( ( ^◡ 𝐹 “ ℝ ) ∈ dom vol ∧ ( ^◡ 𝐹 “ ( ℝ ∖ 𝑥 ) ) ∈ dom vol ) → ( ( ^◡ 𝐹 “ ℝ ) ∖ ( ^◡ 𝐹 “ ( ℝ ∖ 𝑥 ) ) ) ∈ dom vol )
71	23 69 70	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) ∧ 0 ∈ 𝑥 ) → ( ( ^◡ 𝐹 “ ℝ ) ∖ ( ^◡ 𝐹 “ ( ℝ ∖ 𝑥 ) ) ) ∈ dom vol )
72	19 71	eqeltrrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) ∧ 0 ∈ 𝑥 ) → ( ^◡ 𝐹 “ 𝑥 ) ∈ dom vol )
73		eleq2	⊢ ( 𝑦 = 𝑥 → ( 0 ∈ 𝑦 ↔ 0 ∈ 𝑥 ) )
74	73	notbid	⊢ ( 𝑦 = 𝑥 → ( ¬ 0 ∈ 𝑦 ↔ ¬ 0 ∈ 𝑥 ) )
75		imaeq2	⊢ ( 𝑦 = 𝑥 → ( ^◡ 𝐹 “ 𝑦 ) = ( ^◡ 𝐹 “ 𝑥 ) )
76	75	eleq1d	⊢ ( 𝑦 = 𝑥 → ( ( ^◡ 𝐹 “ 𝑦 ) ∈ dom vol ↔ ( ^◡ 𝐹 “ 𝑥 ) ∈ dom vol ) )
77	74 76	imbi12d	⊢ ( 𝑦 = 𝑥 → ( ( ¬ 0 ∈ 𝑦 → ( ^◡ 𝐹 “ 𝑦 ) ∈ dom vol ) ↔ ( ¬ 0 ∈ 𝑥 → ( ^◡ 𝐹 “ 𝑥 ) ∈ dom vol ) ) )
78	77	spvv	⊢ ( ∀ 𝑦 ( ¬ 0 ∈ 𝑦 → ( ^◡ 𝐹 “ 𝑦 ) ∈ dom vol ) → ( ¬ 0 ∈ 𝑥 → ( ^◡ 𝐹 “ 𝑥 ) ∈ dom vol ) )
79	57 78	syl	⊢ ( 𝜑 → ( ¬ 0 ∈ 𝑥 → ( ^◡ 𝐹 “ 𝑥 ) ∈ dom vol ) )
80	79	imp	⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑥 ) → ( ^◡ 𝐹 “ 𝑥 ) ∈ dom vol )
81	80	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) ∧ ¬ 0 ∈ 𝑥 ) → ( ^◡ 𝐹 “ 𝑥 ) ∈ dom vol )
82	72 81	pm2.61dan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ran (,) ) → ( ^◡ 𝐹 “ 𝑥 ) ∈ dom vol )
83	82	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ran (,) ( ^◡ 𝐹 “ 𝑥 ) ∈ dom vol )
84		ismbf	⊢ ( 𝐹 : ℝ ⟶ ℝ → ( 𝐹 ∈ MblFn ↔ ∀ 𝑥 ∈ ran (,) ( ^◡ 𝐹 “ 𝑥 ) ∈ dom vol ) )
85	1 84	syl	⊢ ( 𝜑 → ( 𝐹 ∈ MblFn ↔ ∀ 𝑥 ∈ ran (,) ( ^◡ 𝐹 “ 𝑥 ) ∈ dom vol ) )
86	83 85	mpbird	⊢ ( 𝜑 → 𝐹 ∈ MblFn )
87		mblvol	⊢ ( ( ^◡ 𝐹 “ 𝑦 ) ∈ dom vol → ( vol ‘ ( ^◡ 𝐹 “ 𝑦 ) ) = ( vol* ‘ ( ^◡ 𝐹 “ 𝑦 ) ) )
88	55 87	syl	⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ( vol ‘ ( ^◡ 𝐹 “ 𝑦 ) ) = ( vol* ‘ ( ^◡ 𝐹 “ 𝑦 ) ) )
89		mblss	⊢ ( ( ^◡ 𝐹 “ 𝑦 ) ∈ dom vol → ( ^◡ 𝐹 “ 𝑦 ) ⊆ ℝ )
90	55 89	syl	⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ( ^◡ 𝐹 “ 𝑦 ) ⊆ ℝ )
91		mblvol	⊢ ( ( ^◡ 𝐹 “ { 𝑥 } ) ∈ dom vol → ( vol ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) = ( vol* ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) )
92	51 91	syl	⊢ ( ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) ∧ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ) → ( vol ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) = ( vol* ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) )
93	41 50 4	syl2anc	⊢ ( ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) ∧ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ) → ( vol ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ∈ ℝ )
94	92 93	eqeltrrd	⊢ ( ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) ∧ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ) → ( vol* ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ∈ ℝ )
95	40 94	fsumrecl	⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → Σ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( vol* ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ∈ ℝ )
96	36	fveq2d	⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ( vol* ‘ ∪ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( ^◡ 𝐹 “ { 𝑥 } ) ) = ( vol* ‘ ( ^◡ 𝐹 “ 𝑦 ) ) )
97		mblss	⊢ ( ( ^◡ 𝐹 “ { 𝑥 } ) ∈ dom vol → ( ^◡ 𝐹 “ { 𝑥 } ) ⊆ ℝ )
98	51 97	syl	⊢ ( ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) ∧ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ) → ( ^◡ 𝐹 “ { 𝑥 } ) ⊆ ℝ )
99	98 94	jca	⊢ ( ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) ∧ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ) → ( ( ^◡ 𝐹 “ { 𝑥 } ) ⊆ ℝ ∧ ( vol* ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ∈ ℝ ) )
100	99	ralrimiva	⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ∀ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( ( ^◡ 𝐹 “ { 𝑥 } ) ⊆ ℝ ∧ ( vol* ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ∈ ℝ ) )
101		ovolfiniun	⊢ ( ( ( 𝑦 ∩ ran 𝐹 ) ∈ Fin ∧ ∀ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( ( ^◡ 𝐹 “ { 𝑥 } ) ⊆ ℝ ∧ ( vol* ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ∈ ℝ ) ) → ( vol* ‘ ∪ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( ^◡ 𝐹 “ { 𝑥 } ) ) ≤ Σ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( vol* ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) )
102	40 100 101	syl2anc	⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ( vol* ‘ ∪ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( ^◡ 𝐹 “ { 𝑥 } ) ) ≤ Σ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( vol* ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) )
103	96 102	eqbrtrrd	⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ( vol* ‘ ( ^◡ 𝐹 “ 𝑦 ) ) ≤ Σ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( vol* ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) )
104		ovollecl	⊢ ( ( ( ^◡ 𝐹 “ 𝑦 ) ⊆ ℝ ∧ Σ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( vol* ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ∈ ℝ ∧ ( vol* ‘ ( ^◡ 𝐹 “ 𝑦 ) ) ≤ Σ 𝑥 ∈ ( 𝑦 ∩ ran 𝐹 ) ( vol* ‘ ( ^◡ 𝐹 “ { 𝑥 } ) ) ) → ( vol* ‘ ( ^◡ 𝐹 “ 𝑦 ) ) ∈ ℝ )
105	90 95 103 104	syl3anc	⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ( vol* ‘ ( ^◡ 𝐹 “ 𝑦 ) ) ∈ ℝ )
106	88 105	eqeltrd	⊢ ( ( 𝜑 ∧ ¬ 0 ∈ 𝑦 ) → ( vol ‘ ( ^◡ 𝐹 “ 𝑦 ) ) ∈ ℝ )
107	106	ex	⊢ ( 𝜑 → ( ¬ 0 ∈ 𝑦 → ( vol ‘ ( ^◡ 𝐹 “ 𝑦 ) ) ∈ ℝ ) )
108	107	alrimiv	⊢ ( 𝜑 → ∀ 𝑦 ( ¬ 0 ∈ 𝑦 → ( vol ‘ ( ^◡ 𝐹 “ 𝑦 ) ) ∈ ℝ ) )
109		neldifsn	⊢ ¬ 0 ∈ ( ℝ ∖ { 0 } )
110	61	difexi	⊢ ( ℝ ∖ { 0 } ) ∈ V
111		eleq2	⊢ ( 𝑦 = ( ℝ ∖ { 0 } ) → ( 0 ∈ 𝑦 ↔ 0 ∈ ( ℝ ∖ { 0 } ) ) )
112	111	notbid	⊢ ( 𝑦 = ( ℝ ∖ { 0 } ) → ( ¬ 0 ∈ 𝑦 ↔ ¬ 0 ∈ ( ℝ ∖ { 0 } ) ) )
113		imaeq2	⊢ ( 𝑦 = ( ℝ ∖ { 0 } ) → ( ^◡ 𝐹 “ 𝑦 ) = ( ^◡ 𝐹 “ ( ℝ ∖ { 0 } ) ) )
114	113	fveq2d	⊢ ( 𝑦 = ( ℝ ∖ { 0 } ) → ( vol ‘ ( ^◡ 𝐹 “ 𝑦 ) ) = ( vol ‘ ( ^◡ 𝐹 “ ( ℝ ∖ { 0 } ) ) ) )
115	114	eleq1d	⊢ ( 𝑦 = ( ℝ ∖ { 0 } ) → ( ( vol ‘ ( ^◡ 𝐹 “ 𝑦 ) ) ∈ ℝ ↔ ( vol ‘ ( ^◡ 𝐹 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) )
116	112 115	imbi12d	⊢ ( 𝑦 = ( ℝ ∖ { 0 } ) → ( ( ¬ 0 ∈ 𝑦 → ( vol ‘ ( ^◡ 𝐹 “ 𝑦 ) ) ∈ ℝ ) ↔ ( ¬ 0 ∈ ( ℝ ∖ { 0 } ) → ( vol ‘ ( ^◡ 𝐹 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) ) )
117	110 116	spcv	⊢ ( ∀ 𝑦 ( ¬ 0 ∈ 𝑦 → ( vol ‘ ( ^◡ 𝐹 “ 𝑦 ) ) ∈ ℝ ) → ( ¬ 0 ∈ ( ℝ ∖ { 0 } ) → ( vol ‘ ( ^◡ 𝐹 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) )
118	108 109 117	mpisyl	⊢ ( 𝜑 → ( vol ‘ ( ^◡ 𝐹 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ )
119	1 2 118	3jca	⊢ ( 𝜑 → ( 𝐹 : ℝ ⟶ ℝ ∧ ran 𝐹 ∈ Fin ∧ ( vol ‘ ( ^◡ 𝐹 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) )
120		isi1f	⊢ ( 𝐹 ∈ dom ∫₁ ↔ ( 𝐹 ∈ MblFn ∧ ( 𝐹 : ℝ ⟶ ℝ ∧ ran 𝐹 ∈ Fin ∧ ( vol ‘ ( ^◡ 𝐹 “ ( ℝ ∖ { 0 } ) ) ) ∈ ℝ ) ) )
121	86 119 120	sylanbrc	⊢ ( 𝜑 → 𝐹 ∈ dom ∫₁ )

Metamath Proof Explorer

Theorem i1fd

Proof