icccncfext

Description: A continuous function on a closed interval can be extended to a continuous function on the whole real line. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	icccncfext.1	$⊢ \underline{Ⅎ} x F$
	icccncfext.2	$⊢ J = topGen (ran (.))$
	icccncfext.3	$⊢ Y = ⋃ K$
	icccncfext.4	$⊢ G = (x \in ℝ ⟼ if (x \in [A, B], F (x), if (x < A, F (A), F (B))))$
	icccncfext.5	$⊢ φ \to A \in ℝ$
	icccncfext.6	$⊢ φ \to B \in ℝ$
	icccncfext.7	$⊢ φ \to A \leq B$
	icccncfext.8	$⊢ φ \to K \in Top$
	icccncfext.9	$⊢ φ \to F \in ((J ↾_{𝑡} [A, B]) Cn K)$
Assertion	icccncfext	$⊢ φ \to (G \in (J Cn (K ↾_{𝑡} ran F)) \land {G ↾}_{[A, B]} = F)$

Proof

Step	Hyp	Ref	Expression
1		icccncfext.1	$⊢ \underline{Ⅎ} x F$
2		icccncfext.2	$⊢ J = topGen (ran (.))$
3		icccncfext.3	$⊢ Y = ⋃ K$
4		icccncfext.4	$⊢ G = (x \in ℝ ⟼ if (x \in [A, B], F (x), if (x < A, F (A), F (B))))$
5		icccncfext.5	$⊢ φ \to A \in ℝ$
6		icccncfext.6	$⊢ φ \to B \in ℝ$
7		icccncfext.7	$⊢ φ \to A \leq B$
8		icccncfext.8	$⊢ φ \to K \in Top$
9		icccncfext.9	$⊢ φ \to F \in ((J ↾_{𝑡} [A, B]) Cn K)$
10		retopon	$⊢ topGen (ran (.)) \in TopOn (ℝ)$
11	2 10	eqeltri	$⊢ J \in TopOn (ℝ)$
12	5 6	iccssred	$⊢ φ \to [A, B] \subseteq ℝ$
13		resttopon	$⊢ (J \in TopOn (ℝ) \land [A, B] \subseteq ℝ) \to J ↾_{𝑡} [A, B] \in TopOn ([A, B])$
14	11 12 13	sylancr	$⊢ φ \to J ↾_{𝑡} [A, B] \in TopOn ([A, B])$
15	8 3	jctir	$⊢ φ \to (K \in Top \land Y = ⋃ K)$
16		istopon	$⊢ K \in TopOn (Y) \leftrightarrow (K \in Top \land Y = ⋃ K)$
17	15 16	sylibr	$⊢ φ \to K \in TopOn (Y)$
18		cnf2	$⊢ (J ↾_{𝑡} [A, B] \in TopOn ([A, B]) \land K \in TopOn (Y) \land F \in ((J ↾_{𝑡} [A, B]) Cn K)) \to F : [A, B] ⟶ Y$
19	14 17 9 18	syl3anc	$⊢ φ \to F : [A, B] ⟶ Y$
20	19	ffnd	$⊢ φ \to F Fn [A, B]$
21		dffn3	$⊢ F Fn [A, B] \leftrightarrow F : [A, B] ⟶ ran F$
22	20 21	sylib	$⊢ φ \to F : [A, B] ⟶ ran F$
23	22	ffvelrnda	$⊢ (φ \land y \in [A, B]) \to F (y) \in ran F$
24		fnfun	$⊢ F Fn [A, B] \to Fun F$
25	20 24	syl	$⊢ φ \to Fun F$
26	5	rexrd	$⊢ φ \to A \in ℝ^{*}$
27	6	rexrd	$⊢ φ \to B \in ℝ^{*}$
28		lbicc2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to A \in [A, B]$
29	26 27 7 28	syl3anc	$⊢ φ \to A \in [A, B]$
30		fndm	$⊢ F Fn [A, B] \to dom F = [A, B]$
31	20 30	syl	$⊢ φ \to dom F = [A, B]$
32	31	eqcomd	$⊢ φ \to [A, B] = dom F$
33	29 32	eleqtrd	$⊢ φ \to A \in dom F$
34		fvelrn	$⊢ (Fun F \land A \in dom F) \to F (A) \in ran F$
35	25 33 34	syl2anc	$⊢ φ \to F (A) \in ran F$
36		ubicc2	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land A \leq B) \to B \in [A, B]$
37	26 27 7 36	syl3anc	$⊢ φ \to B \in [A, B]$
38	37 32	eleqtrd	$⊢ φ \to B \in dom F$
39		fvelrn	$⊢ (Fun F \land B \in dom F) \to F (B) \in ran F$
40	25 38 39	syl2anc	$⊢ φ \to F (B) \in ran F$
41	35 40	ifcld	$⊢ φ \to if (y < A, F (A), F (B)) \in ran F$
42	41	adantr	$⊢ (φ \land \neg y \in [A, B]) \to if (y < A, F (A), F (B)) \in ran F$
43	23 42	ifclda	$⊢ φ \to if (y \in [A, B], F (y), if (y < A, F (A), F (B))) \in ran F$
44	43	adantr	$⊢ (φ \land y \in ℝ) \to if (y \in [A, B], F (y), if (y < A, F (A), F (B))) \in ran F$
45		nfv	$⊢ Ⅎ y x \in [A, B]$
46		nfcv	$⊢ \underline{Ⅎ} y F (x)$
47		nfcv	$⊢ \underline{Ⅎ} y if (x < A, F (A), F (B))$
48	45 46 47	nfif	$⊢ \underline{Ⅎ} y if (x \in [A, B], F (x), if (x < A, F (A), F (B)))$
49		nfv	$⊢ Ⅎ x y \in [A, B]$
50		nfcv	$⊢ \underline{Ⅎ} x y$
51	1 50	nffv	$⊢ \underline{Ⅎ} x F (y)$
52		nfv	$⊢ Ⅎ x y < A$
53		nfcv	$⊢ \underline{Ⅎ} x A$
54	1 53	nffv	$⊢ \underline{Ⅎ} x F (A)$
55		nfcv	$⊢ \underline{Ⅎ} x B$
56	1 55	nffv	$⊢ \underline{Ⅎ} x F (B)$
57	52 54 56	nfif	$⊢ \underline{Ⅎ} x if (y < A, F (A), F (B))$
58	49 51 57	nfif	$⊢ \underline{Ⅎ} x if (y \in [A, B], F (y), if (y < A, F (A), F (B)))$
59		eleq1	$⊢ x = y \to (x \in [A, B] \leftrightarrow y \in [A, B])$
60		fveq2	$⊢ x = y \to F (x) = F (y)$
61		breq1	$⊢ x = y \to (x < A \leftrightarrow y < A)$
62	61	ifbid	$⊢ x = y \to if (x < A, F (A), F (B)) = if (y < A, F (A), F (B))$
63	59 60 62	ifbieq12d	$⊢ x = y \to if (x \in [A, B], F (x), if (x < A, F (A), F (B))) = if (y \in [A, B], F (y), if (y < A, F (A), F (B)))$
64	48 58 63	cbvmpt	$⊢ (x \in ℝ ⟼ if (x \in [A, B], F (x), if (x < A, F (A), F (B)))) = (y \in ℝ ⟼ if (y \in [A, B], F (y), if (y < A, F (A), F (B))))$
65	4 64	eqtri	$⊢ G = (y \in ℝ ⟼ if (y \in [A, B], F (y), if (y < A, F (A), F (B))))$
66	44 65	fmptd	$⊢ φ \to G : ℝ ⟶ ran F$
67	66	adantr	$⊢ (φ \land y \in ℝ) \to G : ℝ ⟶ ran F$
68		simplll	$⊢ (((φ \land y \in ℝ) \land u \in (K ↾_{𝑡} ran F)) \land G (y) \in u) \to φ$
69		simplr	$⊢ (((φ \land y \in ℝ) \land u \in (K ↾_{𝑡} ran F)) \land G (y) \in u) \to u \in (K ↾_{𝑡} ran F)$
70	68 69	jca	$⊢ (((φ \land y \in ℝ) \land u \in (K ↾_{𝑡} ran F)) \land G (y) \in u) \to (φ \land u \in (K ↾_{𝑡} ran F))$
71		ssidd	$⊢ φ \to ran F \subseteq ran F$
72	19	frnd	$⊢ φ \to ran F \subseteq Y$
73		cnrest2	$⊢ (K \in TopOn (Y) \land ran F \subseteq ran F \land ran F \subseteq Y) \to (F \in ((J ↾_{𝑡} [A, B]) Cn K) \leftrightarrow F \in ((J ↾_{𝑡} [A, B]) Cn (K ↾_{𝑡} ran F)))$
74	17 71 72 73	syl3anc	$⊢ φ \to (F \in ((J ↾_{𝑡} [A, B]) Cn K) \leftrightarrow F \in ((J ↾_{𝑡} [A, B]) Cn (K ↾_{𝑡} ran F)))$
75	9 74	mpbid	$⊢ φ \to F \in ((J ↾_{𝑡} [A, B]) Cn (K ↾_{𝑡} ran F))$
76	75	anim1i	$⊢ (φ \land u \in (K ↾_{𝑡} ran F)) \to (F \in ((J ↾_{𝑡} [A, B]) Cn (K ↾_{𝑡} ran F)) \land u \in (K ↾_{𝑡} ran F))$
77		cnima	$⊢ (F \in ((J ↾_{𝑡} [A, B]) Cn (K ↾_{𝑡} ran F)) \land u \in (K ↾_{𝑡} ran F)) \to F^{-1} [u] \in (J ↾_{𝑡} [A, B])$
78	70 76 77	3syl	$⊢ (((φ \land y \in ℝ) \land u \in (K ↾_{𝑡} ran F)) \land G (y) \in u) \to F^{-1} [u] \in (J ↾_{𝑡} [A, B])$
79		retop	$⊢ topGen (ran (.)) \in Top$
80	2 79	eqeltri	$⊢ J \in Top$
81	80	a1i	$⊢ φ \to J \in Top$
82		reex	$⊢ ℝ \in V$
83	82	a1i	$⊢ φ \to ℝ \in V$
84	83 12	ssexd	$⊢ φ \to [A, B] \in V$
85	81 84	jca	$⊢ φ \to (J \in Top \land [A, B] \in V)$
86	68 85	syl	$⊢ (((φ \land y \in ℝ) \land u \in (K ↾_{𝑡} ran F)) \land G (y) \in u) \to (J \in Top \land [A, B] \in V)$
87		elrest	$⊢ (J \in Top \land [A, B] \in V) \to (F^{-1} [u] \in (J ↾_{𝑡} [A, B]) \leftrightarrow \exists w \in J F^{-1} [u] = w \cap [A, B])$
88	86 87	syl	$⊢ (((φ \land y \in ℝ) \land u \in (K ↾_{𝑡} ran F)) \land G (y) \in u) \to (F^{-1} [u] \in (J ↾_{𝑡} [A, B]) \leftrightarrow \exists w \in J F^{-1} [u] = w \cap [A, B])$
89	78 88	mpbid	$⊢ (((φ \land y \in ℝ) \land u \in (K ↾_{𝑡} ran F)) \land G (y) \in u) \to \exists w \in J F^{-1} [u] = w \cap [A, B]$
90	68	3ad2ant1	$⊢ ((((φ \land y \in ℝ) \land u \in (K ↾_{𝑡} ran F)) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \to φ$
91		simpllr	$⊢ (((φ \land y \in ℝ) \land u \in (K ↾_{𝑡} ran F)) \land G (y) \in u) \to y \in ℝ$
92	91	3ad2ant1	$⊢ ((((φ \land y \in ℝ) \land u \in (K ↾_{𝑡} ran F)) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \to y \in ℝ$
93		simp1r	$⊢ ((((φ \land y \in ℝ) \land u \in (K ↾_{𝑡} ran F)) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \to G (y) \in u$
94	90 92 93	jca31	$⊢ ((((φ \land y \in ℝ) \land u \in (K ↾_{𝑡} ran F)) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \to ((φ \land y \in ℝ) \land G (y) \in u)$
95		simpll2	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \to w \in J$
96		iooretop	$⊢ (−∞, A) \in topGen (ran (.))$
97	96 2	eleqtrri	$⊢ (−∞, A) \in J$
98		iooretop	$⊢ (B, +∞) \in topGen (ran (.))$
99	98 2	eleqtrri	$⊢ (B, +∞) \in J$
100		unopn	$⊢ (J \in Top \land (−∞, A) \in J \land (B, +∞) \in J) \to (−∞, A) \cup (B, +∞) \in J$
101	80 97 99 100	mp3an	$⊢ (−∞, A) \cup (B, +∞) \in J$
102		unopn	$⊢ (J \in Top \land w \in J \land (−∞, A) \cup (B, +∞) \in J) \to w \cup ((−∞, A) \cup (B, +∞)) \in J$
103	80 101 102	mp3an13	$⊢ w \in J \to w \cup ((−∞, A) \cup (B, +∞)) \in J$
104	95 103	syl	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \to w \cup ((−∞, A) \cup (B, +∞)) \in J$
105		simpl1l	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \to (φ \land y \in ℝ)$
106	105	adantr	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \to (φ \land y \in ℝ)$
107		simpl1r	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \to G (y) \in u$
108	107	adantr	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \to G (y) \in u$
109		simpll3	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \to F^{-1} [u] = w \cap [A, B]$
110		difreicc	$⊢ (A \in ℝ \land B \in ℝ) \to ℝ ∖ [A, B] = (−∞, A) \cup (B, +∞)$
111	5 6 110	syl2anc	$⊢ φ \to ℝ ∖ [A, B] = (−∞, A) \cup (B, +∞)$
112	111	eqcomd	$⊢ φ \to (−∞, A) \cup (B, +∞) = ℝ ∖ [A, B]$
113	112	eleq2d	$⊢ φ \to (y \in ((−∞, A) \cup (B, +∞)) \leftrightarrow y \in (ℝ ∖ [A, B]))$
114	113	notbid	$⊢ φ \to (\neg y \in ((−∞, A) \cup (B, +∞)) \leftrightarrow \neg y \in (ℝ ∖ [A, B]))$
115	114	biimpa	$⊢ (φ \land \neg y \in ((−∞, A) \cup (B, +∞))) \to \neg y \in (ℝ ∖ [A, B])$
116		eldif	$⊢ y \in (ℝ ∖ [A, B]) \leftrightarrow (y \in ℝ \land \neg y \in [A, B])$
117	115 116	sylnib	$⊢ (φ \land \neg y \in ((−∞, A) \cup (B, +∞))) \to \neg (y \in ℝ \land \neg y \in [A, B])$
118		imnan	$⊢ (y \in ℝ \to \neg \neg y \in [A, B]) \leftrightarrow \neg (y \in ℝ \land \neg y \in [A, B])$
119	117 118	sylibr	$⊢ (φ \land \neg y \in ((−∞, A) \cup (B, +∞))) \to (y \in ℝ \to \neg \neg y \in [A, B])$
120	119	imp	$⊢ ((φ \land \neg y \in ((−∞, A) \cup (B, +∞))) \land y \in ℝ) \to \neg \neg y \in [A, B]$
121	120	notnotrd	$⊢ ((φ \land \neg y \in ((−∞, A) \cup (B, +∞))) \land y \in ℝ) \to y \in [A, B]$
122	121	an32s	$⊢ ((φ \land y \in ℝ) \land \neg y \in ((−∞, A) \cup (B, +∞))) \to y \in [A, B]$
123	122	adantlr	$⊢ (((φ \land y \in ℝ) \land G (y) \in u) \land \neg y \in ((−∞, A) \cup (B, +∞))) \to y \in [A, B]$
124		simplll	$⊢ (((φ \land y \in ℝ) \land G (y) \in u) \land \neg y \in ((−∞, A) \cup (B, +∞))) \to φ$
125	12	sselda	$⊢ (φ \land y \in [A, B]) \to y \in ℝ$
126	19	adantr	$⊢ (φ \land y \in [A, B]) \to F : [A, B] ⟶ Y$
127	126	ffvelrnda	$⊢ ((φ \land y \in [A, B]) \land y \in [A, B]) \to F (y) \in Y$
128	19 29	ffvelrnd	$⊢ φ \to F (A) \in Y$
129	128	ad3antrrr	$⊢ (((φ \land y \in [A, B]) \land \neg y \in [A, B]) \land y < A) \to F (A) \in Y$
130	19 37	ffvelrnd	$⊢ φ \to F (B) \in Y$
131	130	ad3antrrr	$⊢ (((φ \land y \in [A, B]) \land \neg y \in [A, B]) \land \neg y < A) \to F (B) \in Y$
132	129 131	ifclda	$⊢ ((φ \land y \in [A, B]) \land \neg y \in [A, B]) \to if (y < A, F (A), F (B)) \in Y$
133	127 132	ifclda	$⊢ (φ \land y \in [A, B]) \to if (y \in [A, B], F (y), if (y < A, F (A), F (B))) \in Y$
134	65	fvmpt2	$⊢ (y \in ℝ \land if (y \in [A, B], F (y), if (y < A, F (A), F (B))) \in Y) \to G (y) = if (y \in [A, B], F (y), if (y < A, F (A), F (B)))$
135	125 133 134	syl2anc	$⊢ (φ \land y \in [A, B]) \to G (y) = if (y \in [A, B], F (y), if (y < A, F (A), F (B)))$
136		simpr	$⊢ (φ \land y \in [A, B]) \to y \in [A, B]$
137	136	iftrued	$⊢ (φ \land y \in [A, B]) \to if (y \in [A, B], F (y), if (y < A, F (A), F (B))) = F (y)$
138	135 137	eqtrd	$⊢ (φ \land y \in [A, B]) \to G (y) = F (y)$
139	138	eqcomd	$⊢ (φ \land y \in [A, B]) \to F (y) = G (y)$
140	124 123 139	syl2anc	$⊢ (((φ \land y \in ℝ) \land G (y) \in u) \land \neg y \in ((−∞, A) \cup (B, +∞))) \to F (y) = G (y)$
141		simplr	$⊢ (((φ \land y \in ℝ) \land G (y) \in u) \land \neg y \in ((−∞, A) \cup (B, +∞))) \to G (y) \in u$
142	140 141	eqeltrd	$⊢ (((φ \land y \in ℝ) \land G (y) \in u) \land \neg y \in ((−∞, A) \cup (B, +∞))) \to F (y) \in u$
143	124 20	syl	$⊢ (((φ \land y \in ℝ) \land G (y) \in u) \land \neg y \in ((−∞, A) \cup (B, +∞))) \to F Fn [A, B]$
144		elpreima	$⊢ F Fn [A, B] \to (y \in F^{-1} [u] \leftrightarrow (y \in [A, B] \land F (y) \in u))$
145	143 144	syl	$⊢ (((φ \land y \in ℝ) \land G (y) \in u) \land \neg y \in ((−∞, A) \cup (B, +∞))) \to (y \in F^{-1} [u] \leftrightarrow (y \in [A, B] \land F (y) \in u))$
146	123 142 145	mpbir2and	$⊢ (((φ \land y \in ℝ) \land G (y) \in u) \land \neg y \in ((−∞, A) \cup (B, +∞))) \to y \in F^{-1} [u]$
147	146	adantlr	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg y \in ((−∞, A) \cup (B, +∞))) \to y \in F^{-1} [u]$
148		simplr	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg y \in ((−∞, A) \cup (B, +∞))) \to F^{-1} [u] = w \cap [A, B]$
149	147 148	eleqtrd	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg y \in ((−∞, A) \cup (B, +∞))) \to y \in (w \cap [A, B])$
150		elin	$⊢ y \in (w \cap [A, B]) \leftrightarrow (y \in w \land y \in [A, B])$
151	149 150	sylib	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg y \in ((−∞, A) \cup (B, +∞))) \to (y \in w \land y \in [A, B])$
152	151	simpld	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg y \in ((−∞, A) \cup (B, +∞))) \to y \in w$
153	152	ex	$⊢ (((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \to (\neg y \in ((−∞, A) \cup (B, +∞)) \to y \in w)$
154	153	orrd	$⊢ (((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \to (y \in ((−∞, A) \cup (B, +∞)) \lor y \in w)$
155	154	orcomd	$⊢ (((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \to (y \in w \lor y \in ((−∞, A) \cup (B, +∞)))$
156		elun	$⊢ y \in (w \cup ((−∞, A) \cup (B, +∞))) \leftrightarrow (y \in w \lor y \in ((−∞, A) \cup (B, +∞)))$
157	155 156	sylibr	$⊢ (((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \to y \in (w \cup ((−∞, A) \cup (B, +∞)))$
158	106 108 109 157	syl21anc	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \to y \in (w \cup ((−∞, A) \cup (B, +∞)))$
159		imaundi	$⊢ G [w \cup ((−∞, A) \cup (B, +∞))] = G [w] \cup G [(−∞, A) \cup (B, +∞)]$
160	106	simpld	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \to φ$
161		toponss	$⊢ (J \in TopOn (ℝ) \land w \in J) \to w \subseteq ℝ$
162	11 95 161	sylancr	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \to w \subseteq ℝ$
163	160 162 109	jca31	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \to ((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B])$
164		simplr	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \to F (A) \in u$
165		simpr	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \to F (B) \in u$
166	4	funmpt2	$⊢ Fun G$
167	166	a1i	$⊢ φ \to Fun G$
168	167	ad5antr	$⊢ (((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \land y \in G [w]) \to Fun G$
169		fvelima	$⊢ (Fun G \land y \in G [w]) \to \exists z \in w G (z) = y$
170	168 169	sylancom	$⊢ (((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \land y \in G [w]) \to \exists z \in w G (z) = y$
171		eqcom	$⊢ G (z) = y \leftrightarrow y = G (z)$
172	171	biimpi	$⊢ G (z) = y \to y = G (z)$
173	172	3ad2ant3	$⊢ ((((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \land y \in G [w]) \land z \in w \land G (z) = y) \to y = G (z)$
174		simp1ll	$⊢ ((((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \land y \in G [w]) \land z \in w \land G (z) = y) \to (((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u)$
175		simp1lr	$⊢ ((((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \land y \in G [w]) \land z \in w \land G (z) = y) \to F (B) \in u$
176		simp2	$⊢ ((((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \land y \in G [w]) \land z \in w \land G (z) = y) \to z \in w$
177		simp-5l	$⊢ ((((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \land z \in w) \land z \in [A, B]) \to (φ \land w \subseteq ℝ)$
178		simp-5r	$⊢ ((((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \land z \in w) \land z \in [A, B]) \to F^{-1} [u] = w \cap [A, B]$
179		simplr	$⊢ ((((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \land z \in w) \land z \in [A, B]) \to z \in w$
180	177 178 179	jca31	$⊢ ((((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \land z \in w) \land z \in [A, B]) \to (((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land z \in w)$
181		eleq1	$⊢ y = z \to (y \in [A, B] \leftrightarrow z \in [A, B])$
182	181	anbi2d	$⊢ y = z \to ((φ \land y \in [A, B]) \leftrightarrow (φ \land z \in [A, B]))$
183		fveq2	$⊢ y = z \to G (y) = G (z)$
184		fveq2	$⊢ y = z \to F (y) = F (z)$
185	183 184	eqeq12d	$⊢ y = z \to (G (y) = F (y) \leftrightarrow G (z) = F (z))$
186	182 185	imbi12d	$⊢ y = z \to (((φ \land y \in [A, B]) \to G (y) = F (y)) \leftrightarrow ((φ \land z \in [A, B]) \to G (z) = F (z)))$
187	186 138	chvarvv	$⊢ (φ \land z \in [A, B]) \to G (z) = F (z)$
188	187	ad4ant14	$⊢ (((φ \land F^{-1} [u] = w \cap [A, B]) \land z \in w) \land z \in [A, B]) \to G (z) = F (z)$
189	188	adantl3r	$⊢ ((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land z \in w) \land z \in [A, B]) \to G (z) = F (z)$
190		simp-4l	$⊢ ((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land z \in w) \land z \in [A, B]) \to φ$
191		simp-4r	$⊢ ((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land z \in w) \land z \in [A, B]) \to w \subseteq ℝ$
192		simplr	$⊢ (((φ \land F^{-1} [u] = w \cap [A, B]) \land z \in w) \land z \in [A, B]) \to z \in w$
193		simpr	$⊢ (((φ \land F^{-1} [u] = w \cap [A, B]) \land z \in w) \land z \in [A, B]) \to z \in [A, B]$
194	192 193	elind	$⊢ (((φ \land F^{-1} [u] = w \cap [A, B]) \land z \in w) \land z \in [A, B]) \to z \in (w \cap [A, B])$
195		eqcom	$⊢ F^{-1} [u] = w \cap [A, B] \leftrightarrow w \cap [A, B] = F^{-1} [u]$
196	195	biimpi	$⊢ F^{-1} [u] = w \cap [A, B] \to w \cap [A, B] = F^{-1} [u]$
197	196	ad3antlr	$⊢ (((φ \land F^{-1} [u] = w \cap [A, B]) \land z \in w) \land z \in [A, B]) \to w \cap [A, B] = F^{-1} [u]$
198	194 197	eleqtrd	$⊢ (((φ \land F^{-1} [u] = w \cap [A, B]) \land z \in w) \land z \in [A, B]) \to z \in F^{-1} [u]$
199	198	adantl3r	$⊢ ((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land z \in w) \land z \in [A, B]) \to z \in F^{-1} [u]$
200		simpr	$⊢ ((φ \land w \subseteq ℝ) \land z \in F^{-1} [u]) \to z \in F^{-1} [u]$
201	20	ad2antrr	$⊢ ((φ \land w \subseteq ℝ) \land z \in F^{-1} [u]) \to F Fn [A, B]$
202		elpreima	$⊢ F Fn [A, B] \to (z \in F^{-1} [u] \leftrightarrow (z \in [A, B] \land F (z) \in u))$
203	201 202	syl	$⊢ ((φ \land w \subseteq ℝ) \land z \in F^{-1} [u]) \to (z \in F^{-1} [u] \leftrightarrow (z \in [A, B] \land F (z) \in u))$
204	200 203	mpbid	$⊢ ((φ \land w \subseteq ℝ) \land z \in F^{-1} [u]) \to (z \in [A, B] \land F (z) \in u)$
205	204	simprd	$⊢ ((φ \land w \subseteq ℝ) \land z \in F^{-1} [u]) \to F (z) \in u$
206	190 191 199 205	syl21anc	$⊢ ((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land z \in w) \land z \in [A, B]) \to F (z) \in u$
207	189 206	eqeltrd	$⊢ ((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land z \in w) \land z \in [A, B]) \to G (z) \in u$
208	180 207	sylancom	$⊢ ((((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \land z \in w) \land z \in [A, B]) \to G (z) \in u$
209		simp-5l	$⊢ (((((φ \land w \subseteq ℝ) \land F (A) \in u) \land F (B) \in u) \land z \in w) \land \neg z \in [A, B]) \to φ$
210		simp-4r	$⊢ (((((φ \land w \subseteq ℝ) \land F (A) \in u) \land F (B) \in u) \land z \in w) \land \neg z \in [A, B]) \to F (A) \in u$
211	209 210	jca	$⊢ (((((φ \land w \subseteq ℝ) \land F (A) \in u) \land F (B) \in u) \land z \in w) \land \neg z \in [A, B]) \to (φ \land F (A) \in u)$
212		simpllr	$⊢ (((((φ \land w \subseteq ℝ) \land F (A) \in u) \land F (B) \in u) \land z \in w) \land \neg z \in [A, B]) \to F (B) \in u$
213		simp-5r	$⊢ (((((φ \land w \subseteq ℝ) \land F (A) \in u) \land F (B) \in u) \land z \in w) \land \neg z \in [A, B]) \to w \subseteq ℝ$
214		simplr	$⊢ (((((φ \land w \subseteq ℝ) \land F (A) \in u) \land F (B) \in u) \land z \in w) \land \neg z \in [A, B]) \to z \in w$
215	213 214	sseldd	$⊢ (((((φ \land w \subseteq ℝ) \land F (A) \in u) \land F (B) \in u) \land z \in w) \land \neg z \in [A, B]) \to z \in ℝ$
216	211 212 215	jca31	$⊢ (((((φ \land w \subseteq ℝ) \land F (A) \in u) \land F (B) \in u) \land z \in w) \land \neg z \in [A, B]) \to (((φ \land F (A) \in u) \land F (B) \in u) \land z \in ℝ)$
217	65	a1i	$⊢ ((((φ \land F (A) \in u) \land F (B) \in u) \land z \in ℝ) \land \neg z \in [A, B]) \to G = (y \in ℝ ⟼ if (y \in [A, B], F (y), if (y < A, F (A), F (B))))$
218		breq1	$⊢ y = z \to (y < A \leftrightarrow z < A)$
219	218	ifbid	$⊢ y = z \to if (y < A, F (A), F (B)) = if (z < A, F (A), F (B))$
220	181 184 219	ifbieq12d	$⊢ y = z \to if (y \in [A, B], F (y), if (y < A, F (A), F (B))) = if (z \in [A, B], F (z), if (z < A, F (A), F (B)))$
221	220	adantl	$⊢ (((((φ \land F (A) \in u) \land F (B) \in u) \land z \in ℝ) \land \neg z \in [A, B]) \land y = z) \to if (y \in [A, B], F (y), if (y < A, F (A), F (B))) = if (z \in [A, B], F (z), if (z < A, F (A), F (B)))$
222		simplr	$⊢ ((((φ \land F (A) \in u) \land F (B) \in u) \land z \in ℝ) \land \neg z \in [A, B]) \to z \in ℝ$
223		iffalse	$⊢ \neg z \in [A, B] \to if (z \in [A, B], F (z), if (z < A, F (A), F (B))) = if (z < A, F (A), F (B))$
224	223	adantl	$⊢ ((((φ \land F (A) \in u) \land F (B) \in u) \land z \in ℝ) \land \neg z \in [A, B]) \to if (z \in [A, B], F (z), if (z < A, F (A), F (B))) = if (z < A, F (A), F (B))$
225		simp-5r	$⊢ (((((φ \land F (A) \in u) \land F (B) \in u) \land z \in ℝ) \land \neg z \in [A, B]) \land z < A) \to F (A) \in u$
226		simp-4r	$⊢ (((((φ \land F (A) \in u) \land F (B) \in u) \land z \in ℝ) \land \neg z \in [A, B]) \land \neg z < A) \to F (B) \in u$
227	225 226	ifclda	$⊢ ((((φ \land F (A) \in u) \land F (B) \in u) \land z \in ℝ) \land \neg z \in [A, B]) \to if (z < A, F (A), F (B)) \in u$
228	224 227	eqeltrd	$⊢ ((((φ \land F (A) \in u) \land F (B) \in u) \land z \in ℝ) \land \neg z \in [A, B]) \to if (z \in [A, B], F (z), if (z < A, F (A), F (B))) \in u$
229	217 221 222 228	fvmptd	$⊢ ((((φ \land F (A) \in u) \land F (B) \in u) \land z \in ℝ) \land \neg z \in [A, B]) \to G (z) = if (z \in [A, B], F (z), if (z < A, F (A), F (B)))$
230	229 224	eqtrd	$⊢ ((((φ \land F (A) \in u) \land F (B) \in u) \land z \in ℝ) \land \neg z \in [A, B]) \to G (z) = if (z < A, F (A), F (B))$
231	230 227	eqeltrd	$⊢ ((((φ \land F (A) \in u) \land F (B) \in u) \land z \in ℝ) \land \neg z \in [A, B]) \to G (z) \in u$
232	216 231	sylancom	$⊢ (((((φ \land w \subseteq ℝ) \land F (A) \in u) \land F (B) \in u) \land z \in w) \land \neg z \in [A, B]) \to G (z) \in u$
233	232	adantl4r	$⊢ ((((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \land z \in w) \land \neg z \in [A, B]) \to G (z) \in u$
234	208 233	pm2.61dan	$⊢ (((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \land z \in w) \to G (z) \in u$
235	174 175 176 234	syl21anc	$⊢ ((((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \land y \in G [w]) \land z \in w \land G (z) = y) \to G (z) \in u$
236	173 235	eqeltrd	$⊢ ((((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \land y \in G [w]) \land z \in w \land G (z) = y) \to y \in u$
237	236	rexlimdv3a	$⊢ (((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \land y \in G [w]) \to (\exists z \in w G (z) = y \to y \in u)$
238	170 237	mpd	$⊢ (((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \land y \in G [w]) \to y \in u$
239	238	ex	$⊢ ((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \to (y \in G [w] \to y \in u)$
240	239	alrimiv	$⊢ ((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \to \forall y (y \in G [w] \to y \in u)$
241	163 164 165 240	syl21anc	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \to \forall y (y \in G [w] \to y \in u)$
242		dfss2	$⊢ G [w] \subseteq u \leftrightarrow \forall y (y \in G [w] \to y \in u)$
243	241 242	sylibr	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \to G [w] \subseteq u$
244		imaundi	$⊢ G [(−∞, A) \cup (B, +∞)] = G [(−∞, A)] \cup G [(B, +∞)]$
245	166	a1i	$⊢ (φ \land t \in G [(−∞, A)]) \to Fun G$
246		fvelima	$⊢ (Fun G \land t \in G [(−∞, A)]) \to \exists z \in (−∞, A) G (z) = t$
247	245 246	sylancom	$⊢ (φ \land t \in G [(−∞, A)]) \to \exists z \in (−∞, A) G (z) = t$
248		simp1l	$⊢ ((φ \land t \in G [(−∞, A)]) \land z \in (−∞, A) \land G (z) = t) \to φ$
249		simp2	$⊢ ((φ \land t \in G [(−∞, A)]) \land z \in (−∞, A) \land G (z) = t) \to z \in (−∞, A)$
250		simp3	$⊢ ((φ \land t \in G [(−∞, A)]) \land z \in (−∞, A) \land G (z) = t) \to G (z) = t$
251	65	a1i	$⊢ (φ \land z \in (−∞, A)) \to G = (y \in ℝ ⟼ if (y \in [A, B], F (y), if (y < A, F (A), F (B))))$
252	220	adantl	$⊢ ((φ \land z \in (−∞, A)) \land y = z) \to if (y \in [A, B], F (y), if (y < A, F (A), F (B))) = if (z \in [A, B], F (z), if (z < A, F (A), F (B)))$
253		elioore	$⊢ z \in (−∞, A) \to z \in ℝ$
254	253	adantl	$⊢ (φ \land z \in (−∞, A)) \to z \in ℝ$
255		elioo3g	$⊢ z \in (−∞, A) \leftrightarrow ((−∞ \in ℝ^{} \land A \in ℝ^{} \land z \in ℝ^{*}) \land (−∞ < z \land z < A))$
256	255	biimpi	$⊢ z \in (−∞, A) \to ((−∞ \in ℝ^{} \land A \in ℝ^{} \land z \in ℝ^{*}) \land (−∞ < z \land z < A))$
257	256	simprrd	$⊢ z \in (−∞, A) \to z < A$
258	257	adantl	$⊢ (φ \land z \in (−∞, A)) \to z < A$
259		ltnle	$⊢ (z \in ℝ \land A \in ℝ) \to (z < A \leftrightarrow \neg A \leq z)$
260	253 5 259	syl2anr	$⊢ (φ \land z \in (−∞, A)) \to (z < A \leftrightarrow \neg A \leq z)$
261	258 260	mpbid	$⊢ (φ \land z \in (−∞, A)) \to \neg A \leq z$
262	261	intn3an2d	$⊢ (φ \land z \in (−∞, A)) \to \neg (z \in ℝ \land A \leq z \land z \leq B)$
263	5 6	jca	$⊢ φ \to (A \in ℝ \land B \in ℝ)$
264	263	adantr	$⊢ (φ \land z \in (−∞, A)) \to (A \in ℝ \land B \in ℝ)$
265		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (z \in [A, B] \leftrightarrow (z \in ℝ \land A \leq z \land z \leq B))$
266	264 265	syl	$⊢ (φ \land z \in (−∞, A)) \to (z \in [A, B] \leftrightarrow (z \in ℝ \land A \leq z \land z \leq B))$
267	262 266	mtbird	$⊢ (φ \land z \in (−∞, A)) \to \neg z \in [A, B]$
268	267	iffalsed	$⊢ (φ \land z \in (−∞, A)) \to if (z \in [A, B], F (z), if (z < A, F (A), F (B))) = if (z < A, F (A), F (B))$
269	257	iftrued	$⊢ z \in (−∞, A) \to if (z < A, F (A), F (B)) = F (A)$
270	269	adantl	$⊢ (φ \land z \in (−∞, A)) \to if (z < A, F (A), F (B)) = F (A)$
271	268 270	eqtrd	$⊢ (φ \land z \in (−∞, A)) \to if (z \in [A, B], F (z), if (z < A, F (A), F (B))) = F (A)$
272	128	adantr	$⊢ (φ \land z \in (−∞, A)) \to F (A) \in Y$
273	271 272	eqeltrd	$⊢ (φ \land z \in (−∞, A)) \to if (z \in [A, B], F (z), if (z < A, F (A), F (B))) \in Y$
274	251 252 254 273	fvmptd	$⊢ (φ \land z \in (−∞, A)) \to G (z) = if (z \in [A, B], F (z), if (z < A, F (A), F (B)))$
275	274	adantr	$⊢ ((φ \land z \in (−∞, A)) \land G (z) = t) \to G (z) = if (z \in [A, B], F (z), if (z < A, F (A), F (B)))$
276		simpr	$⊢ ((φ \land z \in (−∞, A)) \land G (z) = t) \to G (z) = t$
277	271	adantr	$⊢ ((φ \land z \in (−∞, A)) \land G (z) = t) \to if (z \in [A, B], F (z), if (z < A, F (A), F (B))) = F (A)$
278	275 276 277	3eqtr3d	$⊢ ((φ \land z \in (−∞, A)) \land G (z) = t) \to t = F (A)$
279	248 249 250 278	syl21anc	$⊢ ((φ \land t \in G [(−∞, A)]) \land z \in (−∞, A) \land G (z) = t) \to t = F (A)$
280	279	rexlimdv3a	$⊢ (φ \land t \in G [(−∞, A)]) \to (\exists z \in (−∞, A) G (z) = t \to t = F (A))$
281	247 280	mpd	$⊢ (φ \land t \in G [(−∞, A)]) \to t = F (A)$
282		velsn	$⊢ t \in \{F (A)\} \leftrightarrow t = F (A)$
283	281 282	sylibr	$⊢ (φ \land t \in G [(−∞, A)]) \to t \in \{F (A)\}$
284	283	ex	$⊢ φ \to (t \in G [(−∞, A)] \to t \in \{F (A)\})$
285	284	ssrdv	$⊢ φ \to G [(−∞, A)] \subseteq \{F (A)\}$
286	285	adantr	$⊢ (φ \land F (A) \in u) \to G [(−∞, A)] \subseteq \{F (A)\}$
287		simpr	$⊢ (φ \land F (A) \in u) \to F (A) \in u$
288	287	snssd	$⊢ (φ \land F (A) \in u) \to \{F (A)\} \subseteq u$
289	286 288	sstrd	$⊢ (φ \land F (A) \in u) \to G [(−∞, A)] \subseteq u$
290	289	adantr	$⊢ ((φ \land F (A) \in u) \land F (B) \in u) \to G [(−∞, A)] \subseteq u$
291		fvelima	$⊢ (Fun G \land t \in G [(B, +∞)]) \to \exists z \in (B, +∞) G (z) = t$
292	167 291	sylan	$⊢ (φ \land t \in G [(B, +∞)]) \to \exists z \in (B, +∞) G (z) = t$
293		simp1l	$⊢ ((φ \land t \in G [(B, +∞)]) \land z \in (B, +∞) \land G (z) = t) \to φ$
294		simp2	$⊢ ((φ \land t \in G [(B, +∞)]) \land z \in (B, +∞) \land G (z) = t) \to z \in (B, +∞)$
295		simp3	$⊢ ((φ \land t \in G [(B, +∞)]) \land z \in (B, +∞) \land G (z) = t) \to G (z) = t$
296	65	a1i	$⊢ (φ \land z \in (B, +∞)) \to G = (y \in ℝ ⟼ if (y \in [A, B], F (y), if (y < A, F (A), F (B))))$
297	220	adantl	$⊢ ((φ \land z \in (B, +∞)) \land y = z) \to if (y \in [A, B], F (y), if (y < A, F (A), F (B))) = if (z \in [A, B], F (z), if (z < A, F (A), F (B)))$
298		elioore	$⊢ z \in (B, +∞) \to z \in ℝ$
299	298	adantl	$⊢ (φ \land z \in (B, +∞)) \to z \in ℝ$
300	19	ffvelrnda	$⊢ (φ \land z \in [A, B]) \to F (z) \in Y$
301	300	adantlr	$⊢ ((φ \land z \in (B, +∞)) \land z \in [A, B]) \to F (z) \in Y$
302	5	adantr	$⊢ (φ \land z \in (B, +∞)) \to A \in ℝ$
303	6	adantr	$⊢ (φ \land z \in (B, +∞)) \to B \in ℝ$
304	7	adantr	$⊢ (φ \land z \in (B, +∞)) \to A \leq B$
305		elioo3g	$⊢ z \in (B, +∞) \leftrightarrow ((B \in ℝ^{} \land +∞ \in ℝ^{} \land z \in ℝ^{*}) \land (B < z \land z < +∞))$
306	305	biimpi	$⊢ z \in (B, +∞) \to ((B \in ℝ^{} \land +∞ \in ℝ^{} \land z \in ℝ^{*}) \land (B < z \land z < +∞))$
307	306	simprld	$⊢ z \in (B, +∞) \to B < z$
308	307	adantl	$⊢ (φ \land z \in (B, +∞)) \to B < z$
309	302 303 299 304 308	lelttrd	$⊢ (φ \land z \in (B, +∞)) \to A < z$
310	302 299 309	ltnsymd	$⊢ (φ \land z \in (B, +∞)) \to \neg z < A$
311	310	iffalsed	$⊢ (φ \land z \in (B, +∞)) \to if (z < A, F (A), F (B)) = F (B)$
312	130	adantr	$⊢ (φ \land z \in (B, +∞)) \to F (B) \in Y$
313	311 312	eqeltrd	$⊢ (φ \land z \in (B, +∞)) \to if (z < A, F (A), F (B)) \in Y$
314	313	adantr	$⊢ ((φ \land z \in (B, +∞)) \land \neg z \in [A, B]) \to if (z < A, F (A), F (B)) \in Y$
315	301 314	ifclda	$⊢ (φ \land z \in (B, +∞)) \to if (z \in [A, B], F (z), if (z < A, F (A), F (B))) \in Y$
316	296 297 299 315	fvmptd	$⊢ (φ \land z \in (B, +∞)) \to G (z) = if (z \in [A, B], F (z), if (z < A, F (A), F (B)))$
317	316	adantr	$⊢ ((φ \land z \in (B, +∞)) \land G (z) = t) \to G (z) = if (z \in [A, B], F (z), if (z < A, F (A), F (B)))$
318		simpr	$⊢ ((φ \land z \in (B, +∞)) \land G (z) = t) \to G (z) = t$
319	303 299	ltnled	$⊢ (φ \land z \in (B, +∞)) \to (B < z \leftrightarrow \neg z \leq B)$
320	308 319	mpbid	$⊢ (φ \land z \in (B, +∞)) \to \neg z \leq B$
321	320	intn3an3d	$⊢ (φ \land z \in (B, +∞)) \to \neg (z \in ℝ \land A \leq z \land z \leq B)$
322	263	adantr	$⊢ (φ \land z \in (B, +∞)) \to (A \in ℝ \land B \in ℝ)$
323	322 265	syl	$⊢ (φ \land z \in (B, +∞)) \to (z \in [A, B] \leftrightarrow (z \in ℝ \land A \leq z \land z \leq B))$
324	321 323	mtbird	$⊢ (φ \land z \in (B, +∞)) \to \neg z \in [A, B]$
325	324	iffalsed	$⊢ (φ \land z \in (B, +∞)) \to if (z \in [A, B], F (z), if (z < A, F (A), F (B))) = if (z < A, F (A), F (B))$
326	325 311	eqtrd	$⊢ (φ \land z \in (B, +∞)) \to if (z \in [A, B], F (z), if (z < A, F (A), F (B))) = F (B)$
327	326	adantr	$⊢ ((φ \land z \in (B, +∞)) \land G (z) = t) \to if (z \in [A, B], F (z), if (z < A, F (A), F (B))) = F (B)$
328	317 318 327	3eqtr3d	$⊢ ((φ \land z \in (B, +∞)) \land G (z) = t) \to t = F (B)$
329	293 294 295 328	syl21anc	$⊢ ((φ \land t \in G [(B, +∞)]) \land z \in (B, +∞) \land G (z) = t) \to t = F (B)$
330	329	rexlimdv3a	$⊢ (φ \land t \in G [(B, +∞)]) \to (\exists z \in (B, +∞) G (z) = t \to t = F (B))$
331	292 330	mpd	$⊢ (φ \land t \in G [(B, +∞)]) \to t = F (B)$
332		velsn	$⊢ t \in \{F (B)\} \leftrightarrow t = F (B)$
333	331 332	sylibr	$⊢ (φ \land t \in G [(B, +∞)]) \to t \in \{F (B)\}$
334	333	ex	$⊢ φ \to (t \in G [(B, +∞)] \to t \in \{F (B)\})$
335	334	ssrdv	$⊢ φ \to G [(B, +∞)] \subseteq \{F (B)\}$
336	335	adantr	$⊢ (φ \land F (B) \in u) \to G [(B, +∞)] \subseteq \{F (B)\}$
337		simpr	$⊢ (φ \land F (B) \in u) \to F (B) \in u$
338	337	snssd	$⊢ (φ \land F (B) \in u) \to \{F (B)\} \subseteq u$
339	336 338	sstrd	$⊢ (φ \land F (B) \in u) \to G [(B, +∞)] \subseteq u$
340	339	adantlr	$⊢ ((φ \land F (A) \in u) \land F (B) \in u) \to G [(B, +∞)] \subseteq u$
341	290 340	unssd	$⊢ ((φ \land F (A) \in u) \land F (B) \in u) \to G [(−∞, A)] \cup G [(B, +∞)] \subseteq u$
342	244 341	eqsstrid	$⊢ ((φ \land F (A) \in u) \land F (B) \in u) \to G [(−∞, A) \cup (B, +∞)] \subseteq u$
343	160 164 165 342	syl21anc	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \to G [(−∞, A) \cup (B, +∞)] \subseteq u$
344	243 343	unssd	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \to G [w] \cup G [(−∞, A) \cup (B, +∞)] \subseteq u$
345	159 344	eqsstrid	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \to G [w \cup ((−∞, A) \cup (B, +∞))] \subseteq u$
346		eleq2	$⊢ v = w \cup ((−∞, A) \cup (B, +∞)) \to (y \in v \leftrightarrow y \in (w \cup ((−∞, A) \cup (B, +∞))))$
347		imaeq2	$⊢ v = w \cup ((−∞, A) \cup (B, +∞)) \to G [v] = G [w \cup ((−∞, A) \cup (B, +∞))]$
348	347	sseq1d	$⊢ v = w \cup ((−∞, A) \cup (B, +∞)) \to (G [v] \subseteq u \leftrightarrow G [w \cup ((−∞, A) \cup (B, +∞))] \subseteq u)$
349	346 348	anbi12d	$⊢ v = w \cup ((−∞, A) \cup (B, +∞)) \to ((y \in v \land G [v] \subseteq u) \leftrightarrow (y \in (w \cup ((−∞, A) \cup (B, +∞))) \land G [w \cup ((−∞, A) \cup (B, +∞))] \subseteq u))$
350	349	rspcev	$⊢ (w \cup ((−∞, A) \cup (B, +∞)) \in J \land (y \in (w \cup ((−∞, A) \cup (B, +∞))) \land G [w \cup ((−∞, A) \cup (B, +∞))] \subseteq u)) \to \exists v \in J (y \in v \land G [v] \subseteq u)$
351	104 158 345 350	syl12anc	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land F (B) \in u) \to \exists v \in J (y \in v \land G [v] \subseteq u)$
352	80	a1i	$⊢ w \in J \to J \in Top$
353		iooretop	$⊢ (−∞, B) \in topGen (ran (.))$
354	353 2	eleqtrri	$⊢ (−∞, B) \in J$
355		inopn	$⊢ (J \in Top \land w \in J \land (−∞, B) \in J) \to w \cap (−∞, B) \in J$
356	80 354 355	mp3an13	$⊢ w \in J \to w \cap (−∞, B) \in J$
357	97	a1i	$⊢ w \in J \to (−∞, A) \in J$
358		unopn	$⊢ (J \in Top \land w \cap (−∞, B) \in J \land (−∞, A) \in J) \to (w \cap (−∞, B)) \cup (−∞, A) \in J$
359	352 356 357 358	syl3anc	$⊢ w \in J \to (w \cap (−∞, B)) \cup (−∞, A) \in J$
360	359	3ad2ant2	$⊢ (((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \to (w \cap (−∞, B)) \cup (−∞, A) \in J$
361	360	ad2antrr	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land \neg F (B) \in u) \to (w \cap (−∞, B)) \cup (−∞, A) \in J$
362		simpll1	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land \neg F (B) \in u) \to ((φ \land y \in ℝ) \land G (y) \in u)$
363		simpll3	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land \neg F (B) \in u) \to F^{-1} [u] = w \cap [A, B]$
364		simpr	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land \neg F (B) \in u) \to \neg F (B) \in u$
365		simpll	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (B) \in u) \land \neg y \in (−∞, A)) \to (((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B])$
366	263	ad3antrrr	$⊢ (((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (B) \in u) \to (A \in ℝ \land B \in ℝ)$
367		eqimss	$⊢ ℝ ∖ [A, B] = (−∞, A) \cup (B, +∞) \to ℝ ∖ [A, B] \subseteq (−∞, A) \cup (B, +∞)$
368	110 367	syl	$⊢ (A \in ℝ \land B \in ℝ) \to ℝ ∖ [A, B] \subseteq (−∞, A) \cup (B, +∞)$
369		difcom	$⊢ ℝ ∖ [A, B] \subseteq (−∞, A) \cup (B, +∞) \leftrightarrow ℝ ∖ ((−∞, A) \cup (B, +∞)) \subseteq [A, B]$
370	368 369	sylib	$⊢ (A \in ℝ \land B \in ℝ) \to ℝ ∖ ((−∞, A) \cup (B, +∞)) \subseteq [A, B]$
371	366 370	syl	$⊢ (((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (B) \in u) \to ℝ ∖ ((−∞, A) \cup (B, +∞)) \subseteq [A, B]$
372	371	adantr	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (B) \in u) \land \neg y \in (−∞, A)) \to ℝ ∖ ((−∞, A) \cup (B, +∞)) \subseteq [A, B]$
373		simp-4r	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (B) \in u) \land \neg y \in (−∞, A)) \to y \in ℝ$
374		simpr	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (B) \in u) \land \neg y \in (−∞, A)) \to \neg y \in (−∞, A)$
375		elioore	$⊢ y \in (B, +∞) \to y \in ℝ$
376	375	adantl	$⊢ (φ \land y \in (B, +∞)) \to y \in ℝ$
377		elioo3g	$⊢ y \in (B, +∞) \leftrightarrow ((B \in ℝ^{} \land +∞ \in ℝ^{} \land y \in ℝ^{*}) \land (B < y \land y < +∞))$
378	377	biimpi	$⊢ y \in (B, +∞) \to ((B \in ℝ^{} \land +∞ \in ℝ^{} \land y \in ℝ^{*}) \land (B < y \land y < +∞))$
379	378	simprld	$⊢ y \in (B, +∞) \to B < y$
380	379	adantl	$⊢ (φ \land y \in (B, +∞)) \to B < y$
381	6	adantr	$⊢ (φ \land y \in (B, +∞)) \to B \in ℝ$
382	381 376	ltnled	$⊢ (φ \land y \in (B, +∞)) \to (B < y \leftrightarrow \neg y \leq B)$
383	380 382	mpbid	$⊢ (φ \land y \in (B, +∞)) \to \neg y \leq B$
384	383	intn3an3d	$⊢ (φ \land y \in (B, +∞)) \to \neg (y \in ℝ \land A \leq y \land y \leq B)$
385	263	adantr	$⊢ (φ \land y \in (B, +∞)) \to (A \in ℝ \land B \in ℝ)$
386		elicc2	$⊢ (A \in ℝ \land B \in ℝ) \to (y \in [A, B] \leftrightarrow (y \in ℝ \land A \leq y \land y \leq B))$
387	385 386	syl	$⊢ (φ \land y \in (B, +∞)) \to (y \in [A, B] \leftrightarrow (y \in ℝ \land A \leq y \land y \leq B))$
388	384 387	mtbird	$⊢ (φ \land y \in (B, +∞)) \to \neg y \in [A, B]$
389	388	iffalsed	$⊢ (φ \land y \in (B, +∞)) \to if (y \in [A, B], F (y), if (y < A, F (A), F (B))) = if (y < A, F (A), F (B))$
390	5	adantr	$⊢ (φ \land y \in (B, +∞)) \to A \in ℝ$
391	7	adantr	$⊢ (φ \land y \in (B, +∞)) \to A \leq B$
392	390 381 376 391 380	lelttrd	$⊢ (φ \land y \in (B, +∞)) \to A < y$
393	390 376 392	ltnsymd	$⊢ (φ \land y \in (B, +∞)) \to \neg y < A$
394	393	iffalsed	$⊢ (φ \land y \in (B, +∞)) \to if (y < A, F (A), F (B)) = F (B)$
395	389 394	eqtrd	$⊢ (φ \land y \in (B, +∞)) \to if (y \in [A, B], F (y), if (y < A, F (A), F (B))) = F (B)$
396	130	adantr	$⊢ (φ \land y \in (B, +∞)) \to F (B) \in Y$
397	395 396	eqeltrd	$⊢ (φ \land y \in (B, +∞)) \to if (y \in [A, B], F (y), if (y < A, F (A), F (B))) \in Y$
398	376 397 134	syl2anc	$⊢ (φ \land y \in (B, +∞)) \to G (y) = if (y \in [A, B], F (y), if (y < A, F (A), F (B)))$
399	398 395	eqtrd	$⊢ (φ \land y \in (B, +∞)) \to G (y) = F (B)$
400	399	eqcomd	$⊢ (φ \land y \in (B, +∞)) \to F (B) = G (y)$
401	400	adantlr	$⊢ ((φ \land G (y) \in u) \land y \in (B, +∞)) \to F (B) = G (y)$
402		simplr	$⊢ ((φ \land G (y) \in u) \land y \in (B, +∞)) \to G (y) \in u$
403	401 402	eqeltrd	$⊢ ((φ \land G (y) \in u) \land y \in (B, +∞)) \to F (B) \in u$
404	403	adantllr	$⊢ (((φ \land y \in ℝ) \land G (y) \in u) \land y \in (B, +∞)) \to F (B) \in u$
405	404	stoic1a	$⊢ (((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (B) \in u) \to \neg y \in (B, +∞)$
406	405	adantr	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (B) \in u) \land \neg y \in (−∞, A)) \to \neg y \in (B, +∞)$
407		ioran	$⊢ \neg (y \in (−∞, A) \lor y \in (B, +∞)) \leftrightarrow (\neg y \in (−∞, A) \land \neg y \in (B, +∞))$
408	374 406 407	sylanbrc	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (B) \in u) \land \neg y \in (−∞, A)) \to \neg (y \in (−∞, A) \lor y \in (B, +∞))$
409		elun	$⊢ y \in ((−∞, A) \cup (B, +∞)) \leftrightarrow (y \in (−∞, A) \lor y \in (B, +∞))$
410	408 409	sylnibr	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (B) \in u) \land \neg y \in (−∞, A)) \to \neg y \in ((−∞, A) \cup (B, +∞))$
411	373 410	eldifd	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (B) \in u) \land \neg y \in (−∞, A)) \to y \in (ℝ ∖ ((−∞, A) \cup (B, +∞)))$
412	372 411	sseldd	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (B) \in u) \land \neg y \in (−∞, A)) \to y \in [A, B]$
413	412	adantllr	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (B) \in u) \land \neg y \in (−∞, A)) \to y \in [A, B]$
414		simp-4l	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land y \in [A, B]) \to φ$
415		simpllr	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land y \in [A, B]) \to G (y) \in u$
416		simpr	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land y \in [A, B]) \to y \in [A, B]$
417		simpr	$⊢ ((φ \land G (y) \in u) \land y \in [A, B]) \to y \in [A, B]$
418	139	adantlr	$⊢ ((φ \land G (y) \in u) \land y \in [A, B]) \to F (y) = G (y)$
419		simplr	$⊢ ((φ \land G (y) \in u) \land y \in [A, B]) \to G (y) \in u$
420	418 419	eqeltrd	$⊢ ((φ \land G (y) \in u) \land y \in [A, B]) \to F (y) \in u$
421	20	ad2antrr	$⊢ ((φ \land G (y) \in u) \land y \in [A, B]) \to F Fn [A, B]$
422	421 144	syl	$⊢ ((φ \land G (y) \in u) \land y \in [A, B]) \to (y \in F^{-1} [u] \leftrightarrow (y \in [A, B] \land F (y) \in u))$
423	417 420 422	mpbir2and	$⊢ ((φ \land G (y) \in u) \land y \in [A, B]) \to y \in F^{-1} [u]$
424	414 415 416 423	syl21anc	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land y \in [A, B]) \to y \in F^{-1} [u]$
425		simplr	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land y \in [A, B]) \to F^{-1} [u] = w \cap [A, B]$
426	424 425	eleqtrd	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land y \in [A, B]) \to y \in (w \cap [A, B])$
427		elinel1	$⊢ y \in (w \cap [A, B]) \to y \in w$
428	426 427	syl	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land y \in [A, B]) \to y \in w$
429	365 413 428	syl2anc	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (B) \in u) \land \neg y \in (−∞, A)) \to y \in w$
430		simp-4l	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (B) \in u) \land \neg y \in (−∞, A)) \to (φ \land y \in ℝ)$
431		simp-4r	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (B) \in u) \land \neg y \in (−∞, A)) \to G (y) \in u$
432		simplr	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (B) \in u) \land \neg y \in (−∞, A)) \to \neg F (B) \in u$
433		simpl	$⊢ (φ \land y = B) \to φ$
434		simpr	$⊢ (φ \land y = B) \to y = B$
435	37	adantr	$⊢ (φ \land y = B) \to B \in [A, B]$
436	434 435	eqeltrd	$⊢ (φ \land y = B) \to y \in [A, B]$
437	433 436 138	syl2anc	$⊢ (φ \land y = B) \to G (y) = F (y)$
438	434	fveq2d	$⊢ (φ \land y = B) \to F (y) = F (B)$
439	437 438	eqtrd	$⊢ (φ \land y = B) \to G (y) = F (B)$
440	439	ad4ant14	$⊢ (((φ \land y \in ℝ) \land \neg y \in (−∞, B)) \land y = B) \to G (y) = F (B)$
441		simplll	$⊢ (((φ \land y \in ℝ) \land \neg y \in (−∞, B)) \land \neg y = B) \to φ$
442	27	adantr	$⊢ (φ \land y \in ℝ) \to B \in ℝ^{*}$
443		pnfxr	$⊢ +∞ \in ℝ^{*}$
444	443	a1i	$⊢ (φ \land y \in ℝ) \to +∞ \in ℝ^{*}$
445		rexr	$⊢ y \in ℝ \to y \in ℝ^{*}$
446	445	adantl	$⊢ (φ \land y \in ℝ) \to y \in ℝ^{*}$
447	442 444 446	3jca	$⊢ (φ \land y \in ℝ) \to (B \in ℝ^{} \land +∞ \in ℝ^{} \land y \in ℝ^{*})$
448	447	ad2antrr	$⊢ (((φ \land y \in ℝ) \land \neg y \in (−∞, B)) \land \neg y = B) \to (B \in ℝ^{} \land +∞ \in ℝ^{} \land y \in ℝ^{*})$
449		mnflt	$⊢ y \in ℝ \to −∞ < y$
450	449	ad2antlr	$⊢ ((φ \land y \in ℝ) \land \neg y \in (−∞, B)) \to −∞ < y$
451		mnfxr	$⊢ −∞ \in ℝ^{*}$
452	451	a1i	$⊢ (φ \land y \in ℝ) \to −∞ \in ℝ^{*}$
453	452 442 446	3jca	$⊢ (φ \land y \in ℝ) \to (−∞ \in ℝ^{} \land B \in ℝ^{} \land y \in ℝ^{*})$
454		elioo3g	$⊢ y \in (−∞, B) \leftrightarrow ((−∞ \in ℝ^{} \land B \in ℝ^{} \land y \in ℝ^{*}) \land (−∞ < y \land y < B))$
455	454	notbii	$⊢ \neg y \in (−∞, B) \leftrightarrow \neg ((−∞ \in ℝ^{} \land B \in ℝ^{} \land y \in ℝ^{*}) \land (−∞ < y \land y < B))$
456	455	biimpi	$⊢ \neg y \in (−∞, B) \to \neg ((−∞ \in ℝ^{} \land B \in ℝ^{} \land y \in ℝ^{*}) \land (−∞ < y \land y < B))$
457	456	adantl	$⊢ ((φ \land y \in ℝ) \land \neg y \in (−∞, B)) \to \neg ((−∞ \in ℝ^{} \land B \in ℝ^{} \land y \in ℝ^{*}) \land (−∞ < y \land y < B))$
458		nan	$⊢ (((φ \land y \in ℝ) \land \neg y \in (−∞, B)) \to \neg ((−∞ \in ℝ^{} \land B \in ℝ^{} \land y \in ℝ^{}) \land (−∞ < y \land y < B))) \leftrightarrow ((((φ \land y \in ℝ) \land \neg y \in (−∞, B)) \land (−∞ \in ℝ^{} \land B \in ℝ^{} \land y \in ℝ^{})) \to \neg (−∞ < y \land y < B))$
459	457 458	mpbi	$⊢ (((φ \land y \in ℝ) \land \neg y \in (−∞, B)) \land (−∞ \in ℝ^{} \land B \in ℝ^{} \land y \in ℝ^{*})) \to \neg (−∞ < y \land y < B)$
460	453 459	mpidan	$⊢ ((φ \land y \in ℝ) \land \neg y \in (−∞, B)) \to \neg (−∞ < y \land y < B)$
461		nan	$⊢ (((φ \land y \in ℝ) \land \neg y \in (−∞, B)) \to \neg (−∞ < y \land y < B)) \leftrightarrow ((((φ \land y \in ℝ) \land \neg y \in (−∞, B)) \land −∞ < y) \to \neg y < B)$
462	460 461	mpbi	$⊢ (((φ \land y \in ℝ) \land \neg y \in (−∞, B)) \land −∞ < y) \to \neg y < B$
463	450 462	mpdan	$⊢ ((φ \land y \in ℝ) \land \neg y \in (−∞, B)) \to \neg y < B$
464	463	anim1i	$⊢ (((φ \land y \in ℝ) \land \neg y \in (−∞, B)) \land \neg y = B) \to (\neg y < B \land \neg y = B)$
465		pm4.56	$⊢ (\neg y < B \land \neg y = B) \leftrightarrow \neg (y < B \lor y = B)$
466	464 465	sylib	$⊢ (((φ \land y \in ℝ) \land \neg y \in (−∞, B)) \land \neg y = B) \to \neg (y < B \lor y = B)$
467		simpr	$⊢ (φ \land y \in ℝ) \to y \in ℝ$
468	6	adantr	$⊢ (φ \land y \in ℝ) \to B \in ℝ$
469	467 468	jca	$⊢ (φ \land y \in ℝ) \to (y \in ℝ \land B \in ℝ)$
470	469	ad2antrr	$⊢ (((φ \land y \in ℝ) \land \neg y \in (−∞, B)) \land \neg y = B) \to (y \in ℝ \land B \in ℝ)$
471		leloe	$⊢ (y \in ℝ \land B \in ℝ) \to (y \leq B \leftrightarrow (y < B \lor y = B))$
472	470 471	syl	$⊢ (((φ \land y \in ℝ) \land \neg y \in (−∞, B)) \land \neg y = B) \to (y \leq B \leftrightarrow (y < B \lor y = B))$
473	466 472	mtbird	$⊢ (((φ \land y \in ℝ) \land \neg y \in (−∞, B)) \land \neg y = B) \to \neg y \leq B$
474	6	anim1i	$⊢ (φ \land y \in ℝ) \to (B \in ℝ \land y \in ℝ)$
475	474	ad2antrr	$⊢ (((φ \land y \in ℝ) \land \neg y \in (−∞, B)) \land \neg y = B) \to (B \in ℝ \land y \in ℝ)$
476		ltnle	$⊢ (B \in ℝ \land y \in ℝ) \to (B < y \leftrightarrow \neg y \leq B)$
477	475 476	syl	$⊢ (((φ \land y \in ℝ) \land \neg y \in (−∞, B)) \land \neg y = B) \to (B < y \leftrightarrow \neg y \leq B)$
478	473 477	mpbird	$⊢ (((φ \land y \in ℝ) \land \neg y \in (−∞, B)) \land \neg y = B) \to B < y$
479		simpllr	$⊢ (((φ \land y \in ℝ) \land \neg y \in (−∞, B)) \land \neg y = B) \to y \in ℝ$
480	479	ltpnfd	$⊢ (((φ \land y \in ℝ) \land \neg y \in (−∞, B)) \land \neg y = B) \to y < +∞$
481	478 480	jca	$⊢ (((φ \land y \in ℝ) \land \neg y \in (−∞, B)) \land \neg y = B) \to (B < y \land y < +∞)$
482	448 481 377	sylanbrc	$⊢ (((φ \land y \in ℝ) \land \neg y \in (−∞, B)) \land \neg y = B) \to y \in (B, +∞)$
483	441 482 399	syl2anc	$⊢ (((φ \land y \in ℝ) \land \neg y \in (−∞, B)) \land \neg y = B) \to G (y) = F (B)$
484	440 483	pm2.61dan	$⊢ ((φ \land y \in ℝ) \land \neg y \in (−∞, B)) \to G (y) = F (B)$
485	484	eqcomd	$⊢ ((φ \land y \in ℝ) \land \neg y \in (−∞, B)) \to F (B) = G (y)$
486	485	adantlr	$⊢ (((φ \land y \in ℝ) \land G (y) \in u) \land \neg y \in (−∞, B)) \to F (B) = G (y)$
487		simplr	$⊢ (((φ \land y \in ℝ) \land G (y) \in u) \land \neg y \in (−∞, B)) \to G (y) \in u$
488	486 487	eqeltrd	$⊢ (((φ \land y \in ℝ) \land G (y) \in u) \land \neg y \in (−∞, B)) \to F (B) \in u$
489	488	stoic1a	$⊢ (((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (B) \in u) \to \neg \neg y \in (−∞, B)$
490	489	notnotrd	$⊢ (((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (B) \in u) \to y \in (−∞, B)$
491	430 431 432 490	syl21anc	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (B) \in u) \land \neg y \in (−∞, A)) \to y \in (−∞, B)$
492	429 491	elind	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (B) \in u) \land \neg y \in (−∞, A)) \to y \in (w \cap (−∞, B))$
493	492	ex	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (B) \in u) \to (\neg y \in (−∞, A) \to y \in (w \cap (−∞, B)))$
494	493	orrd	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (B) \in u) \to (y \in (−∞, A) \lor y \in (w \cap (−∞, B)))$
495	494	orcomd	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (B) \in u) \to (y \in (w \cap (−∞, B)) \lor y \in (−∞, A))$
496		elun	$⊢ y \in ((w \cap (−∞, B)) \cup (−∞, A)) \leftrightarrow (y \in (w \cap (−∞, B)) \lor y \in (−∞, A))$
497	495 496	sylibr	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (B) \in u) \to y \in ((w \cap (−∞, B)) \cup (−∞, A))$
498	362 363 364 497	syl21anc	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land \neg F (B) \in u) \to y \in ((w \cap (−∞, B)) \cup (−∞, A))$
499	105	simpld	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \to φ$
500	499	adantr	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land \neg F (B) \in u) \to φ$
501		simpll2	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land \neg F (B) \in u) \to w \in J$
502	11 501 161	sylancr	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land \neg F (B) \in u) \to w \subseteq ℝ$
503	500 502	jca	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land \neg F (B) \in u) \to (φ \land w \subseteq ℝ)$
504		simplr	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land \neg F (B) \in u) \to F (A) \in u$
505	66	ffnd	$⊢ φ \to G Fn ℝ$
506	505	ad3antrrr	$⊢ (((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \to G Fn ℝ$
507		ssinss1	$⊢ w \subseteq ℝ \to w \cap (−∞, B) \subseteq ℝ$
508	507	ad3antlr	$⊢ (((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \to w \cap (−∞, B) \subseteq ℝ$
509		ioossre	$⊢ (−∞, A) \subseteq ℝ$
510	509	a1i	$⊢ (((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \to (−∞, A) \subseteq ℝ$
511		unima	$⊢ (G Fn ℝ \land w \cap (−∞, B) \subseteq ℝ \land (−∞, A) \subseteq ℝ) \to G [(w \cap (−∞, B)) \cup (−∞, A)] = G [w \cap (−∞, B)] \cup G [(−∞, A)]$
512	506 508 510 511	syl3anc	$⊢ (((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \to G [(w \cap (−∞, B)) \cup (−∞, A)] = G [w \cap (−∞, B)] \cup G [(−∞, A)]$
513	166	a1i	$⊢ ((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land y \in G [w \cap (−∞, B)]) \to Fun G$
514		fvelima	$⊢ (Fun G \land y \in G [w \cap (−∞, B)]) \to \exists z \in (w \cap (−∞, B)) G (z) = y$
515	513 514	sylancom	$⊢ ((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land y \in G [w \cap (−∞, B)]) \to \exists z \in (w \cap (−∞, B)) G (z) = y$
516	172	3ad2ant3	$⊢ ((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land z \in (w \cap (−∞, B)) \land G (z) = y) \to y = G (z)$
517		simp-5l	$⊢ (((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land z \in (w \cap (−∞, B))) \land z \in (−∞, A)) \to φ$
518		simpllr	$⊢ (((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land z \in (w \cap (−∞, B))) \land z \in (−∞, A)) \to F (A) \in u$
519		simpr	$⊢ (((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land z \in (w \cap (−∞, B))) \land z \in (−∞, A)) \to z \in (−∞, A)$
520	274 268 270	3eqtrd	$⊢ (φ \land z \in (−∞, A)) \to G (z) = F (A)$
521	520	3adant2	$⊢ (φ \land F (A) \in u \land z \in (−∞, A)) \to G (z) = F (A)$
522		simp2	$⊢ (φ \land F (A) \in u \land z \in (−∞, A)) \to F (A) \in u$
523	521 522	eqeltrd	$⊢ (φ \land F (A) \in u \land z \in (−∞, A)) \to G (z) \in u$
524	517 518 519 523	syl3anc	$⊢ (((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land z \in (w \cap (−∞, B))) \land z \in (−∞, A)) \to G (z) \in u$
525		simplll	$⊢ (((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land z \in (w \cap (−∞, B))) \land \neg z \in (−∞, A)) \to ((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B])$
526		simp-5l	$⊢ (((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land z \in (w \cap (−∞, B))) \land \neg z \in (−∞, A)) \to φ$
527		simplr	$⊢ (((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land z \in (w \cap (−∞, B))) \land \neg z \in (−∞, A)) \to z \in (w \cap (−∞, B))$
528		simpr	$⊢ (((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land z \in (w \cap (−∞, B))) \land \neg z \in (−∞, A)) \to \neg z \in (−∞, A)$
529		elinel1	$⊢ z \in (w \cap (−∞, B)) \to z \in w$
530	529	3ad2ant2	$⊢ (φ \land z \in (w \cap (−∞, B)) \land \neg z \in (−∞, A)) \to z \in w$
531		elinel2	$⊢ z \in (w \cap (−∞, B)) \to z \in (−∞, B)$
532		elioore	$⊢ z \in (−∞, B) \to z \in ℝ$
533	531 532	syl	$⊢ z \in (w \cap (−∞, B)) \to z \in ℝ$
534	533	3ad2ant2	$⊢ (φ \land z \in (w \cap (−∞, B)) \land \neg z \in (−∞, A)) \to z \in ℝ$
535	26	3ad2ant1	$⊢ (φ \land z \in (w \cap (−∞, B)) \land \neg z \in (−∞, A)) \to A \in ℝ^{*}$
536	534	rexrd	$⊢ (φ \land z \in (w \cap (−∞, B)) \land \neg z \in (−∞, A)) \to z \in ℝ^{*}$
537		mnflt	$⊢ z \in ℝ \to −∞ < z$
538	534 537	syl	$⊢ (φ \land z \in (w \cap (−∞, B)) \land \neg z \in (−∞, A)) \to −∞ < z$
539	451	a1i	$⊢ (φ \land z \in (w \cap (−∞, B)) \land \neg z \in (−∞, A)) \to −∞ \in ℝ^{*}$
540	539 535 536	3jca	$⊢ (φ \land z \in (w \cap (−∞, B)) \land \neg z \in (−∞, A)) \to (−∞ \in ℝ^{} \land A \in ℝ^{} \land z \in ℝ^{*})$
541		simp3	$⊢ (φ \land z \in (w \cap (−∞, B)) \land \neg z \in (−∞, A)) \to \neg z \in (−∞, A)$
542	541 255	sylnib	$⊢ (φ \land z \in (w \cap (−∞, B)) \land \neg z \in (−∞, A)) \to \neg ((−∞ \in ℝ^{} \land A \in ℝ^{} \land z \in ℝ^{*}) \land (−∞ < z \land z < A))$
543		nan	$⊢ ((φ \land z \in (w \cap (−∞, B)) \land \neg z \in (−∞, A)) \to \neg ((−∞ \in ℝ^{} \land A \in ℝ^{} \land z \in ℝ^{}) \land (−∞ < z \land z < A))) \leftrightarrow (((φ \land z \in (w \cap (−∞, B)) \land \neg z \in (−∞, A)) \land (−∞ \in ℝ^{} \land A \in ℝ^{} \land z \in ℝ^{})) \to \neg (−∞ < z \land z < A))$
544	542 543	mpbi	$⊢ ((φ \land z \in (w \cap (−∞, B)) \land \neg z \in (−∞, A)) \land (−∞ \in ℝ^{} \land A \in ℝ^{} \land z \in ℝ^{*})) \to \neg (−∞ < z \land z < A)$
545	540 544	mpdan	$⊢ (φ \land z \in (w \cap (−∞, B)) \land \neg z \in (−∞, A)) \to \neg (−∞ < z \land z < A)$
546		nan	$⊢ ((φ \land z \in (w \cap (−∞, B)) \land \neg z \in (−∞, A)) \to \neg (−∞ < z \land z < A)) \leftrightarrow (((φ \land z \in (w \cap (−∞, B)) \land \neg z \in (−∞, A)) \land −∞ < z) \to \neg z < A)$
547	545 546	mpbi	$⊢ ((φ \land z \in (w \cap (−∞, B)) \land \neg z \in (−∞, A)) \land −∞ < z) \to \neg z < A$
548	538 547	mpdan	$⊢ (φ \land z \in (w \cap (−∞, B)) \land \neg z \in (−∞, A)) \to \neg z < A$
549	535 536 548	xrnltled	$⊢ (φ \land z \in (w \cap (−∞, B)) \land \neg z \in (−∞, A)) \to A \leq z$
550		simp1	$⊢ (φ \land z \in (w \cap (−∞, B)) \land \neg z \in (−∞, A)) \to φ$
551	531	3ad2ant2	$⊢ (φ \land z \in (w \cap (−∞, B)) \land \neg z \in (−∞, A)) \to z \in (−∞, B)$
552	532	adantl	$⊢ (φ \land z \in (−∞, B)) \to z \in ℝ$
553	6	adantr	$⊢ (φ \land z \in (−∞, B)) \to B \in ℝ$
554		elioo3g	$⊢ z \in (−∞, B) \leftrightarrow ((−∞ \in ℝ^{} \land B \in ℝ^{} \land z \in ℝ^{*}) \land (−∞ < z \land z < B))$
555	554	biimpi	$⊢ z \in (−∞, B) \to ((−∞ \in ℝ^{} \land B \in ℝ^{} \land z \in ℝ^{*}) \land (−∞ < z \land z < B))$
556	555	simprrd	$⊢ z \in (−∞, B) \to z < B$
557	556	adantl	$⊢ (φ \land z \in (−∞, B)) \to z < B$
558	552 553 557	ltled	$⊢ (φ \land z \in (−∞, B)) \to z \leq B$
559	550 551 558	syl2anc	$⊢ (φ \land z \in (w \cap (−∞, B)) \land \neg z \in (−∞, A)) \to z \leq B$
560	263	3ad2ant1	$⊢ (φ \land z \in (w \cap (−∞, B)) \land \neg z \in (−∞, A)) \to (A \in ℝ \land B \in ℝ)$
561	560 265	syl	$⊢ (φ \land z \in (w \cap (−∞, B)) \land \neg z \in (−∞, A)) \to (z \in [A, B] \leftrightarrow (z \in ℝ \land A \leq z \land z \leq B))$
562	534 549 559 561	mpbir3and	$⊢ (φ \land z \in (w \cap (−∞, B)) \land \neg z \in (−∞, A)) \to z \in [A, B]$
563	530 562	elind	$⊢ (φ \land z \in (w \cap (−∞, B)) \land \neg z \in (−∞, A)) \to z \in (w \cap [A, B])$
564	526 527 528 563	syl3anc	$⊢ (((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land z \in (w \cap (−∞, B))) \land \neg z \in (−∞, A)) \to z \in (w \cap [A, B])$
565		elinel2	$⊢ z \in (w \cap [A, B]) \to z \in [A, B]$
566	565	anim2i	$⊢ (φ \land z \in (w \cap [A, B])) \to (φ \land z \in [A, B])$
567	566	adantlr	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land z \in (w \cap [A, B])) \to (φ \land z \in [A, B])$
568	567 187	syl	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land z \in (w \cap [A, B])) \to G (z) = F (z)$
569	20	ad2antrr	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land z \in (w \cap [A, B])) \to F Fn [A, B]$
570		simpr	$⊢ (F^{-1} [u] = w \cap [A, B] \land z \in (w \cap [A, B])) \to z \in (w \cap [A, B])$
571	196	adantr	$⊢ (F^{-1} [u] = w \cap [A, B] \land z \in (w \cap [A, B])) \to w \cap [A, B] = F^{-1} [u]$
572	570 571	eleqtrd	$⊢ (F^{-1} [u] = w \cap [A, B] \land z \in (w \cap [A, B])) \to z \in F^{-1} [u]$
573	572	adantll	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land z \in (w \cap [A, B])) \to z \in F^{-1} [u]$
574	202	simplbda	$⊢ (F Fn [A, B] \land z \in F^{-1} [u]) \to F (z) \in u$
575	569 573 574	syl2anc	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land z \in (w \cap [A, B])) \to F (z) \in u$
576	568 575	eqeltrd	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land z \in (w \cap [A, B])) \to G (z) \in u$
577	576	adantllr	$⊢ (((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land z \in (w \cap [A, B])) \to G (z) \in u$
578	525 564 577	syl2anc	$⊢ (((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land z \in (w \cap (−∞, B))) \land \neg z \in (−∞, A)) \to G (z) \in u$
579	524 578	pm2.61dan	$⊢ ((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land z \in (w \cap (−∞, B))) \to G (z) \in u$
580	579	3adant3	$⊢ ((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land z \in (w \cap (−∞, B)) \land G (z) = y) \to G (z) \in u$
581	516 580	eqeltrd	$⊢ ((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land z \in (w \cap (−∞, B)) \land G (z) = y) \to y \in u$
582	581	3adant1r	$⊢ (((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land y \in G [w \cap (−∞, B)]) \land z \in (w \cap (−∞, B)) \land G (z) = y) \to y \in u$
583	582	rexlimdv3a	$⊢ ((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land y \in G [w \cap (−∞, B)]) \to (\exists z \in (w \cap (−∞, B)) G (z) = y \to y \in u)$
584	515 583	mpd	$⊢ ((((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land y \in G [w \cap (−∞, B)]) \to y \in u$
585	584	ex	$⊢ (((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \to (y \in G [w \cap (−∞, B)] \to y \in u)$
586	585	ssrdv	$⊢ (((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \to G [w \cap (−∞, B)] \subseteq u$
587	289	ad4ant14	$⊢ (((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \to G [(−∞, A)] \subseteq u$
588	586 587	unssd	$⊢ (((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \to G [w \cap (−∞, B)] \cup G [(−∞, A)] \subseteq u$
589	512 588	eqsstrd	$⊢ (((φ \land w \subseteq ℝ) \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \to G [(w \cap (−∞, B)) \cup (−∞, A)] \subseteq u$
590	503 363 504 589	syl21anc	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land \neg F (B) \in u) \to G [(w \cap (−∞, B)) \cup (−∞, A)] \subseteq u$
591		eleq2	$⊢ v = (w \cap (−∞, B)) \cup (−∞, A) \to (y \in v \leftrightarrow y \in ((w \cap (−∞, B)) \cup (−∞, A)))$
592		imaeq2	$⊢ v = (w \cap (−∞, B)) \cup (−∞, A) \to G [v] = G [(w \cap (−∞, B)) \cup (−∞, A)]$
593	592	sseq1d	$⊢ v = (w \cap (−∞, B)) \cup (−∞, A) \to (G [v] \subseteq u \leftrightarrow G [(w \cap (−∞, B)) \cup (−∞, A)] \subseteq u)$
594	591 593	anbi12d	$⊢ v = (w \cap (−∞, B)) \cup (−∞, A) \to ((y \in v \land G [v] \subseteq u) \leftrightarrow (y \in ((w \cap (−∞, B)) \cup (−∞, A)) \land G [(w \cap (−∞, B)) \cup (−∞, A)] \subseteq u))$
595	594	rspcev	$⊢ ((w \cap (−∞, B)) \cup (−∞, A) \in J \land (y \in ((w \cap (−∞, B)) \cup (−∞, A)) \land G [(w \cap (−∞, B)) \cup (−∞, A)] \subseteq u)) \to \exists v \in J (y \in v \land G [v] \subseteq u)$
596	361 498 590 595	syl12anc	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \land \neg F (B) \in u) \to \exists v \in J (y \in v \land G [v] \subseteq u)$
597	351 596	pm2.61dan	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land F (A) \in u) \to \exists v \in J (y \in v \land G [v] \subseteq u)$
598		simpll2	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land F (B) \in u) \to w \in J$
599		iooretop	$⊢ (A, +∞) \in topGen (ran (.))$
600	599 2	eleqtrri	$⊢ (A, +∞) \in J$
601		inopn	$⊢ (J \in Top \land w \in J \land (A, +∞) \in J) \to w \cap (A, +∞) \in J$
602	80 600 601	mp3an13	$⊢ w \in J \to w \cap (A, +∞) \in J$
603	99	a1i	$⊢ w \in J \to (B, +∞) \in J$
604		unopn	$⊢ (J \in Top \land w \cap (A, +∞) \in J \land (B, +∞) \in J) \to (w \cap (A, +∞)) \cup (B, +∞) \in J$
605	352 602 603 604	syl3anc	$⊢ w \in J \to (w \cap (A, +∞)) \cup (B, +∞) \in J$
606	598 605	syl	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land F (B) \in u) \to (w \cap (A, +∞)) \cup (B, +∞) \in J$
607		simplll	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg y \in (B, +∞)) \to ((φ \land y \in ℝ) \land G (y) \in u)$
608	607	simpld	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg y \in (B, +∞)) \to (φ \land y \in ℝ)$
609	608	simpld	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg y \in (B, +∞)) \to φ$
610		simp-4r	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg y \in (B, +∞)) \to G (y) \in u$
611		simp-5r	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg y \in (B, +∞)) \to y \in ℝ$
612		simplr	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg y \in (B, +∞)) \to \neg F (A) \in u$
613		simpll	$⊢ ((φ \land y \in ℝ) \land y < A) \to φ$
614	26	adantr	$⊢ (φ \land y \in ℝ) \to A \in ℝ^{*}$
615	452 614 446	3jca	$⊢ (φ \land y \in ℝ) \to (−∞ \in ℝ^{} \land A \in ℝ^{} \land y \in ℝ^{*})$
616	615	adantr	$⊢ ((φ \land y \in ℝ) \land y < A) \to (−∞ \in ℝ^{} \land A \in ℝ^{} \land y \in ℝ^{*})$
617	449	anim1i	$⊢ (y \in ℝ \land y < A) \to (−∞ < y \land y < A)$
618	617	adantll	$⊢ ((φ \land y \in ℝ) \land y < A) \to (−∞ < y \land y < A)$
619		elioo3g	$⊢ y \in (−∞, A) \leftrightarrow ((−∞ \in ℝ^{} \land A \in ℝ^{} \land y \in ℝ^{*}) \land (−∞ < y \land y < A))$
620	616 618 619	sylanbrc	$⊢ ((φ \land y \in ℝ) \land y < A) \to y \in (−∞, A)$
621		eleq1	$⊢ z = y \to (z \in (−∞, A) \leftrightarrow y \in (−∞, A))$
622	621	anbi2d	$⊢ z = y \to ((φ \land z \in (−∞, A)) \leftrightarrow (φ \land y \in (−∞, A)))$
623		fveq2	$⊢ z = y \to G (z) = G (y)$
624	623	eqeq1d	$⊢ z = y \to (G (z) = F (A) \leftrightarrow G (y) = F (A))$
625	622 624	imbi12d	$⊢ z = y \to (((φ \land z \in (−∞, A)) \to G (z) = F (A)) \leftrightarrow ((φ \land y \in (−∞, A)) \to G (y) = F (A)))$
626	625 520	chvarvv	$⊢ (φ \land y \in (−∞, A)) \to G (y) = F (A)$
627	613 620 626	syl2anc	$⊢ ((φ \land y \in ℝ) \land y < A) \to G (y) = F (A)$
628	627	eqcomd	$⊢ ((φ \land y \in ℝ) \land y < A) \to F (A) = G (y)$
629	628	ad4ant14	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (A) \in u) \land y < A) \to F (A) = G (y)$
630		simpllr	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (A) \in u) \land y < A) \to G (y) \in u$
631	629 630	eqeltrd	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (A) \in u) \land y < A) \to F (A) \in u$
632		simplr	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (A) \in u) \land y < A) \to \neg F (A) \in u$
633	631 632	pm2.65da	$⊢ (((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (A) \in u) \to \neg y < A$
634	5	anim1i	$⊢ (φ \land y \in ℝ) \to (A \in ℝ \land y \in ℝ)$
635	634	ad2antrr	$⊢ (((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (A) \in u) \to (A \in ℝ \land y \in ℝ)$
636		lenlt	$⊢ (A \in ℝ \land y \in ℝ) \to (A \leq y \leftrightarrow \neg y < A)$
637	635 636	syl	$⊢ (((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (A) \in u) \to (A \leq y \leftrightarrow \neg y < A)$
638	633 637	mpbird	$⊢ (((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (A) \in u) \to A \leq y$
639	607 612 638	syl2anc	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg y \in (B, +∞)) \to A \leq y$
640		ltpnf	$⊢ y \in ℝ \to y < +∞$
641	640	ad2antlr	$⊢ ((φ \land y \in ℝ) \land \neg y \in (B, +∞)) \to y < +∞$
642	447	adantr	$⊢ ((φ \land y \in ℝ) \land \neg y \in (B, +∞)) \to (B \in ℝ^{} \land +∞ \in ℝ^{} \land y \in ℝ^{*})$
643	377	notbii	$⊢ \neg y \in (B, +∞) \leftrightarrow \neg ((B \in ℝ^{} \land +∞ \in ℝ^{} \land y \in ℝ^{*}) \land (B < y \land y < +∞))$
644	643	biimpi	$⊢ \neg y \in (B, +∞) \to \neg ((B \in ℝ^{} \land +∞ \in ℝ^{} \land y \in ℝ^{*}) \land (B < y \land y < +∞))$
645	644	adantl	$⊢ ((φ \land y \in ℝ) \land \neg y \in (B, +∞)) \to \neg ((B \in ℝ^{} \land +∞ \in ℝ^{} \land y \in ℝ^{*}) \land (B < y \land y < +∞))$
646		imnan	$⊢ ((B \in ℝ^{} \land +∞ \in ℝ^{} \land y \in ℝ^{}) \to \neg (B < y \land y < +∞)) \leftrightarrow \neg ((B \in ℝ^{} \land +∞ \in ℝ^{} \land y \in ℝ^{}) \land (B < y \land y < +∞))$
647	645 646	sylibr	$⊢ ((φ \land y \in ℝ) \land \neg y \in (B, +∞)) \to ((B \in ℝ^{} \land +∞ \in ℝ^{} \land y \in ℝ^{*}) \to \neg (B < y \land y < +∞))$
648	642 647	mpd	$⊢ ((φ \land y \in ℝ) \land \neg y \in (B, +∞)) \to \neg (B < y \land y < +∞)$
649		ancom	$⊢ (B < y \land y < +∞) \leftrightarrow (y < +∞ \land B < y)$
650	648 649	sylnib	$⊢ ((φ \land y \in ℝ) \land \neg y \in (B, +∞)) \to \neg (y < +∞ \land B < y)$
651		imnan	$⊢ (y < +∞ \to \neg B < y) \leftrightarrow \neg (y < +∞ \land B < y)$
652	650 651	sylibr	$⊢ ((φ \land y \in ℝ) \land \neg y \in (B, +∞)) \to (y < +∞ \to \neg B < y)$
653	641 652	mpd	$⊢ ((φ \land y \in ℝ) \land \neg y \in (B, +∞)) \to \neg B < y$
654	469	adantr	$⊢ ((φ \land y \in ℝ) \land \neg y \in (B, +∞)) \to (y \in ℝ \land B \in ℝ)$
655		lenlt	$⊢ (y \in ℝ \land B \in ℝ) \to (y \leq B \leftrightarrow \neg B < y)$
656	654 655	syl	$⊢ ((φ \land y \in ℝ) \land \neg y \in (B, +∞)) \to (y \leq B \leftrightarrow \neg B < y)$
657	653 656	mpbird	$⊢ ((φ \land y \in ℝ) \land \neg y \in (B, +∞)) \to y \leq B$
658	608 657	sylancom	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg y \in (B, +∞)) \to y \leq B$
659	263	ad5antr	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg y \in (B, +∞)) \to (A \in ℝ \land B \in ℝ)$
660	659 386	syl	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg y \in (B, +∞)) \to (y \in [A, B] \leftrightarrow (y \in ℝ \land A \leq y \land y \leq B))$
661	611 639 658 660	mpbir3and	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg y \in (B, +∞)) \to y \in [A, B]$
662	609 610 661 423	syl21anc	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg y \in (B, +∞)) \to y \in F^{-1} [u]$
663		simpllr	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg y \in (B, +∞)) \to F^{-1} [u] = w \cap [A, B]$
664	662 663	eleqtrd	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg y \in (B, +∞)) \to y \in (w \cap [A, B])$
665	664 427	syl	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg y \in (B, +∞)) \to y \in w$
666		fveq2	$⊢ y = A \to G (y) = G (A)$
667	29	ancli	$⊢ φ \to (φ \land A \in [A, B])$
668		eleq1	$⊢ y = A \to (y \in [A, B] \leftrightarrow A \in [A, B])$
669	668	anbi2d	$⊢ y = A \to ((φ \land y \in [A, B]) \leftrightarrow (φ \land A \in [A, B]))$
670		fveq2	$⊢ y = A \to F (y) = F (A)$
671	666 670	eqeq12d	$⊢ y = A \to (G (y) = F (y) \leftrightarrow G (A) = F (A))$
672	669 671	imbi12d	$⊢ y = A \to (((φ \land y \in [A, B]) \to G (y) = F (y)) \leftrightarrow ((φ \land A \in [A, B]) \to G (A) = F (A)))$
673	672 138	vtoclg	$⊢ A \in ℝ \to ((φ \land A \in [A, B]) \to G (A) = F (A))$
674	5 667 673	sylc	$⊢ φ \to G (A) = F (A)$
675	666 674	sylan9eqr	$⊢ (φ \land y = A) \to G (y) = F (A)$
676	675	ad4ant14	$⊢ (((φ \land y \in ℝ) \land \neg y \in (A, +∞)) \land y = A) \to G (y) = F (A)$
677		simplll	$⊢ (((φ \land y \in ℝ) \land \neg y \in (A, +∞)) \land \neg y = A) \to φ$
678	615	ad2antrr	$⊢ (((φ \land y \in ℝ) \land \neg y \in (A, +∞)) \land \neg y = A) \to (−∞ \in ℝ^{} \land A \in ℝ^{} \land y \in ℝ^{*})$
679	449	ad3antlr	$⊢ (((φ \land y \in ℝ) \land \neg y \in (A, +∞)) \land \neg y = A) \to −∞ < y$
680		simpllr	$⊢ (((φ \land y \in ℝ) \land \neg y \in (A, +∞)) \land \neg y = A) \to y \in ℝ$
681	677 5	syl	$⊢ (((φ \land y \in ℝ) \land \neg y \in (A, +∞)) \land \neg y = A) \to A \in ℝ$
682	446	adantr	$⊢ ((φ \land y \in ℝ) \land \neg y \in (A, +∞)) \to y \in ℝ^{*}$
683	26	ad2antrr	$⊢ ((φ \land y \in ℝ) \land \neg y \in (A, +∞)) \to A \in ℝ^{*}$
684	640	ad2antlr	$⊢ ((φ \land y \in ℝ) \land \neg y \in (A, +∞)) \to y < +∞$
685		simpr	$⊢ ((φ \land y \in ℝ) \land \neg y \in (A, +∞)) \to \neg y \in (A, +∞)$
686	443	a1i	$⊢ ((φ \land y \in ℝ) \land \neg y \in (A, +∞)) \to +∞ \in ℝ^{*}$
687	683 686 682	3jca	$⊢ ((φ \land y \in ℝ) \land \neg y \in (A, +∞)) \to (A \in ℝ^{} \land +∞ \in ℝ^{} \land y \in ℝ^{*})$
688		elioo3g	$⊢ y \in (A, +∞) \leftrightarrow ((A \in ℝ^{} \land +∞ \in ℝ^{} \land y \in ℝ^{*}) \land (A < y \land y < +∞))$
689	688	notbii	$⊢ \neg y \in (A, +∞) \leftrightarrow \neg ((A \in ℝ^{} \land +∞ \in ℝ^{} \land y \in ℝ^{*}) \land (A < y \land y < +∞))$
690	689	biimpi	$⊢ \neg y \in (A, +∞) \to \neg ((A \in ℝ^{} \land +∞ \in ℝ^{} \land y \in ℝ^{*}) \land (A < y \land y < +∞))$
691		nan	$⊢ (\neg y \in (A, +∞) \to \neg ((A \in ℝ^{} \land +∞ \in ℝ^{} \land y \in ℝ^{}) \land (A < y \land y < +∞))) \leftrightarrow ((\neg y \in (A, +∞) \land (A \in ℝ^{} \land +∞ \in ℝ^{} \land y \in ℝ^{})) \to \neg (A < y \land y < +∞))$
692	690 691	mpbi	$⊢ (\neg y \in (A, +∞) \land (A \in ℝ^{} \land +∞ \in ℝ^{} \land y \in ℝ^{*})) \to \neg (A < y \land y < +∞)$
693	685 687 692	syl2anc	$⊢ ((φ \land y \in ℝ) \land \neg y \in (A, +∞)) \to \neg (A < y \land y < +∞)$
694		ancom	$⊢ (A < y \land y < +∞) \leftrightarrow (y < +∞ \land A < y)$
695	693 694	sylnib	$⊢ ((φ \land y \in ℝ) \land \neg y \in (A, +∞)) \to \neg (y < +∞ \land A < y)$
696		nan	$⊢ (((φ \land y \in ℝ) \land \neg y \in (A, +∞)) \to \neg (y < +∞ \land A < y)) \leftrightarrow ((((φ \land y \in ℝ) \land \neg y \in (A, +∞)) \land y < +∞) \to \neg A < y)$
697	695 696	mpbi	$⊢ (((φ \land y \in ℝ) \land \neg y \in (A, +∞)) \land y < +∞) \to \neg A < y$
698	684 697	mpdan	$⊢ ((φ \land y \in ℝ) \land \neg y \in (A, +∞)) \to \neg A < y$
699	682 683 698	xrnltled	$⊢ ((φ \land y \in ℝ) \land \neg y \in (A, +∞)) \to y \leq A$
700	699	adantr	$⊢ (((φ \land y \in ℝ) \land \neg y \in (A, +∞)) \land \neg y = A) \to y \leq A$
701		neqne	$⊢ \neg y = A \to y \neq A$
702	701	necomd	$⊢ \neg y = A \to A \neq y$
703	702	adantl	$⊢ (((φ \land y \in ℝ) \land \neg y \in (A, +∞)) \land \neg y = A) \to A \neq y$
704	680 681 700 703	leneltd	$⊢ (((φ \land y \in ℝ) \land \neg y \in (A, +∞)) \land \neg y = A) \to y < A$
705	679 704	jca	$⊢ (((φ \land y \in ℝ) \land \neg y \in (A, +∞)) \land \neg y = A) \to (−∞ < y \land y < A)$
706	678 705 619	sylanbrc	$⊢ (((φ \land y \in ℝ) \land \neg y \in (A, +∞)) \land \neg y = A) \to y \in (−∞, A)$
707	677 706 626	syl2anc	$⊢ (((φ \land y \in ℝ) \land \neg y \in (A, +∞)) \land \neg y = A) \to G (y) = F (A)$
708	676 707	pm2.61dan	$⊢ ((φ \land y \in ℝ) \land \neg y \in (A, +∞)) \to G (y) = F (A)$
709	708	eqcomd	$⊢ ((φ \land y \in ℝ) \land \neg y \in (A, +∞)) \to F (A) = G (y)$
710	709	ad4ant14	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (A) \in u) \land \neg y \in (A, +∞)) \to F (A) = G (y)$
711		simpllr	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (A) \in u) \land \neg y \in (A, +∞)) \to G (y) \in u$
712	710 711	eqeltrd	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (A) \in u) \land \neg y \in (A, +∞)) \to F (A) \in u$
713		simplr	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (A) \in u) \land \neg y \in (A, +∞)) \to \neg F (A) \in u$
714	712 713	condan	$⊢ (((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (A) \in u) \to y \in (A, +∞)$
715	607 612 714	syl2anc	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg y \in (B, +∞)) \to y \in (A, +∞)$
716	665 715	elind	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg y \in (B, +∞)) \to y \in (w \cap (A, +∞))$
717	716	adantlr	$⊢ ((((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land F (B) \in u) \land \neg y \in (B, +∞)) \to y \in (w \cap (A, +∞))$
718		pm5.6	$⊢ (((((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land F (B) \in u) \land \neg y \in (B, +∞)) \to y \in (w \cap (A, +∞))) \leftrightarrow ((((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land F (B) \in u) \to (y \in (B, +∞) \lor y \in (w \cap (A, +∞))))$
719	717 718	mpbi	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land F (B) \in u) \to (y \in (B, +∞) \lor y \in (w \cap (A, +∞)))$
720	719	orcomd	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land F (B) \in u) \to (y \in (w \cap (A, +∞)) \lor y \in (B, +∞))$
721		elun	$⊢ y \in ((w \cap (A, +∞)) \cup (B, +∞)) \leftrightarrow (y \in (w \cap (A, +∞)) \lor y \in (B, +∞))$
722	720 721	sylibr	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land F (B) \in u) \to y \in ((w \cap (A, +∞)) \cup (B, +∞))$
723	722	3adantll2	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land F (B) \in u) \to y \in ((w \cap (A, +∞)) \cup (B, +∞))$
724		simp1ll	$⊢ (((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \to φ$
725	724	ad2antrr	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land F (B) \in u) \to φ$
726		simpll3	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land F (B) \in u) \to F^{-1} [u] = w \cap [A, B]$
727		simpr	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land F (B) \in u) \to F (B) \in u$
728	505	ad2antrr	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land F (B) \in u) \to G Fn ℝ$
729		ioossre	$⊢ (A, +∞) \subseteq ℝ$
730	729	olci	$⊢ (w \subseteq ℝ \lor (A, +∞) \subseteq ℝ)$
731		inss	$⊢ (w \subseteq ℝ \lor (A, +∞) \subseteq ℝ) \to w \cap (A, +∞) \subseteq ℝ$
732	730 731	ax-mp	$⊢ w \cap (A, +∞) \subseteq ℝ$
733	732	a1i	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land F (B) \in u) \to w \cap (A, +∞) \subseteq ℝ$
734		ioossre	$⊢ (B, +∞) \subseteq ℝ$
735	734	a1i	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land F (B) \in u) \to (B, +∞) \subseteq ℝ$
736		unima	$⊢ (G Fn ℝ \land w \cap (A, +∞) \subseteq ℝ \land (B, +∞) \subseteq ℝ) \to G [(w \cap (A, +∞)) \cup (B, +∞)] = G [w \cap (A, +∞)] \cup G [(B, +∞)]$
737	728 733 735 736	syl3anc	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land F (B) \in u) \to G [(w \cap (A, +∞)) \cup (B, +∞)] = G [w \cap (A, +∞)] \cup G [(B, +∞)]$
738		simpll	$⊢ ((φ \land y \in (w \cap (A, +∞))) \land B < y) \to φ$
739	732	sseli	$⊢ y \in (w \cap (A, +∞)) \to y \in ℝ$
740	739	ad2antlr	$⊢ ((φ \land y \in (w \cap (A, +∞))) \land B < y) \to y \in ℝ$
741	738 740 447	syl2anc	$⊢ ((φ \land y \in (w \cap (A, +∞))) \land B < y) \to (B \in ℝ^{} \land +∞ \in ℝ^{} \land y \in ℝ^{*})$
742		simpr	$⊢ (y \in (w \cap (A, +∞)) \land B < y) \to B < y$
743	739	ltpnfd	$⊢ y \in (w \cap (A, +∞)) \to y < +∞$
744	743	adantr	$⊢ (y \in (w \cap (A, +∞)) \land B < y) \to y < +∞$
745	742 744	jca	$⊢ (y \in (w \cap (A, +∞)) \land B < y) \to (B < y \land y < +∞)$
746	745	adantll	$⊢ ((φ \land y \in (w \cap (A, +∞))) \land B < y) \to (B < y \land y < +∞)$
747	741 746 377	sylanbrc	$⊢ ((φ \land y \in (w \cap (A, +∞))) \land B < y) \to y \in (B, +∞)$
748	738 747 399	syl2anc	$⊢ ((φ \land y \in (w \cap (A, +∞))) \land B < y) \to G (y) = F (B)$
749	748	adantllr	$⊢ (((φ \land F (B) \in u) \land y \in (w \cap (A, +∞))) \land B < y) \to G (y) = F (B)$
750		simpllr	$⊢ (((φ \land F (B) \in u) \land y \in (w \cap (A, +∞))) \land B < y) \to F (B) \in u$
751	749 750	eqeltrd	$⊢ (((φ \land F (B) \in u) \land y \in (w \cap (A, +∞))) \land B < y) \to G (y) \in u$
752	751	adantl3r	$⊢ ((((φ \land F^{-1} [u] = w \cap [A, B]) \land F (B) \in u) \land y \in (w \cap (A, +∞))) \land B < y) \to G (y) \in u$
753		simp-4l	$⊢ ((((φ \land F^{-1} [u] = w \cap [A, B]) \land F (B) \in u) \land y \in (w \cap (A, +∞))) \land \neg B < y) \to φ$
754		simplr	$⊢ ((((φ \land F^{-1} [u] = w \cap [A, B]) \land F (B) \in u) \land y \in (w \cap (A, +∞))) \land \neg B < y) \to y \in (w \cap (A, +∞))$
755		simpr	$⊢ ((((φ \land F^{-1} [u] = w \cap [A, B]) \land F (B) \in u) \land y \in (w \cap (A, +∞))) \land \neg B < y) \to \neg B < y$
756		simpll	$⊢ ((φ \land y \in (w \cap (A, +∞))) \land \neg B < y) \to φ$
757	739	adantl	$⊢ (φ \land y \in (w \cap (A, +∞))) \to y \in ℝ$
758	757	adantr	$⊢ ((φ \land y \in (w \cap (A, +∞))) \land \neg B < y) \to y \in ℝ$
759	5	adantr	$⊢ (φ \land y \in (w \cap (A, +∞))) \to A \in ℝ$
760		elinel2	$⊢ y \in (w \cap (A, +∞)) \to y \in (A, +∞)$
761	688	biimpi	$⊢ y \in (A, +∞) \to ((A \in ℝ^{} \land +∞ \in ℝ^{} \land y \in ℝ^{*}) \land (A < y \land y < +∞))$
762	761	simprld	$⊢ y \in (A, +∞) \to A < y$
763	760 762	syl	$⊢ y \in (w \cap (A, +∞)) \to A < y$
764	763	adantl	$⊢ (φ \land y \in (w \cap (A, +∞))) \to A < y$
765	759 757 764	ltled	$⊢ (φ \land y \in (w \cap (A, +∞))) \to A \leq y$
766	765	adantr	$⊢ ((φ \land y \in (w \cap (A, +∞))) \land \neg B < y) \to A \leq y$
767		simpr	$⊢ ((φ \land y \in (w \cap (A, +∞))) \land \neg B < y) \to \neg B < y$
768	756 758 469	syl2anc	$⊢ ((φ \land y \in (w \cap (A, +∞))) \land \neg B < y) \to (y \in ℝ \land B \in ℝ)$
769	768 655	syl	$⊢ ((φ \land y \in (w \cap (A, +∞))) \land \neg B < y) \to (y \leq B \leftrightarrow \neg B < y)$
770	767 769	mpbird	$⊢ ((φ \land y \in (w \cap (A, +∞))) \land \neg B < y) \to y \leq B$
771	263	ad2antrr	$⊢ ((φ \land y \in (w \cap (A, +∞))) \land \neg B < y) \to (A \in ℝ \land B \in ℝ)$
772	771 386	syl	$⊢ ((φ \land y \in (w \cap (A, +∞))) \land \neg B < y) \to (y \in [A, B] \leftrightarrow (y \in ℝ \land A \leq y \land y \leq B))$
773	758 766 770 772	mpbir3and	$⊢ ((φ \land y \in (w \cap (A, +∞))) \land \neg B < y) \to y \in [A, B]$
774	756 773 138	syl2anc	$⊢ ((φ \land y \in (w \cap (A, +∞))) \land \neg B < y) \to G (y) = F (y)$
775	753 754 755 774	syl21anc	$⊢ ((((φ \land F^{-1} [u] = w \cap [A, B]) \land F (B) \in u) \land y \in (w \cap (A, +∞))) \land \neg B < y) \to G (y) = F (y)$
776		elinel1	$⊢ y \in (w \cap (A, +∞)) \to y \in w$
777	776	ad2antlr	$⊢ ((φ \land y \in (w \cap (A, +∞))) \land \neg B < y) \to y \in w$
778	777 773	jca	$⊢ ((φ \land y \in (w \cap (A, +∞))) \land \neg B < y) \to (y \in w \land y \in [A, B])$
779	778	adantllr	$⊢ (((φ \land F^{-1} [u] = w \cap [A, B]) \land y \in (w \cap (A, +∞))) \land \neg B < y) \to (y \in w \land y \in [A, B])$
780	779 150	sylibr	$⊢ (((φ \land F^{-1} [u] = w \cap [A, B]) \land y \in (w \cap (A, +∞))) \land \neg B < y) \to y \in (w \cap [A, B])$
781	196	ad3antlr	$⊢ (((φ \land F^{-1} [u] = w \cap [A, B]) \land y \in (w \cap (A, +∞))) \land \neg B < y) \to w \cap [A, B] = F^{-1} [u]$
782	780 781	eleqtrd	$⊢ (((φ \land F^{-1} [u] = w \cap [A, B]) \land y \in (w \cap (A, +∞))) \land \neg B < y) \to y \in F^{-1} [u]$
783	20	ad3antrrr	$⊢ (((φ \land F^{-1} [u] = w \cap [A, B]) \land y \in (w \cap (A, +∞))) \land \neg B < y) \to F Fn [A, B]$
784	783 144	syl	$⊢ (((φ \land F^{-1} [u] = w \cap [A, B]) \land y \in (w \cap (A, +∞))) \land \neg B < y) \to (y \in F^{-1} [u] \leftrightarrow (y \in [A, B] \land F (y) \in u))$
785	782 784	mpbid	$⊢ (((φ \land F^{-1} [u] = w \cap [A, B]) \land y \in (w \cap (A, +∞))) \land \neg B < y) \to (y \in [A, B] \land F (y) \in u)$
786	785	simprd	$⊢ (((φ \land F^{-1} [u] = w \cap [A, B]) \land y \in (w \cap (A, +∞))) \land \neg B < y) \to F (y) \in u$
787	786	adantllr	$⊢ ((((φ \land F^{-1} [u] = w \cap [A, B]) \land F (B) \in u) \land y \in (w \cap (A, +∞))) \land \neg B < y) \to F (y) \in u$
788	775 787	eqeltrd	$⊢ ((((φ \land F^{-1} [u] = w \cap [A, B]) \land F (B) \in u) \land y \in (w \cap (A, +∞))) \land \neg B < y) \to G (y) \in u$
789	752 788	pm2.61dan	$⊢ (((φ \land F^{-1} [u] = w \cap [A, B]) \land F (B) \in u) \land y \in (w \cap (A, +∞))) \to G (y) \in u$
790	789	ralrimiva	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land F (B) \in u) \to \forall y \in (w \cap (A, +∞)) G (y) \in u$
791		fndm	$⊢ G Fn ℝ \to dom G = ℝ$
792	505 791	syl	$⊢ φ \to dom G = ℝ$
793	732 792	sseqtrrid	$⊢ φ \to w \cap (A, +∞) \subseteq dom G$
794	167 793	jca	$⊢ φ \to (Fun G \land w \cap (A, +∞) \subseteq dom G)$
795	794	ad2antrr	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land F (B) \in u) \to (Fun G \land w \cap (A, +∞) \subseteq dom G)$
796		funimass4	$⊢ (Fun G \land w \cap (A, +∞) \subseteq dom G) \to (G [w \cap (A, +∞)] \subseteq u \leftrightarrow \forall y \in (w \cap (A, +∞)) G (y) \in u)$
797	795 796	syl	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land F (B) \in u) \to (G [w \cap (A, +∞)] \subseteq u \leftrightarrow \forall y \in (w \cap (A, +∞)) G (y) \in u)$
798	790 797	mpbird	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land F (B) \in u) \to G [w \cap (A, +∞)] \subseteq u$
799	339	adantlr	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land F (B) \in u) \to G [(B, +∞)] \subseteq u$
800	798 799	unssd	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land F (B) \in u) \to G [w \cap (A, +∞)] \cup G [(B, +∞)] \subseteq u$
801	737 800	eqsstrd	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land F (B) \in u) \to G [(w \cap (A, +∞)) \cup (B, +∞)] \subseteq u$
802	725 726 727 801	syl21anc	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land F (B) \in u) \to G [(w \cap (A, +∞)) \cup (B, +∞)] \subseteq u$
803		eleq2	$⊢ v = (w \cap (A, +∞)) \cup (B, +∞) \to (y \in v \leftrightarrow y \in ((w \cap (A, +∞)) \cup (B, +∞)))$
804		imaeq2	$⊢ v = (w \cap (A, +∞)) \cup (B, +∞) \to G [v] = G [(w \cap (A, +∞)) \cup (B, +∞)]$
805	804	sseq1d	$⊢ v = (w \cap (A, +∞)) \cup (B, +∞) \to (G [v] \subseteq u \leftrightarrow G [(w \cap (A, +∞)) \cup (B, +∞)] \subseteq u)$
806	803 805	anbi12d	$⊢ v = (w \cap (A, +∞)) \cup (B, +∞) \to ((y \in v \land G [v] \subseteq u) \leftrightarrow (y \in ((w \cap (A, +∞)) \cup (B, +∞)) \land G [(w \cap (A, +∞)) \cup (B, +∞)] \subseteq u))$
807	806	rspcev	$⊢ ((w \cap (A, +∞)) \cup (B, +∞) \in J \land (y \in ((w \cap (A, +∞)) \cup (B, +∞)) \land G [(w \cap (A, +∞)) \cup (B, +∞)] \subseteq u)) \to \exists v \in J (y \in v \land G [v] \subseteq u)$
808	606 723 802 807	syl12anc	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land F (B) \in u) \to \exists v \in J (y \in v \land G [v] \subseteq u)$
809		simpll2	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg F (B) \in u) \to w \in J$
810		iooretop	$⊢ (A, B) \in topGen (ran (.))$
811	810 2	eleqtrri	$⊢ (A, B) \in J$
812		inopn	$⊢ (J \in Top \land w \in J \land (A, B) \in J) \to w \cap (A, B) \in J$
813	80 811 812	mp3an13	$⊢ w \in J \to w \cap (A, B) \in J$
814	809 813	syl	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg F (B) \in u) \to w \cap (A, B) \in J$
815		simp-4r	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (A) \in u) \land \neg F (B) \in u) \to y \in ℝ$
816	638	adantr	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (A) \in u) \land \neg F (B) \in u) \to A \leq y$
817		simpll	$⊢ (((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (B) \in u) \to (φ \land y \in ℝ)$
818	817 405 657	syl2anc	$⊢ (((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (B) \in u) \to y \leq B$
819	818	adantlr	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (A) \in u) \land \neg F (B) \in u) \to y \leq B$
820		simp-4l	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (A) \in u) \land \neg F (B) \in u) \to φ$
821	820 263	syl	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (A) \in u) \land \neg F (B) \in u) \to (A \in ℝ \land B \in ℝ)$
822	821 386	syl	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (A) \in u) \land \neg F (B) \in u) \to (y \in [A, B] \leftrightarrow (y \in ℝ \land A \leq y \land y \leq B))$
823	815 816 819 822	mpbir3and	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (A) \in u) \land \neg F (B) \in u) \to y \in [A, B]$
824	823	adantllr	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg F (B) \in u) \to y \in [A, B]$
825	820 823 138	syl2anc	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land \neg F (A) \in u) \land \neg F (B) \in u) \to G (y) = F (y)$
826	825	adantllr	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg F (B) \in u) \to G (y) = F (y)$
827		simp-4r	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg F (B) \in u) \to G (y) \in u$
828	826 827	eqeltrrd	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg F (B) \in u) \to F (y) \in u$
829		simp-5l	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg F (B) \in u) \to φ$
830	829 20	syl	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg F (B) \in u) \to F Fn [A, B]$
831	830 144	syl	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg F (B) \in u) \to (y \in F^{-1} [u] \leftrightarrow (y \in [A, B] \land F (y) \in u))$
832	824 828 831	mpbir2and	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg F (B) \in u) \to y \in F^{-1} [u]$
833		simpllr	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg F (B) \in u) \to F^{-1} [u] = w \cap [A, B]$
834	832 833	eleqtrd	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg F (B) \in u) \to y \in (w \cap [A, B])$
835	834 427	syl	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg F (B) \in u) \to y \in w$
836		simp-5r	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg F (B) \in u) \to y \in ℝ$
837	829 836 824	jca31	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg F (B) \in u) \to ((φ \land y \in ℝ) \land y \in [A, B])$
838		simplr	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg F (B) \in u) \to \neg F (A) \in u$
839	828 838	jca	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg F (B) \in u) \to (F (y) \in u \land \neg F (A) \in u)$
840		nelneq	$⊢ (F (y) \in u \land \neg F (A) \in u) \to \neg F (y) = F (A)$
841	670	necon3bi	$⊢ \neg F (y) = F (A) \to y \neq A$
842	839 840 841	3syl	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg F (B) \in u) \to y \neq A$
843		simpr	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg F (B) \in u) \to \neg F (B) \in u$
844	828 843	jca	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg F (B) \in u) \to (F (y) \in u \land \neg F (B) \in u)$
845		nelneq	$⊢ (F (y) \in u \land \neg F (B) \in u) \to \neg F (y) = F (B)$
846		fveq2	$⊢ y = B \to F (y) = F (B)$
847	846	necon3bi	$⊢ \neg F (y) = F (B) \to y \neq B$
848	844 845 847	3syl	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg F (B) \in u) \to y \neq B$
849	614	ad3antrrr	$⊢ ((((φ \land y \in ℝ) \land y \in [A, B]) \land y \neq A) \land y \neq B) \to A \in ℝ^{*}$
850	442	ad3antrrr	$⊢ ((((φ \land y \in ℝ) \land y \in [A, B]) \land y \neq A) \land y \neq B) \to B \in ℝ^{*}$
851	445	ad4antlr	$⊢ ((((φ \land y \in ℝ) \land y \in [A, B]) \land y \neq A) \land y \neq B) \to y \in ℝ^{*}$
852	849 850 851	3jca	$⊢ ((((φ \land y \in ℝ) \land y \in [A, B]) \land y \neq A) \land y \neq B) \to (A \in ℝ^{} \land B \in ℝ^{} \land y \in ℝ^{*})$
853		simpr	$⊢ (((φ \land y \in ℝ) \land y \in [A, B]) \land y \neq A) \to y \neq A$
854	5	ad2antrr	$⊢ ((φ \land y \in ℝ) \land y \in [A, B]) \to A \in ℝ$
855		simplr	$⊢ ((φ \land y \in ℝ) \land y \in [A, B]) \to y \in ℝ$
856	263	adantr	$⊢ (φ \land y \in [A, B]) \to (A \in ℝ \land B \in ℝ)$
857	856 386	syl	$⊢ (φ \land y \in [A, B]) \to (y \in [A, B] \leftrightarrow (y \in ℝ \land A \leq y \land y \leq B))$
858	136 857	mpbid	$⊢ (φ \land y \in [A, B]) \to (y \in ℝ \land A \leq y \land y \leq B)$
859	858	simp2d	$⊢ (φ \land y \in [A, B]) \to A \leq y$
860	859	adantlr	$⊢ ((φ \land y \in ℝ) \land y \in [A, B]) \to A \leq y$
861	854 855 860	3jca	$⊢ ((φ \land y \in ℝ) \land y \in [A, B]) \to (A \in ℝ \land y \in ℝ \land A \leq y)$
862	861	adantr	$⊢ (((φ \land y \in ℝ) \land y \in [A, B]) \land y \neq A) \to (A \in ℝ \land y \in ℝ \land A \leq y)$
863		leltne	$⊢ (A \in ℝ \land y \in ℝ \land A \leq y) \to (A < y \leftrightarrow y \neq A)$
864	862 863	syl	$⊢ (((φ \land y \in ℝ) \land y \in [A, B]) \land y \neq A) \to (A < y \leftrightarrow y \neq A)$
865	853 864	mpbird	$⊢ (((φ \land y \in ℝ) \land y \in [A, B]) \land y \neq A) \to A < y$
866	865	adantr	$⊢ ((((φ \land y \in ℝ) \land y \in [A, B]) \land y \neq A) \land y \neq B) \to A < y$
867		necom	$⊢ y \neq B \leftrightarrow B \neq y$
868	867	biimpi	$⊢ y \neq B \to B \neq y$
869	868	adantl	$⊢ (((φ \land y \in ℝ) \land y \in [A, B]) \land y \neq B) \to B \neq y$
870	6	ad2antrr	$⊢ ((φ \land y \in ℝ) \land y \in [A, B]) \to B \in ℝ$
871	858	simp3d	$⊢ (φ \land y \in [A, B]) \to y \leq B$
872	871	adantlr	$⊢ ((φ \land y \in ℝ) \land y \in [A, B]) \to y \leq B$
873	855 870 872	3jca	$⊢ ((φ \land y \in ℝ) \land y \in [A, B]) \to (y \in ℝ \land B \in ℝ \land y \leq B)$
874	873	adantr	$⊢ (((φ \land y \in ℝ) \land y \in [A, B]) \land y \neq B) \to (y \in ℝ \land B \in ℝ \land y \leq B)$
875		leltne	$⊢ (y \in ℝ \land B \in ℝ \land y \leq B) \to (y < B \leftrightarrow B \neq y)$
876	874 875	syl	$⊢ (((φ \land y \in ℝ) \land y \in [A, B]) \land y \neq B) \to (y < B \leftrightarrow B \neq y)$
877	869 876	mpbird	$⊢ (((φ \land y \in ℝ) \land y \in [A, B]) \land y \neq B) \to y < B$
878	877	adantlr	$⊢ ((((φ \land y \in ℝ) \land y \in [A, B]) \land y \neq A) \land y \neq B) \to y < B$
879	866 878	jca	$⊢ ((((φ \land y \in ℝ) \land y \in [A, B]) \land y \neq A) \land y \neq B) \to (A < y \land y < B)$
880		elioo3g	$⊢ y \in (A, B) \leftrightarrow ((A \in ℝ^{} \land B \in ℝ^{} \land y \in ℝ^{*}) \land (A < y \land y < B))$
881	852 879 880	sylanbrc	$⊢ ((((φ \land y \in ℝ) \land y \in [A, B]) \land y \neq A) \land y \neq B) \to y \in (A, B)$
882	837 842 848 881	syl21anc	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg F (B) \in u) \to y \in (A, B)$
883	835 882	elind	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg F (B) \in u) \to y \in (w \cap (A, B))$
884	883	3adantll2	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg F (B) \in u) \to y \in (w \cap (A, B))$
885	166	a1i	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land t \in G [w \cap (A, B)]) \to Fun G$
886		fvelima	$⊢ (Fun G \land t \in G [w \cap (A, B)]) \to \exists y \in (w \cap (A, B)) G (y) = t$
887	885 886	sylancom	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land t \in G [w \cap (A, B)]) \to \exists y \in (w \cap (A, B)) G (y) = t$
888		simp3	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land y \in (w \cap (A, B)) \land G (y) = t) \to G (y) = t$
889		simp1l	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land y \in (w \cap (A, B)) \land G (y) = t) \to φ$
890		inss2	$⊢ w \cap (A, B) \subseteq (A, B)$
891		ioossicc	$⊢ (A, B) \subseteq [A, B]$
892	890 891	sstri	$⊢ w \cap (A, B) \subseteq [A, B]$
893	892	sseli	$⊢ y \in (w \cap (A, B)) \to y \in [A, B]$
894	893	3ad2ant2	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land y \in (w \cap (A, B)) \land G (y) = t) \to y \in [A, B]$
895	889 894 138	syl2anc	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land y \in (w \cap (A, B)) \land G (y) = t) \to G (y) = F (y)$
896		sslin	$⊢ (A, B) \subseteq [A, B] \to w \cap (A, B) \subseteq w \cap [A, B]$
897	891 896	ax-mp	$⊢ w \cap (A, B) \subseteq w \cap [A, B]$
898	897	sseli	$⊢ y \in (w \cap (A, B)) \to y \in (w \cap [A, B])$
899	898	adantl	$⊢ (F^{-1} [u] = w \cap [A, B] \land y \in (w \cap (A, B))) \to y \in (w \cap [A, B])$
900	196	adantr	$⊢ (F^{-1} [u] = w \cap [A, B] \land y \in (w \cap (A, B))) \to w \cap [A, B] = F^{-1} [u]$
901	899 900	eleqtrd	$⊢ (F^{-1} [u] = w \cap [A, B] \land y \in (w \cap (A, B))) \to y \in F^{-1} [u]$
902	901	adantll	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land y \in (w \cap (A, B))) \to y \in F^{-1} [u]$
903	20	ad2antrr	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land y \in (w \cap (A, B))) \to F Fn [A, B]$
904	903 144	syl	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land y \in (w \cap (A, B))) \to (y \in F^{-1} [u] \leftrightarrow (y \in [A, B] \land F (y) \in u))$
905	902 904	mpbid	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land y \in (w \cap (A, B))) \to (y \in [A, B] \land F (y) \in u)$
906	905	simprd	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land y \in (w \cap (A, B))) \to F (y) \in u$
907	906	3adant3	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land y \in (w \cap (A, B)) \land G (y) = t) \to F (y) \in u$
908	895 907	eqeltrd	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land y \in (w \cap (A, B)) \land G (y) = t) \to G (y) \in u$
909	888 908	eqeltrrd	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land y \in (w \cap (A, B)) \land G (y) = t) \to t \in u$
910	909	3exp	$⊢ (φ \land F^{-1} [u] = w \cap [A, B]) \to (y \in (w \cap (A, B)) \to (G (y) = t \to t \in u))$
911	910	adantr	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land t \in G [w \cap (A, B)]) \to (y \in (w \cap (A, B)) \to (G (y) = t \to t \in u))$
912	911	rexlimdv	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land t \in G [w \cap (A, B)]) \to (\exists y \in (w \cap (A, B)) G (y) = t \to t \in u)$
913	887 912	mpd	$⊢ ((φ \land F^{-1} [u] = w \cap [A, B]) \land t \in G [w \cap (A, B)]) \to t \in u$
914	913	ralrimiva	$⊢ (φ \land F^{-1} [u] = w \cap [A, B]) \to \forall t \in G [w \cap (A, B)] t \in u$
915		dfss3	$⊢ G [w \cap (A, B)] \subseteq u \leftrightarrow \forall t \in G [w \cap (A, B)] t \in u$
916	914 915	sylibr	$⊢ (φ \land F^{-1} [u] = w \cap [A, B]) \to G [w \cap (A, B)] \subseteq u$
917	916	ad4ant14	$⊢ (((φ \land y \in ℝ) \land G (y) \in u) \land F^{-1} [u] = w \cap [A, B]) \to G [w \cap (A, B)] \subseteq u$
918	917	3adant2	$⊢ (((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \to G [w \cap (A, B)] \subseteq u$
919	918	ad2antrr	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg F (B) \in u) \to G [w \cap (A, B)] \subseteq u$
920		eleq2	$⊢ v = w \cap (A, B) \to (y \in v \leftrightarrow y \in (w \cap (A, B)))$
921		imaeq2	$⊢ v = w \cap (A, B) \to G [v] = G [w \cap (A, B)]$
922	921	sseq1d	$⊢ v = w \cap (A, B) \to (G [v] \subseteq u \leftrightarrow G [w \cap (A, B)] \subseteq u)$
923	920 922	anbi12d	$⊢ v = w \cap (A, B) \to ((y \in v \land G [v] \subseteq u) \leftrightarrow (y \in (w \cap (A, B)) \land G [w \cap (A, B)] \subseteq u))$
924	923	rspcev	$⊢ (w \cap (A, B) \in J \land (y \in (w \cap (A, B)) \land G [w \cap (A, B)] \subseteq u)) \to \exists v \in J (y \in v \land G [v] \subseteq u)$
925	814 884 919 924	syl12anc	$⊢ (((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \land \neg F (B) \in u) \to \exists v \in J (y \in v \land G [v] \subseteq u)$
926	808 925	pm2.61dan	$⊢ ((((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \land \neg F (A) \in u) \to \exists v \in J (y \in v \land G [v] \subseteq u)$
927	597 926	pm2.61dan	$⊢ (((φ \land y \in ℝ) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \to \exists v \in J (y \in v \land G [v] \subseteq u)$
928	94 927	syld3an1	$⊢ ((((φ \land y \in ℝ) \land u \in (K ↾_{𝑡} ran F)) \land G (y) \in u) \land w \in J \land F^{-1} [u] = w \cap [A, B]) \to \exists v \in J (y \in v \land G [v] \subseteq u)$
929	928	rexlimdv3a	$⊢ (((φ \land y \in ℝ) \land u \in (K ↾_{𝑡} ran F)) \land G (y) \in u) \to (\exists w \in J F^{-1} [u] = w \cap [A, B] \to \exists v \in J (y \in v \land G [v] \subseteq u))$
930	89 929	mpd	$⊢ (((φ \land y \in ℝ) \land u \in (K ↾_{𝑡} ran F)) \land G (y) \in u) \to \exists v \in J (y \in v \land G [v] \subseteq u)$
931	930	ex	$⊢ ((φ \land y \in ℝ) \land u \in (K ↾_{𝑡} ran F)) \to (G (y) \in u \to \exists v \in J (y \in v \land G [v] \subseteq u))$
932	931	ralrimiva	$⊢ (φ \land y \in ℝ) \to \forall u \in (K ↾_{𝑡} ran F) (G (y) \in u \to \exists v \in J (y \in v \land G [v] \subseteq u))$
933	11	a1i	$⊢ (φ \land y \in ℝ) \to J \in TopOn (ℝ)$
934		resttopon	$⊢ (K \in TopOn (Y) \land ran F \subseteq Y) \to K ↾_{𝑡} ran F \in TopOn (ran F)$
935	17 72 934	syl2anc	$⊢ φ \to K ↾_{𝑡} ran F \in TopOn (ran F)$
936	935	adantr	$⊢ (φ \land y \in ℝ) \to K ↾_{𝑡} ran F \in TopOn (ran F)$
937		iscnp	$⊢ (J \in TopOn (ℝ) \land K ↾_{𝑡} ran F \in TopOn (ran F) \land y \in ℝ) \to (G \in (J CnP (K ↾_{𝑡} ran F)) (y) \leftrightarrow (G : ℝ ⟶ ran F \land \forall u \in (K ↾_{𝑡} ran F) (G (y) \in u \to \exists v \in J (y \in v \land G [v] \subseteq u))))$
938	933 936 467 937	syl3anc	$⊢ (φ \land y \in ℝ) \to (G \in (J CnP (K ↾_{𝑡} ran F)) (y) \leftrightarrow (G : ℝ ⟶ ran F \land \forall u \in (K ↾_{𝑡} ran F) (G (y) \in u \to \exists v \in J (y \in v \land G [v] \subseteq u))))$
939	67 932 938	mpbir2and	$⊢ (φ \land y \in ℝ) \to G \in (J CnP (K ↾_{𝑡} ran F)) (y)$
940	939	ralrimiva	$⊢ φ \to \forall y \in ℝ G \in (J CnP (K ↾_{𝑡} ran F)) (y)$
941		cncnp	$⊢ (J \in TopOn (ℝ) \land K ↾_{𝑡} ran F \in TopOn (ran F)) \to (G \in (J Cn (K ↾_{𝑡} ran F)) \leftrightarrow (G : ℝ ⟶ ran F \land \forall y \in ℝ G \in (J CnP (K ↾_{𝑡} ran F)) (y)))$
942	11 935 941	sylancr	$⊢ φ \to (G \in (J Cn (K ↾_{𝑡} ran F)) \leftrightarrow (G : ℝ ⟶ ran F \land \forall y \in ℝ G \in (J CnP (K ↾_{𝑡} ran F)) (y)))$
943	66 940 942	mpbir2and	$⊢ φ \to G \in (J Cn (K ↾_{𝑡} ran F))$
944		fnssres	$⊢ (G Fn ℝ \land [A, B] \subseteq ℝ) \to ({G ↾}_{[A, B]}) Fn [A, B]$
945	505 12 944	syl2anc	$⊢ φ \to ({G ↾}_{[A, B]}) Fn [A, B]$
946		fvres	$⊢ y \in [A, B] \to ({G ↾}_{[A, B]}) (y) = G (y)$
947	946	adantl	$⊢ (φ \land y \in [A, B]) \to ({G ↾}_{[A, B]}) (y) = G (y)$
948	947 138	eqtrd	$⊢ (φ \land y \in [A, B]) \to ({G ↾}_{[A, B]}) (y) = F (y)$
949	945 20 948	eqfnfvd	$⊢ φ \to {G ↾}_{[A, B]} = F$
950	943 949	jca	$⊢ φ \to (G \in (J Cn (K ↾_{𝑡} ran F)) \land {G ↾}_{[A, B]} = F)$

Metamath Proof Explorer

Theorem icccncfext

Proof