ovolicc2lem5

	Ref	Expression
Hypotheses	ovolicc.1	$⊢ φ \to A \in ℝ$
	ovolicc.2	$⊢ φ \to B \in ℝ$
	ovolicc.3	$⊢ φ \to A \leq B$
	ovolicc2.4	$⊢ S = seq 1 (+ ((abs \circ -) \circ F))$
	ovolicc2.5	$⊢ φ \to F : ℕ ⟶ \leq \cap ℝ^{2}$
	ovolicc2.6	$⊢ φ \to U \in (𝒫 ran ((.) \circ F) \cap Fin)$
	ovolicc2.7	$⊢ φ \to [A, B] \subseteq ⋃ U$
	ovolicc2.8	$⊢ φ \to G : U ⟶ ℕ$
	ovolicc2.9	$⊢ (φ \land t \in U) \to ((.) \circ F) (G (t)) = t$
	ovolicc2.10	$⊢ T = \{u \in U \| u \cap [A, B] \neq \emptyset\}$
Assertion	ovolicc2lem5	$⊢ φ \to B - A \leq sup (ran S ℝ^{*} <)$

Proof

Step	Hyp	Ref	Expression
1		ovolicc.1	$⊢ φ \to A \in ℝ$
2		ovolicc.2	$⊢ φ \to B \in ℝ$
3		ovolicc.3	$⊢ φ \to A \leq B$
4		ovolicc2.4	$⊢ S = seq 1 (+ ((abs \circ -) \circ F))$
5		ovolicc2.5	$⊢ φ \to F : ℕ ⟶ \leq \cap ℝ^{2}$
6		ovolicc2.6	$⊢ φ \to U \in (𝒫 ran ((.) \circ F) \cap Fin)$
7		ovolicc2.7	$⊢ φ \to [A, B] \subseteq ⋃ U$
8		ovolicc2.8	$⊢ φ \to G : U ⟶ ℕ$
9		ovolicc2.9	$⊢ (φ \land t \in U) \to ((.) \circ F) (G (t)) = t$
10		ovolicc2.10	$⊢ T = \{u \in U \| u \cap [A, B] \neq \emptyset\}$
11	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
12	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
13		lbicc2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to A \in [A, B]$
14	11 12 3 13	syl3anc	$⊢ φ \to A \in [A, B]$
15	7 14	sseldd	$⊢ φ \to A \in ⋃ U$
16		eluni2	$⊢ A \in ⋃ U \leftrightarrow \exists z \in U A \in z$
17	15 16	sylib	$⊢ φ \to \exists z \in U A \in z$
18	6	elin2d	$⊢ φ \to U \in Fin$
19	10	ssrab3	$⊢ T \subseteq U$
20		ssfi	$⊢ (U \in Fin \land T \subseteq U) \to T \in Fin$
21	18 19 20	sylancl	$⊢ φ \to T \in Fin$
22	7	adantr	$⊢ (φ \land t \in T) \to [A, B] \subseteq ⋃ U$
23		ineq1	$⊢ u = t \to u \cap [A, B] = t \cap [A, B]$
24	23	neeq1d	$⊢ u = t \to (u \cap [A, B] \neq \emptyset \leftrightarrow t \cap [A, B] \neq \emptyset)$
25	24 10	elrab2	$⊢ t \in T \leftrightarrow (t \in U \land t \cap [A, B] \neq \emptyset)$
26	25	simplbi	$⊢ t \in T \to t \in U$
27		ffvelcdm	$⊢ (G : U ⟶ ℕ \land t \in U) \to G (t) \in ℕ$
28	8 26 27	syl2an	$⊢ (φ \land t \in T) \to G (t) \in ℕ$
29	5	ffvelcdmda	$⊢ (φ \land G (t) \in ℕ) \to F (G (t)) \in (\leq \cap ℝ^{2})$
30	28 29	syldan	$⊢ (φ \land t \in T) \to F (G (t)) \in (\leq \cap ℝ^{2})$
31	30	elin2d	$⊢ (φ \land t \in T) \to F (G (t)) \in ℝ^{2}$
32		xp2nd	$⊢ F (G (t)) \in ℝ^{2} \to 2^{nd} (F (G (t))) \in ℝ$
33	31 32	syl	$⊢ (φ \land t \in T) \to 2^{nd} (F (G (t))) \in ℝ$
34	2	adantr	$⊢ (φ \land t \in T) \to B \in ℝ$
35	33 34	ifcld	$⊢ (φ \land t \in T) \to if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in ℝ$
36	25	simprbi	$⊢ t \in T \to t \cap [A, B] \neq \emptyset$
37	36	adantl	$⊢ (φ \land t \in T) \to t \cap [A, B] \neq \emptyset$
38		n0	$⊢ t \cap [A, B] \neq \emptyset \leftrightarrow \exists y y \in (t \cap [A, B])$
39	37 38	sylib	$⊢ (φ \land t \in T) \to \exists y y \in (t \cap [A, B])$
40	1	adantr	$⊢ (φ \land (t \in T \land y \in (t \cap [A, B]))) \to A \in ℝ$
41		simprr	$⊢ (φ \land (t \in T \land y \in (t \cap [A, B]))) \to y \in (t \cap [A, B])$
42	41	elin2d	$⊢ (φ \land (t \in T \land y \in (t \cap [A, B]))) \to y \in [A, B]$
43	2	adantr	$⊢ (φ \land (t \in T \land y \in (t \cap [A, B]))) \to B \in ℝ$
44		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (y \in [A, B] \leftrightarrow (y \in ℝ \land A \leq y \land y \leq B))$
45	1 43 44	syl2an2r	$⊢ (φ \land (t \in T \land y \in (t \cap [A, B]))) \to (y \in [A, B] \leftrightarrow (y \in ℝ \land A \leq y \land y \leq B))$
46	42 45	mpbid	$⊢ (φ \land (t \in T \land y \in (t \cap [A, B]))) \to (y \in ℝ \land A \leq y \land y \leq B)$
47	46	simp1d	$⊢ (φ \land (t \in T \land y \in (t \cap [A, B]))) \to y \in ℝ$
48	31	adantrr	$⊢ (φ \land (t \in T \land y \in (t \cap [A, B]))) \to F (G (t)) \in ℝ^{2}$
49	48 32	syl	$⊢ (φ \land (t \in T \land y \in (t \cap [A, B]))) \to 2^{nd} (F (G (t))) \in ℝ$
50	46	simp2d	$⊢ (φ \land (t \in T \land y \in (t \cap [A, B]))) \to A \leq y$
51	41	elin1d	$⊢ (φ \land (t \in T \land y \in (t \cap [A, B]))) \to y \in t$
52	28	adantrr	$⊢ (φ \land (t \in T \land y \in (t \cap [A, B]))) \to G (t) \in ℕ$
53		fvco3	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land G (t) \in ℕ) \to ((.) \circ F) (G (t)) = (.) (F (G (t)))$
54	5 52 53	syl2an2r	$⊢ (φ \land (t \in T \land y \in (t \cap [A, B]))) \to ((.) \circ F) (G (t)) = (.) (F (G (t)))$
55	26 9	sylan2	$⊢ (φ \land t \in T) \to ((.) \circ F) (G (t)) = t$
56	55	adantrr	$⊢ (φ \land (t \in T \land y \in (t \cap [A, B]))) \to ((.) \circ F) (G (t)) = t$
57		1st2nd2	$⊢ F (G (t)) \in ℝ^{2} \to F (G (t)) = ⟨1^{st} (F (G (t))), 2^{nd} (F (G (t)))⟩$
58	48 57	syl	$⊢ (φ \land (t \in T \land y \in (t \cap [A, B]))) \to F (G (t)) = ⟨1^{st} (F (G (t))), 2^{nd} (F (G (t)))⟩$
59	58	fveq2d	$⊢ (φ \land (t \in T \land y \in (t \cap [A, B]))) \to (.) (F (G (t))) = (.) (⟨1^{st} (F (G (t))), 2^{nd} (F (G (t)))⟩)$
60		df-ov	$⊢ (1^{st} (F (G (t))), 2^{nd} (F (G (t)))) = (.) (⟨1^{st} (F (G (t))), 2^{nd} (F (G (t)))⟩)$
61	59 60	eqtr4di	$⊢ (φ \land (t \in T \land y \in (t \cap [A, B]))) \to (.) (F (G (t))) = (1^{st} (F (G (t))), 2^{nd} (F (G (t))))$
62	54 56 61	3eqtr3d	$⊢ (φ \land (t \in T \land y \in (t \cap [A, B]))) \to t = (1^{st} (F (G (t))), 2^{nd} (F (G (t))))$
63	51 62	eleqtrd	$⊢ (φ \land (t \in T \land y \in (t \cap [A, B]))) \to y \in (1^{st} (F (G (t))), 2^{nd} (F (G (t))))$
64		xp1st	$⊢ F (G (t)) \in ℝ^{2} \to 1^{st} (F (G (t))) \in ℝ$
65	48 64	syl	$⊢ (φ \land (t \in T \land y \in (t \cap [A, B]))) \to 1^{st} (F (G (t))) \in ℝ$
66		rexr	$⊢ 1^{st} (F (G (t))) \in ℝ \to 1^{st} (F (G (t))) \in ℝ^{*}$
67		rexr	$⊢ 2^{nd} (F (G (t))) \in ℝ \to 2^{nd} (F (G (t))) \in ℝ^{*}$
68		elioo2	$⊢ (1^{st} (F (G (t))) \in ℝ^{} \land 2^{nd} (F (G (t))) \in ℝ^{}) \to (y \in (1^{st} (F (G (t))), 2^{nd} (F (G (t)))) \leftrightarrow (y \in ℝ \land 1^{st} (F (G (t))) < y \land y < 2^{nd} (F (G (t)))))$
69	66 67 68	syl2an	$⊢ (1^{st} (F (G (t))) \in ℝ \land 2^{nd} (F (G (t))) \in ℝ) \to (y \in (1^{st} (F (G (t))), 2^{nd} (F (G (t)))) \leftrightarrow (y \in ℝ \land 1^{st} (F (G (t))) < y \land y < 2^{nd} (F (G (t)))))$
70	65 49 69	syl2anc	$⊢ (φ \land (t \in T \land y \in (t \cap [A, B]))) \to (y \in (1^{st} (F (G (t))), 2^{nd} (F (G (t)))) \leftrightarrow (y \in ℝ \land 1^{st} (F (G (t))) < y \land y < 2^{nd} (F (G (t)))))$
71	63 70	mpbid	$⊢ (φ \land (t \in T \land y \in (t \cap [A, B]))) \to (y \in ℝ \land 1^{st} (F (G (t))) < y \land y < 2^{nd} (F (G (t))))$
72	71	simp3d	$⊢ (φ \land (t \in T \land y \in (t \cap [A, B]))) \to y < 2^{nd} (F (G (t)))$
73	47 49 72	ltled	$⊢ (φ \land (t \in T \land y \in (t \cap [A, B]))) \to y \leq 2^{nd} (F (G (t)))$
74	40 47 49 50 73	letrd	$⊢ (φ \land (t \in T \land y \in (t \cap [A, B]))) \to A \leq 2^{nd} (F (G (t)))$
75	74	expr	$⊢ (φ \land t \in T) \to (y \in (t \cap [A, B]) \to A \leq 2^{nd} (F (G (t))))$
76	75	exlimdv	$⊢ (φ \land t \in T) \to (\exists y y \in (t \cap [A, B]) \to A \leq 2^{nd} (F (G (t))))$
77	39 76	mpd	$⊢ (φ \land t \in T) \to A \leq 2^{nd} (F (G (t)))$
78	3	adantr	$⊢ (φ \land t \in T) \to A \leq B$
79		breq2	$⊢ 2^{nd} (F (G (t))) = if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \to (A \leq 2^{nd} (F (G (t))) \leftrightarrow A \leq if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B))$
80		breq2	$⊢ B = if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \to (A \leq B \leftrightarrow A \leq if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B))$
81	79 80	ifboth	$⊢ (A \leq 2^{nd} (F (G (t))) \land A \leq B) \to A \leq if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B)$
82	77 78 81	syl2anc	$⊢ (φ \land t \in T) \to A \leq if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B)$
83		min2	$⊢ (2^{nd} (F (G (t))) \in ℝ \land B \in ℝ) \to if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \leq B$
84	33 34 83	syl2anc	$⊢ (φ \land t \in T) \to if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \leq B$
85		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in [A, B] \leftrightarrow (if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in ℝ \land A \leq if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \land if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \leq B))$
86	1 2 85	syl2anc	$⊢ φ \to (if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in [A, B] \leftrightarrow (if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in ℝ \land A \leq if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \land if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \leq B))$
87	86	adantr	$⊢ (φ \land t \in T) \to (if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in [A, B] \leftrightarrow (if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in ℝ \land A \leq if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \land if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \leq B))$
88	35 82 84 87	mpbir3and	$⊢ (φ \land t \in T) \to if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in [A, B]$
89	22 88	sseldd	$⊢ (φ \land t \in T) \to if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in ⋃ U$
90		eluni2	$⊢ if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in ⋃ U \leftrightarrow \exists x \in U if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in x$
91	89 90	sylib	$⊢ (φ \land t \in T) \to \exists x \in U if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in x$
92		simprl	$⊢ ((φ \land t \in T) \land (x \in U \land if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in x)) \to x \in U$
93		simprr	$⊢ ((φ \land t \in T) \land (x \in U \land if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in x)) \to if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in x$
94	88	adantr	$⊢ ((φ \land t \in T) \land (x \in U \land if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in x)) \to if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in [A, B]$
95		inelcm	$⊢ (if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in x \land if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in [A, B]) \to x \cap [A, B] \neq \emptyset$
96	93 94 95	syl2anc	$⊢ ((φ \land t \in T) \land (x \in U \land if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in x)) \to x \cap [A, B] \neq \emptyset$
97		ineq1	$⊢ u = x \to u \cap [A, B] = x \cap [A, B]$
98	97	neeq1d	$⊢ u = x \to (u \cap [A, B] \neq \emptyset \leftrightarrow x \cap [A, B] \neq \emptyset)$
99	98 10	elrab2	$⊢ x \in T \leftrightarrow (x \in U \land x \cap [A, B] \neq \emptyset)$
100	92 96 99	sylanbrc	$⊢ ((φ \land t \in T) \land (x \in U \land if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in x)) \to x \in T$
101	91 100 93	reximssdv	$⊢ (φ \land t \in T) \to \exists x \in T if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in x$
102	101	ralrimiva	$⊢ φ \to \forall t \in T \exists x \in T if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in x$
103		eleq2	$⊢ x = h (t) \to (if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in x \leftrightarrow if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in h (t))$
104	103	ac6sfi	$⊢ (T \in Fin \land \forall t \in T \exists x \in T if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in x) \to \exists h (h : T ⟶ T \land \forall t \in T if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in h (t))$
105	21 102 104	syl2anc	$⊢ φ \to \exists h (h : T ⟶ T \land \forall t \in T if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in h (t))$
106	105	adantr	$⊢ (φ \land (z \in U \land A \in z)) \to \exists h (h : T ⟶ T \land \forall t \in T if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in h (t))$
107		2fveq3	$⊢ x = t \to F (G (x)) = F (G (t))$
108	107	fveq2d	$⊢ x = t \to 2^{nd} (F (G (x))) = 2^{nd} (F (G (t)))$
109	108	breq1d	$⊢ x = t \to (2^{nd} (F (G (x))) \leq B \leftrightarrow 2^{nd} (F (G (t))) \leq B)$
110	109 108	ifbieq1d	$⊢ x = t \to if (2^{nd} (F (G (x))) \leq B, 2^{nd} (F (G (x))), B) = if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B)$
111		fveq2	$⊢ x = t \to h (x) = h (t)$
112	110 111	eleq12d	$⊢ x = t \to (if (2^{nd} (F (G (x))) \leq B, 2^{nd} (F (G (x))), B) \in h (x) \leftrightarrow if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in h (t))$
113	112	cbvralvw	$⊢ \forall x \in T if (2^{nd} (F (G (x))) \leq B, 2^{nd} (F (G (x))), B) \in h (x) \leftrightarrow \forall t \in T if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in h (t)$
114	1	adantr	$⊢ (φ \land ((z \in U \land A \in z) \land (h : T ⟶ T \land \forall x \in T if (2^{nd} (F (G (x))) \leq B, 2^{nd} (F (G (x))), B) \in h (x)))) \to A \in ℝ$
115	2	adantr	$⊢ (φ \land ((z \in U \land A \in z) \land (h : T ⟶ T \land \forall x \in T if (2^{nd} (F (G (x))) \leq B, 2^{nd} (F (G (x))), B) \in h (x)))) \to B \in ℝ$
116	3	adantr	$⊢ (φ \land ((z \in U \land A \in z) \land (h : T ⟶ T \land \forall x \in T if (2^{nd} (F (G (x))) \leq B, 2^{nd} (F (G (x))), B) \in h (x)))) \to A \leq B$
117	5	adantr	$⊢ (φ \land ((z \in U \land A \in z) \land (h : T ⟶ T \land \forall x \in T if (2^{nd} (F (G (x))) \leq B, 2^{nd} (F (G (x))), B) \in h (x)))) \to F : ℕ ⟶ \leq \cap ℝ^{2}$
118	6	adantr	$⊢ (φ \land ((z \in U \land A \in z) \land (h : T ⟶ T \land \forall x \in T if (2^{nd} (F (G (x))) \leq B, 2^{nd} (F (G (x))), B) \in h (x)))) \to U \in (𝒫 ran ((.) \circ F) \cap Fin)$
119	7	adantr	$⊢ (φ \land ((z \in U \land A \in z) \land (h : T ⟶ T \land \forall x \in T if (2^{nd} (F (G (x))) \leq B, 2^{nd} (F (G (x))), B) \in h (x)))) \to [A, B] \subseteq ⋃ U$
120	8	adantr	$⊢ (φ \land ((z \in U \land A \in z) \land (h : T ⟶ T \land \forall x \in T if (2^{nd} (F (G (x))) \leq B, 2^{nd} (F (G (x))), B) \in h (x)))) \to G : U ⟶ ℕ$
121	9	adantlr	$⊢ ((φ \land ((z \in U \land A \in z) \land (h : T ⟶ T \land \forall x \in T if (2^{nd} (F (G (x))) \leq B, 2^{nd} (F (G (x))), B) \in h (x)))) \land t \in U) \to ((.) \circ F) (G (t)) = t$
122		simprrl	$⊢ (φ \land ((z \in U \land A \in z) \land (h : T ⟶ T \land \forall x \in T if (2^{nd} (F (G (x))) \leq B, 2^{nd} (F (G (x))), B) \in h (x)))) \to h : T ⟶ T$
123		simprrr	$⊢ (φ \land ((z \in U \land A \in z) \land (h : T ⟶ T \land \forall x \in T if (2^{nd} (F (G (x))) \leq B, 2^{nd} (F (G (x))), B) \in h (x)))) \to \forall x \in T if (2^{nd} (F (G (x))) \leq B, 2^{nd} (F (G (x))), B) \in h (x)$
124	112	rspccva	$⊢ (\forall x \in T if (2^{nd} (F (G (x))) \leq B, 2^{nd} (F (G (x))), B) \in h (x) \land t \in T) \to if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in h (t)$
125	123 124	sylan	$⊢ ((φ \land ((z \in U \land A \in z) \land (h : T ⟶ T \land \forall x \in T if (2^{nd} (F (G (x))) \leq B, 2^{nd} (F (G (x))), B) \in h (x)))) \land t \in T) \to if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in h (t)$
126		simprlr	$⊢ (φ \land ((z \in U \land A \in z) \land (h : T ⟶ T \land \forall x \in T if (2^{nd} (F (G (x))) \leq B, 2^{nd} (F (G (x))), B) \in h (x)))) \to A \in z$
127		simprll	$⊢ (φ \land ((z \in U \land A \in z) \land (h : T ⟶ T \land \forall x \in T if (2^{nd} (F (G (x))) \leq B, 2^{nd} (F (G (x))), B) \in h (x)))) \to z \in U$
128	14	adantr	$⊢ (φ \land ((z \in U \land A \in z) \land (h : T ⟶ T \land \forall x \in T if (2^{nd} (F (G (x))) \leq B, 2^{nd} (F (G (x))), B) \in h (x)))) \to A \in [A, B]$
129		inelcm	$⊢ (A \in z \land A \in [A, B]) \to z \cap [A, B] \neq \emptyset$
130	126 128 129	syl2anc	$⊢ (φ \land ((z \in U \land A \in z) \land (h : T ⟶ T \land \forall x \in T if (2^{nd} (F (G (x))) \leq B, 2^{nd} (F (G (x))), B) \in h (x)))) \to z \cap [A, B] \neq \emptyset$
131		ineq1	$⊢ u = z \to u \cap [A, B] = z \cap [A, B]$
132	131	neeq1d	$⊢ u = z \to (u \cap [A, B] \neq \emptyset \leftrightarrow z \cap [A, B] \neq \emptyset)$
133	132 10	elrab2	$⊢ z \in T \leftrightarrow (z \in U \land z \cap [A, B] \neq \emptyset)$
134	127 130 133	sylanbrc	$⊢ (φ \land ((z \in U \land A \in z) \land (h : T ⟶ T \land \forall x \in T if (2^{nd} (F (G (x))) \leq B, 2^{nd} (F (G (x))), B) \in h (x)))) \to z \in T$
135		eqid	$⊢ seq 1 ((h \circ 1^{st}), (ℕ \times \{z\})) = seq 1 ((h \circ 1^{st}), (ℕ \times \{z\}))$
136		fveq2	$⊢ m = n \to seq 1 ((h \circ 1^{st}), (ℕ \times \{z\})) (m) = seq 1 ((h \circ 1^{st}), (ℕ \times \{z\})) (n)$
137	136	eleq2d	$⊢ m = n \to (B \in seq 1 ((h \circ 1^{st}), (ℕ \times \{z\})) (m) \leftrightarrow B \in seq 1 ((h \circ 1^{st}), (ℕ \times \{z\})) (n))$
138	137	cbvrabv	$⊢ \{m \in ℕ \| B \in seq 1 ((h \circ 1^{st}), (ℕ \times \{z\})) (m)\} = \{n \in ℕ \| B \in seq 1 ((h \circ 1^{st}), (ℕ \times \{z\})) (n)\}$
139		eqid	$⊢ inf (\{m \in ℕ \| B \in seq 1 ((h \circ 1^{st}), (ℕ \times \{z\})) (m)\} ℝ <) = inf (\{m \in ℕ \| B \in seq 1 ((h \circ 1^{st}), (ℕ \times \{z\})) (m)\} ℝ <)$
140	114 115 116 4 117 118 119 120 121 10 122 125 126 134 135 138 139	ovolicc2lem4	$⊢ (φ \land ((z \in U \land A \in z) \land (h : T ⟶ T \land \forall x \in T if (2^{nd} (F (G (x))) \leq B, 2^{nd} (F (G (x))), B) \in h (x)))) \to B - A \leq sup (ran S ℝ^{*} <)$
141	140	anassrs	$⊢ ((φ \land (z \in U \land A \in z)) \land (h : T ⟶ T \land \forall x \in T if (2^{nd} (F (G (x))) \leq B, 2^{nd} (F (G (x))), B) \in h (x))) \to B - A \leq sup (ran S ℝ^{*} <)$
142	141	expr	$⊢ ((φ \land (z \in U \land A \in z)) \land h : T ⟶ T) \to (\forall x \in T if (2^{nd} (F (G (x))) \leq B, 2^{nd} (F (G (x))), B) \in h (x) \to B - A \leq sup (ran S ℝ^{*} <))$
143	113 142	biimtrrid	$⊢ ((φ \land (z \in U \land A \in z)) \land h : T ⟶ T) \to (\forall t \in T if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in h (t) \to B - A \leq sup (ran S ℝ^{*} <))$
144	143	expimpd	$⊢ (φ \land (z \in U \land A \in z)) \to ((h : T ⟶ T \land \forall t \in T if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in h (t)) \to B - A \leq sup (ran S ℝ^{*} <))$
145	144	exlimdv	$⊢ (φ \land (z \in U \land A \in z)) \to (\exists h (h : T ⟶ T \land \forall t \in T if (2^{nd} (F (G (t))) \leq B, 2^{nd} (F (G (t))), B) \in h (t)) \to B - A \leq sup (ran S ℝ^{*} <))$
146	106 145	mpd	$⊢ (φ \land (z \in U \land A \in z)) \to B - A \leq sup (ran S ℝ^{*} <)$
147	17 146	rexlimddv	$⊢ φ \to B - A \leq sup (ran S ℝ^{*} <)$

Metamath Proof Explorer

Theorem ovolicc2lem5

Proof