Theorem ovolval4lem1 46678

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 13464	. . . . . . . 8 ⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ
2	1	a1i 11	. . . . . . 7 ⊢ (𝜑 → (,):(ℝ* × ℝ*)⟶𝒫 ℝ)
3		ovolval4lem1.f	. . . . . . 7 ⊢ (𝜑 → 𝐹:ℕ⟶(ℝ* × ℝ*))
4		fco 6730	. . . . . . 7 ⊢ (((,):(ℝ* × ℝ*)⟶𝒫 ℝ ∧ 𝐹:ℕ⟶(ℝ* × ℝ*)) → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
5	2, 3, 4	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
6	5	ffnd 6707	. . . . 5 ⊢ (𝜑 → ((,) ∘ 𝐹) Fn ℕ)
7		fniunfv 7239	. . . . 5 ⊢ (((,) ∘ 𝐹) Fn ℕ → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = ∪ ran ((,) ∘ 𝐹))
8	6, 7	syl 17	. . . 4 ⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = ∪ ran ((,) ∘ 𝐹))
9	8	eqcomd 2741	. . 3 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) = ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛))
10		ovolval4lem1.a	. . . . . . . . 9 ⊢ 𝐴 = {𝑛 ∈ ℕ ∣ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))}
11		ssrab2 4055	. . . . . . . . 9 ⊢ {𝑛 ∈ ℕ ∣ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))} ⊆ ℕ
12	10, 11	eqsstri 4005	. . . . . . . 8 ⊢ 𝐴 ⊆ ℕ
13		undif 4457	. . . . . . . 8 ⊢ (𝐴 ⊆ ℕ ↔ (𝐴 ∪ (ℕ ∖ 𝐴)) = ℕ)
14	12, 13	mpbi 230	. . . . . . 7 ⊢ (𝐴 ∪ (ℕ ∖ 𝐴)) = ℕ
15	14	eqcomi 2744	. . . . . 6 ⊢ ℕ = (𝐴 ∪ (ℕ ∖ 𝐴))
16	15	iuneq1i 45109	. . . . 5 ⊢ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = ∪ 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐹)‘𝑛)
17		iunxun 5070	. . . . 5 ⊢ ∪ 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐹)‘𝑛) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛))
18	16, 17	eqtri 2758	. . . 4 ⊢ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛))
19	18	a1i 11	. . 3 ⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛)))
20	3	ffvelcdmda 7074	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ (ℝ* × ℝ*))
21		xp1st 8020	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑛) ∈ (ℝ* × ℝ*) → (1st ‘(𝐹‘𝑛)) ∈ ℝ*)
22	20, 21	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐹‘𝑛)) ∈ ℝ*)
23		xp2nd 8021	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑛) ∈ (ℝ* × ℝ*) → (2nd ‘(𝐹‘𝑛)) ∈ ℝ*)
24	20, 23	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐹‘𝑛)) ∈ ℝ*)
25	24, 22	ifcld 4547	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))) ∈ ℝ*)
26	22, 25	opelxpd 5693	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩ ∈ (ℝ* × ℝ*))
27		ovolval4lem1.g	. . . . . . . . 9 ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩)
28	26, 27	fmptd 7104	. . . . . . . 8 ⊢ (𝜑 → 𝐺:ℕ⟶(ℝ* × ℝ*))
29		fco 6730	. . . . . . . 8 ⊢ (((,):(ℝ* × ℝ*)⟶𝒫 ℝ ∧ 𝐺:ℕ⟶(ℝ* × ℝ*)) → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
30	2, 28, 29	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
31	30	ffnd 6707	. . . . . 6 ⊢ (𝜑 → ((,) ∘ 𝐺) Fn ℕ)
32		fniunfv 7239	. . . . . 6 ⊢ (((,) ∘ 𝐺) Fn ℕ → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = ∪ ran ((,) ∘ 𝐺))
33	31, 32	syl 17	. . . . 5 ⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = ∪ ran ((,) ∘ 𝐺))
34	33	eqcomd 2741	. . . 4 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛))
35	15	iuneq1i 45109	. . . . . 6 ⊢ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = ∪ 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐺)‘𝑛)
36		iunxun 5070	. . . . . 6 ⊢ ∪ 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐺)‘𝑛) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛))
37	35, 36	eqtri 2758	. . . . 5 ⊢ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛))
38	37	a1i 11	. . . 4 ⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛)))
39	28	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐺:ℕ⟶(ℝ* × ℝ*))
40	12	sseli 3954	. . . . . . . . 9 ⊢ (𝑛 ∈ 𝐴 → 𝑛 ∈ ℕ)
41	40	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ ℕ)
42		fvco3 6978	. . . . . . . 8 ⊢ ((𝐺:ℕ⟶(ℝ* × ℝ*) ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐺)‘𝑛) = ((,)‘(𝐺‘𝑛)))
43	39, 41, 42	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) = ((,)‘(𝐺‘𝑛)))
44	3	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐹:ℕ⟶(ℝ* × ℝ*))
45		fvco3 6978	. . . . . . . . 9 ⊢ ((𝐹:ℕ⟶(ℝ* × ℝ*) ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹‘𝑛)))
46	44, 41, 45	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹‘𝑛)))
47		simpl 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝜑)
48		1st2nd2 8027	. . . . . . . . . . . 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 3483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩ ∈ V)
53	51, 52	fvmpt2d 6999	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩)
54	47, 41, 53	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐺‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩)
55	10	eleq2i 2826	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ 𝐴 ↔ 𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))})
56	55	biimpi 216	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ 𝐴 → 𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))})
57		rabid 3437	. . . . . . . . . . . . . . . 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 4508	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))) = (2nd ‘(𝐹‘𝑛)))
62	61	opeq2d 4856	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩ = ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
63		eqidd 2736	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩ = ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
64	54, 62, 63	3eqtrd 2774	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐺‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
65	50, 64	eqtr4d 2773	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐹‘𝑛) = (𝐺‘𝑛))
66	65	fveq2d 6880	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((,)‘(𝐹‘𝑛)) = ((,)‘(𝐺‘𝑛)))
67	46, 66	eqtrd 2770	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐺‘𝑛)))
68	43, 67	eqtr4d 2773	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) = (((,) ∘ 𝐹)‘𝑛))
69	68	iuneq2dv 4992	. . . . 5 ⊢ (𝜑 → ∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) = ∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛))
70	28	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → 𝐺:ℕ⟶(ℝ* × ℝ*))
71		eldifi 4106	. . . . . . . . . . 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 4107	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (ℕ ∖ 𝐴) → ¬ 𝑛 ∈ 𝐴)
81	80	ad2antlr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) → ¬ 𝑛 ∈ 𝐴)
82	79, 81	pm2.65da 816	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ¬ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)))
83	82	iffalsed 4511	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))) = (1st ‘(𝐹‘𝑛)))
84	83	opeq2d 4856	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩ = ⟨(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))⟩)
85	75, 84	eqtrd 2770	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (𝐺‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))⟩)
86	85	fveq2d 6880	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘(𝐺‘𝑛)) = ((,)‘⟨(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))⟩))
87		iooid 13390	. . . . . . . . . . . 12 ⊢ ((1st ‘(𝐹‘𝑛))(,)(1st ‘(𝐹‘𝑛))) = ∅
88	87	eqcomi 2744	. . . . . . . . . . 11 ⊢ ∅ = ((1st ‘(𝐹‘𝑛))(,)(1st ‘(𝐹‘𝑛)))
89		df-ov 7408	. . . . . . . . . . 11 ⊢ ((1st ‘(𝐹‘𝑛))(,)(1st ‘(𝐹‘𝑛))) = ((,)‘⟨(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))⟩)
90	88, 89	eqtr2i 2759	. . . . . . . . . 10 ⊢ ((,)‘⟨(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))⟩) = ∅
91	90	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘⟨(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))⟩) = ∅)
92	73, 86, 91	3eqtrd 2774	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐺)‘𝑛) = ∅)
93	92	iuneq2dv 4992	. . . . . . 7 ⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛) = ∪ 𝑛 ∈ (ℕ ∖ 𝐴)∅)
94		iun0 5038	. . . . . . . 8 ⊢ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)∅ = ∅
95	94	a1i 11	. . . . . . 7 ⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)∅ = ∅)
96	93, 95	eqtrd 2770	. . . . . 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 6880	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘(𝐹‘𝑛)) = ((,)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩))
101		df-ov 7408	. . . . . . . . . . 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 45390	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → ((1st ‘(𝐹‘𝑛)) < (2nd ‘(𝐹‘𝑛)) ↔ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))))
110	108, 109	mpbird 257	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → (1st ‘(𝐹‘𝑛)) < (2nd ‘(𝐹‘𝑛)))
111	105, 107, 110	xrltled 13166	. . . . . . . . . . . . 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 13387	. . . . . . . . . . . 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 2772	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩) = ∅)
119	98, 100, 118	3eqtrd 2774	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐹)‘𝑛) = ∅)
120	119	iuneq2dv 4992	. . . . . . 7 ⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛) = ∪ 𝑛 ∈ (ℕ ∖ 𝐴)∅)
121	120, 95	eqtrd 2770	. . . . . 6 ⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛) = ∅)
122	96, 121	eqtr4d 2773	. . . . 5 ⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛) = ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛))
123	69, 122	uneq12d 4144	. . . 4 ⊢ (𝜑 → (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛)) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛)))
124	34, 38, 123	3eqtrrd 2775	. . 3 ⊢ (𝜑 → (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛)) = ∪ ran ((,) ∘ 𝐺))
125	9, 19, 124	3eqtrd 2774	. 2 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) = ∪ ran ((,) ∘ 𝐺))
126		volf 25482	. . . . . 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 6880	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((,)‘(𝐹‘𝑛)) = ((,)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩))
132	101	eqcomi 2744	. . . . . . . . . . 11 ⊢ ((,)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩) = ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛)))
133	132	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((,)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩) = ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))))
134	130, 131, 133	3eqtrd 2774	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))))
135		ioombl 25518	. . . . . . . . . 10 ⊢ ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) ∈ dom vol
136	135	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) ∈ dom vol)
137	134, 136	eqeltrd 2834	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) ∈ dom vol)
138	137	ralrimiva 3132	. . . . . . 7 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) ∈ dom vol)
139	6, 138	jca 511	. . . . . 6 ⊢ (𝜑 → (((,) ∘ 𝐹) Fn ℕ ∧ ∀𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) ∈ dom vol))
140		ffnfv 7109	. . . . . 6 ⊢ (((,) ∘ 𝐹):ℕ⟶dom vol ↔ (((,) ∘ 𝐹) Fn ℕ ∧ ∀𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) ∈ dom vol))
141	139, 140	sylibr 234	. . . . 5 ⊢ (𝜑 → ((,) ∘ 𝐹):ℕ⟶dom vol)
142		fco 6730	. . . . 5 ⊢ ((vol:dom vol⟶(0[,]+∞) ∧ ((,) ∘ 𝐹):ℕ⟶dom vol) → (vol ∘ ((,) ∘ 𝐹)):ℕ⟶(0[,]+∞))
143	127, 141, 142	syl2anc 584	. . . 4 ⊢ (𝜑 → (vol ∘ ((,) ∘ 𝐹)):ℕ⟶(0[,]+∞))
144	143	ffnd 6707	. . 3 ⊢ (𝜑 → (vol ∘ ((,) ∘ 𝐹)) Fn ℕ)
145	68	adantlr 715	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) = (((,) ∘ 𝐹)‘𝑛))
146	137	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) ∈ dom vol)
147	145, 146	eqeltrd 2834	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol)
148		simpll 766	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐴) → 𝜑)
149		eldif 3936	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (ℕ ∖ 𝐴) ↔ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐴))
150	149	bicomi 224	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐴) ↔ 𝑛 ∈ (ℕ ∖ 𝐴))
151	150	biimpi 216	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐴) → 𝑛 ∈ (ℕ ∖ 𝐴))
152	151	adantll 714	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐴) → 𝑛 ∈ (ℕ ∖ 𝐴))
153	117, 135	eqeltrrdi 2843	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ∅ ∈ dom vol)
154	92, 153	eqeltrd 2834	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol)
155	148, 152, 154	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol)
156	147, 155	pm2.61dan 812	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol)
157	156	ralrimiva 3132	. . . . . . 7 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) ∈ dom vol)
158	31, 157	jca 511	. . . . . 6 ⊢ (𝜑 → (((,) ∘ 𝐺) Fn ℕ ∧ ∀𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) ∈ dom vol))
159		ffnfv 7109	. . . . . 6 ⊢ (((,) ∘ 𝐺):ℕ⟶dom vol ↔ (((,) ∘ 𝐺) Fn ℕ ∧ ∀𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) ∈ dom vol))
160	158, 159	sylibr 234	. . . . 5 ⊢ (𝜑 → ((,) ∘ 𝐺):ℕ⟶dom vol)
161		fco 6730	. . . . 5 ⊢ ((vol:dom vol⟶(0[,]+∞) ∧ ((,) ∘ 𝐺):ℕ⟶dom vol) → (vol ∘ ((,) ∘ 𝐺)):ℕ⟶(0[,]+∞))
162	127, 160, 161	syl2anc 584	. . . 4 ⊢ (𝜑 → (vol ∘ ((,) ∘ 𝐺)):ℕ⟶(0[,]+∞))
163	162	ffnd 6707	. . 3 ⊢ (𝜑 → (vol ∘ ((,) ∘ 𝐺)) Fn ℕ)
164	145	eqcomd 2741	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛))
165	119, 92	eqtr4d 2773	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛))
166	148, 152, 165	syl2anc 584	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛))
167	164, 166	pm2.61dan 812	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛))
168	167	fveq2d 6880	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (vol‘(((,) ∘ 𝐹)‘𝑛)) = (vol‘(((,) ∘ 𝐺)‘𝑛)))
169		fnfun 6638	. . . . . . 7 ⊢ (((,) ∘ 𝐹) Fn ℕ → Fun ((,) ∘ 𝐹))
170	6, 169	syl 17	. . . . . 6 ⊢ (𝜑 → Fun ((,) ∘ 𝐹))
171	170	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Fun ((,) ∘ 𝐹))
172	5	fdmd 6716	. . . . . . . 8 ⊢ (𝜑 → dom ((,) ∘ 𝐹) = ℕ)
173	172	eqcomd 2741	. . . . . . 7 ⊢ (𝜑 → ℕ = dom ((,) ∘ 𝐹))
174	173	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ℕ = dom ((,) ∘ 𝐹))
175	129, 174	eleqtrd 2836	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ dom ((,) ∘ 𝐹))
176		fvco 6977	. . . . 5 ⊢ ((Fun ((,) ∘ 𝐹) ∧ 𝑛 ∈ dom ((,) ∘ 𝐹)) → ((vol ∘ ((,) ∘ 𝐹))‘𝑛) = (vol‘(((,) ∘ 𝐹)‘𝑛)))
177	171, 175, 176	syl2anc 584	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol ∘ ((,) ∘ 𝐹))‘𝑛) = (vol‘(((,) ∘ 𝐹)‘𝑛)))
178		fnfun 6638	. . . . . . 7 ⊢ (((,) ∘ 𝐺) Fn ℕ → Fun ((,) ∘ 𝐺))
179	31, 178	syl 17	. . . . . 6 ⊢ (𝜑 → Fun ((,) ∘ 𝐺))
180	179	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Fun ((,) ∘ 𝐺))
181	30	fdmd 6716	. . . . . . . 8 ⊢ (𝜑 → dom ((,) ∘ 𝐺) = ℕ)
182	181	eqcomd 2741	. . . . . . 7 ⊢ (𝜑 → ℕ = dom ((,) ∘ 𝐺))
183	182	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ℕ = dom ((,) ∘ 𝐺))
184	129, 183	eleqtrd 2836	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ dom ((,) ∘ 𝐺))
185		fvco 6977	. . . . 5 ⊢ ((Fun ((,) ∘ 𝐺) ∧ 𝑛 ∈ dom ((,) ∘ 𝐺)) → ((vol ∘ ((,) ∘ 𝐺))‘𝑛) = (vol‘(((,) ∘ 𝐺)‘𝑛)))
186	180, 184, 185	syl2anc 584	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol ∘ ((,) ∘ 𝐺))‘𝑛) = (vol‘(((,) ∘ 𝐺)‘𝑛)))
187	168, 177, 186	3eqtr4d 2780	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol ∘ ((,) ∘ 𝐹))‘𝑛) = ((vol ∘ ((,) ∘ 𝐺))‘𝑛))
188	144, 163, 187	eqfnfvd 7024	. 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 2108  ∀wral 3051  {crab 3415  Vcvv 3459   ∖ cdif 3923   ∪ cun 3924   ⊆ wss 3926  ∅c0 4308  ifcif 4500  𝒫 cpw 4575  ⟨cop 4607  ∪ cuni 4883  ∪ ciun 4967   class class class wbr 5119   ↦ cmpt 5201   × cxp 5652  dom cdm 5654  ran crn 5655   ∘ ccom 5658  Fun wfun 6525   Fn wfn 6526  ⟶wf 6527  ‘cfv 6531  (class class class)co 7405  1^st c1st 7986  2^nd c2nd 7987  ℝcr 11128  0cc0 11129  +∞cpnf 11266  ℝ^*cxr 11268   < clt 11269   ≤ cle 11270  ℕcn 12240  (,)cioo 13362  [,]cicc 13365  volcvol 25416

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 2707  ax-rep 5249  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729  ax-inf2 9655  ax-cnex 11185  ax-resscn 11186  ax-1cn 11187  ax-icn 11188  ax-addcl 11189  ax-addrcl 11190  ax-mulcl 11191  ax-mulrcl 11192  ax-mulcom 11193  ax-addass 11194  ax-mulass 11195  ax-distr 11196  ax-i2m1 11197  ax-1ne0 11198  ax-1rid 11199  ax-rnegex 11200  ax-rrecex 11201  ax-cnre 11202  ax-pre-lttri 11203  ax-pre-lttrn 11204  ax-pre-ltadd 11205  ax-pre-mulgt0 11206  ax-pre-sup 11207

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3359  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-int 4923  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-se 5607  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-isom 6540  df-riota 7362  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7671  df-om 7862  df-1st 7988  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-2o 8481  df-er 8719  df-map 8842  df-pm 8843  df-en 8960  df-dom 8961  df-sdom 8962  df-fin 8963  df-sup 9454  df-inf 9455  df-oi 9524  df-dju 9915  df-card 9953  df-pnf 11271  df-mnf 11272  df-xr 11273  df-ltxr 11274  df-le 11275  df-sub 11468  df-neg 11469  df-div 11895  df-nn 12241  df-2 12303  df-3 12304  df-n0 12502  df-z 12589  df-uz 12853  df-q 12965  df-rp 13009  df-xadd 13129  df-ioo 13366  df-ico 13368  df-icc 13369  df-fz 13525  df-fzo 13672  df-fl 13809  df-seq 14020  df-exp 14080  df-hash 14349  df-cj 15118  df-re 15119  df-im 15120  df-sqrt 15254  df-abs 15255  df-clim 15504  df-rlim 15505  df-sum 15703  df-xmet 21308  df-met 21309  df-ovol 25417  df-vol 25418

This theorem is referenced by:  ovolval4lem2  46679