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

Metamath Proof Explorer

Theorem icccncfext

Proof