Theorem ovolval4lem1 46640

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 13384	. . . . . . . 8 ⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ
2	1	a1i 11	. . . . . . 7 ⊢ (𝜑 → (,):(ℝ* × ℝ*)⟶𝒫 ℝ)
3		ovolval4lem1.f	. . . . . . 7 ⊢ (𝜑 → 𝐹:ℕ⟶(ℝ* × ℝ*))
4		fco 6694	. . . . . . 7 ⊢ (((,):(ℝ* × ℝ*)⟶𝒫 ℝ ∧ 𝐹:ℕ⟶(ℝ* × ℝ*)) → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
5	2, 3, 4	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
6	5	ffnd 6671	. . . . 5 ⊢ (𝜑 → ((,) ∘ 𝐹) Fn ℕ)
7		fniunfv 7203	. . . . 5 ⊢ (((,) ∘ 𝐹) Fn ℕ → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = ∪ ran ((,) ∘ 𝐹))
8	6, 7	syl 17	. . . 4 ⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = ∪ ran ((,) ∘ 𝐹))
9	8	eqcomd 2735	. . 3 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) = ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛))
10		ovolval4lem1.a	. . . . . . . . 9 ⊢ 𝐴 = {𝑛 ∈ ℕ ∣ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))}
11		ssrab2 4039	. . . . . . . . 9 ⊢ {𝑛 ∈ ℕ ∣ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))} ⊆ ℕ
12	10, 11	eqsstri 3990	. . . . . . . 8 ⊢ 𝐴 ⊆ ℕ
13		undif 4441	. . . . . . . 8 ⊢ (𝐴 ⊆ ℕ ↔ (𝐴 ∪ (ℕ ∖ 𝐴)) = ℕ)
14	12, 13	mpbi 230	. . . . . . 7 ⊢ (𝐴 ∪ (ℕ ∖ 𝐴)) = ℕ
15	14	eqcomi 2738	. . . . . 6 ⊢ ℕ = (𝐴 ∪ (ℕ ∖ 𝐴))
16	15	iuneq1i 45072	. . . . 5 ⊢ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = ∪ 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐹)‘𝑛)
17		iunxun 5053	. . . . 5 ⊢ ∪ 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐹)‘𝑛) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛))
18	16, 17	eqtri 2752	. . . 4 ⊢ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛))
19	18	a1i 11	. . 3 ⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛)))
20	3	ffvelcdmda 7038	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ (ℝ* × ℝ*))
21		xp1st 7979	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑛) ∈ (ℝ* × ℝ*) → (1st ‘(𝐹‘𝑛)) ∈ ℝ*)
22	20, 21	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐹‘𝑛)) ∈ ℝ*)
23		xp2nd 7980	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑛) ∈ (ℝ* × ℝ*) → (2nd ‘(𝐹‘𝑛)) ∈ ℝ*)
24	20, 23	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐹‘𝑛)) ∈ ℝ*)
25	24, 22	ifcld 4531	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))) ∈ ℝ*)
26	22, 25	opelxpd 5670	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩ ∈ (ℝ* × ℝ*))
27		ovolval4lem1.g	. . . . . . . . 9 ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩)
28	26, 27	fmptd 7068	. . . . . . . 8 ⊢ (𝜑 → 𝐺:ℕ⟶(ℝ* × ℝ*))
29		fco 6694	. . . . . . . 8 ⊢ (((,):(ℝ* × ℝ*)⟶𝒫 ℝ ∧ 𝐺:ℕ⟶(ℝ* × ℝ*)) → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
30	2, 28, 29	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
31	30	ffnd 6671	. . . . . 6 ⊢ (𝜑 → ((,) ∘ 𝐺) Fn ℕ)
32		fniunfv 7203	. . . . . 6 ⊢ (((,) ∘ 𝐺) Fn ℕ → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = ∪ ran ((,) ∘ 𝐺))
33	31, 32	syl 17	. . . . 5 ⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = ∪ ran ((,) ∘ 𝐺))
34	33	eqcomd 2735	. . . 4 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛))
35	15	iuneq1i 45072	. . . . . 6 ⊢ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = ∪ 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐺)‘𝑛)
36		iunxun 5053	. . . . . 6 ⊢ ∪ 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐺)‘𝑛) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛))
37	35, 36	eqtri 2752	. . . . 5 ⊢ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛))
38	37	a1i 11	. . . 4 ⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛)))
39	28	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐺:ℕ⟶(ℝ* × ℝ*))
40	12	sseli 3939	. . . . . . . . 9 ⊢ (𝑛 ∈ 𝐴 → 𝑛 ∈ ℕ)
41	40	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ ℕ)
42		fvco3 6942	. . . . . . . 8 ⊢ ((𝐺:ℕ⟶(ℝ* × ℝ*) ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐺)‘𝑛) = ((,)‘(𝐺‘𝑛)))
43	39, 41, 42	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) = ((,)‘(𝐺‘𝑛)))
44	3	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐹:ℕ⟶(ℝ* × ℝ*))
45		fvco3 6942	. . . . . . . . 9 ⊢ ((𝐹:ℕ⟶(ℝ* × ℝ*) ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹‘𝑛)))
46	44, 41, 45	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹‘𝑛)))
47		simpl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝜑)
48		1st2nd2 7986	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑛) ∈ (ℝ* × ℝ*) → (𝐹‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
49	20, 48	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
50	47, 41, 49	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐹‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
51	27	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺 = (𝑛 ∈ ℕ ↦ ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩))
52	26	elexd 3468	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩ ∈ V)
53	51, 52	fvmpt2d 6963	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩)
54	47, 41, 53	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐺‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩)
55	10	eleq2i 2820	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ 𝐴 ↔ 𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))})
56	55	biimpi 216	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ 𝐴 → 𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))})
57		rabid 3424	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))} ↔ (𝑛 ∈ ℕ ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))))
58	56, 57	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ 𝐴 → (𝑛 ∈ ℕ ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))))
59	58	simprd 495	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ 𝐴 → (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)))
60	59	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)))
61	60	iftrued 4492	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))) = (2nd ‘(𝐹‘𝑛)))
62	61	opeq2d 4840	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩ = ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
63		eqidd 2730	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩ = ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
64	54, 62, 63	3eqtrd 2768	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐺‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
65	50, 64	eqtr4d 2767	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐹‘𝑛) = (𝐺‘𝑛))
66	65	fveq2d 6844	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((,)‘(𝐹‘𝑛)) = ((,)‘(𝐺‘𝑛)))
67	46, 66	eqtrd 2764	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐺‘𝑛)))
68	43, 67	eqtr4d 2767	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) = (((,) ∘ 𝐹)‘𝑛))
69	68	iuneq2dv 4976	. . . . 5 ⊢ (𝜑 → ∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) = ∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛))
70	28	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → 𝐺:ℕ⟶(ℝ* × ℝ*))
71		eldifi 4090	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (ℕ ∖ 𝐴) → 𝑛 ∈ ℕ)
72	71	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → 𝑛 ∈ ℕ)
73	70, 72, 42	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐺)‘𝑛) = ((,)‘(𝐺‘𝑛)))
74		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → 𝜑)
75	74, 72, 53	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (𝐺‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩)
76	71	anim1i 615	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑛 ∈ (ℕ ∖ 𝐴) ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) → (𝑛 ∈ ℕ ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))))
77	76, 57	sylibr 234	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ (ℕ ∖ 𝐴) ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) → 𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))})
78	77, 55	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ (ℕ ∖ 𝐴) ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) → 𝑛 ∈ 𝐴)
79	78	adantll 714	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) → 𝑛 ∈ 𝐴)
80		eldifn 4091	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (ℕ ∖ 𝐴) → ¬ 𝑛 ∈ 𝐴)
81	80	ad2antlr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) → ¬ 𝑛 ∈ 𝐴)
82	79, 81	pm2.65da 816	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ¬ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)))
83	82	iffalsed 4495	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))) = (1st ‘(𝐹‘𝑛)))
84	83	opeq2d 4840	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩ = ⟨(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))⟩)
85	75, 84	eqtrd 2764	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (𝐺‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))⟩)
86	85	fveq2d 6844	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘(𝐺‘𝑛)) = ((,)‘⟨(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))⟩))
87		iooid 13310	. . . . . . . . . . . 12 ⊢ ((1st ‘(𝐹‘𝑛))(,)(1st ‘(𝐹‘𝑛))) = ∅
88	87	eqcomi 2738	. . . . . . . . . . 11 ⊢ ∅ = ((1st ‘(𝐹‘𝑛))(,)(1st ‘(𝐹‘𝑛)))
89		df-ov 7372	. . . . . . . . . . 11 ⊢ ((1st ‘(𝐹‘𝑛))(,)(1st ‘(𝐹‘𝑛))) = ((,)‘⟨(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))⟩)
90	88, 89	eqtr2i 2753	. . . . . . . . . 10 ⊢ ((,)‘⟨(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))⟩) = ∅
91	90	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘⟨(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))⟩) = ∅)
92	73, 86, 91	3eqtrd 2768	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐺)‘𝑛) = ∅)
93	92	iuneq2dv 4976	. . . . . . 7 ⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛) = ∪ 𝑛 ∈ (ℕ ∖ 𝐴)∅)
94		iun0 5021	. . . . . . . 8 ⊢ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)∅ = ∅
95	94	a1i 11	. . . . . . 7 ⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)∅ = ∅)
96	93, 95	eqtrd 2764	. . . . . 6 ⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛) = ∅)
97	74, 3	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → 𝐹:ℕ⟶(ℝ* × ℝ*))
98	97, 72, 45	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹‘𝑛)))
99	74, 72, 49	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (𝐹‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
100	99	fveq2d 6844	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘(𝐹‘𝑛)) = ((,)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩))
101		df-ov 7372	. . . . . . . . . . 11 ⊢ ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ((,)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
102	101	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ((,)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩))
103		simplr 768	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → 𝑛 ∈ (ℕ ∖ 𝐴))
104	72, 22	syldan 591	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (1st ‘(𝐹‘𝑛)) ∈ ℝ*)
105	104	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → (1st ‘(𝐹‘𝑛)) ∈ ℝ*)
106	72, 24	syldan 591	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (2nd ‘(𝐹‘𝑛)) ∈ ℝ*)
107	106	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → (2nd ‘(𝐹‘𝑛)) ∈ ℝ*)
108		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛)))
109	105, 107	xrltnled 45352	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → ((1st ‘(𝐹‘𝑛)) < (2nd ‘(𝐹‘𝑛)) ↔ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))))
110	108, 109	mpbird 257	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → (1st ‘(𝐹‘𝑛)) < (2nd ‘(𝐹‘𝑛)))
111	105, 107, 110	xrltled 13086	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)))
112	103, 111, 78	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → 𝑛 ∈ 𝐴)
113	80	ad2antlr 727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → ¬ 𝑛 ∈ 𝐴)
114	112, 113	condan 817	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛)))
115		ioo0 13307	. . . . . . . . . . . 12 ⊢ (((1st ‘(𝐹‘𝑛)) ∈ ℝ* ∧ (2nd ‘(𝐹‘𝑛)) ∈ ℝ*) → (((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ∅ ↔ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))))
116	104, 106, 115	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ∅ ↔ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))))
117	114, 116	mpbird 257	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ∅)
118	102, 117	eqtr3d 2766	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩) = ∅)
119	98, 100, 118	3eqtrd 2768	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐹)‘𝑛) = ∅)
120	119	iuneq2dv 4976	. . . . . . 7 ⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛) = ∪ 𝑛 ∈ (ℕ ∖ 𝐴)∅)
121	120, 95	eqtrd 2764	. . . . . 6 ⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛) = ∅)
122	96, 121	eqtr4d 2767	. . . . 5 ⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛) = ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛))
123	69, 122	uneq12d 4128	. . . 4 ⊢ (𝜑 → (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛)) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛)))
124	34, 38, 123	3eqtrrd 2769	. . 3 ⊢ (𝜑 → (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛)) = ∪ ran ((,) ∘ 𝐺))
125	9, 19, 124	3eqtrd 2768	. 2 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) = ∪ ran ((,) ∘ 𝐺))
126		volf 25463	. . . . . 6 ⊢ vol:dom vol⟶(0[,]+∞)
127	126	a1i 11	. . . . 5 ⊢ (𝜑 → vol:dom vol⟶(0[,]+∞))
128	3	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐹:ℕ⟶(ℝ* × ℝ*))
129		simpr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
130	128, 129, 45	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹‘𝑛)))
131	49	fveq2d 6844	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((,)‘(𝐹‘𝑛)) = ((,)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩))
132	101	eqcomi 2738	. . . . . . . . . . 11 ⊢ ((,)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩) = ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛)))
133	132	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((,)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩) = ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))))
134	130, 131, 133	3eqtrd 2768	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))))
135		ioombl 25499	. . . . . . . . . 10 ⊢ ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) ∈ dom vol
136	135	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) ∈ dom vol)
137	134, 136	eqeltrd 2828	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) ∈ dom vol)
138	137	ralrimiva 3125	. . . . . . 7 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) ∈ dom vol)
139	6, 138	jca 511	. . . . . 6 ⊢ (𝜑 → (((,) ∘ 𝐹) Fn ℕ ∧ ∀𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) ∈ dom vol))
140		ffnfv 7073	. . . . . 6 ⊢ (((,) ∘ 𝐹):ℕ⟶dom vol ↔ (((,) ∘ 𝐹) Fn ℕ ∧ ∀𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) ∈ dom vol))
141	139, 140	sylibr 234	. . . . 5 ⊢ (𝜑 → ((,) ∘ 𝐹):ℕ⟶dom vol)
142		fco 6694	. . . . 5 ⊢ ((vol:dom vol⟶(0[,]+∞) ∧ ((,) ∘ 𝐹):ℕ⟶dom vol) → (vol ∘ ((,) ∘ 𝐹)):ℕ⟶(0[,]+∞))
143	127, 141, 142	syl2anc 584	. . . 4 ⊢ (𝜑 → (vol ∘ ((,) ∘ 𝐹)):ℕ⟶(0[,]+∞))
144	143	ffnd 6671	. . 3 ⊢ (𝜑 → (vol ∘ ((,) ∘ 𝐹)) Fn ℕ)
145	68	adantlr 715	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) = (((,) ∘ 𝐹)‘𝑛))
146	137	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) ∈ dom vol)
147	145, 146	eqeltrd 2828	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol)
148		simpll 766	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐴) → 𝜑)
149		eldif 3921	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (ℕ ∖ 𝐴) ↔ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐴))
150	149	bicomi 224	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐴) ↔ 𝑛 ∈ (ℕ ∖ 𝐴))
151	150	biimpi 216	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐴) → 𝑛 ∈ (ℕ ∖ 𝐴))
152	151	adantll 714	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐴) → 𝑛 ∈ (ℕ ∖ 𝐴))
153	117, 135	eqeltrrdi 2837	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ∅ ∈ dom vol)
154	92, 153	eqeltrd 2828	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol)
155	148, 152, 154	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol)
156	147, 155	pm2.61dan 812	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol)
157	156	ralrimiva 3125	. . . . . . 7 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) ∈ dom vol)
158	31, 157	jca 511	. . . . . 6 ⊢ (𝜑 → (((,) ∘ 𝐺) Fn ℕ ∧ ∀𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) ∈ dom vol))
159		ffnfv 7073	. . . . . 6 ⊢ (((,) ∘ 𝐺):ℕ⟶dom vol ↔ (((,) ∘ 𝐺) Fn ℕ ∧ ∀𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) ∈ dom vol))
160	158, 159	sylibr 234	. . . . 5 ⊢ (𝜑 → ((,) ∘ 𝐺):ℕ⟶dom vol)
161		fco 6694	. . . . 5 ⊢ ((vol:dom vol⟶(0[,]+∞) ∧ ((,) ∘ 𝐺):ℕ⟶dom vol) → (vol ∘ ((,) ∘ 𝐺)):ℕ⟶(0[,]+∞))
162	127, 160, 161	syl2anc 584	. . . 4 ⊢ (𝜑 → (vol ∘ ((,) ∘ 𝐺)):ℕ⟶(0[,]+∞))
163	162	ffnd 6671	. . 3 ⊢ (𝜑 → (vol ∘ ((,) ∘ 𝐺)) Fn ℕ)
164	145	eqcomd 2735	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛))
165	119, 92	eqtr4d 2767	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛))
166	148, 152, 165	syl2anc 584	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛))
167	164, 166	pm2.61dan 812	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛))
168	167	fveq2d 6844	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘(((,) ∘ 𝐹)‘𝑛)) = (vol‘(((,) ∘ 𝐺)‘𝑛)))
169		fnfun 6600	. . . . . . 7 ⊢ (((,) ∘ 𝐹) Fn ℕ → Fun ((,) ∘ 𝐹))
170	6, 169	syl 17	. . . . . 6 ⊢ (𝜑 → Fun ((,) ∘ 𝐹))
171	170	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Fun ((,) ∘ 𝐹))
172	5	fdmd 6680	. . . . . . . 8 ⊢ (𝜑 → dom ((,) ∘ 𝐹) = ℕ)
173	172	eqcomd 2735	. . . . . . 7 ⊢ (𝜑 → ℕ = dom ((,) ∘ 𝐹))
174	173	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ℕ = dom ((,) ∘ 𝐹))
175	129, 174	eleqtrd 2830	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ dom ((,) ∘ 𝐹))
176		fvco 6941	. . . . 5 ⊢ ((Fun ((,) ∘ 𝐹) ∧ 𝑛 ∈ dom ((,) ∘ 𝐹)) → ((vol ∘ ((,) ∘ 𝐹))‘𝑛) = (vol‘(((,) ∘ 𝐹)‘𝑛)))
177	171, 175, 176	syl2anc 584	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol ∘ ((,) ∘ 𝐹))‘𝑛) = (vol‘(((,) ∘ 𝐹)‘𝑛)))
178		fnfun 6600	. . . . . . 7 ⊢ (((,) ∘ 𝐺) Fn ℕ → Fun ((,) ∘ 𝐺))
179	31, 178	syl 17	. . . . . 6 ⊢ (𝜑 → Fun ((,) ∘ 𝐺))
180	179	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Fun ((,) ∘ 𝐺))
181	30	fdmd 6680	. . . . . . . 8 ⊢ (𝜑 → dom ((,) ∘ 𝐺) = ℕ)
182	181	eqcomd 2735	. . . . . . 7 ⊢ (𝜑 → ℕ = dom ((,) ∘ 𝐺))
183	182	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ℕ = dom ((,) ∘ 𝐺))
184	129, 183	eleqtrd 2830	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ dom ((,) ∘ 𝐺))
185		fvco 6941	. . . . 5 ⊢ ((Fun ((,) ∘ 𝐺) ∧ 𝑛 ∈ dom ((,) ∘ 𝐺)) → ((vol ∘ ((,) ∘ 𝐺))‘𝑛) = (vol‘(((,) ∘ 𝐺)‘𝑛)))
186	180, 184, 185	syl2anc 584	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol ∘ ((,) ∘ 𝐺))‘𝑛) = (vol‘(((,) ∘ 𝐺)‘𝑛)))
187	168, 177, 186	3eqtr4d 2774	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol ∘ ((,) ∘ 𝐹))‘𝑛) = ((vol ∘ ((,) ∘ 𝐺))‘𝑛))
188	144, 163, 187	eqfnfvd 6988	. 2 ⊢ (𝜑 → (vol ∘ ((,) ∘ 𝐹)) = (vol ∘ ((,) ∘ 𝐺)))
189	125, 188	jca 511	1 ⊢ (𝜑 → (∪ ran ((,) ∘ 𝐹) = ∪ ran ((,) ∘ 𝐺) ∧ (vol ∘ ((,) ∘ 𝐹)) = (vol ∘ ((,) ∘ 𝐺))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044  {crab 3402  Vcvv 3444   ∖ cdif 3908   ∪ cun 3909   ⊆ wss 3911  ∅c0 4292  ifcif 4484  𝒫 cpw 4559  ⟨cop 4591  ∪ cuni 4867  ∪ ciun 4951   class class class wbr 5102   ↦ cmpt 5183   × cxp 5629  dom cdm 5631  ran crn 5632   ∘ ccom 5635  Fun wfun 6493   Fn wfn 6494  ⟶wf 6495  ‘cfv 6499  (class class class)co 7369  1^st c1st 7945  2^nd c2nd 7946  ℝcr 11043  0cc0 11044  +∞cpnf 11181  ℝ^*cxr 11183   < clt 11184   ≤ cle 11185  ℕcn 12162  (,)cioo 13282  [,]cicc 13285  volcvol 25397

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5229  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-inf2 9570  ax-cnex 11100  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120  ax-pre-mulgt0 11121  ax-pre-sup 11122

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3351  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-int 4907  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-se 5585  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-isom 6508  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-of 7633  df-om 7823  df-1st 7947  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-1o 8411  df-2o 8412  df-er 8648  df-map 8778  df-pm 8779  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-sup 9369  df-inf 9370  df-oi 9439  df-dju 9830  df-card 9868  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190  df-sub 11383  df-neg 11384  df-div 11812  df-nn 12163  df-2 12225  df-3 12226  df-n0 12419  df-z 12506  df-uz 12770  df-q 12884  df-rp 12928  df-xadd 13049  df-ioo 13286  df-ico 13288  df-icc 13289  df-fz 13445  df-fzo 13592  df-fl 13730  df-seq 13943  df-exp 14003  df-hash 14272  df-cj 15041  df-re 15042  df-im 15043  df-sqrt 15177  df-abs 15178  df-clim 15430  df-rlim 15431  df-sum 15629  df-xmet 21289  df-met 21290  df-ovol 25398  df-vol 25399

This theorem is referenced by:  ovolval4lem2  46641