ovolval4lem1

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

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

Proof

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

Metamath Proof Explorer

Theorem ovolval4lem1

Proof