uniioombllem3a

	Ref	Expression
Hypotheses	uniioombl.1	$⊢ φ \to F : ℕ ⟶ \leq \cap ℝ^{2}$
	uniioombl.2	$⊢ φ \to \underset{x \in ℕ}{Disj} (.) (F (x))$
	uniioombl.3	$⊢ S = seq 1 (+ ((abs \circ -) \circ F))$
	uniioombl.a	$⊢ A = ⋃ ran ((.) \circ F)$
	uniioombl.e	$⊢ φ \to {vol}^{*} (E) \in ℝ$
	uniioombl.c	$⊢ φ \to C \in ℝ^{+}$
	uniioombl.g	$⊢ φ \to G : ℕ ⟶ \leq \cap ℝ^{2}$
	uniioombl.s	$⊢ φ \to E \subseteq ⋃ ran ((.) \circ G)$
	uniioombl.t	$⊢ T = seq 1 (+ ((abs \circ -) \circ G))$
	uniioombl.v	$⊢ φ \to sup (ran T ℝ^{} <) \leq {vol}^{} (E) + C$
	uniioombl.m	$⊢ φ \to M \in ℕ$
	uniioombl.m2	$⊢ φ \to \|T (M) - sup (ran T ℝ^{*} <)\| < C$
	uniioombl.k	$⊢ K = ⋃ ((.) \circ G) [(1 \dots M)]$
Assertion	uniioombllem3a	$⊢ φ \to (K = ⋃_{j = 1}^{M} (.) (G (j)) \land {vol}^{*} (K) \in ℝ)$

Proof

Step	Hyp	Ref	Expression
1		uniioombl.1	$⊢ φ \to F : ℕ ⟶ \leq \cap ℝ^{2}$
2		uniioombl.2	$⊢ φ \to \underset{x \in ℕ}{Disj} (.) (F (x))$
3		uniioombl.3	$⊢ S = seq 1 (+ ((abs \circ -) \circ F))$
4		uniioombl.a	$⊢ A = ⋃ ran ((.) \circ F)$
5		uniioombl.e	$⊢ φ \to {vol}^{*} (E) \in ℝ$
6		uniioombl.c	$⊢ φ \to C \in ℝ^{+}$
7		uniioombl.g	$⊢ φ \to G : ℕ ⟶ \leq \cap ℝ^{2}$
8		uniioombl.s	$⊢ φ \to E \subseteq ⋃ ran ((.) \circ G)$
9		uniioombl.t	$⊢ T = seq 1 (+ ((abs \circ -) \circ G))$
10		uniioombl.v	$⊢ φ \to sup (ran T ℝ^{} <) \leq {vol}^{} (E) + C$
11		uniioombl.m	$⊢ φ \to M \in ℕ$
12		uniioombl.m2	$⊢ φ \to \|T (M) - sup (ran T ℝ^{*} <)\| < C$
13		uniioombl.k	$⊢ K = ⋃ ((.) \circ G) [(1 \dots M)]$
14		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
15		inss2	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{2}$
16		rexpssxrxp	$⊢ ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
17	15 16	sstri	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
18		fss	$⊢ (G : ℕ ⟶ \leq \cap ℝ^{2} \land \leq \cap ℝ^{2} \subseteq ℝ^{} \times ℝ^{}) \to G : ℕ ⟶ ℝ^{} \times ℝ^{}$
19	7 17 18	sylancl	$⊢ φ \to G : ℕ ⟶ ℝ^{} \times ℝ^{}$
20		fco	$⊢ ((.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \land G : ℕ ⟶ ℝ^{} \times ℝ^{}) \to ((.) \circ G) : ℕ ⟶ 𝒫 ℝ$
21	14 19 20	sylancr	$⊢ φ \to ((.) \circ G) : ℕ ⟶ 𝒫 ℝ$
22		ffun	$⊢ ((.) \circ G) : ℕ ⟶ 𝒫 ℝ \to Fun ((.) \circ G)$
23		funiunfv	$⊢ Fun ((.) \circ G) \to ⋃_{j = 1}^{M} ((.) \circ G) (j) = ⋃ ((.) \circ G) [(1 \dots M)]$
24	21 22 23	3syl	$⊢ φ \to ⋃_{j = 1}^{M} ((.) \circ G) (j) = ⋃ ((.) \circ G) [(1 \dots M)]$
25		elfznn	$⊢ j \in (1 \dots M) \to j \in ℕ$
26		fvco3	$⊢ (G : ℕ ⟶ \leq \cap ℝ^{2} \land j \in ℕ) \to ((.) \circ G) (j) = (.) (G (j))$
27	7 25 26	syl2an	$⊢ (φ \land j \in (1 \dots M)) \to ((.) \circ G) (j) = (.) (G (j))$
28	27	iuneq2dv	$⊢ φ \to ⋃_{j = 1}^{M} ((.) \circ G) (j) = ⋃_{j = 1}^{M} (.) (G (j))$
29	24 28	eqtr3d	$⊢ φ \to ⋃ ((.) \circ G) [(1 \dots M)] = ⋃_{j = 1}^{M} (.) (G (j))$
30	13 29	syl5eq	$⊢ φ \to K = ⋃_{j = 1}^{M} (.) (G (j))$
31		ffvelrn	$⊢ (G : ℕ ⟶ \leq \cap ℝ^{2} \land j \in ℕ) \to G (j) \in (\leq \cap ℝ^{2})$
32	7 25 31	syl2an	$⊢ (φ \land j \in (1 \dots M)) \to G (j) \in (\leq \cap ℝ^{2})$
33	32	elin2d	$⊢ (φ \land j \in (1 \dots M)) \to G (j) \in ℝ^{2}$
34		1st2nd2	$⊢ G (j) \in ℝ^{2} \to G (j) = ⟨1^{st} (G (j)), 2^{nd} (G (j))⟩$
35	33 34	syl	$⊢ (φ \land j \in (1 \dots M)) \to G (j) = ⟨1^{st} (G (j)), 2^{nd} (G (j))⟩$
36	35	fveq2d	$⊢ (φ \land j \in (1 \dots M)) \to (.) (G (j)) = (.) (⟨1^{st} (G (j)), 2^{nd} (G (j))⟩)$
37		df-ov	$⊢ (1^{st} (G (j)), 2^{nd} (G (j))) = (.) (⟨1^{st} (G (j)), 2^{nd} (G (j))⟩)$
38	36 37	eqtr4di	$⊢ (φ \land j \in (1 \dots M)) \to (.) (G (j)) = (1^{st} (G (j)), 2^{nd} (G (j)))$
39		ioossre	$⊢ (1^{st} (G (j)), 2^{nd} (G (j))) \subseteq ℝ$
40	38 39	eqsstrdi	$⊢ (φ \land j \in (1 \dots M)) \to (.) (G (j)) \subseteq ℝ$
41	40	ralrimiva	$⊢ φ \to \forall j \in (1 \dots M) (.) (G (j)) \subseteq ℝ$
42		iunss	$⊢ ⋃_{j = 1}^{M} (.) (G (j)) \subseteq ℝ \leftrightarrow \forall j \in (1 \dots M) (.) (G (j)) \subseteq ℝ$
43	41 42	sylibr	$⊢ φ \to ⋃_{j = 1}^{M} (.) (G (j)) \subseteq ℝ$
44	30 43	eqsstrd	$⊢ φ \to K \subseteq ℝ$
45		fzfid	$⊢ φ \to (1 \dots M) \in Fin$
46	38	fveq2d	$⊢ (φ \land j \in (1 \dots M)) \to {vol}^{} ((.) (G (j))) = {vol}^{} ((1^{st} (G (j)), 2^{nd} (G (j))))$
47		ovolfcl	$⊢ (G : ℕ ⟶ \leq \cap ℝ^{2} \land j \in ℕ) \to (1^{st} (G (j)) \in ℝ \land 2^{nd} (G (j)) \in ℝ \land 1^{st} (G (j)) \leq 2^{nd} (G (j)))$
48	7 25 47	syl2an	$⊢ (φ \land j \in (1 \dots M)) \to (1^{st} (G (j)) \in ℝ \land 2^{nd} (G (j)) \in ℝ \land 1^{st} (G (j)) \leq 2^{nd} (G (j)))$
49		ovolioo	$⊢ (1^{st} (G (j)) \in ℝ \land 2^{nd} (G (j)) \in ℝ \land 1^{st} (G (j)) \leq 2^{nd} (G (j))) \to {vol}^{*} ((1^{st} (G (j)), 2^{nd} (G (j)))) = 2^{nd} (G (j)) - 1^{st} (G (j))$
50	48 49	syl	$⊢ (φ \land j \in (1 \dots M)) \to {vol}^{*} ((1^{st} (G (j)), 2^{nd} (G (j)))) = 2^{nd} (G (j)) - 1^{st} (G (j))$
51	46 50	eqtrd	$⊢ (φ \land j \in (1 \dots M)) \to {vol}^{*} ((.) (G (j))) = 2^{nd} (G (j)) - 1^{st} (G (j))$
52	48	simp2d	$⊢ (φ \land j \in (1 \dots M)) \to 2^{nd} (G (j)) \in ℝ$
53	48	simp1d	$⊢ (φ \land j \in (1 \dots M)) \to 1^{st} (G (j)) \in ℝ$
54	52 53	resubcld	$⊢ (φ \land j \in (1 \dots M)) \to 2^{nd} (G (j)) - 1^{st} (G (j)) \in ℝ$
55	51 54	eqeltrd	$⊢ (φ \land j \in (1 \dots M)) \to {vol}^{*} ((.) (G (j))) \in ℝ$
56	45 55	fsumrecl	$⊢ φ \to \sum_{j = 1}^{M} {vol}^{*} ((.) (G (j))) \in ℝ$
57	30	fveq2d	$⊢ φ \to {vol}^{} (K) = {vol}^{} (⋃_{j = 1}^{M} (.) (G (j)))$
58	40 55	jca	$⊢ (φ \land j \in (1 \dots M)) \to ((.) (G (j)) \subseteq ℝ \land {vol}^{*} ((.) (G (j))) \in ℝ)$
59	58	ralrimiva	$⊢ φ \to \forall j \in (1 \dots M) ((.) (G (j)) \subseteq ℝ \land {vol}^{*} ((.) (G (j))) \in ℝ)$
60		ovolfiniun	$⊢ ((1 \dots M) \in Fin \land \forall j \in (1 \dots M) ((.) (G (j)) \subseteq ℝ \land {vol}^{} ((.) (G (j))) \in ℝ)) \to {vol}^{} (⋃_{j = 1}^{M} (.) (G (j))) \leq \sum_{j = 1}^{M} {vol}^{*} ((.) (G (j)))$
61	45 59 60	syl2anc	$⊢ φ \to {vol}^{} (⋃_{j = 1}^{M} (.) (G (j))) \leq \sum_{j = 1}^{M} {vol}^{} ((.) (G (j)))$
62	57 61	eqbrtrd	$⊢ φ \to {vol}^{} (K) \leq \sum_{j = 1}^{M} {vol}^{} ((.) (G (j)))$
63		ovollecl	$⊢ (K \subseteq ℝ \land \sum_{j = 1}^{M} {vol}^{} ((.) (G (j))) \in ℝ \land {vol}^{} (K) \leq \sum_{j = 1}^{M} {vol}^{} ((.) (G (j)))) \to {vol}^{} (K) \in ℝ$
64	44 56 62 63	syl3anc	$⊢ φ \to {vol}^{*} (K) \in ℝ$
65	30 64	jca	$⊢ φ \to (K = ⋃_{j = 1}^{M} (.) (G (j)) \land {vol}^{*} (K) \in ℝ)$

Metamath Proof Explorer

Theorem uniioombllem3a

Proof