Theorem ovolval4lem1 47092

Description: |- ( ( ph /\ n e. A ) -> ( ( (,) o. G ) 𝑛) = (((,) ∘ 𝐹) n ) ) (Contributed by Glauco Siliprandi, 3-Mar-2021.)

Hypotheses

Ref	Expression
ovolval4lem1.f	⊢ (𝜑 → 𝐹:ℕ⟶(ℝ* × ℝ*))
ovolval4lem1.g	⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩)
ovolval4lem1.a	⊢ 𝐴 = {𝑛 ∈ ℕ ∣ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))}

Assertion

Ref	Expression
ovolval4lem1	⊢ (𝜑 → (∪ ran ((,) ∘ 𝐹) = ∪ ran ((,) ∘ 𝐺) ∧ (vol ∘ ((,) ∘ 𝐹)) = (vol ∘ ((,) ∘ 𝐺))))

Distinct variable groups:   𝐴,𝑛   𝑛,𝐹   𝑛,𝐺   𝜑,𝑛

Proof of Theorem ovolval4lem1

Step	Hyp	Ref	Expression
1		ioof 13391	. . . . . . . 8 ⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ
2	1	a1i 11	. . . . . . 7 ⊢ (𝜑 → (,):(ℝ* × ℝ*)⟶𝒫 ℝ)
3		ovolval4lem1.f	. . . . . . 7 ⊢ (𝜑 → 𝐹:ℕ⟶(ℝ* × ℝ*))
4		fco 6679	. . . . . . 7 ⊢ (((,):(ℝ* × ℝ*)⟶𝒫 ℝ ∧ 𝐹:ℕ⟶(ℝ* × ℝ*)) → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
5	2, 3, 4	syl2anc 590	. . . . . 6 ⊢ (𝜑 → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
6	5	ffnd 6656	. . . . 5 ⊢ (𝜑 → ((,) ∘ 𝐹) Fn ℕ)
7		fniunfv 7191	. . . . 5 ⊢ (((,) ∘ 𝐹) Fn ℕ → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = ∪ ran ((,) ∘ 𝐹))
8	6, 7	syl 17	. . . 4 ⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = ∪ ran ((,) ∘ 𝐹))
9	8	eqcomd 2745	. . 3 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) = ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛))
10		ovolval4lem1.a	. . . . . . . . 9 ⊢ 𝐴 = {𝑛 ∈ ℕ ∣ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))}
11		ssrab2 4011	. . . . . . . . 9 ⊢ {𝑛 ∈ ℕ ∣ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))} ⊆ ℕ
12	10, 11	eqsstri 3961	. . . . . . . 8 ⊢ 𝐴 ⊆ ℕ
13		undif 4410	. . . . . . . 8 ⊢ (𝐴 ⊆ ℕ ↔ (𝐴 ∪ (ℕ ∖ 𝐴)) = ℕ)
14	12, 13	mpbi 231	. . . . . . 7 ⊢ (𝐴 ∪ (ℕ ∖ 𝐴)) = ℕ
15	14	eqcomi 2748	. . . . . 6 ⊢ ℕ = (𝐴 ∪ (ℕ ∖ 𝐴))
16	15	iuneq1i 45532	. . . . 5 ⊢ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = ∪ 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐹)‘𝑛)
17		iunxun 5023	. . . . 5 ⊢ ∪ 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐹)‘𝑛) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛))
18	16, 17	eqtri 2762	. . . 4 ⊢ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛))
19	18	a1i 11	. . 3 ⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛)))
20	3	ffvelcdmda 7025	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ (ℝ* × ℝ*))
21		xp1st 7963	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑛) ∈ (ℝ* × ℝ*) → (1st ‘(𝐹‘𝑛)) ∈ ℝ*)
22	20, 21	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐹‘𝑛)) ∈ ℝ*)
23		xp2nd 7964	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑛) ∈ (ℝ* × ℝ*) → (2nd ‘(𝐹‘𝑛)) ∈ ℝ*)
24	20, 23	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐹‘𝑛)) ∈ ℝ*)
25	24, 22	ifcld 4501	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))) ∈ ℝ*)
26	22, 25	opelxpd 5657	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩ ∈ (ℝ* × ℝ*))
27		ovolval4lem1.g	. . . . . . . . 9 ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩)
28	26, 27	fmptd 7055	. . . . . . . 8 ⊢ (𝜑 → 𝐺:ℕ⟶(ℝ* × ℝ*))
29		fco 6679	. . . . . . . 8 ⊢ (((,):(ℝ* × ℝ*)⟶𝒫 ℝ ∧ 𝐺:ℕ⟶(ℝ* × ℝ*)) → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
30	2, 28, 29	syl2anc 590	. . . . . . 7 ⊢ (𝜑 → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
31	30	ffnd 6656	. . . . . 6 ⊢ (𝜑 → ((,) ∘ 𝐺) Fn ℕ)
32		fniunfv 7191	. . . . . 6 ⊢ (((,) ∘ 𝐺) Fn ℕ → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = ∪ ran ((,) ∘ 𝐺))
33	31, 32	syl 17	. . . . 5 ⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = ∪ ran ((,) ∘ 𝐺))
34	33	eqcomd 2745	. . . 4 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛))
35	15	iuneq1i 45532	. . . . . 6 ⊢ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = ∪ 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐺)‘𝑛)
36		iunxun 5023	. . . . . 6 ⊢ ∪ 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐺)‘𝑛) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛))
37	35, 36	eqtri 2762	. . . . 5 ⊢ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛))
38	37	a1i 11	. . . 4 ⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛)))
39	28	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐺:ℕ⟶(ℝ* × ℝ*))
40	12	sseli 3911	. . . . . . . . 9 ⊢ (𝑛 ∈ 𝐴 → 𝑛 ∈ ℕ)
41	40	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ ℕ)
42		fvco3 6927	. . . . . . . 8 ⊢ ((𝐺:ℕ⟶(ℝ* × ℝ*) ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐺)‘𝑛) = ((,)‘(𝐺‘𝑛)))
43	39, 41, 42	syl2anc 590	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) = ((,)‘(𝐺‘𝑛)))
44	3	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐹:ℕ⟶(ℝ* × ℝ*))
45		fvco3 6927	. . . . . . . . 9 ⊢ ((𝐹:ℕ⟶(ℝ* × ℝ*) ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹‘𝑛)))
46	44, 41, 45	syl2anc 590	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹‘𝑛)))
47		simpl 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝜑)
48		1st2nd2 7970	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑛) ∈ (ℝ* × ℝ*) → (𝐹‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
49	20, 48	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
50	47, 41, 49	syl2anc 590	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐹‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
51	27	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺 = (𝑛 ∈ ℕ ↦ ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩))
52	26	elexd 3454	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩ ∈ V)
53	51, 52	fvmpt2d 6949	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩)
54	47, 41, 53	syl2anc 590	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐺‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩)
55	10	eleq2i 2831	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ 𝐴 ↔ 𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))})
56	55	biimpi 217	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ 𝐴 → 𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))})
57		rabid 3412	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))} ↔ (𝑛 ∈ ℕ ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))))
58	56, 57	sylib 219	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ 𝐴 → (𝑛 ∈ ℕ ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))))
59	58	simprd 496	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ 𝐴 → (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)))
60	59	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)))
61	60	iftrued 4462	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))) = (2nd ‘(𝐹‘𝑛)))
62	61	opeq2d 4811	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩ = ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
63		eqidd 2740	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩ = ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
64	54, 62, 63	3eqtrd 2778	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐺‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
65	50, 64	eqtr4d 2777	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐹‘𝑛) = (𝐺‘𝑛))
66	65	fveq2d 6831	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((,)‘(𝐹‘𝑛)) = ((,)‘(𝐺‘𝑛)))
67	46, 66	eqtrd 2774	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐺‘𝑛)))
68	43, 67	eqtr4d 2777	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) = (((,) ∘ 𝐹)‘𝑛))
69	68	iuneq2dv 4946	. . . . 5 ⊢ (𝜑 → ∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) = ∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛))
70	28	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → 𝐺:ℕ⟶(ℝ* × ℝ*))
71		eldifi 4061	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (ℕ ∖ 𝐴) → 𝑛 ∈ ℕ)
72	71	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → 𝑛 ∈ ℕ)
73	70, 72, 42	syl2anc 590	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐺)‘𝑛) = ((,)‘(𝐺‘𝑛)))
74		simpl 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → 𝜑)
75	74, 72, 53	syl2anc 590	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (𝐺‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩)
76	71	anim1i 621	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (ℕ ∖ 𝐴) ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) → (𝑛 ∈ ℕ ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))))
77	76, 57	sylibr 235	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ (ℕ ∖ 𝐴) ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) → 𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))})
78	77, 55	sylibr 235	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ (ℕ ∖ 𝐴) ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) → 𝑛 ∈ 𝐴)
79	78	adantll 720	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) → 𝑛 ∈ 𝐴)
80		eldifn 4062	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (ℕ ∖ 𝐴) → ¬ 𝑛 ∈ 𝐴)
81	80	ad2antlr 733	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) → ¬ 𝑛 ∈ 𝐴)
82	79, 81	pm2.65da 822	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ¬ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)))
83	82	iffalsed 4465	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))) = (1st ‘(𝐹‘𝑛)))
84	83	opeq2d 4811	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩ = ⟨(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))⟩)
85	75, 84	eqtrd 2774	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (𝐺‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))⟩)
86	85	fveq2d 6831	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘(𝐺‘𝑛)) = ((,)‘⟨(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))⟩))
87		iooid 13317	. . . . . . . . . . . 12 ⊢ ((1st ‘(𝐹‘𝑛))(,)(1st ‘(𝐹‘𝑛))) = ∅
88	87	eqcomi 2748	. . . . . . . . . . 11 ⊢ ∅ = ((1st ‘(𝐹‘𝑛))(,)(1st ‘(𝐹‘𝑛)))
89		df-ov 7359	. . . . . . . . . . 11 ⊢ ((1st ‘(𝐹‘𝑛))(,)(1st ‘(𝐹‘𝑛))) = ((,)‘⟨(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))⟩)
90	88, 89	eqtr2i 2763	. . . . . . . . . 10 ⊢ ((,)‘⟨(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))⟩) = ∅
91	90	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘⟨(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))⟩) = ∅)
92	73, 86, 91	3eqtrd 2778	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐺)‘𝑛) = ∅)
93	92	iuneq2dv 4946	. . . . . . 7 ⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛) = ∪ 𝑛 ∈ (ℕ ∖ 𝐴)∅)
94		iun0 4991	. . . . . . . 8 ⊢ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)∅ = ∅
95	94	a1i 11	. . . . . . 7 ⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)∅ = ∅)
96	93, 95	eqtrd 2774	. . . . . 6 ⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛) = ∅)
97	74, 3	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → 𝐹:ℕ⟶(ℝ* × ℝ*))
98	97, 72, 45	syl2anc 590	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹‘𝑛)))
99	74, 72, 49	syl2anc 590	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (𝐹‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
100	99	fveq2d 6831	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘(𝐹‘𝑛)) = ((,)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩))
101		df-ov 7359	. . . . . . . . . . 11 ⊢ ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ((,)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
102	101	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ((,)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩))
103		simplr 774	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → 𝑛 ∈ (ℕ ∖ 𝐴))
104	72, 22	syldan 597	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (1st ‘(𝐹‘𝑛)) ∈ ℝ*)
105	104	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → (1st ‘(𝐹‘𝑛)) ∈ ℝ*)
106	72, 24	syldan 597	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (2nd ‘(𝐹‘𝑛)) ∈ ℝ*)
107	106	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → (2nd ‘(𝐹‘𝑛)) ∈ ℝ*)
108		simpr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛)))
109	105, 107	xrltnled 11204	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → ((1st ‘(𝐹‘𝑛)) < (2nd ‘(𝐹‘𝑛)) ↔ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))))
110	108, 109	mpbird 258	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → (1st ‘(𝐹‘𝑛)) < (2nd ‘(𝐹‘𝑛)))
111	105, 107, 110	xrltled 13092	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)))
112	103, 111, 78	syl2anc 590	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → 𝑛 ∈ 𝐴)
113	80	ad2antlr 733	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → ¬ 𝑛 ∈ 𝐴)
114	112, 113	condan 823	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛)))
115		ioo0 13314	. . . . . . . . . . . 12 ⊢ (((1st ‘(𝐹‘𝑛)) ∈ ℝ* ∧ (2nd ‘(𝐹‘𝑛)) ∈ ℝ*) → (((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ∅ ↔ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))))
116	104, 106, 115	syl2anc 590	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ∅ ↔ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))))
117	114, 116	mpbird 258	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ∅)
118	102, 117	eqtr3d 2776	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩) = ∅)
119	98, 100, 118	3eqtrd 2778	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐹)‘𝑛) = ∅)
120	119	iuneq2dv 4946	. . . . . . 7 ⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛) = ∪ 𝑛 ∈ (ℕ ∖ 𝐴)∅)
121	120, 95	eqtrd 2774	. . . . . 6 ⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛) = ∅)
122	96, 121	eqtr4d 2777	. . . . 5 ⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛) = ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛))
123	69, 122	uneq12d 4099	. . . 4 ⊢ (𝜑 → (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛)) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛)))
124	34, 38, 123	3eqtrrd 2779	. . 3 ⊢ (𝜑 → (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛)) = ∪ ran ((,) ∘ 𝐺))
125	9, 19, 124	3eqtrd 2778	. 2 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) = ∪ ran ((,) ∘ 𝐺))
126		volf 25514	. . . . . 6 ⊢ vol:dom vol⟶(0[,]+∞)
127	126	a1i 11	. . . . 5 ⊢ (𝜑 → vol:dom vol⟶(0[,]+∞))
128	3	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹:ℕ⟶(ℝ* × ℝ*))
129		simpr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
130	128, 129, 45	syl2anc 590	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹‘𝑛)))
131	49	fveq2d 6831	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((,)‘(𝐹‘𝑛)) = ((,)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩))
132	101	eqcomi 2748	. . . . . . . . . . 11 ⊢ ((,)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩) = ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛)))
133	132	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((,)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩) = ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))))
134	130, 131, 133	3eqtrd 2778	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))))
135		ioombl 25550	. . . . . . . . . 10 ⊢ ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) ∈ dom vol
136	135	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) ∈ dom vol)
137	134, 136	eqeltrd 2839	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) ∈ dom vol)
138	137	ralrimiva 3131	. . . . . . 7 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) ∈ dom vol)
139	6, 138	jca 516	. . . . . 6 ⊢ (𝜑 → (((,) ∘ 𝐹) Fn ℕ ∧ ∀𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) ∈ dom vol))
140		ffnfv 7060	. . . . . 6 ⊢ (((,) ∘ 𝐹):ℕ⟶dom vol ↔ (((,) ∘ 𝐹) Fn ℕ ∧ ∀𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) ∈ dom vol))
141	139, 140	sylibr 235	. . . . 5 ⊢ (𝜑 → ((,) ∘ 𝐹):ℕ⟶dom vol)
142		fco 6679	. . . . 5 ⊢ ((vol:dom vol⟶(0[,]+∞) ∧ ((,) ∘ 𝐹):ℕ⟶dom vol) → (vol ∘ ((,) ∘ 𝐹)):ℕ⟶(0[,]+∞))
143	127, 141, 142	syl2anc 590	. . . 4 ⊢ (𝜑 → (vol ∘ ((,) ∘ 𝐹)):ℕ⟶(0[,]+∞))
144	143	ffnd 6656	. . 3 ⊢ (𝜑 → (vol ∘ ((,) ∘ 𝐹)) Fn ℕ)
145	68	adantlr 721	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) = (((,) ∘ 𝐹)‘𝑛))
146	137	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) ∈ dom vol)
147	145, 146	eqeltrd 2839	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol)
148		simpll 772	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐴) → 𝜑)
149		eldif 3893	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (ℕ ∖ 𝐴) ↔ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐴))
150	149	bicomi 225	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐴) ↔ 𝑛 ∈ (ℕ ∖ 𝐴))
151	150	biimpi 217	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐴) → 𝑛 ∈ (ℕ ∖ 𝐴))
152	151	adantll 720	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐴) → 𝑛 ∈ (ℕ ∖ 𝐴))
153	117, 135	eqeltrrdi 2848	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ∅ ∈ dom vol)
154	92, 153	eqeltrd 2839	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol)
155	148, 152, 154	syl2anc 590	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol)
156	147, 155	pm2.61dan 818	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol)
157	156	ralrimiva 3131	. . . . . . 7 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) ∈ dom vol)
158	31, 157	jca 516	. . . . . 6 ⊢ (𝜑 → (((,) ∘ 𝐺) Fn ℕ ∧ ∀𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) ∈ dom vol))
159		ffnfv 7060	. . . . . 6 ⊢ (((,) ∘ 𝐺):ℕ⟶dom vol ↔ (((,) ∘ 𝐺) Fn ℕ ∧ ∀𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) ∈ dom vol))
160	158, 159	sylibr 235	. . . . 5 ⊢ (𝜑 → ((,) ∘ 𝐺):ℕ⟶dom vol)
161		fco 6679	. . . . 5 ⊢ ((vol:dom vol⟶(0[,]+∞) ∧ ((,) ∘ 𝐺):ℕ⟶dom vol) → (vol ∘ ((,) ∘ 𝐺)):ℕ⟶(0[,]+∞))
162	127, 160, 161	syl2anc 590	. . . 4 ⊢ (𝜑 → (vol ∘ ((,) ∘ 𝐺)):ℕ⟶(0[,]+∞))
163	162	ffnd 6656	. . 3 ⊢ (𝜑 → (vol ∘ ((,) ∘ 𝐺)) Fn ℕ)
164	145	eqcomd 2745	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛))
165	119, 92	eqtr4d 2777	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛))
166	148, 152, 165	syl2anc 590	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛))
167	164, 166	pm2.61dan 818	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛))
168	167	fveq2d 6831	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘(((,) ∘ 𝐹)‘𝑛)) = (vol‘(((,) ∘ 𝐺)‘𝑛)))
169		fnfun 6585	. . . . . . 7 ⊢ (((,) ∘ 𝐹) Fn ℕ → Fun ((,) ∘ 𝐹))
170	6, 169	syl 17	. . . . . 6 ⊢ (𝜑 → Fun ((,) ∘ 𝐹))
171	170	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Fun ((,) ∘ 𝐹))
172	5	fdmd 6665	. . . . . . . 8 ⊢ (𝜑 → dom ((,) ∘ 𝐹) = ℕ)
173	172	eqcomd 2745	. . . . . . 7 ⊢ (𝜑 → ℕ = dom ((,) ∘ 𝐹))
174	173	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ℕ = dom ((,) ∘ 𝐹))
175	129, 174	eleqtrd 2841	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ dom ((,) ∘ 𝐹))
176		fvco 6925	. . . . 5 ⊢ ((Fun ((,) ∘ 𝐹) ∧ 𝑛 ∈ dom ((,) ∘ 𝐹)) → ((vol ∘ ((,) ∘ 𝐹))‘𝑛) = (vol‘(((,) ∘ 𝐹)‘𝑛)))
177	171, 175, 176	syl2anc 590	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol ∘ ((,) ∘ 𝐹))‘𝑛) = (vol‘(((,) ∘ 𝐹)‘𝑛)))
178		fnfun 6585	. . . . . . 7 ⊢ (((,) ∘ 𝐺) Fn ℕ → Fun ((,) ∘ 𝐺))
179	31, 178	syl 17	. . . . . 6 ⊢ (𝜑 → Fun ((,) ∘ 𝐺))
180	179	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Fun ((,) ∘ 𝐺))
181	30	fdmd 6665	. . . . . . . 8 ⊢ (𝜑 → dom ((,) ∘ 𝐺) = ℕ)
182	181	eqcomd 2745	. . . . . . 7 ⊢ (𝜑 → ℕ = dom ((,) ∘ 𝐺))
183	182	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ℕ = dom ((,) ∘ 𝐺))
184	129, 183	eleqtrd 2841	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ dom ((,) ∘ 𝐺))
185		fvco 6925	. . . . 5 ⊢ ((Fun ((,) ∘ 𝐺) ∧ 𝑛 ∈ dom ((,) ∘ 𝐺)) → ((vol ∘ ((,) ∘ 𝐺))‘𝑛) = (vol‘(((,) ∘ 𝐺)‘𝑛)))
186	180, 184, 185	syl2anc 590	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol ∘ ((,) ∘ 𝐺))‘𝑛) = (vol‘(((,) ∘ 𝐺)‘𝑛)))
187	168, 177, 186	3eqtr4d 2784	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol ∘ ((,) ∘ 𝐹))‘𝑛) = ((vol ∘ ((,) ∘ 𝐺))‘𝑛))
188	144, 163, 187	eqfnfvd 6974	. 2 ⊢ (𝜑 → (vol ∘ ((,) ∘ 𝐹)) = (vol ∘ ((,) ∘ 𝐺)))
189	125, 188	jca 516	1 ⊢ (𝜑 → (∪ ran ((,) ∘ 𝐹) = ∪ ran ((,) ∘ 𝐺) ∧ (vol ∘ ((,) ∘ 𝐹)) = (vol ∘ ((,) ∘ 𝐺))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ∀wral 3053  {crab 3391  Vcvv 3431   ∖ cdif 3880   ∪ cun 3881   ⊆ wss 3883  ∅c0 4261  ifcif 4454  𝒫 cpw 4529  ⟨cop 4561  ∪ cuni 4838  ∪ ciun 4921   class class class wbr 5072   ↦ cmpt 5153   × cxp 5616  dom cdm 5618  ran crn 5619   ∘ ccom 5622  Fun wfun 6479   Fn wfn 6480  ⟶wf 6481  ‘cfv 6485  (class class class)co 7356  1^st c1st 7929  2^nd c2nd 7930  ℝcr 11028  0cc0 11029  +∞cpnf 11167  ℝ^*cxr 11169   < clt 11170   ≤ cle 11171  ℕcn 12165  (,)cioo 13289  [,]cicc 13292  volcvol 25448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-rep 5199  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-inf2 9553  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106  ax-pre-sup 11107

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-rmo 3344  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-int 4878  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-se 5572  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-isom 6494  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-of 7620  df-om 7807  df-1st 7931  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-1o 8395  df-2o 8396  df-er 8633  df-map 8765  df-pm 8766  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-sup 9345  df-inf 9346  df-oi 9415  df-dju 9816  df-card 9854  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-div 11799  df-nn 12166  df-2 12235  df-3 12236  df-n0 12429  df-z 12516  df-uz 12780  df-q 12890  df-rp 12934  df-xadd 13055  df-ioo 13293  df-ico 13295  df-icc 13296  df-fz 13453  df-fzo 13600  df-fl 13742  df-seq 13955  df-exp 14015  df-hash 14284  df-cj 15052  df-re 15053  df-im 15054  df-sqrt 15188  df-abs 15189  df-clim 15441  df-rlim 15442  df-sum 15640  df-xmet 21340  df-met 21341  df-ovol 25449  df-vol 25450

This theorem is referenced by:  ovolval4lem2  47093