pimincfltioc

Description: Given a nondecreasing function, the preimage of an unbounded below, open interval, when the supremum of the preimage belongs to the preimage. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	pimincfltioc.x	$⊢ Ⅎ x φ$
	pimincfltioc.h	$⊢ Ⅎ y φ$
	pimincfltioc.a	$⊢ φ \to A \subseteq ℝ$
	pimincfltioc.f	$⊢ φ \to F : A ⟶ ℝ^{*}$
	pimincfltioc.i	$⊢ φ \to \forall x \in A \forall y \in A (x \leq y \to F (x) \leq F (y))$
	pimincfltioc.r	$⊢ φ \to R \in ℝ^{*}$
	pimincfltioc.y	$⊢ Y = \{x \in A \| F (x) < R\}$
	pimincfltioc.c	$⊢ S = sup (Y ℝ^{*} <)$
	pimincfltioc.e	$⊢ φ \to S \in Y$
	pimincfltioc.d	$⊢ I = (−∞, S]$
Assertion	pimincfltioc	$⊢ φ \to Y = I \cap A$

Proof

Step	Hyp	Ref	Expression
1		pimincfltioc.x	$⊢ Ⅎ x φ$
2		pimincfltioc.h	$⊢ Ⅎ y φ$
3		pimincfltioc.a	$⊢ φ \to A \subseteq ℝ$
4		pimincfltioc.f	$⊢ φ \to F : A ⟶ ℝ^{*}$
5		pimincfltioc.i	$⊢ φ \to \forall x \in A \forall y \in A (x \leq y \to F (x) \leq F (y))$
6		pimincfltioc.r	$⊢ φ \to R \in ℝ^{*}$
7		pimincfltioc.y	$⊢ Y = \{x \in A \| F (x) < R\}$
8		pimincfltioc.c	$⊢ S = sup (Y ℝ^{*} <)$
9		pimincfltioc.e	$⊢ φ \to S \in Y$
10		pimincfltioc.d	$⊢ I = (−∞, S]$
11		ssrab2	$⊢ \{x \in A \| F (x) < R\} \subseteq A$
12	7 11	eqsstri	$⊢ Y \subseteq A$
13	12	a1i	$⊢ φ \to Y \subseteq A$
14	13 3	sstrd	$⊢ φ \to Y \subseteq ℝ$
15	14 8 9 10	ressiocsup	$⊢ φ \to Y \subseteq I$
16	15 13	ssind	$⊢ φ \to Y \subseteq I \cap A$
17		elinel2	$⊢ x \in (I \cap A) \to x \in A$
18	17	adantl	$⊢ (φ \land x \in (I \cap A)) \to x \in A$
19	4	adantr	$⊢ (φ \land x \in (I \cap A)) \to F : A ⟶ ℝ^{*}$
20	19 18	ffvelcdmd	$⊢ (φ \land x \in (I \cap A)) \to F (x) \in ℝ^{*}$
21	12 9	sselid	$⊢ φ \to S \in A$
22	4 21	ffvelcdmd	$⊢ φ \to F (S) \in ℝ^{*}$
23	22	adantr	$⊢ (φ \land x \in (I \cap A)) \to F (S) \in ℝ^{*}$
24	6	adantr	$⊢ (φ \land x \in (I \cap A)) \to R \in ℝ^{*}$
25		eleq1w	$⊢ z = x \to (z \in (I \cap A) \leftrightarrow x \in (I \cap A))$
26	25	anbi2d	$⊢ z = x \to ((φ \land z \in (I \cap A)) \leftrightarrow (φ \land x \in (I \cap A)))$
27		fveq2	$⊢ z = x \to F (z) = F (x)$
28	27	breq1d	$⊢ z = x \to (F (z) \leq F (S) \leftrightarrow F (x) \leq F (S))$
29	26 28	imbi12d	$⊢ z = x \to (((φ \land z \in (I \cap A)) \to F (z) \leq F (S)) \leftrightarrow ((φ \land x \in (I \cap A)) \to F (x) \leq F (S)))$
30		nfv	$⊢ Ⅎ x z \in (I \cap A)$
31	1 30	nfan	$⊢ Ⅎ x (φ \land z \in (I \cap A))$
32		nfv	$⊢ Ⅎ y z \in (I \cap A)$
33	2 32	nfan	$⊢ Ⅎ y (φ \land z \in (I \cap A))$
34	5	adantr	$⊢ (φ \land z \in (I \cap A)) \to \forall x \in A \forall y \in A (x \leq y \to F (x) \leq F (y))$
35		elinel2	$⊢ z \in (I \cap A) \to z \in A$
36	35	adantl	$⊢ (φ \land z \in (I \cap A)) \to z \in A$
37	21	adantr	$⊢ (φ \land z \in (I \cap A)) \to S \in A$
38		mnfxr	$⊢ −∞ \in ℝ^{*}$
39	38	a1i	$⊢ (φ \land z \in (I \cap A)) \to −∞ \in ℝ^{*}$
40		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
41	14 9	sseldd	$⊢ φ \to S \in ℝ$
42	40 41	sselid	$⊢ φ \to S \in ℝ^{*}$
43	42	adantr	$⊢ (φ \land z \in (I \cap A)) \to S \in ℝ^{*}$
44		elinel1	$⊢ z \in (I \cap A) \to z \in I$
45	44 10	eleqtrdi	$⊢ z \in (I \cap A) \to z \in (−∞, S]$
46	45	adantl	$⊢ (φ \land z \in (I \cap A)) \to z \in (−∞, S]$
47		iocleub	$⊢ (−∞ \in ℝ^{} \land S \in ℝ^{} \land z \in (−∞, S]) \to z \leq S$
48	39 43 46 47	syl3anc	$⊢ (φ \land z \in (I \cap A)) \to z \leq S$
49	31 33 34 36 37 48	dmrelrnrel	$⊢ (φ \land z \in (I \cap A)) \to F (z) \leq F (S)$
50	29 49	chvarvv	$⊢ (φ \land x \in (I \cap A)) \to F (x) \leq F (S)$
51		fveq2	$⊢ x = S \to F (x) = F (S)$
52	51	breq1d	$⊢ x = S \to (F (x) < R \leftrightarrow F (S) < R)$
53	52 7	elrab2	$⊢ S \in Y \leftrightarrow (S \in A \land F (S) < R)$
54	9 53	sylib	$⊢ φ \to (S \in A \land F (S) < R)$
55	54	simprd	$⊢ φ \to F (S) < R$
56	55	adantr	$⊢ (φ \land x \in (I \cap A)) \to F (S) < R$
57	20 23 24 50 56	xrlelttrd	$⊢ (φ \land x \in (I \cap A)) \to F (x) < R$
58	18 57	jca	$⊢ (φ \land x \in (I \cap A)) \to (x \in A \land F (x) < R)$
59	7	reqabi	$⊢ x \in Y \leftrightarrow (x \in A \land F (x) < R)$
60	58 59	sylibr	$⊢ (φ \land x \in (I \cap A)) \to x \in Y$
61	60	ex	$⊢ φ \to (x \in (I \cap A) \to x \in Y)$
62	1 61	ralrimi	$⊢ φ \to \forall x \in (I \cap A) x \in Y$
63	30	nfci	$⊢ \underline{Ⅎ} x (I \cap A)$
64		nfrab1	$⊢ \underline{Ⅎ} x \{x \in A \| F (x) < R\}$
65	7 64	nfcxfr	$⊢ \underline{Ⅎ} x Y$
66	63 65	dfss3f	$⊢ I \cap A \subseteq Y \leftrightarrow \forall x \in (I \cap A) x \in Y$
67	62 66	sylibr	$⊢ φ \to I \cap A \subseteq Y$
68	16 67	eqssd	$⊢ φ \to Y = I \cap A$

Metamath Proof Explorer

Theorem pimincfltioc

Proof