ovolval4lem1

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

	Ref	Expression
Hypotheses	ovolval4lem1.f	$⊢ φ \to F : ℕ ⟶ ℝ^{} \times ℝ^{}$
	ovolval4lem1.g	$⊢ G = (n \in ℕ ⟼ ⟨1^{st} (F (n)), if (1^{st} (F (n)) \leq 2^{nd} (F (n)), 2^{nd} (F (n)), 1^{st} (F (n)))⟩)$
	ovolval4lem1.a	$⊢ A = \{n \in ℕ \| 1^{st} (F (n)) \leq 2^{nd} (F (n))\}$
Assertion	ovolval4lem1	$⊢ φ \to (⋃ ran ((.) \circ F) = ⋃ ran ((.) \circ G) \land vol \circ ((.) \circ F) = vol \circ ((.) \circ G))$

Proof

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

Metamath Proof Explorer

Theorem ovolval4lem1

Proof