pimdecfgtioo

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

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

Proof

Step	Hyp	Ref	Expression
1		pimdecfgtioo.x	$⊢ Ⅎ x φ$
2		pimdecfgtioo.h	$⊢ Ⅎ y φ$
3		pimdecfgtioo.a	$⊢ φ \to A \subseteq ℝ$
4		pimdecfgtioo.f	$⊢ φ \to F : A ⟶ ℝ^{*}$
5		pimdecfgtioo.d	$⊢ φ \to \forall x \in A \forall y \in A (x \leq y \to F (y) \leq F (x))$
6		pimdecfgtioo.r	$⊢ φ \to R \in ℝ^{*}$
7		pimdecfgtioo.y	$⊢ Y = \{x \in A \| R < F (x)\}$
8		pimdecfgtioo.c	$⊢ S = sup (Y ℝ^{*} <)$
9		pimdecfgtioo.e	$⊢ φ \to \neg S \in Y$
10		pimdecfgtioo.i	$⊢ I = (−∞, S)$
11		ssrab2	$⊢ \{x \in A \| R < F (x)\} \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	ressioosup	$⊢ φ \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		mnfxr	$⊢ −∞ \in ℝ^{*}$
20	19	a1i	$⊢ (φ \land x \in (I \cap A)) \to −∞ \in ℝ^{*}$
21		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
22	14 21	sstrdi	$⊢ φ \to Y \subseteq ℝ^{*}$
23	22	supxrcld	$⊢ φ \to sup (Y ℝ^{} <) \in ℝ^{}$
24	8 23	eqeltrid	$⊢ φ \to S \in ℝ^{*}$
25	24	adantr	$⊢ (φ \land x \in (I \cap A)) \to S \in ℝ^{*}$
26		elinel1	$⊢ x \in (I \cap A) \to x \in I$
27	26 10	eleqtrdi	$⊢ x \in (I \cap A) \to x \in (−∞, S)$
28	27	adantl	$⊢ (φ \land x \in (I \cap A)) \to x \in (−∞, S)$
29		iooltub	$⊢ (−∞ \in ℝ^{} \land S \in ℝ^{} \land x \in (−∞, S)) \to x < S$
30	20 25 28 29	syl3anc	$⊢ (φ \land x \in (I \cap A)) \to x < S$
31	30	adantr	$⊢ ((φ \land x \in (I \cap A)) \land \neg R < F (x)) \to x < S$
32		simpr	$⊢ ((φ \land x \in (I \cap A)) \land \neg R < F (x)) \to \neg R < F (x)$
33	4	adantr	$⊢ (φ \land x \in (I \cap A)) \to F : A ⟶ ℝ^{*}$
34	33 18	ffvelcdmd	$⊢ (φ \land x \in (I \cap A)) \to F (x) \in ℝ^{*}$
35	34	adantr	$⊢ ((φ \land x \in (I \cap A)) \land \neg R < F (x)) \to F (x) \in ℝ^{*}$
36	6	adantr	$⊢ (φ \land x \in (I \cap A)) \to R \in ℝ^{*}$
37	36	adantr	$⊢ ((φ \land x \in (I \cap A)) \land \neg R < F (x)) \to R \in ℝ^{*}$
38	35 37	xrlenltd	$⊢ ((φ \land x \in (I \cap A)) \land \neg R < F (x)) \to (F (x) \leq R \leftrightarrow \neg R < F (x))$
39	32 38	mpbird	$⊢ ((φ \land x \in (I \cap A)) \land \neg R < F (x)) \to F (x) \leq R$
40		nfv	$⊢ Ⅎ y x \in (I \cap A)$
41	2 40	nfan	$⊢ Ⅎ y (φ \land x \in (I \cap A))$
42		nfv	$⊢ Ⅎ y F (x) \leq R$
43	41 42	nfan	$⊢ Ⅎ y ((φ \land x \in (I \cap A)) \land F (x) \leq R)$
44		fveq2	$⊢ x = y \to F (x) = F (y)$
45	44	breq2d	$⊢ x = y \to (R < F (x) \leftrightarrow R < F (y))$
46	45 7	elrab2	$⊢ y \in Y \leftrightarrow (y \in A \land R < F (y))$
47	46	biimpi	$⊢ y \in Y \to (y \in A \land R < F (y))$
48	47	simprd	$⊢ y \in Y \to R < F (y)$
49	48	ad2antlr	$⊢ ((((φ \land x \in (I \cap A)) \land F (x) \leq R) \land y \in Y) \land \neg y \leq x) \to R < F (y)$
50	3	adantr	$⊢ (φ \land x \in (I \cap A)) \to A \subseteq ℝ$
51	50 18	sseldd	$⊢ (φ \land x \in (I \cap A)) \to x \in ℝ$
52	51	ad2antrr	$⊢ (((φ \land x \in (I \cap A)) \land y \in Y) \land \neg y \leq x) \to x \in ℝ$
53	14	sselda	$⊢ (φ \land y \in Y) \to y \in ℝ$
54	53	ad4ant13	$⊢ (((φ \land x \in (I \cap A)) \land y \in Y) \land \neg y \leq x) \to y \in ℝ$
55		simpr	$⊢ (((φ \land x \in (I \cap A)) \land y \in Y) \land \neg y \leq x) \to \neg y \leq x$
56	52 54	ltnled	$⊢ (((φ \land x \in (I \cap A)) \land y \in Y) \land \neg y \leq x) \to (x < y \leftrightarrow \neg y \leq x)$
57	55 56	mpbird	$⊢ (((φ \land x \in (I \cap A)) \land y \in Y) \land \neg y \leq x) \to x < y$
58	52 54 57	ltled	$⊢ (((φ \land x \in (I \cap A)) \land y \in Y) \land \neg y \leq x) \to x \leq y$
59	58	adantllr	$⊢ ((((φ \land x \in (I \cap A)) \land F (x) \leq R) \land y \in Y) \land \neg y \leq x) \to x \leq y$
60	4	adantr	$⊢ (φ \land y \in Y) \to F : A ⟶ ℝ^{*}$
61	13	sselda	$⊢ (φ \land y \in Y) \to y \in A$
62	60 61	ffvelcdmd	$⊢ (φ \land y \in Y) \to F (y) \in ℝ^{*}$
63	62	ad5ant14	$⊢ ((((φ \land x \in (I \cap A)) \land F (x) \leq R) \land y \in Y) \land x \leq y) \to F (y) \in ℝ^{*}$
64	34	ad3antrrr	$⊢ ((((φ \land x \in (I \cap A)) \land F (x) \leq R) \land y \in Y) \land x \leq y) \to F (x) \in ℝ^{*}$
65	36	ad3antrrr	$⊢ ((((φ \land x \in (I \cap A)) \land F (x) \leq R) \land y \in Y) \land x \leq y) \to R \in ℝ^{*}$
66		simpr	$⊢ (((φ \land x \in (I \cap A)) \land y \in Y) \land x \leq y) \to x \leq y$
67		rspa	$⊢ (\forall x \in A \forall y \in A (x \leq y \to F (y) \leq F (x)) \land x \in A) \to \forall y \in A (x \leq y \to F (y) \leq F (x))$
68	5 17 67	syl2an	$⊢ (φ \land x \in (I \cap A)) \to \forall y \in A (x \leq y \to F (y) \leq F (x))$
69	68	ad2antrr	$⊢ (((φ \land x \in (I \cap A)) \land y \in Y) \land x \leq y) \to \forall y \in A (x \leq y \to F (y) \leq F (x))$
70	61	ad4ant13	$⊢ (((φ \land x \in (I \cap A)) \land y \in Y) \land x \leq y) \to y \in A$
71		rspa	$⊢ (\forall y \in A (x \leq y \to F (y) \leq F (x)) \land y \in A) \to (x \leq y \to F (y) \leq F (x))$
72	69 70 71	syl2anc	$⊢ (((φ \land x \in (I \cap A)) \land y \in Y) \land x \leq y) \to (x \leq y \to F (y) \leq F (x))$
73	66 72	mpd	$⊢ (((φ \land x \in (I \cap A)) \land y \in Y) \land x \leq y) \to F (y) \leq F (x)$
74	73	adantllr	$⊢ ((((φ \land x \in (I \cap A)) \land F (x) \leq R) \land y \in Y) \land x \leq y) \to F (y) \leq F (x)$
75		simpllr	$⊢ ((((φ \land x \in (I \cap A)) \land F (x) \leq R) \land y \in Y) \land x \leq y) \to F (x) \leq R$
76	63 64 65 74 75	xrletrd	$⊢ ((((φ \land x \in (I \cap A)) \land F (x) \leq R) \land y \in Y) \land x \leq y) \to F (y) \leq R$
77	63 65	xrlenltd	$⊢ ((((φ \land x \in (I \cap A)) \land F (x) \leq R) \land y \in Y) \land x \leq y) \to (F (y) \leq R \leftrightarrow \neg R < F (y))$
78	76 77	mpbid	$⊢ ((((φ \land x \in (I \cap A)) \land F (x) \leq R) \land y \in Y) \land x \leq y) \to \neg R < F (y)$
79	59 78	syldan	$⊢ ((((φ \land x \in (I \cap A)) \land F (x) \leq R) \land y \in Y) \land \neg y \leq x) \to \neg R < F (y)$
80	49 79	condan	$⊢ (((φ \land x \in (I \cap A)) \land F (x) \leq R) \land y \in Y) \to y \leq x$
81	80	ex	$⊢ ((φ \land x \in (I \cap A)) \land F (x) \leq R) \to (y \in Y \to y \leq x)$
82	43 81	ralrimi	$⊢ ((φ \land x \in (I \cap A)) \land F (x) \leq R) \to \forall y \in Y y \leq x$
83	39 82	syldan	$⊢ ((φ \land x \in (I \cap A)) \land \neg R < F (x)) \to \forall y \in Y y \leq x$
84	22	adantr	$⊢ (φ \land x \in (I \cap A)) \to Y \subseteq ℝ^{*}$
85	21 51	sselid	$⊢ (φ \land x \in (I \cap A)) \to x \in ℝ^{*}$
86		supxrleub	$⊢ (Y \subseteq ℝ^{} \land x \in ℝ^{}) \to (sup (Y ℝ^{*} <) \leq x \leftrightarrow \forall y \in Y y \leq x)$
87	84 85 86	syl2anc	$⊢ (φ \land x \in (I \cap A)) \to (sup (Y ℝ^{*} <) \leq x \leftrightarrow \forall y \in Y y \leq x)$
88	87	adantr	$⊢ ((φ \land x \in (I \cap A)) \land \neg R < F (x)) \to (sup (Y ℝ^{*} <) \leq x \leftrightarrow \forall y \in Y y \leq x)$
89	83 88	mpbird	$⊢ ((φ \land x \in (I \cap A)) \land \neg R < F (x)) \to sup (Y ℝ^{*} <) \leq x$
90	8 89	eqbrtrid	$⊢ ((φ \land x \in (I \cap A)) \land \neg R < F (x)) \to S \leq x$
91	25	adantr	$⊢ ((φ \land x \in (I \cap A)) \land \neg R < F (x)) \to S \in ℝ^{*}$
92	85	adantr	$⊢ ((φ \land x \in (I \cap A)) \land \neg R < F (x)) \to x \in ℝ^{*}$
93	91 92	xrlenltd	$⊢ ((φ \land x \in (I \cap A)) \land \neg R < F (x)) \to (S \leq x \leftrightarrow \neg x < S)$
94	90 93	mpbid	$⊢ ((φ \land x \in (I \cap A)) \land \neg R < F (x)) \to \neg x < S$
95	31 94	condan	$⊢ (φ \land x \in (I \cap A)) \to R < F (x)$
96	18 95	jca	$⊢ (φ \land x \in (I \cap A)) \to (x \in A \land R < F (x))$
97	7	reqabi	$⊢ x \in Y \leftrightarrow (x \in A \land R < F (x))$
98	96 97	sylibr	$⊢ (φ \land x \in (I \cap A)) \to x \in Y$
99	98	ex	$⊢ φ \to (x \in (I \cap A) \to x \in Y)$
100	1 99	ralrimi	$⊢ φ \to \forall x \in (I \cap A) x \in Y$
101		nfcv	$⊢ \underline{Ⅎ} x (I \cap A)$
102		nfrab1	$⊢ \underline{Ⅎ} x \{x \in A \| R < F (x)\}$
103	7 102	nfcxfr	$⊢ \underline{Ⅎ} x Y$
104	101 103	dfss3f	$⊢ I \cap A \subseteq Y \leftrightarrow \forall x \in (I \cap A) x \in Y$
105	100 104	sylibr	$⊢ φ \to I \cap A \subseteq Y$
106	16 105	eqssd	$⊢ φ \to Y = I \cap A$

Metamath Proof Explorer

Theorem pimdecfgtioo

Proof