Theorem ovolval4lem1 42938

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 12838	. . . . . . . 8 ⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ
2	1	a1i 11	. . . . . . 7 ⊢ (𝜑 → (,):(ℝ* × ℝ*)⟶𝒫 ℝ)
3		ovolval4lem1.f	. . . . . . 7 ⊢ (𝜑 → 𝐹:ℕ⟶(ℝ* × ℝ*))
4		fco 6533	. . . . . . 7 ⊢ (((,):(ℝ* × ℝ*)⟶𝒫 ℝ ∧ 𝐹:ℕ⟶(ℝ* × ℝ*)) → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
5	2, 3, 4	syl2anc 586	. . . . . 6 ⊢ (𝜑 → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
6	5	ffnd 6517	. . . . 5 ⊢ (𝜑 → ((,) ∘ 𝐹) Fn ℕ)
7		fniunfv 7008	. . . . 5 ⊢ (((,) ∘ 𝐹) Fn ℕ → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = ∪ ran ((,) ∘ 𝐹))
8	6, 7	syl 17	. . . 4 ⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = ∪ ran ((,) ∘ 𝐹))
9	8	eqcomd 2829	. . 3 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) = ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛))
10		ovolval4lem1.a	. . . . . . . . 9 ⊢ 𝐴 = {𝑛 ∈ ℕ ∣ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))}
11		ssrab2 4058	. . . . . . . . 9 ⊢ {𝑛 ∈ ℕ ∣ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))} ⊆ ℕ
12	10, 11	eqsstri 4003	. . . . . . . 8 ⊢ 𝐴 ⊆ ℕ
13		undif 4432	. . . . . . . 8 ⊢ (𝐴 ⊆ ℕ ↔ (𝐴 ∪ (ℕ ∖ 𝐴)) = ℕ)
14	12, 13	mpbi 232	. . . . . . 7 ⊢ (𝐴 ∪ (ℕ ∖ 𝐴)) = ℕ
15	14	eqcomi 2832	. . . . . 6 ⊢ ℕ = (𝐴 ∪ (ℕ ∖ 𝐴))
16	15	iuneq1i 41357	. . . . 5 ⊢ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = ∪ 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐹)‘𝑛)
17		iunxun 5018	. . . . 5 ⊢ ∪ 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐹)‘𝑛) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛))
18	16, 17	eqtri 2846	. . . 4 ⊢ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛))
19	18	a1i 11	. . 3 ⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛)))
20	3	ffvelrnda 6853	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ (ℝ* × ℝ*))
21		xp1st 7723	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑛) ∈ (ℝ* × ℝ*) → (1st ‘(𝐹‘𝑛)) ∈ ℝ*)
22	20, 21	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐹‘𝑛)) ∈ ℝ*)
23		xp2nd 7724	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑛) ∈ (ℝ* × ℝ*) → (2nd ‘(𝐹‘𝑛)) ∈ ℝ*)
24	20, 23	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐹‘𝑛)) ∈ ℝ*)
25	24, 22	ifcld 4514	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))) ∈ ℝ*)
26	22, 25	opelxpd 5595	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩ ∈ (ℝ* × ℝ*))
27		ovolval4lem1.g	. . . . . . . . 9 ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩)
28	26, 27	fmptd 6880	. . . . . . . 8 ⊢ (𝜑 → 𝐺:ℕ⟶(ℝ* × ℝ*))
29		fco 6533	. . . . . . . 8 ⊢ (((,):(ℝ* × ℝ*)⟶𝒫 ℝ ∧ 𝐺:ℕ⟶(ℝ* × ℝ*)) → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
30	2, 28, 29	syl2anc 586	. . . . . . 7 ⊢ (𝜑 → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
31	30	ffnd 6517	. . . . . 6 ⊢ (𝜑 → ((,) ∘ 𝐺) Fn ℕ)
32		fniunfv 7008	. . . . . 6 ⊢ (((,) ∘ 𝐺) Fn ℕ → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = ∪ ran ((,) ∘ 𝐺))
33	31, 32	syl 17	. . . . 5 ⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = ∪ ran ((,) ∘ 𝐺))
34	33	eqcomd 2829	. . . 4 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛))
35	15	iuneq1i 41357	. . . . . 6 ⊢ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = ∪ 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐺)‘𝑛)
36		iunxun 5018	. . . . . 6 ⊢ ∪ 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐺)‘𝑛) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛))
37	35, 36	eqtri 2846	. . . . 5 ⊢ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛))
38	37	a1i 11	. . . 4 ⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛)))
39	28	adantr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐺:ℕ⟶(ℝ* × ℝ*))
40	12	sseli 3965	. . . . . . . . 9 ⊢ (𝑛 ∈ 𝐴 → 𝑛 ∈ ℕ)
41	40	adantl 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ ℕ)
42		fvco3 6762	. . . . . . . 8 ⊢ ((𝐺:ℕ⟶(ℝ* × ℝ*) ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐺)‘𝑛) = ((,)‘(𝐺‘𝑛)))
43	39, 41, 42	syl2anc 586	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) = ((,)‘(𝐺‘𝑛)))
44	3	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐹:ℕ⟶(ℝ* × ℝ*))
45		fvco3 6762	. . . . . . . . 9 ⊢ ((𝐹:ℕ⟶(ℝ* × ℝ*) ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹‘𝑛)))
46	44, 41, 45	syl2anc 586	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹‘𝑛)))
47		simpl 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝜑)
48		1st2nd2 7730	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑛) ∈ (ℝ* × ℝ*) → (𝐹‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
49	20, 48	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
50	47, 41, 49	syl2anc 586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐹‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
51	27	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺 = (𝑛 ∈ ℕ ↦ ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩))
52	26	elexd 3516	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩ ∈ V)
53	51, 52	fvmpt2d 6783	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩)
54	47, 41, 53	syl2anc 586	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐺‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩)
55	10	eleq2i 2906	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ 𝐴 ↔ 𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))})
56	55	biimpi 218	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ 𝐴 → 𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))})
57		rabid 3380	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))} ↔ (𝑛 ∈ ℕ ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))))
58	56, 57	sylib 220	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ 𝐴 → (𝑛 ∈ ℕ ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))))
59	58	simprd 498	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ 𝐴 → (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)))
60	59	adantl 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)))
61	60	iftrued 4477	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))) = (2nd ‘(𝐹‘𝑛)))
62	61	opeq2d 4812	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩ = ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
63		eqidd 2824	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩ = ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
64	54, 62, 63	3eqtrd 2862	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐺‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
65	50, 64	eqtr4d 2861	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐹‘𝑛) = (𝐺‘𝑛))
66	65	fveq2d 6676	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((,)‘(𝐹‘𝑛)) = ((,)‘(𝐺‘𝑛)))
67	46, 66	eqtrd 2858	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐺‘𝑛)))
68	43, 67	eqtr4d 2861	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) = (((,) ∘ 𝐹)‘𝑛))
69	68	iuneq2dv 4945	. . . . 5 ⊢ (𝜑 → ∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) = ∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛))
70	28	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → 𝐺:ℕ⟶(ℝ* × ℝ*))
71		eldifi 4105	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (ℕ ∖ 𝐴) → 𝑛 ∈ ℕ)
72	71	adantl 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → 𝑛 ∈ ℕ)
73	70, 72, 42	syl2anc 586	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐺)‘𝑛) = ((,)‘(𝐺‘𝑛)))
74		simpl 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → 𝜑)
75	74, 72, 53	syl2anc 586	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (𝐺‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩)
76	71	anim1i 616	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (ℕ ∖ 𝐴) ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) → (𝑛 ∈ ℕ ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))))
77	76, 57	sylibr 236	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ (ℕ ∖ 𝐴) ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) → 𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))})
78	77, 55	sylibr 236	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ (ℕ ∖ 𝐴) ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) → 𝑛 ∈ 𝐴)
79	78	adantll 712	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) → 𝑛 ∈ 𝐴)
80		eldifn 4106	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (ℕ ∖ 𝐴) → ¬ 𝑛 ∈ 𝐴)
81	80	ad2antlr 725	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) → ¬ 𝑛 ∈ 𝐴)
82	79, 81	pm2.65da 815	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ¬ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)))
83	82	iffalsed 4480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))) = (1st ‘(𝐹‘𝑛)))
84	83	opeq2d 4812	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩ = ⟨(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))⟩)
85	75, 84	eqtrd 2858	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (𝐺‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))⟩)
86	85	fveq2d 6676	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘(𝐺‘𝑛)) = ((,)‘⟨(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))⟩))
87		iooid 12769	. . . . . . . . . . . 12 ⊢ ((1st ‘(𝐹‘𝑛))(,)(1st ‘(𝐹‘𝑛))) = ∅
88	87	eqcomi 2832	. . . . . . . . . . 11 ⊢ ∅ = ((1st ‘(𝐹‘𝑛))(,)(1st ‘(𝐹‘𝑛)))
89		df-ov 7161	. . . . . . . . . . 11 ⊢ ((1st ‘(𝐹‘𝑛))(,)(1st ‘(𝐹‘𝑛))) = ((,)‘⟨(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))⟩)
90	88, 89	eqtr2i 2847	. . . . . . . . . 10 ⊢ ((,)‘⟨(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))⟩) = ∅
91	90	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘⟨(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))⟩) = ∅)
92	73, 86, 91	3eqtrd 2862	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐺)‘𝑛) = ∅)
93	92	iuneq2dv 4945	. . . . . . 7 ⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛) = ∪ 𝑛 ∈ (ℕ ∖ 𝐴)∅)
94		iun0 4987	. . . . . . . 8 ⊢ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)∅ = ∅
95	94	a1i 11	. . . . . . 7 ⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)∅ = ∅)
96	93, 95	eqtrd 2858	. . . . . 6 ⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛) = ∅)
97	74, 3	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → 𝐹:ℕ⟶(ℝ* × ℝ*))
98	97, 72, 45	syl2anc 586	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹‘𝑛)))
99	74, 72, 49	syl2anc 586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (𝐹‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
100	99	fveq2d 6676	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘(𝐹‘𝑛)) = ((,)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩))
101		df-ov 7161	. . . . . . . . . . 11 ⊢ ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ((,)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
102	101	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ((,)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩))
103		simplr 767	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → 𝑛 ∈ (ℕ ∖ 𝐴))
104	72, 22	syldan 593	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (1st ‘(𝐹‘𝑛)) ∈ ℝ*)
105	104	adantr 483	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → (1st ‘(𝐹‘𝑛)) ∈ ℝ*)
106	72, 24	syldan 593	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (2nd ‘(𝐹‘𝑛)) ∈ ℝ*)
107	106	adantr 483	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → (2nd ‘(𝐹‘𝑛)) ∈ ℝ*)
108		simpr 487	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛)))
109	105, 107	xrltnled 41638	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → ((1st ‘(𝐹‘𝑛)) < (2nd ‘(𝐹‘𝑛)) ↔ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))))
110	108, 109	mpbird 259	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → (1st ‘(𝐹‘𝑛)) < (2nd ‘(𝐹‘𝑛)))
111	105, 107, 110	xrltled 12546	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)))
112	103, 111, 78	syl2anc 586	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → 𝑛 ∈ 𝐴)
113	80	ad2antlr 725	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → ¬ 𝑛 ∈ 𝐴)
114	112, 113	condan 816	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛)))
115		ioo0 12766	. . . . . . . . . . . 12 ⊢ (((1st ‘(𝐹‘𝑛)) ∈ ℝ* ∧ (2nd ‘(𝐹‘𝑛)) ∈ ℝ*) → (((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ∅ ↔ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))))
116	104, 106, 115	syl2anc 586	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ∅ ↔ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))))
117	114, 116	mpbird 259	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ∅)
118	102, 117	eqtr3d 2860	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩) = ∅)
119	98, 100, 118	3eqtrd 2862	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐹)‘𝑛) = ∅)
120	119	iuneq2dv 4945	. . . . . . 7 ⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛) = ∪ 𝑛 ∈ (ℕ ∖ 𝐴)∅)
121	120, 95	eqtrd 2858	. . . . . 6 ⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛) = ∅)
122	96, 121	eqtr4d 2861	. . . . 5 ⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛) = ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛))
123	69, 122	uneq12d 4142	. . . 4 ⊢ (𝜑 → (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛)) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛)))
124	34, 38, 123	3eqtrrd 2863	. . 3 ⊢ (𝜑 → (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛)) = ∪ ran ((,) ∘ 𝐺))
125	9, 19, 124	3eqtrd 2862	. 2 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) = ∪ ran ((,) ∘ 𝐺))
126		volf 24132	. . . . . 6 ⊢ vol:dom vol⟶(0[,]+∞)
127	126	a1i 11	. . . . 5 ⊢ (𝜑 → vol:dom vol⟶(0[,]+∞))
128	3	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹:ℕ⟶(ℝ* × ℝ*))
129		simpr 487	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
130	128, 129, 45	syl2anc 586	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹‘𝑛)))
131	49	fveq2d 6676	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((,)‘(𝐹‘𝑛)) = ((,)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩))
132	101	eqcomi 2832	. . . . . . . . . . 11 ⊢ ((,)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩) = ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛)))
133	132	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((,)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩) = ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))))
134	130, 131, 133	3eqtrd 2862	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))))
135		ioombl 24168	. . . . . . . . . 10 ⊢ ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) ∈ dom vol
136	135	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) ∈ dom vol)
137	134, 136	eqeltrd 2915	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) ∈ dom vol)
138	137	ralrimiva 3184	. . . . . . 7 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) ∈ dom vol)
139	6, 138	jca 514	. . . . . 6 ⊢ (𝜑 → (((,) ∘ 𝐹) Fn ℕ ∧ ∀𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) ∈ dom vol))
140		ffnfv 6884	. . . . . 6 ⊢ (((,) ∘ 𝐹):ℕ⟶dom vol ↔ (((,) ∘ 𝐹) Fn ℕ ∧ ∀𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) ∈ dom vol))
141	139, 140	sylibr 236	. . . . 5 ⊢ (𝜑 → ((,) ∘ 𝐹):ℕ⟶dom vol)
142		fco 6533	. . . . 5 ⊢ ((vol:dom vol⟶(0[,]+∞) ∧ ((,) ∘ 𝐹):ℕ⟶dom vol) → (vol ∘ ((,) ∘ 𝐹)):ℕ⟶(0[,]+∞))
143	127, 141, 142	syl2anc 586	. . . 4 ⊢ (𝜑 → (vol ∘ ((,) ∘ 𝐹)):ℕ⟶(0[,]+∞))
144	143	ffnd 6517	. . 3 ⊢ (𝜑 → (vol ∘ ((,) ∘ 𝐹)) Fn ℕ)
145	68	adantlr 713	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) = (((,) ∘ 𝐹)‘𝑛))
146	137	adantr 483	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) ∈ dom vol)
147	145, 146	eqeltrd 2915	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol)
148		simpll 765	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐴) → 𝜑)
149		eldif 3948	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (ℕ ∖ 𝐴) ↔ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐴))
150	149	bicomi 226	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐴) ↔ 𝑛 ∈ (ℕ ∖ 𝐴))
151	150	biimpi 218	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐴) → 𝑛 ∈ (ℕ ∖ 𝐴))
152	151	adantll 712	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐴) → 𝑛 ∈ (ℕ ∖ 𝐴))
153	117, 135	eqeltrrdi 2924	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ∅ ∈ dom vol)
154	92, 153	eqeltrd 2915	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol)
155	148, 152, 154	syl2anc 586	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol)
156	147, 155	pm2.61dan 811	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol)
157	156	ralrimiva 3184	. . . . . . 7 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) ∈ dom vol)
158	31, 157	jca 514	. . . . . 6 ⊢ (𝜑 → (((,) ∘ 𝐺) Fn ℕ ∧ ∀𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) ∈ dom vol))
159		ffnfv 6884	. . . . . 6 ⊢ (((,) ∘ 𝐺):ℕ⟶dom vol ↔ (((,) ∘ 𝐺) Fn ℕ ∧ ∀𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) ∈ dom vol))
160	158, 159	sylibr 236	. . . . 5 ⊢ (𝜑 → ((,) ∘ 𝐺):ℕ⟶dom vol)
161		fco 6533	. . . . 5 ⊢ ((vol:dom vol⟶(0[,]+∞) ∧ ((,) ∘ 𝐺):ℕ⟶dom vol) → (vol ∘ ((,) ∘ 𝐺)):ℕ⟶(0[,]+∞))
162	127, 160, 161	syl2anc 586	. . . 4 ⊢ (𝜑 → (vol ∘ ((,) ∘ 𝐺)):ℕ⟶(0[,]+∞))
163	162	ffnd 6517	. . 3 ⊢ (𝜑 → (vol ∘ ((,) ∘ 𝐺)) Fn ℕ)
164	145	eqcomd 2829	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛))
165	119, 92	eqtr4d 2861	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛))
166	148, 152, 165	syl2anc 586	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛))
167	164, 166	pm2.61dan 811	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛))
168	167	fveq2d 6676	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘(((,) ∘ 𝐹)‘𝑛)) = (vol‘(((,) ∘ 𝐺)‘𝑛)))
169		fnfun 6455	. . . . . . 7 ⊢ (((,) ∘ 𝐹) Fn ℕ → Fun ((,) ∘ 𝐹))
170	6, 169	syl 17	. . . . . 6 ⊢ (𝜑 → Fun ((,) ∘ 𝐹))
171	170	adantr 483	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Fun ((,) ∘ 𝐹))
172	5	fdmd 6525	. . . . . . . 8 ⊢ (𝜑 → dom ((,) ∘ 𝐹) = ℕ)
173	172	eqcomd 2829	. . . . . . 7 ⊢ (𝜑 → ℕ = dom ((,) ∘ 𝐹))
174	173	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ℕ = dom ((,) ∘ 𝐹))
175	129, 174	eleqtrd 2917	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ dom ((,) ∘ 𝐹))
176		fvco 6761	. . . . 5 ⊢ ((Fun ((,) ∘ 𝐹) ∧ 𝑛 ∈ dom ((,) ∘ 𝐹)) → ((vol ∘ ((,) ∘ 𝐹))‘𝑛) = (vol‘(((,) ∘ 𝐹)‘𝑛)))
177	171, 175, 176	syl2anc 586	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol ∘ ((,) ∘ 𝐹))‘𝑛) = (vol‘(((,) ∘ 𝐹)‘𝑛)))
178		fnfun 6455	. . . . . . 7 ⊢ (((,) ∘ 𝐺) Fn ℕ → Fun ((,) ∘ 𝐺))
179	31, 178	syl 17	. . . . . 6 ⊢ (𝜑 → Fun ((,) ∘ 𝐺))
180	179	adantr 483	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Fun ((,) ∘ 𝐺))
181	30	fdmd 6525	. . . . . . . 8 ⊢ (𝜑 → dom ((,) ∘ 𝐺) = ℕ)
182	181	eqcomd 2829	. . . . . . 7 ⊢ (𝜑 → ℕ = dom ((,) ∘ 𝐺))
183	182	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ℕ = dom ((,) ∘ 𝐺))
184	129, 183	eleqtrd 2917	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ dom ((,) ∘ 𝐺))
185		fvco 6761	. . . . 5 ⊢ ((Fun ((,) ∘ 𝐺) ∧ 𝑛 ∈ dom ((,) ∘ 𝐺)) → ((vol ∘ ((,) ∘ 𝐺))‘𝑛) = (vol‘(((,) ∘ 𝐺)‘𝑛)))
186	180, 184, 185	syl2anc 586	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol ∘ ((,) ∘ 𝐺))‘𝑛) = (vol‘(((,) ∘ 𝐺)‘𝑛)))
187	168, 177, 186	3eqtr4d 2868	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol ∘ ((,) ∘ 𝐹))‘𝑛) = ((vol ∘ ((,) ∘ 𝐺))‘𝑛))
188	144, 163, 187	eqfnfvd 6807	. 2 ⊢ (𝜑 → (vol ∘ ((,) ∘ 𝐹)) = (vol ∘ ((,) ∘ 𝐺)))
189	125, 188	jca 514	1 ⊢ (𝜑 → (∪ ran ((,) ∘ 𝐹) = ∪ ran ((,) ∘ 𝐺) ∧ (vol ∘ ((,) ∘ 𝐹)) = (vol ∘ ((,) ∘ 𝐺))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∀wral 3140  {crab 3144  Vcvv 3496   ∖ cdif 3935   ∪ cun 3936   ⊆ wss 3938  ∅c0 4293  ifcif 4469  𝒫 cpw 4541  ⟨cop 4575  ∪ cuni 4840  ∪ ciun 4921   class class class wbr 5068   ↦ cmpt 5148   × cxp 5555  dom cdm 5557  ran crn 5558   ∘ ccom 5561  Fun wfun 6351   Fn wfn 6352  ⟶wf 6353  ‘cfv 6357  (class class class)co 7158  1^st c1st 7689  2^nd c2nd 7690  ℝcr 10538  0cc0 10539  +∞cpnf 10674  ℝ^*cxr 10676   < clt 10677   ≤ cle 10678  ℕcn 11640  (,)cioo 12741  [,]cicc 12744  volcvol 24066

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-rlim 14848  df-sum 15045  df-xmet 20540  df-met 20541  df-ovol 24067  df-vol 24068

This theorem is referenced by:  ovolval4lem2  42939