pimincfltioo

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

Proof

Step	Hyp	Ref	Expression
1		pimincfltioo.x	$⊢ Ⅎ x φ$
2		pimincfltioo.h	$⊢ Ⅎ y φ$
3		pimincfltioo.a	$⊢ φ \to A \subseteq ℝ$
4		pimincfltioo.f	$⊢ φ \to F : A ⟶ ℝ^{*}$
5		pimincfltioo.i	$⊢ φ \to \forall x \in A \forall y \in A (x \leq y \to F (x) \leq F (y))$
6		pimincfltioo.r	$⊢ φ \to R \in ℝ^{*}$
7		pimincfltioo.y	$⊢ Y = \{x \in A \| F (x) < R\}$
8		pimincfltioo.c	$⊢ S = sup (Y ℝ^{*} <)$
9		pimincfltioo.e	$⊢ φ \to \neg S \in Y$
10		pimincfltioo.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	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 F (x) < R) \to x < S$
32		simpr	$⊢ ((φ \land x \in (I \cap A)) \land \neg F (x) < R) \to \neg F (x) < R$
33	6	adantr	$⊢ (φ \land x \in (I \cap A)) \to R \in ℝ^{*}$
34	33	adantr	$⊢ ((φ \land x \in (I \cap A)) \land \neg F (x) < R) \to R \in ℝ^{*}$
35	4	adantr	$⊢ (φ \land x \in (I \cap A)) \to F : A ⟶ ℝ^{*}$
36	35 18	ffvelrnd	$⊢ (φ \land x \in (I \cap A)) \to F (x) \in ℝ^{*}$
37	36	adantr	$⊢ ((φ \land x \in (I \cap A)) \land \neg F (x) < R) \to F (x) \in ℝ^{*}$
38	34 37	xrlenltd	$⊢ ((φ \land x \in (I \cap A)) \land \neg F (x) < R) \to (R \leq F (x) \leftrightarrow \neg F (x) < R)$
39	32 38	mpbird	$⊢ ((φ \land x \in (I \cap A)) \land \neg F (x) < R) \to R \leq F (x)$
40		nfv	$⊢ Ⅎ y x \in (I \cap A)$
41	2 40	nfan	$⊢ Ⅎ y (φ \land x \in (I \cap A))$
42		nfv	$⊢ Ⅎ y R \leq F (x)$
43	41 42	nfan	$⊢ Ⅎ y ((φ \land x \in (I \cap A)) \land R \leq F (x))$
44		fveq2	$⊢ x = y \to F (x) = F (y)$
45	44	breq1d	$⊢ x = y \to (F (x) < R \leftrightarrow F (y) < R)$
46	45 7	elrab2	$⊢ y \in Y \leftrightarrow (y \in A \land F (y) < R)$
47	46	biimpi	$⊢ y \in Y \to (y \in A \land F (y) < R)$
48	47	simprd	$⊢ y \in Y \to F (y) < R$
49	48	adantl	$⊢ (φ \land y \in Y) \to F (y) < R$
50	49	ad5ant14	$⊢ ((((φ \land x \in (I \cap A)) \land R \leq F (x)) \land y \in Y) \land \neg y \leq x) \to F (y) < R$
51	3	adantr	$⊢ (φ \land x \in (I \cap A)) \to A \subseteq ℝ$
52	51 18	sseldd	$⊢ (φ \land x \in (I \cap A)) \to x \in ℝ$
53	52	ad3antrrr	$⊢ ((((φ \land x \in (I \cap A)) \land R \leq F (x)) \land y \in Y) \land \neg y \leq x) \to x \in ℝ$
54	14	sselda	$⊢ (φ \land y \in Y) \to y \in ℝ$
55	54	ad5ant14	$⊢ ((((φ \land x \in (I \cap A)) \land R \leq F (x)) \land y \in Y) \land \neg y \leq x) \to y \in ℝ$
56		simpr	$⊢ (((φ \land x \in (I \cap A)) \land y \in Y) \land \neg y \leq x) \to \neg y \leq x$
57	52	ad2antrr	$⊢ (((φ \land x \in (I \cap A)) \land y \in Y) \land \neg y \leq x) \to x \in ℝ$
58	54	ad4ant13	$⊢ (((φ \land x \in (I \cap A)) \land y \in Y) \land \neg y \leq x) \to y \in ℝ$
59	57 58	ltnled	$⊢ (((φ \land x \in (I \cap A)) \land y \in Y) \land \neg y \leq x) \to (x < y \leftrightarrow \neg y \leq x)$
60	56 59	mpbird	$⊢ (((φ \land x \in (I \cap A)) \land y \in Y) \land \neg y \leq x) \to x < y$
61	60	adantllr	$⊢ ((((φ \land x \in (I \cap A)) \land R \leq F (x)) \land y \in Y) \land \neg y \leq x) \to x < y$
62	53 55 61	ltled	$⊢ ((((φ \land x \in (I \cap A)) \land R \leq F (x)) \land y \in Y) \land \neg y \leq x) \to x \leq y$
63	33	ad3antrrr	$⊢ ((((φ \land x \in (I \cap A)) \land R \leq F (x)) \land y \in Y) \land x \leq y) \to R \in ℝ^{*}$
64	36	ad3antrrr	$⊢ ((((φ \land x \in (I \cap A)) \land R \leq F (x)) \land y \in Y) \land x \leq y) \to F (x) \in ℝ^{*}$
65	4	adantr	$⊢ (φ \land y \in Y) \to F : A ⟶ ℝ^{*}$
66	13	sselda	$⊢ (φ \land y \in Y) \to y \in A$
67	65 66	ffvelrnd	$⊢ (φ \land y \in Y) \to F (y) \in ℝ^{*}$
68	67	ad5ant14	$⊢ ((((φ \land x \in (I \cap A)) \land R \leq F (x)) \land y \in Y) \land x \leq y) \to F (y) \in ℝ^{*}$
69		simpllr	$⊢ ((((φ \land x \in (I \cap A)) \land R \leq F (x)) \land y \in Y) \land x \leq y) \to R \leq F (x)$
70		nfv	$⊢ Ⅎ w (((φ \land x \in (I \cap A)) \land y \in Y) \land x \leq y)$
71		nfv	$⊢ Ⅎ z (((φ \land x \in (I \cap A)) \land y \in Y) \land x \leq y)$
72		breq1	$⊢ w = x \to (w \leq z \leftrightarrow x \leq z)$
73		fveq2	$⊢ w = x \to F (w) = F (x)$
74	73	breq1d	$⊢ w = x \to (F (w) \leq F (z) \leftrightarrow F (x) \leq F (z))$
75	72 74	imbi12d	$⊢ w = x \to ((w \leq z \to F (w) \leq F (z)) \leftrightarrow (x \leq z \to F (x) \leq F (z)))$
76		breq2	$⊢ z = y \to (x \leq z \leftrightarrow x \leq y)$
77		fveq2	$⊢ z = y \to F (z) = F (y)$
78	77	breq2d	$⊢ z = y \to (F (x) \leq F (z) \leftrightarrow F (x) \leq F (y))$
79	76 78	imbi12d	$⊢ z = y \to ((x \leq z \to F (x) \leq F (z)) \leftrightarrow (x \leq y \to F (x) \leq F (y)))$
80	75 79	cbvral2vw	$⊢ \forall w \in A \forall z \in A (w \leq z \to F (w) \leq F (z)) \leftrightarrow \forall x \in A \forall y \in A (x \leq y \to F (x) \leq F (y))$
81	5 80	sylibr	$⊢ φ \to \forall w \in A \forall z \in A (w \leq z \to F (w) \leq F (z))$
82	81	ad3antrrr	$⊢ (((φ \land x \in (I \cap A)) \land y \in Y) \land x \leq y) \to \forall w \in A \forall z \in A (w \leq z \to F (w) \leq F (z))$
83	18	ad2antrr	$⊢ (((φ \land x \in (I \cap A)) \land y \in Y) \land x \leq y) \to x \in A$
84	66	ad4ant13	$⊢ (((φ \land x \in (I \cap A)) \land y \in Y) \land x \leq y) \to y \in A$
85		simpr	$⊢ (((φ \land x \in (I \cap A)) \land y \in Y) \land x \leq y) \to x \leq y$
86	70 71 82 83 84 85	dmrelrnrel	$⊢ (((φ \land x \in (I \cap A)) \land y \in Y) \land x \leq y) \to F (x) \leq F (y)$
87	86	adantllr	$⊢ ((((φ \land x \in (I \cap A)) \land R \leq F (x)) \land y \in Y) \land x \leq y) \to F (x) \leq F (y)$
88	63 64 68 69 87	xrletrd	$⊢ ((((φ \land x \in (I \cap A)) \land R \leq F (x)) \land y \in Y) \land x \leq y) \to R \leq F (y)$
89	63 68	xrlenltd	$⊢ ((((φ \land x \in (I \cap A)) \land R \leq F (x)) \land y \in Y) \land x \leq y) \to (R \leq F (y) \leftrightarrow \neg F (y) < R)$
90	88 89	mpbid	$⊢ ((((φ \land x \in (I \cap A)) \land R \leq F (x)) \land y \in Y) \land x \leq y) \to \neg F (y) < R$
91	62 90	syldan	$⊢ ((((φ \land x \in (I \cap A)) \land R \leq F (x)) \land y \in Y) \land \neg y \leq x) \to \neg F (y) < R$
92	50 91	condan	$⊢ (((φ \land x \in (I \cap A)) \land R \leq F (x)) \land y \in Y) \to y \leq x$
93	92	ex	$⊢ ((φ \land x \in (I \cap A)) \land R \leq F (x)) \to (y \in Y \to y \leq x)$
94	43 93	ralrimi	$⊢ ((φ \land x \in (I \cap A)) \land R \leq F (x)) \to \forall y \in Y y \leq x$
95	39 94	syldan	$⊢ ((φ \land x \in (I \cap A)) \land \neg F (x) < R) \to \forall y \in Y y \leq x$
96	22	adantr	$⊢ (φ \land x \in (I \cap A)) \to Y \subseteq ℝ^{*}$
97	21 52	sseldi	$⊢ (φ \land x \in (I \cap A)) \to x \in ℝ^{*}$
98		supxrleub	$⊢ (Y \subseteq ℝ^{} \land x \in ℝ^{}) \to (sup (Y ℝ^{*} <) \leq x \leftrightarrow \forall y \in Y y \leq x)$
99	96 97 98	syl2anc	$⊢ (φ \land x \in (I \cap A)) \to (sup (Y ℝ^{*} <) \leq x \leftrightarrow \forall y \in Y y \leq x)$
100	99	adantr	$⊢ ((φ \land x \in (I \cap A)) \land \neg F (x) < R) \to (sup (Y ℝ^{*} <) \leq x \leftrightarrow \forall y \in Y y \leq x)$
101	95 100	mpbird	$⊢ ((φ \land x \in (I \cap A)) \land \neg F (x) < R) \to sup (Y ℝ^{*} <) \leq x$
102	8 101	eqbrtrid	$⊢ ((φ \land x \in (I \cap A)) \land \neg F (x) < R) \to S \leq x$
103	25	adantr	$⊢ ((φ \land x \in (I \cap A)) \land \neg F (x) < R) \to S \in ℝ^{*}$
104	97	adantr	$⊢ ((φ \land x \in (I \cap A)) \land \neg F (x) < R) \to x \in ℝ^{*}$
105	103 104	xrlenltd	$⊢ ((φ \land x \in (I \cap A)) \land \neg F (x) < R) \to (S \leq x \leftrightarrow \neg x < S)$
106	102 105	mpbid	$⊢ ((φ \land x \in (I \cap A)) \land \neg F (x) < R) \to \neg x < S$
107	31 106	condan	$⊢ (φ \land x \in (I \cap A)) \to F (x) < R$
108	18 107	jca	$⊢ (φ \land x \in (I \cap A)) \to (x \in A \land F (x) < R)$
109	7	rabeq2i	$⊢ x \in Y \leftrightarrow (x \in A \land F (x) < R)$
110	108 109	sylibr	$⊢ (φ \land x \in (I \cap A)) \to x \in Y$
111	110	ex	$⊢ φ \to (x \in (I \cap A) \to x \in Y)$
112	1 111	ralrimi	$⊢ φ \to \forall x \in (I \cap A) x \in Y$
113		nfcv	$⊢ \underline{Ⅎ} x (I \cap A)$
114		nfrab1	$⊢ \underline{Ⅎ} x \{x \in A \| F (x) < R\}$
115	7 114	nfcxfr	$⊢ \underline{Ⅎ} x Y$
116	113 115	dfss3f	$⊢ I \cap A \subseteq Y \leftrightarrow \forall x \in (I \cap A) x \in Y$
117	112 116	sylibr	$⊢ φ \to I \cap A \subseteq Y$
118	16 117	eqssd	$⊢ φ \to Y = I \cap A$

Metamath Proof Explorer

Theorem pimincfltioo

Proof