uniioombllem2a

	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$
Assertion	uniioombllem2a	$⊢ ((φ \land J \in ℕ) \land z \in ℕ) \to (.) (F (z)) \cap (.) (G (J)) \in ran (.)$

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	1	adantr	$⊢ (φ \land J \in ℕ) \to F : ℕ ⟶ \leq \cap ℝ^{2}$
12	11	ffvelcdmda	$⊢ ((φ \land J \in ℕ) \land z \in ℕ) \to F (z) \in (\leq \cap ℝ^{2})$
13	12	elin2d	$⊢ ((φ \land J \in ℕ) \land z \in ℕ) \to F (z) \in ℝ^{2}$
14		1st2nd2	$⊢ F (z) \in ℝ^{2} \to F (z) = ⟨1^{st} (F (z)), 2^{nd} (F (z))⟩$
15	13 14	syl	$⊢ ((φ \land J \in ℕ) \land z \in ℕ) \to F (z) = ⟨1^{st} (F (z)), 2^{nd} (F (z))⟩$
16	15	fveq2d	$⊢ ((φ \land J \in ℕ) \land z \in ℕ) \to (.) (F (z)) = (.) (⟨1^{st} (F (z)), 2^{nd} (F (z))⟩)$
17		df-ov	$⊢ (1^{st} (F (z)), 2^{nd} (F (z))) = (.) (⟨1^{st} (F (z)), 2^{nd} (F (z))⟩)$
18	16 17	eqtr4di	$⊢ ((φ \land J \in ℕ) \land z \in ℕ) \to (.) (F (z)) = (1^{st} (F (z)), 2^{nd} (F (z)))$
19	7	ffvelcdmda	$⊢ (φ \land J \in ℕ) \to G (J) \in (\leq \cap ℝ^{2})$
20	19	elin2d	$⊢ (φ \land J \in ℕ) \to G (J) \in ℝ^{2}$
21		1st2nd2	$⊢ G (J) \in ℝ^{2} \to G (J) = ⟨1^{st} (G (J)), 2^{nd} (G (J))⟩$
22	20 21	syl	$⊢ (φ \land J \in ℕ) \to G (J) = ⟨1^{st} (G (J)), 2^{nd} (G (J))⟩$
23	22	fveq2d	$⊢ (φ \land J \in ℕ) \to (.) (G (J)) = (.) (⟨1^{st} (G (J)), 2^{nd} (G (J))⟩)$
24		df-ov	$⊢ (1^{st} (G (J)), 2^{nd} (G (J))) = (.) (⟨1^{st} (G (J)), 2^{nd} (G (J))⟩)$
25	23 24	eqtr4di	$⊢ (φ \land J \in ℕ) \to (.) (G (J)) = (1^{st} (G (J)), 2^{nd} (G (J)))$
26	25	adantr	$⊢ ((φ \land J \in ℕ) \land z \in ℕ) \to (.) (G (J)) = (1^{st} (G (J)), 2^{nd} (G (J)))$
27	18 26	ineq12d	$⊢ ((φ \land J \in ℕ) \land z \in ℕ) \to (.) (F (z)) \cap (.) (G (J)) = (1^{st} (F (z)), 2^{nd} (F (z))) \cap (1^{st} (G (J)), 2^{nd} (G (J)))$
28		ovolfcl	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land z \in ℕ) \to (1^{st} (F (z)) \in ℝ \land 2^{nd} (F (z)) \in ℝ \land 1^{st} (F (z)) \leq 2^{nd} (F (z)))$
29	11 28	sylan	$⊢ ((φ \land J \in ℕ) \land z \in ℕ) \to (1^{st} (F (z)) \in ℝ \land 2^{nd} (F (z)) \in ℝ \land 1^{st} (F (z)) \leq 2^{nd} (F (z)))$
30	29	simp1d	$⊢ ((φ \land J \in ℕ) \land z \in ℕ) \to 1^{st} (F (z)) \in ℝ$
31	30	rexrd	$⊢ ((φ \land J \in ℕ) \land z \in ℕ) \to 1^{st} (F (z)) \in ℝ^{*}$
32	29	simp2d	$⊢ ((φ \land J \in ℕ) \land z \in ℕ) \to 2^{nd} (F (z)) \in ℝ$
33	32	rexrd	$⊢ ((φ \land J \in ℕ) \land z \in ℕ) \to 2^{nd} (F (z)) \in ℝ^{*}$
34		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)))$
35	7 34	sylan	$⊢ (φ \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)))$
36	35	simp1d	$⊢ (φ \land J \in ℕ) \to 1^{st} (G (J)) \in ℝ$
37	36	rexrd	$⊢ (φ \land J \in ℕ) \to 1^{st} (G (J)) \in ℝ^{*}$
38	37	adantr	$⊢ ((φ \land J \in ℕ) \land z \in ℕ) \to 1^{st} (G (J)) \in ℝ^{*}$
39	35	simp2d	$⊢ (φ \land J \in ℕ) \to 2^{nd} (G (J)) \in ℝ$
40	39	rexrd	$⊢ (φ \land J \in ℕ) \to 2^{nd} (G (J)) \in ℝ^{*}$
41	40	adantr	$⊢ ((φ \land J \in ℕ) \land z \in ℕ) \to 2^{nd} (G (J)) \in ℝ^{*}$
42		iooin	$⊢ ((1^{st} (F (z)) \in ℝ^{} \land 2^{nd} (F (z)) \in ℝ^{}) \land (1^{st} (G (J)) \in ℝ^{} \land 2^{nd} (G (J)) \in ℝ^{})) \to (1^{st} (F (z)), 2^{nd} (F (z))) \cap (1^{st} (G (J)), 2^{nd} (G (J))) = (if (1^{st} (F (z)) \leq 1^{st} (G (J)), 1^{st} (G (J)), 1^{st} (F (z))), if (2^{nd} (F (z)) \leq 2^{nd} (G (J)), 2^{nd} (F (z)), 2^{nd} (G (J))))$
43	31 33 38 41 42	syl22anc	$⊢ ((φ \land J \in ℕ) \land z \in ℕ) \to (1^{st} (F (z)), 2^{nd} (F (z))) \cap (1^{st} (G (J)), 2^{nd} (G (J))) = (if (1^{st} (F (z)) \leq 1^{st} (G (J)), 1^{st} (G (J)), 1^{st} (F (z))), if (2^{nd} (F (z)) \leq 2^{nd} (G (J)), 2^{nd} (F (z)), 2^{nd} (G (J))))$
44	27 43	eqtrd	$⊢ ((φ \land J \in ℕ) \land z \in ℕ) \to (.) (F (z)) \cap (.) (G (J)) = (if (1^{st} (F (z)) \leq 1^{st} (G (J)), 1^{st} (G (J)), 1^{st} (F (z))), if (2^{nd} (F (z)) \leq 2^{nd} (G (J)), 2^{nd} (F (z)), 2^{nd} (G (J))))$
45		ioorebas	$⊢ (if (1^{st} (F (z)) \leq 1^{st} (G (J)), 1^{st} (G (J)), 1^{st} (F (z))), if (2^{nd} (F (z)) \leq 2^{nd} (G (J)), 2^{nd} (F (z)), 2^{nd} (G (J)))) \in ran (.)$
46	44 45	eqeltrdi	$⊢ ((φ \land J \in ℕ) \land z \in ℕ) \to (.) (F (z)) \cap (.) (G (J)) \in ran (.)$

Metamath Proof Explorer

Theorem uniioombllem2a

Proof