Theorem ovolval4lem1 44532

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 13280	. . . . . . . 8 ⊢ (,):(ℝ* × ℝ*)⟶𝒫 ℝ
2	1	a1i 11	. . . . . . 7 ⊢ (𝜑 → (,):(ℝ* × ℝ*)⟶𝒫 ℝ)
3		ovolval4lem1.f	. . . . . . 7 ⊢ (𝜑 → 𝐹:ℕ⟶(ℝ* × ℝ*))
4		fco 6675	. . . . . . 7 ⊢ (((,):(ℝ* × ℝ*)⟶𝒫 ℝ ∧ 𝐹:ℕ⟶(ℝ* × ℝ*)) → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
5	2, 3, 4	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ((,) ∘ 𝐹):ℕ⟶𝒫 ℝ)
6	5	ffnd 6652	. . . . 5 ⊢ (𝜑 → ((,) ∘ 𝐹) Fn ℕ)
7		fniunfv 7176	. . . . 5 ⊢ (((,) ∘ 𝐹) Fn ℕ → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = ∪ ran ((,) ∘ 𝐹))
8	6, 7	syl 17	. . . 4 ⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = ∪ ran ((,) ∘ 𝐹))
9	8	eqcomd 2742	. . 3 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) = ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛))
10		ovolval4lem1.a	. . . . . . . . 9 ⊢ 𝐴 = {𝑛 ∈ ℕ ∣ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))}
11		ssrab2 4025	. . . . . . . . 9 ⊢ {𝑛 ∈ ℕ ∣ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))} ⊆ ℕ
12	10, 11	eqsstri 3966	. . . . . . . 8 ⊢ 𝐴 ⊆ ℕ
13		undif 4428	. . . . . . . 8 ⊢ (𝐴 ⊆ ℕ ↔ (𝐴 ∪ (ℕ ∖ 𝐴)) = ℕ)
14	12, 13	mpbi 229	. . . . . . 7 ⊢ (𝐴 ∪ (ℕ ∖ 𝐴)) = ℕ
15	14	eqcomi 2745	. . . . . 6 ⊢ ℕ = (𝐴 ∪ (ℕ ∖ 𝐴))
16	15	iuneq1i 42963	. . . . 5 ⊢ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = ∪ 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐹)‘𝑛)
17		iunxun 5041	. . . . 5 ⊢ ∪ 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐹)‘𝑛) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛))
18	16, 17	eqtri 2764	. . . 4 ⊢ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛))
19	18	a1i 11	. . 3 ⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛)))
20	3	ffvelcdmda 7017	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ (ℝ* × ℝ*))
21		xp1st 7931	. . . . . . . . . . 11 ⊢ ((𝐹‘𝑛) ∈ (ℝ* × ℝ*) → (1st ‘(𝐹‘𝑛)) ∈ ℝ*)
22	20, 21	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1st ‘(𝐹‘𝑛)) ∈ ℝ*)
23		xp2nd 7932	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑛) ∈ (ℝ* × ℝ*) → (2nd ‘(𝐹‘𝑛)) ∈ ℝ*)
24	20, 23	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2nd ‘(𝐹‘𝑛)) ∈ ℝ*)
25	24, 22	ifcld 4519	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))) ∈ ℝ*)
26	22, 25	opelxpd 5658	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩ ∈ (ℝ* × ℝ*))
27		ovolval4lem1.g	. . . . . . . . 9 ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩)
28	26, 27	fmptd 7044	. . . . . . . 8 ⊢ (𝜑 → 𝐺:ℕ⟶(ℝ* × ℝ*))
29		fco 6675	. . . . . . . 8 ⊢ (((,):(ℝ* × ℝ*)⟶𝒫 ℝ ∧ 𝐺:ℕ⟶(ℝ* × ℝ*)) → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
30	2, 28, 29	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → ((,) ∘ 𝐺):ℕ⟶𝒫 ℝ)
31	30	ffnd 6652	. . . . . 6 ⊢ (𝜑 → ((,) ∘ 𝐺) Fn ℕ)
32		fniunfv 7176	. . . . . 6 ⊢ (((,) ∘ 𝐺) Fn ℕ → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = ∪ ran ((,) ∘ 𝐺))
33	31, 32	syl 17	. . . . 5 ⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = ∪ ran ((,) ∘ 𝐺))
34	33	eqcomd 2742	. . . 4 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐺) = ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛))
35	15	iuneq1i 42963	. . . . . 6 ⊢ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = ∪ 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐺)‘𝑛)
36		iunxun 5041	. . . . . 6 ⊢ ∪ 𝑛 ∈ (𝐴 ∪ (ℕ ∖ 𝐴))(((,) ∘ 𝐺)‘𝑛) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛))
37	35, 36	eqtri 2764	. . . . 5 ⊢ ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛))
38	37	a1i 11	. . . 4 ⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛)))
39	28	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐺:ℕ⟶(ℝ* × ℝ*))
40	12	sseli 3928	. . . . . . . . 9 ⊢ (𝑛 ∈ 𝐴 → 𝑛 ∈ ℕ)
41	40	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝑛 ∈ ℕ)
42		fvco3 6923	. . . . . . . 8 ⊢ ((𝐺:ℕ⟶(ℝ* × ℝ*) ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐺)‘𝑛) = ((,)‘(𝐺‘𝑛)))
43	39, 41, 42	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) = ((,)‘(𝐺‘𝑛)))
44	3	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝐹:ℕ⟶(ℝ* × ℝ*))
45		fvco3 6923	. . . . . . . . 9 ⊢ ((𝐹:ℕ⟶(ℝ* × ℝ*) ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹‘𝑛)))
46	44, 41, 45	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹‘𝑛)))
47		simpl 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → 𝜑)
48		1st2nd2 7938	. . . . . . . . . . . 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 3461	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩ ∈ V)
53	51, 52	fvmpt2d 6944	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐺‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩)
54	47, 41, 53	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐺‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩)
55	10	eleq2i 2828	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ 𝐴 ↔ 𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))})
56	55	biimpi 215	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ 𝐴 → 𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))})
57		rabid 3423	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))} ↔ (𝑛 ∈ ℕ ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))))
58	56, 57	sylib 217	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ 𝐴 → (𝑛 ∈ ℕ ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))))
59	58	simprd 496	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ 𝐴 → (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)))
60	59	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)))
61	60	iftrued 4481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))) = (2nd ‘(𝐹‘𝑛)))
62	61	opeq2d 4824	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩ = ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
63		eqidd 2737	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩ = ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
64	54, 62, 63	3eqtrd 2780	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐺‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
65	50, 64	eqtr4d 2779	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (𝐹‘𝑛) = (𝐺‘𝑛))
66	65	fveq2d 6829	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → ((,)‘(𝐹‘𝑛)) = ((,)‘(𝐺‘𝑛)))
67	46, 66	eqtrd 2776	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐺‘𝑛)))
68	43, 67	eqtr4d 2779	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) = (((,) ∘ 𝐹)‘𝑛))
69	68	iuneq2dv 4965	. . . . 5 ⊢ (𝜑 → ∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) = ∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛))
70	28	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → 𝐺:ℕ⟶(ℝ* × ℝ*))
71		eldifi 4073	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (ℕ ∖ 𝐴) → 𝑛 ∈ ℕ)
72	71	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → 𝑛 ∈ ℕ)
73	70, 72, 42	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐺)‘𝑛) = ((,)‘(𝐺‘𝑛)))
74		simpl 483	. . . . . . . . . . . 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 233	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ (ℕ ∖ 𝐴) ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) → 𝑛 ∈ {𝑛 ∈ ℕ ∣ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))})
78	77, 55	sylibr 233	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ (ℕ ∖ 𝐴) ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) → 𝑛 ∈ 𝐴)
79	78	adantll 711	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) → 𝑛 ∈ 𝐴)
80		eldifn 4074	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (ℕ ∖ 𝐴) → ¬ 𝑛 ∈ 𝐴)
81	80	ad2antlr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛))) → ¬ 𝑛 ∈ 𝐴)
82	79, 81	pm2.65da 814	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ¬ (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)))
83	82	iffalsed 4484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))) = (1st ‘(𝐹‘𝑛)))
84	83	opeq2d 4824	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ⟨(1st ‘(𝐹‘𝑛)), if((1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛)))⟩ = ⟨(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))⟩)
85	75, 84	eqtrd 2776	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (𝐺‘𝑛) = ⟨(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))⟩)
86	85	fveq2d 6829	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘(𝐺‘𝑛)) = ((,)‘⟨(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))⟩))
87		iooid 13208	. . . . . . . . . . . 12 ⊢ ((1st ‘(𝐹‘𝑛))(,)(1st ‘(𝐹‘𝑛))) = ∅
88	87	eqcomi 2745	. . . . . . . . . . 11 ⊢ ∅ = ((1st ‘(𝐹‘𝑛))(,)(1st ‘(𝐹‘𝑛)))
89		df-ov 7340	. . . . . . . . . . 11 ⊢ ((1st ‘(𝐹‘𝑛))(,)(1st ‘(𝐹‘𝑛))) = ((,)‘⟨(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))⟩)
90	88, 89	eqtr2i 2765	. . . . . . . . . 10 ⊢ ((,)‘⟨(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))⟩) = ∅
91	90	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘⟨(1st ‘(𝐹‘𝑛)), (1st ‘(𝐹‘𝑛))⟩) = ∅)
92	73, 86, 91	3eqtrd 2780	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐺)‘𝑛) = ∅)
93	92	iuneq2dv 4965	. . . . . . 7 ⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛) = ∪ 𝑛 ∈ (ℕ ∖ 𝐴)∅)
94		iun0 5009	. . . . . . . 8 ⊢ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)∅ = ∅
95	94	a1i 11	. . . . . . 7 ⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)∅ = ∅)
96	93, 95	eqtrd 2776	. . . . . 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 6829	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘(𝐹‘𝑛)) = ((,)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩))
101		df-ov 7340	. . . . . . . . . . 11 ⊢ ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ((,)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩)
102	101	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ((,)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩))
103		simplr 766	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → 𝑛 ∈ (ℕ ∖ 𝐴))
104	72, 22	syldan 591	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (1st ‘(𝐹‘𝑛)) ∈ ℝ*)
105	104	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → (1st ‘(𝐹‘𝑛)) ∈ ℝ*)
106	72, 24	syldan 591	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (2nd ‘(𝐹‘𝑛)) ∈ ℝ*)
107	106	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → (2nd ‘(𝐹‘𝑛)) ∈ ℝ*)
108		simpr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛)))
109	105, 107	xrltnled 43245	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → ((1st ‘(𝐹‘𝑛)) < (2nd ‘(𝐹‘𝑛)) ↔ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))))
110	108, 109	mpbird 256	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → (1st ‘(𝐹‘𝑛)) < (2nd ‘(𝐹‘𝑛)))
111	105, 107, 110	xrltled 12985	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → (1st ‘(𝐹‘𝑛)) ≤ (2nd ‘(𝐹‘𝑛)))
112	103, 111, 78	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → 𝑛 ∈ 𝐴)
113	80	ad2antlr 724	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) ∧ ¬ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))) → ¬ 𝑛 ∈ 𝐴)
114	112, 113	condan 815	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛)))
115		ioo0 13205	. . . . . . . . . . . 12 ⊢ (((1st ‘(𝐹‘𝑛)) ∈ ℝ* ∧ (2nd ‘(𝐹‘𝑛)) ∈ ℝ*) → (((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ∅ ↔ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))))
116	104, 106, 115	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ∅ ↔ (2nd ‘(𝐹‘𝑛)) ≤ (1st ‘(𝐹‘𝑛))))
117	114, 116	mpbird 256	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) = ∅)
118	102, 117	eqtr3d 2778	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ((,)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩) = ∅)
119	98, 100, 118	3eqtrd 2780	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐹)‘𝑛) = ∅)
120	119	iuneq2dv 4965	. . . . . . 7 ⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛) = ∪ 𝑛 ∈ (ℕ ∖ 𝐴)∅)
121	120, 95	eqtrd 2776	. . . . . 6 ⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛) = ∅)
122	96, 121	eqtr4d 2779	. . . . 5 ⊢ (𝜑 → ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛) = ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛))
123	69, 122	uneq12d 4111	. . . 4 ⊢ (𝜑 → (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐺)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐺)‘𝑛)) = (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛)))
124	34, 38, 123	3eqtrrd 2781	. . 3 ⊢ (𝜑 → (∪ 𝑛 ∈ 𝐴 (((,) ∘ 𝐹)‘𝑛) ∪ ∪ 𝑛 ∈ (ℕ ∖ 𝐴)(((,) ∘ 𝐹)‘𝑛)) = ∪ ran ((,) ∘ 𝐺))
125	9, 19, 124	3eqtrd 2780	. 2 ⊢ (𝜑 → ∪ ran ((,) ∘ 𝐹) = ∪ ran ((,) ∘ 𝐺))
126		volf 24799	. . . . . 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 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = ((,)‘(𝐹‘𝑛)))
131	49	fveq2d 6829	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((,)‘(𝐹‘𝑛)) = ((,)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩))
132	101	eqcomi 2745	. . . . . . . . . . 11 ⊢ ((,)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩) = ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛)))
133	132	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((,)‘⟨(1st ‘(𝐹‘𝑛)), (2nd ‘(𝐹‘𝑛))⟩) = ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))))
134	130, 131, 133	3eqtrd 2780	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))))
135		ioombl 24835	. . . . . . . . . 10 ⊢ ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) ∈ dom vol
136	135	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((1st ‘(𝐹‘𝑛))(,)(2nd ‘(𝐹‘𝑛))) ∈ dom vol)
137	134, 136	eqeltrd 2837	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) ∈ dom vol)
138	137	ralrimiva 3139	. . . . . . 7 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) ∈ dom vol)
139	6, 138	jca 512	. . . . . 6 ⊢ (𝜑 → (((,) ∘ 𝐹) Fn ℕ ∧ ∀𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) ∈ dom vol))
140		ffnfv 7048	. . . . . 6 ⊢ (((,) ∘ 𝐹):ℕ⟶dom vol ↔ (((,) ∘ 𝐹) Fn ℕ ∧ ∀𝑛 ∈ ℕ (((,) ∘ 𝐹)‘𝑛) ∈ dom vol))
141	139, 140	sylibr 233	. . . . 5 ⊢ (𝜑 → ((,) ∘ 𝐹):ℕ⟶dom vol)
142		fco 6675	. . . . 5 ⊢ ((vol:dom vol⟶(0[,]+∞) ∧ ((,) ∘ 𝐹):ℕ⟶dom vol) → (vol ∘ ((,) ∘ 𝐹)):ℕ⟶(0[,]+∞))
143	127, 141, 142	syl2anc 584	. . . 4 ⊢ (𝜑 → (vol ∘ ((,) ∘ 𝐹)):ℕ⟶(0[,]+∞))
144	143	ffnd 6652	. . 3 ⊢ (𝜑 → (vol ∘ ((,) ∘ 𝐹)) Fn ℕ)
145	68	adantlr 712	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) = (((,) ∘ 𝐹)‘𝑛))
146	137	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) ∈ dom vol)
147	145, 146	eqeltrd 2837	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol)
148		simpll 764	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐴) → 𝜑)
149		eldif 3908	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (ℕ ∖ 𝐴) ↔ (𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐴))
150	149	bicomi 223	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐴) ↔ 𝑛 ∈ (ℕ ∖ 𝐴))
151	150	biimpi 215	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ ℕ ∧ ¬ 𝑛 ∈ 𝐴) → 𝑛 ∈ (ℕ ∖ 𝐴))
152	151	adantll 711	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐴) → 𝑛 ∈ (ℕ ∖ 𝐴))
153	117, 135	eqeltrrdi 2846	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → ∅ ∈ dom vol)
154	92, 153	eqeltrd 2837	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol)
155	148, 152, 154	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol)
156	147, 155	pm2.61dan 810	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐺)‘𝑛) ∈ dom vol)
157	156	ralrimiva 3139	. . . . . . 7 ⊢ (𝜑 → ∀𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) ∈ dom vol)
158	31, 157	jca 512	. . . . . 6 ⊢ (𝜑 → (((,) ∘ 𝐺) Fn ℕ ∧ ∀𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) ∈ dom vol))
159		ffnfv 7048	. . . . . 6 ⊢ (((,) ∘ 𝐺):ℕ⟶dom vol ↔ (((,) ∘ 𝐺) Fn ℕ ∧ ∀𝑛 ∈ ℕ (((,) ∘ 𝐺)‘𝑛) ∈ dom vol))
160	158, 159	sylibr 233	. . . . 5 ⊢ (𝜑 → ((,) ∘ 𝐺):ℕ⟶dom vol)
161		fco 6675	. . . . 5 ⊢ ((vol:dom vol⟶(0[,]+∞) ∧ ((,) ∘ 𝐺):ℕ⟶dom vol) → (vol ∘ ((,) ∘ 𝐺)):ℕ⟶(0[,]+∞))
162	127, 160, 161	syl2anc 584	. . . 4 ⊢ (𝜑 → (vol ∘ ((,) ∘ 𝐺)):ℕ⟶(0[,]+∞))
163	162	ffnd 6652	. . 3 ⊢ (𝜑 → (vol ∘ ((,) ∘ 𝐺)) Fn ℕ)
164	145	eqcomd 2742	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛))
165	119, 92	eqtr4d 2779	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℕ ∖ 𝐴)) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛))
166	148, 152, 165	syl2anc 584	. . . . . 6 ⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ ¬ 𝑛 ∈ 𝐴) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛))
167	164, 166	pm2.61dan 810	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((,) ∘ 𝐹)‘𝑛) = (((,) ∘ 𝐺)‘𝑛))
168	167	fveq2d 6829	. . . 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 6662	. . . . . . . 8 ⊢ (𝜑 → dom ((,) ∘ 𝐹) = ℕ)
173	172	eqcomd 2742	. . . . . . 7 ⊢ (𝜑 → ℕ = dom ((,) ∘ 𝐹))
174	173	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ℕ = dom ((,) ∘ 𝐹))
175	129, 174	eleqtrd 2839	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ dom ((,) ∘ 𝐹))
176		fvco 6922	. . . . 5 ⊢ ((Fun ((,) ∘ 𝐹) ∧ 𝑛 ∈ dom ((,) ∘ 𝐹)) → ((vol ∘ ((,) ∘ 𝐹))‘𝑛) = (vol‘(((,) ∘ 𝐹)‘𝑛)))
177	171, 175, 176	syl2anc 584	. . . 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 6662	. . . . . . . 8 ⊢ (𝜑 → dom ((,) ∘ 𝐺) = ℕ)
182	181	eqcomd 2742	. . . . . . 7 ⊢ (𝜑 → ℕ = dom ((,) ∘ 𝐺))
183	182	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ℕ = dom ((,) ∘ 𝐺))
184	129, 183	eleqtrd 2839	. . . . 5 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ dom ((,) ∘ 𝐺))
185		fvco 6922	. . . . 5 ⊢ ((Fun ((,) ∘ 𝐺) ∧ 𝑛 ∈ dom ((,) ∘ 𝐺)) → ((vol ∘ ((,) ∘ 𝐺))‘𝑛) = (vol‘(((,) ∘ 𝐺)‘𝑛)))
186	180, 184, 185	syl2anc 584	. . . 4 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol ∘ ((,) ∘ 𝐺))‘𝑛) = (vol‘(((,) ∘ 𝐺)‘𝑛)))
187	168, 177, 186	3eqtr4d 2786	. . 3 ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((vol ∘ ((,) ∘ 𝐹))‘𝑛) = ((vol ∘ ((,) ∘ 𝐺))‘𝑛))
188	144, 163, 187	eqfnfvd 6968	. 2 ⊢ (𝜑 → (vol ∘ ((,) ∘ 𝐹)) = (vol ∘ ((,) ∘ 𝐺)))
189	125, 188	jca 512	1 ⊢ (𝜑 → (∪ ran ((,) ∘ 𝐹) = ∪ ran ((,) ∘ 𝐺) ∧ (vol ∘ ((,) ∘ 𝐹)) = (vol ∘ ((,) ∘ 𝐺))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1540   ∈ wcel 2105  ∀wral 3061  {crab 3403  Vcvv 3441   ∖ cdif 3895   ∪ cun 3896   ⊆ wss 3898  ∅c0 4269  ifcif 4473  𝒫 cpw 4547  ⟨cop 4579  ∪ cuni 4852  ∪ ciun 4941   class class class wbr 5092   ↦ cmpt 5175   × cxp 5618  dom cdm 5620  ran crn 5621   ∘ ccom 5624  Fun wfun 6473   Fn wfn 6474  ⟶wf 6475  ‘cfv 6479  (class class class)co 7337  1^st c1st 7897  2^nd c2nd 7898  ℝcr 10971  0cc0 10972  +∞cpnf 11107  ℝ^*cxr 11109   < clt 11110   ≤ cle 11111  ℕcn 12074  (,)cioo 13180  [,]cicc 13183  volcvol 24733

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5229  ax-sep 5243  ax-nul 5250  ax-pow 5308  ax-pr 5372  ax-un 7650  ax-inf2 9498  ax-cnex 11028  ax-resscn 11029  ax-1cn 11030  ax-icn 11031  ax-addcl 11032  ax-addrcl 11033  ax-mulcl 11034  ax-mulrcl 11035  ax-mulcom 11036  ax-addass 11037  ax-mulass 11038  ax-distr 11039  ax-i2m1 11040  ax-1ne0 11041  ax-1rid 11042  ax-rnegex 11043  ax-rrecex 11044  ax-cnre 11045  ax-pre-lttri 11046  ax-pre-lttrn 11047  ax-pre-ltadd 11048  ax-pre-mulgt0 11049  ax-pre-sup 11050

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4270  df-if 4474  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4853  df-int 4895  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5176  df-tr 5210  df-id 5518  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5575  df-se 5576  df-we 5577  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-pred 6238  df-ord 6305  df-on 6306  df-lim 6307  df-suc 6308  df-iota 6431  df-fun 6481  df-fn 6482  df-f 6483  df-f1 6484  df-fo 6485  df-f1o 6486  df-fv 6487  df-isom 6488  df-riota 7293  df-ov 7340  df-oprab 7341  df-mpo 7342  df-of 7595  df-om 7781  df-1st 7899  df-2nd 7900  df-frecs 8167  df-wrecs 8198  df-recs 8272  df-rdg 8311  df-1o 8367  df-2o 8368  df-er 8569  df-map 8688  df-pm 8689  df-en 8805  df-dom 8806  df-sdom 8807  df-fin 8808  df-sup 9299  df-inf 9300  df-oi 9367  df-dju 9758  df-card 9796  df-pnf 11112  df-mnf 11113  df-xr 11114  df-ltxr 11115  df-le 11116  df-sub 11308  df-neg 11309  df-div 11734  df-nn 12075  df-2 12137  df-3 12138  df-n0 12335  df-z 12421  df-uz 12684  df-q 12790  df-rp 12832  df-xadd 12950  df-ioo 13184  df-ico 13186  df-icc 13187  df-fz 13341  df-fzo 13484  df-fl 13613  df-seq 13823  df-exp 13884  df-hash 14146  df-cj 14909  df-re 14910  df-im 14911  df-sqrt 15045  df-abs 15046  df-clim 15296  df-rlim 15297  df-sum 15497  df-xmet 20696  df-met 20697  df-ovol 24734  df-vol 24735

This theorem is referenced by:  ovolval4lem2  44533