Theorem ovolval4lem1

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

	Ref	Expression
Hypotheses	ovolval4lem1.f	$$⊢\phi \to F:\mathbb{N}⟶{ℝ}^{*}\times {ℝ}^{*}$$
	ovolval4lem1.g	$$⊢G=\left(n\in \mathbb{N}⟼⟨1^{st}\left(F\left(n\right)\right),if\left(1^{st}\left(F\left(n\right)\right)\le 2^{nd}\left(F\left(n\right)\right),2^{nd}\left(F\left(n\right)\right),1^{st}\left(F\left(n\right)\right)\right)⟩\right)$$
	ovolval4lem1.a	$$⊢A=\left\{n\in \mathbb{N}|1^{st}\left(F\left(n\right)\right)\le 2^{nd}\left(F\left(n\right)\right)\right\}$$
Assertion	ovolval4lem1	$$⊢\phi \to \left(\bigcup \mathrm{ran}\left(\left(.\right)\circ F\right)=\bigcup \mathrm{ran}\left(\left(.\right)\circ G\right)\wedge vol\circ \left(\left(.\right)\circ F\right)=vol\circ \left(\left(.\right)\circ G\right)\right)$$

Proof

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