uniioombllem2

	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$
	uniioombllem2.h	$⊢ H = (z \in ℕ ⟼ (.) (F (z)) \cap (.) (G (J)))$
	uniioombllem2.k	$⊢ K = (x \in ran (.) ⟼ if (x = \emptyset, ⟨0, 0⟩, ⟨inf (x ℝ^{} <), sup (x ℝ^{} <)⟩))$
Assertion	uniioombllem2	$⊢ (φ \land J \in ℕ) \to seq 1 (+ ({vol}^{} \circ H)) ⇝ {vol}^{} ((.) (G (J)) \cap A)$

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		uniioombllem2.h	$⊢ H = (z \in ℕ ⟼ (.) (F (z)) \cap (.) (G (J)))$
12		uniioombllem2.k	$⊢ K = (x \in ran (.) ⟼ if (x = \emptyset, ⟨0, 0⟩, ⟨inf (x ℝ^{} <), sup (x ℝ^{} <)⟩))$
13		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
14		eqid	$⊢ seq 1 (+ ((abs \circ -) \circ (K \circ H))) = seq 1 (+ ((abs \circ -) \circ (K \circ H)))$
15		1zzd	$⊢ (φ \land J \in ℕ) \to 1 \in ℤ$
16		eqidd	$⊢ ((φ \land J \in ℕ) \land n \in ℕ) \to ((abs \circ -) \circ (K \circ H)) (n) = ((abs \circ -) \circ (K \circ H)) (n)$
17	1 2 3 4 5 6 7 8 9 10	uniioombllem2a	$⊢ ((φ \land J \in ℕ) \land z \in ℕ) \to (.) (F (z)) \cap (.) (G (J)) \in ran (.)$
18	11	a1i	$⊢ (φ \land J \in ℕ) \to H = (z \in ℕ ⟼ (.) (F (z)) \cap (.) (G (J)))$
19	12	ioorf	$⊢ K : ran (.) ⟶ \leq \cap (ℝ^{} \times ℝ^{})$
20	19	a1i	$⊢ (φ \land J \in ℕ) \to K : ran (.) ⟶ \leq \cap (ℝ^{} \times ℝ^{})$
21	20	feqmptd	$⊢ (φ \land J \in ℕ) \to K = (y \in ran (.) ⟼ K (y))$
22		fveq2	$⊢ y = (.) (F (z)) \cap (.) (G (J)) \to K (y) = K ((.) (F (z)) \cap (.) (G (J)))$
23	17 18 21 22	fmptco	$⊢ (φ \land J \in ℕ) \to K \circ H = (z \in ℕ ⟼ K ((.) (F (z)) \cap (.) (G (J))))$
24		inss2	$⊢ (.) (F (z)) \cap (.) (G (J)) \subseteq (.) (G (J))$
25		inss2	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{2}$
26	7	ffvelcdmda	$⊢ (φ \land J \in ℕ) \to G (J) \in (\leq \cap ℝ^{2})$
27	25 26	sselid	$⊢ (φ \land J \in ℕ) \to G (J) \in ℝ^{2}$
28		1st2nd2	$⊢ G (J) \in ℝ^{2} \to G (J) = ⟨1^{st} (G (J)), 2^{nd} (G (J))⟩$
29	27 28	syl	$⊢ (φ \land J \in ℕ) \to G (J) = ⟨1^{st} (G (J)), 2^{nd} (G (J))⟩$
30	29	fveq2d	$⊢ (φ \land J \in ℕ) \to (.) (G (J)) = (.) (⟨1^{st} (G (J)), 2^{nd} (G (J))⟩)$
31		df-ov	$⊢ (1^{st} (G (J)), 2^{nd} (G (J))) = (.) (⟨1^{st} (G (J)), 2^{nd} (G (J))⟩)$
32	30 31	eqtr4di	$⊢ (φ \land J \in ℕ) \to (.) (G (J)) = (1^{st} (G (J)), 2^{nd} (G (J)))$
33		ioossre	$⊢ (1^{st} (G (J)), 2^{nd} (G (J))) \subseteq ℝ$
34	32 33	eqsstrdi	$⊢ (φ \land J \in ℕ) \to (.) (G (J)) \subseteq ℝ$
35	32	fveq2d	$⊢ (φ \land J \in ℕ) \to {vol}^{} ((.) (G (J))) = {vol}^{} ((1^{st} (G (J)), 2^{nd} (G (J))))$
36		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)))$
37	7 36	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)))$
38		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))$
39	37 38	syl	$⊢ (φ \land J \in ℕ) \to {vol}^{*} ((1^{st} (G (J)), 2^{nd} (G (J)))) = 2^{nd} (G (J)) - 1^{st} (G (J))$
40	35 39	eqtrd	$⊢ (φ \land J \in ℕ) \to {vol}^{*} ((.) (G (J))) = 2^{nd} (G (J)) - 1^{st} (G (J))$
41	37	simp2d	$⊢ (φ \land J \in ℕ) \to 2^{nd} (G (J)) \in ℝ$
42	37	simp1d	$⊢ (φ \land J \in ℕ) \to 1^{st} (G (J)) \in ℝ$
43	41 42	resubcld	$⊢ (φ \land J \in ℕ) \to 2^{nd} (G (J)) - 1^{st} (G (J)) \in ℝ$
44	40 43	eqeltrd	$⊢ (φ \land J \in ℕ) \to {vol}^{*} ((.) (G (J))) \in ℝ$
45		ovolsscl	$⊢ ((.) (F (z)) \cap (.) (G (J)) \subseteq (.) (G (J)) \land (.) (G (J)) \subseteq ℝ \land {vol}^{} ((.) (G (J))) \in ℝ) \to {vol}^{} ((.) (F (z)) \cap (.) (G (J))) \in ℝ$
46	24 34 44 45	mp3an2i	$⊢ (φ \land J \in ℕ) \to {vol}^{*} ((.) (F (z)) \cap (.) (G (J))) \in ℝ$
47	46	adantr	$⊢ ((φ \land J \in ℕ) \land z \in ℕ) \to {vol}^{*} ((.) (F (z)) \cap (.) (G (J))) \in ℝ$
48	12	ioorcl	$⊢ ((.) (F (z)) \cap (.) (G (J)) \in ran (.) \land {vol}^{*} ((.) (F (z)) \cap (.) (G (J))) \in ℝ) \to K ((.) (F (z)) \cap (.) (G (J))) \in (\leq \cap ℝ^{2})$
49	17 47 48	syl2anc	$⊢ ((φ \land J \in ℕ) \land z \in ℕ) \to K ((.) (F (z)) \cap (.) (G (J))) \in (\leq \cap ℝ^{2})$
50	23 49	fmpt3d	$⊢ (φ \land J \in ℕ) \to (K \circ H) : ℕ ⟶ \leq \cap ℝ^{2}$
51		eqid	$⊢ (abs \circ -) \circ (K \circ H) = (abs \circ -) \circ (K \circ H)$
52	51	ovolfsf	$⊢ (K \circ H) : ℕ ⟶ \leq \cap ℝ^{2} \to ((abs \circ -) \circ (K \circ H)) : ℕ ⟶ [0, +∞)$
53	50 52	syl	$⊢ (φ \land J \in ℕ) \to ((abs \circ -) \circ (K \circ H)) : ℕ ⟶ [0, +∞)$
54	53	ffvelcdmda	$⊢ ((φ \land J \in ℕ) \land n \in ℕ) \to ((abs \circ -) \circ (K \circ H)) (n) \in [0, +∞)$
55		elrege0	$⊢ ((abs \circ -) \circ (K \circ H)) (n) \in [0, +∞) \leftrightarrow (((abs \circ -) \circ (K \circ H)) (n) \in ℝ \land 0 \leq ((abs \circ -) \circ (K \circ H)) (n))$
56	54 55	sylib	$⊢ ((φ \land J \in ℕ) \land n \in ℕ) \to (((abs \circ -) \circ (K \circ H)) (n) \in ℝ \land 0 \leq ((abs \circ -) \circ (K \circ H)) (n))$
57	56	simpld	$⊢ ((φ \land J \in ℕ) \land n \in ℕ) \to ((abs \circ -) \circ (K \circ H)) (n) \in ℝ$
58	56	simprd	$⊢ ((φ \land J \in ℕ) \land n \in ℕ) \to 0 \leq ((abs \circ -) \circ (K \circ H)) (n)$
59	23	fveq1d	$⊢ (φ \land J \in ℕ) \to (K \circ H) (z) = (z \in ℕ ⟼ K ((.) (F (z)) \cap (.) (G (J)))) (z)$
60		fvex	$⊢ K ((.) (F (z)) \cap (.) (G (J))) \in V$
61		eqid	$⊢ (z \in ℕ ⟼ K ((.) (F (z)) \cap (.) (G (J)))) = (z \in ℕ ⟼ K ((.) (F (z)) \cap (.) (G (J))))$
62	61	fvmpt2	$⊢ (z \in ℕ \land K ((.) (F (z)) \cap (.) (G (J))) \in V) \to (z \in ℕ ⟼ K ((.) (F (z)) \cap (.) (G (J)))) (z) = K ((.) (F (z)) \cap (.) (G (J)))$
63	60 62	mpan2	$⊢ z \in ℕ \to (z \in ℕ ⟼ K ((.) (F (z)) \cap (.) (G (J)))) (z) = K ((.) (F (z)) \cap (.) (G (J)))$
64	59 63	sylan9eq	$⊢ ((φ \land J \in ℕ) \land z \in ℕ) \to (K \circ H) (z) = K ((.) (F (z)) \cap (.) (G (J)))$
65	64	fveq2d	$⊢ ((φ \land J \in ℕ) \land z \in ℕ) \to (.) ((K \circ H) (z)) = (.) (K ((.) (F (z)) \cap (.) (G (J))))$
66	12	ioorinv	$⊢ (.) (F (z)) \cap (.) (G (J)) \in ran (.) \to (.) (K ((.) (F (z)) \cap (.) (G (J)))) = (.) (F (z)) \cap (.) (G (J))$
67	17 66	syl	$⊢ ((φ \land J \in ℕ) \land z \in ℕ) \to (.) (K ((.) (F (z)) \cap (.) (G (J)))) = (.) (F (z)) \cap (.) (G (J))$
68	65 67	eqtrd	$⊢ ((φ \land J \in ℕ) \land z \in ℕ) \to (.) ((K \circ H) (z)) = (.) (F (z)) \cap (.) (G (J))$
69	68	ralrimiva	$⊢ (φ \land J \in ℕ) \to \forall z \in ℕ (.) ((K \circ H) (z)) = (.) (F (z)) \cap (.) (G (J))$
70		2fveq3	$⊢ z = x \to (.) ((K \circ H) (z)) = (.) ((K \circ H) (x))$
71		2fveq3	$⊢ z = x \to (.) (F (z)) = (.) (F (x))$
72	71	ineq1d	$⊢ z = x \to (.) (F (z)) \cap (.) (G (J)) = (.) (F (x)) \cap (.) (G (J))$
73	70 72	eqeq12d	$⊢ z = x \to ((.) ((K \circ H) (z)) = (.) (F (z)) \cap (.) (G (J)) \leftrightarrow (.) ((K \circ H) (x)) = (.) (F (x)) \cap (.) (G (J)))$
74	73	rspccva	$⊢ (\forall z \in ℕ (.) ((K \circ H) (z)) = (.) (F (z)) \cap (.) (G (J)) \land x \in ℕ) \to (.) ((K \circ H) (x)) = (.) (F (x)) \cap (.) (G (J))$
75	69 74	sylan	$⊢ ((φ \land J \in ℕ) \land x \in ℕ) \to (.) ((K \circ H) (x)) = (.) (F (x)) \cap (.) (G (J))$
76		inss1	$⊢ (.) (F (x)) \cap (.) (G (J)) \subseteq (.) (F (x))$
77	75 76	eqsstrdi	$⊢ ((φ \land J \in ℕ) \land x \in ℕ) \to (.) ((K \circ H) (x)) \subseteq (.) (F (x))$
78	77	ralrimiva	$⊢ (φ \land J \in ℕ) \to \forall x \in ℕ (.) ((K \circ H) (x)) \subseteq (.) (F (x))$
79	2	adantr	$⊢ (φ \land J \in ℕ) \to \underset{x \in ℕ}{Disj} (.) (F (x))$
80		disjss2	$⊢ \forall x \in ℕ (.) ((K \circ H) (x)) \subseteq (.) (F (x)) \to (\underset{x \in ℕ}{Disj} (.) (F (x)) \to \underset{x \in ℕ}{Disj} (.) ((K \circ H) (x)))$
81	78 79 80	sylc	$⊢ (φ \land J \in ℕ) \to \underset{x \in ℕ}{Disj} (.) ((K \circ H) (x))$
82	50 81 14	uniioovol	$⊢ (φ \land J \in ℕ) \to {vol}^{} (⋃ ran ((.) \circ (K \circ H))) = sup (ran seq 1 (+ ((abs \circ -) \circ (K \circ H))) ℝ^{} <)$
83	67	mpteq2dva	$⊢ (φ \land J \in ℕ) \to (z \in ℕ ⟼ (.) (K ((.) (F (z)) \cap (.) (G (J))))) = (z \in ℕ ⟼ (.) (F (z)) \cap (.) (G (J)))$
84		rexpssxrxp	$⊢ ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
85	25 84	sstri	$⊢ \leq \cap ℝ^{2} \subseteq ℝ^{} \times ℝ^{}$
86	85 49	sselid	$⊢ ((φ \land J \in ℕ) \land z \in ℕ) \to K ((.) (F (z)) \cap (.) (G (J))) \in (ℝ^{} \times ℝ^{})$
87		ioof	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
88	87	a1i	$⊢ (φ \land J \in ℕ) \to (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ$
89	88	feqmptd	$⊢ (φ \land J \in ℕ) \to (.) = (y \in (ℝ^{} \times ℝ^{}) ⟼ (.) (y))$
90		fveq2	$⊢ y = K ((.) (F (z)) \cap (.) (G (J))) \to (.) (y) = (.) (K ((.) (F (z)) \cap (.) (G (J))))$
91	86 23 89 90	fmptco	$⊢ (φ \land J \in ℕ) \to (.) \circ (K \circ H) = (z \in ℕ ⟼ (.) (K ((.) (F (z)) \cap (.) (G (J)))))$
92	83 91 18	3eqtr4d	$⊢ (φ \land J \in ℕ) \to (.) \circ (K \circ H) = H$
93	92	rneqd	$⊢ (φ \land J \in ℕ) \to ran ((.) \circ (K \circ H)) = ran H$
94	93	unieqd	$⊢ (φ \land J \in ℕ) \to ⋃ ran ((.) \circ (K \circ H)) = ⋃ ran H$
95		fvex	$⊢ (.) (F (z)) \in V$
96	95	inex1	$⊢ (.) (F (z)) \cap (.) (G (J)) \in V$
97	11	fvmpt2	$⊢ (z \in ℕ \land (.) (F (z)) \cap (.) (G (J)) \in V) \to H (z) = (.) (F (z)) \cap (.) (G (J))$
98	96 97	mpan2	$⊢ z \in ℕ \to H (z) = (.) (F (z)) \cap (.) (G (J))$
99		incom	$⊢ (.) (F (z)) \cap (.) (G (J)) = (.) (G (J)) \cap (.) (F (z))$
100	98 99	eqtrdi	$⊢ z \in ℕ \to H (z) = (.) (G (J)) \cap (.) (F (z))$
101	100	iuneq2i	$⊢ ⋃_{z \in ℕ} H (z) = ⋃_{z \in ℕ} ((.) (G (J)) \cap (.) (F (z)))$
102		iunin2	$⊢ ⋃_{z \in ℕ} ((.) (G (J)) \cap (.) (F (z))) = (.) (G (J)) \cap ⋃_{z \in ℕ} (.) (F (z))$
103	101 102	eqtri	$⊢ ⋃_{z \in ℕ} H (z) = (.) (G (J)) \cap ⋃_{z \in ℕ} (.) (F (z))$
104	17 11	fmptd	$⊢ (φ \land J \in ℕ) \to H : ℕ ⟶ ran (.)$
105	104	ffnd	$⊢ (φ \land J \in ℕ) \to H Fn ℕ$
106		fniunfv	$⊢ H Fn ℕ \to ⋃_{z \in ℕ} H (z) = ⋃ ran H$
107	105 106	syl	$⊢ (φ \land J \in ℕ) \to ⋃_{z \in ℕ} H (z) = ⋃ ran H$
108	103 107	eqtr3id	$⊢ (φ \land J \in ℕ) \to (.) (G (J)) \cap ⋃_{z \in ℕ} (.) (F (z)) = ⋃ ran H$
109	1	adantr	$⊢ (φ \land J \in ℕ) \to F : ℕ ⟶ \leq \cap ℝ^{2}$
110		fvco3	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land z \in ℕ) \to ((.) \circ F) (z) = (.) (F (z))$
111	109 110	sylan	$⊢ ((φ \land J \in ℕ) \land z \in ℕ) \to ((.) \circ F) (z) = (.) (F (z))$
112	111	iuneq2dv	$⊢ (φ \land J \in ℕ) \to ⋃_{z \in ℕ} ((.) \circ F) (z) = ⋃_{z \in ℕ} (.) (F (z))$
113		ffn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ \to (.) Fn (ℝ^{} \times ℝ^{})$
114	87 113	ax-mp	$⊢ (.) Fn (ℝ^{} \times ℝ^{})$
115		fss	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land \leq \cap ℝ^{2} \subseteq ℝ^{} \times ℝ^{}) \to F : ℕ ⟶ ℝ^{} \times ℝ^{}$
116	109 85 115	sylancl	$⊢ (φ \land J \in ℕ) \to F : ℕ ⟶ ℝ^{} \times ℝ^{}$
117		fnfco	$⊢ ((.) Fn (ℝ^{} \times ℝ^{}) \land F : ℕ ⟶ ℝ^{} \times ℝ^{}) \to ((.) \circ F) Fn ℕ$
118	114 116 117	sylancr	$⊢ (φ \land J \in ℕ) \to ((.) \circ F) Fn ℕ$
119		fniunfv	$⊢ ((.) \circ F) Fn ℕ \to ⋃_{z \in ℕ} ((.) \circ F) (z) = ⋃ ran ((.) \circ F)$
120	118 119	syl	$⊢ (φ \land J \in ℕ) \to ⋃_{z \in ℕ} ((.) \circ F) (z) = ⋃ ran ((.) \circ F)$
121	120 4	eqtr4di	$⊢ (φ \land J \in ℕ) \to ⋃_{z \in ℕ} ((.) \circ F) (z) = A$
122	112 121	eqtr3d	$⊢ (φ \land J \in ℕ) \to ⋃_{z \in ℕ} (.) (F (z)) = A$
123	122	ineq2d	$⊢ (φ \land J \in ℕ) \to (.) (G (J)) \cap ⋃_{z \in ℕ} (.) (F (z)) = (.) (G (J)) \cap A$
124	94 108 123	3eqtr2d	$⊢ (φ \land J \in ℕ) \to ⋃ ran ((.) \circ (K \circ H)) = (.) (G (J)) \cap A$
125	124	fveq2d	$⊢ (φ \land J \in ℕ) \to {vol}^{} (⋃ ran ((.) \circ (K \circ H))) = {vol}^{} ((.) (G (J)) \cap A)$
126	82 125	eqtr3d	$⊢ (φ \land J \in ℕ) \to sup (ran seq 1 (+ ((abs \circ -) \circ (K \circ H))) ℝ^{} <) = {vol}^{} ((.) (G (J)) \cap A)$
127		inss1	$⊢ (.) (G (J)) \cap A \subseteq (.) (G (J))$
128		ovolsscl	$⊢ ((.) (G (J)) \cap A \subseteq (.) (G (J)) \land (.) (G (J)) \subseteq ℝ \land {vol}^{} ((.) (G (J))) \in ℝ) \to {vol}^{} ((.) (G (J)) \cap A) \in ℝ$
129	127 34 44 128	mp3an2i	$⊢ (φ \land J \in ℕ) \to {vol}^{*} ((.) (G (J)) \cap A) \in ℝ$
130	126 129	eqeltrd	$⊢ (φ \land J \in ℕ) \to sup (ran seq 1 (+ ((abs \circ -) \circ (K \circ H))) ℝ^{*} <) \in ℝ$
131	51 14	ovolsf	$⊢ (K \circ H) : ℕ ⟶ \leq \cap ℝ^{2} \to seq 1 (+ ((abs \circ -) \circ (K \circ H))) : ℕ ⟶ [0, +∞)$
132	50 131	syl	$⊢ (φ \land J \in ℕ) \to seq 1 (+ ((abs \circ -) \circ (K \circ H))) : ℕ ⟶ [0, +∞)$
133	132	frnd	$⊢ (φ \land J \in ℕ) \to ran seq 1 (+ ((abs \circ -) \circ (K \circ H))) \subseteq [0, +∞)$
134		icossxr	$⊢ [0, +∞) \subseteq ℝ^{*}$
135	133 134	sstrdi	$⊢ (φ \land J \in ℕ) \to ran seq 1 (+ ((abs \circ -) \circ (K \circ H))) \subseteq ℝ^{*}$
136	132	ffnd	$⊢ (φ \land J \in ℕ) \to seq 1 (+ ((abs \circ -) \circ (K \circ H))) Fn ℕ$
137		fnfvelrn	$⊢ (seq 1 (+ ((abs \circ -) \circ (K \circ H))) Fn ℕ \land y \in ℕ) \to seq 1 (+ ((abs \circ -) \circ (K \circ H))) (y) \in ran seq 1 (+ ((abs \circ -) \circ (K \circ H)))$
138	136 137	sylan	$⊢ ((φ \land J \in ℕ) \land y \in ℕ) \to seq 1 (+ ((abs \circ -) \circ (K \circ H))) (y) \in ran seq 1 (+ ((abs \circ -) \circ (K \circ H)))$
139		supxrub	$⊢ (ran seq 1 (+ ((abs \circ -) \circ (K \circ H))) \subseteq ℝ^{} \land seq 1 (+ ((abs \circ -) \circ (K \circ H))) (y) \in ran seq 1 (+ ((abs \circ -) \circ (K \circ H)))) \to seq 1 (+ ((abs \circ -) \circ (K \circ H))) (y) \leq sup (ran seq 1 (+ ((abs \circ -) \circ (K \circ H))) ℝ^{} <)$
140	135 138 139	syl2an2r	$⊢ ((φ \land J \in ℕ) \land y \in ℕ) \to seq 1 (+ ((abs \circ -) \circ (K \circ H))) (y) \leq sup (ran seq 1 (+ ((abs \circ -) \circ (K \circ H))) ℝ^{*} <)$
141	140	ralrimiva	$⊢ (φ \land J \in ℕ) \to \forall y \in ℕ seq 1 (+ ((abs \circ -) \circ (K \circ H))) (y) \leq sup (ran seq 1 (+ ((abs \circ -) \circ (K \circ H))) ℝ^{*} <)$
142		brralrspcev	$⊢ (sup (ran seq 1 (+ ((abs \circ -) \circ (K \circ H))) ℝ^{} <) \in ℝ \land \forall y \in ℕ seq 1 (+ ((abs \circ -) \circ (K \circ H))) (y) \leq sup (ran seq 1 (+ ((abs \circ -) \circ (K \circ H))) ℝ^{} <)) \to \exists x \in ℝ \forall y \in ℕ seq 1 (+ ((abs \circ -) \circ (K \circ H))) (y) \leq x$
143	130 141 142	syl2anc	$⊢ (φ \land J \in ℕ) \to \exists x \in ℝ \forall y \in ℕ seq 1 (+ ((abs \circ -) \circ (K \circ H))) (y) \leq x$
144	13 14 15 16 57 58 143	isumsup2	$⊢ (φ \land J \in ℕ) \to seq 1 (+ ((abs \circ -) \circ (K \circ H))) ⇝ sup (ran seq 1 (+ ((abs \circ -) \circ (K \circ H))) ℝ <)$
145	51	ovolfs2	$⊢ (K \circ H) : ℕ ⟶ \leq \cap ℝ^{2} \to (abs \circ -) \circ (K \circ H) = ({vol}^{*} \circ (.)) \circ (K \circ H)$
146	50 145	syl	$⊢ (φ \land J \in ℕ) \to (abs \circ -) \circ (K \circ H) = ({vol}^{*} \circ (.)) \circ (K \circ H)$
147		coass	$⊢ ({vol}^{} \circ (.)) \circ (K \circ H) = {vol}^{} \circ ((.) \circ (K \circ H))$
148	92	coeq2d	$⊢ (φ \land J \in ℕ) \to {vol}^{} \circ ((.) \circ (K \circ H)) = {vol}^{} \circ H$
149	147 148	eqtrid	$⊢ (φ \land J \in ℕ) \to ({vol}^{} \circ (.)) \circ (K \circ H) = {vol}^{} \circ H$
150	146 149	eqtrd	$⊢ (φ \land J \in ℕ) \to (abs \circ -) \circ (K \circ H) = {vol}^{*} \circ H$
151	150	seqeq3d	$⊢ (φ \land J \in ℕ) \to seq 1 (+ ((abs \circ -) \circ (K \circ H))) = seq 1 (+ ({vol}^{*} \circ H))$
152		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
153	133 152	sstrdi	$⊢ (φ \land J \in ℕ) \to ran seq 1 (+ ((abs \circ -) \circ (K \circ H))) \subseteq ℝ$
154		1nn	$⊢ 1 \in ℕ$
155	132	fdmd	$⊢ (φ \land J \in ℕ) \to dom seq 1 (+ ((abs \circ -) \circ (K \circ H))) = ℕ$
156	154 155	eleqtrrid	$⊢ (φ \land J \in ℕ) \to 1 \in dom seq 1 (+ ((abs \circ -) \circ (K \circ H)))$
157	156	ne0d	$⊢ (φ \land J \in ℕ) \to dom seq 1 (+ ((abs \circ -) \circ (K \circ H))) \neq \emptyset$
158		dm0rn0	$⊢ dom seq 1 (+ ((abs \circ -) \circ (K \circ H))) = \emptyset \leftrightarrow ran seq 1 (+ ((abs \circ -) \circ (K \circ H))) = \emptyset$
159	158	necon3bii	$⊢ dom seq 1 (+ ((abs \circ -) \circ (K \circ H))) \neq \emptyset \leftrightarrow ran seq 1 (+ ((abs \circ -) \circ (K \circ H))) \neq \emptyset$
160	157 159	sylib	$⊢ (φ \land J \in ℕ) \to ran seq 1 (+ ((abs \circ -) \circ (K \circ H))) \neq \emptyset$
161		breq1	$⊢ z = seq 1 (+ ((abs \circ -) \circ (K \circ H))) (y) \to (z \leq x \leftrightarrow seq 1 (+ ((abs \circ -) \circ (K \circ H))) (y) \leq x)$
162	161	ralrn	$⊢ seq 1 (+ ((abs \circ -) \circ (K \circ H))) Fn ℕ \to (\forall z \in ran seq 1 (+ ((abs \circ -) \circ (K \circ H))) z \leq x \leftrightarrow \forall y \in ℕ seq 1 (+ ((abs \circ -) \circ (K \circ H))) (y) \leq x)$
163	136 162	syl	$⊢ (φ \land J \in ℕ) \to (\forall z \in ran seq 1 (+ ((abs \circ -) \circ (K \circ H))) z \leq x \leftrightarrow \forall y \in ℕ seq 1 (+ ((abs \circ -) \circ (K \circ H))) (y) \leq x)$
164	163	rexbidv	$⊢ (φ \land J \in ℕ) \to (\exists x \in ℝ \forall z \in ran seq 1 (+ ((abs \circ -) \circ (K \circ H))) z \leq x \leftrightarrow \exists x \in ℝ \forall y \in ℕ seq 1 (+ ((abs \circ -) \circ (K \circ H))) (y) \leq x)$
165	143 164	mpbird	$⊢ (φ \land J \in ℕ) \to \exists x \in ℝ \forall z \in ran seq 1 (+ ((abs \circ -) \circ (K \circ H))) z \leq x$
166		supxrre	$⊢ (ran seq 1 (+ ((abs \circ -) \circ (K \circ H))) \subseteq ℝ \land ran seq 1 (+ ((abs \circ -) \circ (K \circ H))) \neq \emptyset \land \exists x \in ℝ \forall z \in ran seq 1 (+ ((abs \circ -) \circ (K \circ H))) z \leq x) \to sup (ran seq 1 (+ ((abs \circ -) \circ (K \circ H))) ℝ^{*} <) = sup (ran seq 1 (+ ((abs \circ -) \circ (K \circ H))) ℝ <)$
167	153 160 165 166	syl3anc	$⊢ (φ \land J \in ℕ) \to sup (ran seq 1 (+ ((abs \circ -) \circ (K \circ H))) ℝ^{*} <) = sup (ran seq 1 (+ ((abs \circ -) \circ (K \circ H))) ℝ <)$
168	167 126	eqtr3d	$⊢ (φ \land J \in ℕ) \to sup (ran seq 1 (+ ((abs \circ -) \circ (K \circ H))) ℝ <) = {vol}^{*} ((.) (G (J)) \cap A)$
169	144 151 168	3brtr3d	$⊢ (φ \land J \in ℕ) \to seq 1 (+ ({vol}^{} \circ H)) ⇝ {vol}^{} ((.) (G (J)) \cap A)$

Metamath Proof Explorer

Theorem uniioombllem2

Proof