Theorem 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	⊢ Ⅎ 𝑥 𝜑
	pimincfltioc.h	⊢ Ⅎ 𝑦 𝜑
	pimincfltioc.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	pimincfltioc.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
	pimincfltioc.i	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
	pimincfltioc.r	⊢ ( 𝜑 → 𝑅 ∈ ℝ* )
	pimincfltioc.y	⊢ 𝑌 = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑅 }
	pimincfltioc.c	⊢ 𝑆 = sup ( 𝑌 , ℝ* , < )
	pimincfltioc.e	⊢ ( 𝜑 → 𝑆 ∈ 𝑌 )
	pimincfltioc.d	⊢ 𝐼 = ( -∞ (,] 𝑆 )
Assertion	pimincfltioc	⊢ ( 𝜑 → 𝑌 = ( 𝐼 ∩ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		pimincfltioc.x	⊢ Ⅎ 𝑥 𝜑
2		pimincfltioc.h	⊢ Ⅎ 𝑦 𝜑
3		pimincfltioc.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
4		pimincfltioc.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
5		pimincfltioc.i	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
6		pimincfltioc.r	⊢ ( 𝜑 → 𝑅 ∈ ℝ* )
7		pimincfltioc.y	⊢ 𝑌 = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑅 }
8		pimincfltioc.c	⊢ 𝑆 = sup ( 𝑌 , ℝ* , < )
9		pimincfltioc.e	⊢ ( 𝜑 → 𝑆 ∈ 𝑌 )
10		pimincfltioc.d	⊢ 𝐼 = ( -∞ (,] 𝑆 )
11		ssrab2	⊢ { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑅 } ⊆ 𝐴
12	7 11	eqsstri	⊢ 𝑌 ⊆ 𝐴
13	12	a1i	⊢ ( 𝜑 → 𝑌 ⊆ 𝐴 )
14	13 3	sstrd	⊢ ( 𝜑 → 𝑌 ⊆ ℝ )
15	14 8 9 10	ressiocsup	⊢ ( 𝜑 → 𝑌 ⊆ 𝐼 )
16	15 13	ssind	⊢ ( 𝜑 → 𝑌 ⊆ ( 𝐼 ∩ 𝐴 ) )
17		elinel2	⊢ ( 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) → 𝑥 ∈ 𝐴 )
18	17	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝑥 ∈ 𝐴 )
19	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝐹 : 𝐴 ⟶ ℝ* )
20	19 18	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ* )
21	12 9	sselid	⊢ ( 𝜑 → 𝑆 ∈ 𝐴 )
22	4 21	ffvelcdmd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑆 ) ∈ ℝ* )
23	22	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → ( 𝐹 ‘ 𝑆 ) ∈ ℝ* )
24	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝑅 ∈ ℝ* )
25		eleq1w	⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ ( 𝐼 ∩ 𝐴 ) ↔ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) )
26	25	anbi2d	⊢ ( 𝑧 = 𝑥 → ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐼 ∩ 𝐴 ) ) ↔ ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ) )
27		fveq2	⊢ ( 𝑧 = 𝑥 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) )
28	27	breq1d	⊢ ( 𝑧 = 𝑥 → ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑆 ) ↔ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑆 ) ) )
29	26 28	imbi12d	⊢ ( 𝑧 = 𝑥 → ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐼 ∩ 𝐴 ) ) → ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑆 ) ) ↔ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑆 ) ) ) )
30		nfv	⊢ Ⅎ 𝑥 𝑧 ∈ ( 𝐼 ∩ 𝐴 )
31	1 30	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑧 ∈ ( 𝐼 ∩ 𝐴 ) )
32		nfv	⊢ Ⅎ 𝑦 𝑧 ∈ ( 𝐼 ∩ 𝐴 )
33	2 32	nfan	⊢ Ⅎ 𝑦 ( 𝜑 ∧ 𝑧 ∈ ( 𝐼 ∩ 𝐴 ) )
34	5	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐼 ∩ 𝐴 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
35		elinel2	⊢ ( 𝑧 ∈ ( 𝐼 ∩ 𝐴 ) → 𝑧 ∈ 𝐴 )
36	35	adantl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝑧 ∈ 𝐴 )
37	21	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝑆 ∈ 𝐴 )
38		mnfxr	⊢ -∞ ∈ ℝ*
39	38	a1i	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐼 ∩ 𝐴 ) ) → -∞ ∈ ℝ* )
40		ressxr	⊢ ℝ ⊆ ℝ*
41	14 9	sseldd	⊢ ( 𝜑 → 𝑆 ∈ ℝ )
42	40 41	sselid	⊢ ( 𝜑 → 𝑆 ∈ ℝ* )
43	42	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝑆 ∈ ℝ* )
44		elinel1	⊢ ( 𝑧 ∈ ( 𝐼 ∩ 𝐴 ) → 𝑧 ∈ 𝐼 )
45	44 10	eleqtrdi	⊢ ( 𝑧 ∈ ( 𝐼 ∩ 𝐴 ) → 𝑧 ∈ ( -∞ (,] 𝑆 ) )
46	45	adantl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝑧 ∈ ( -∞ (,] 𝑆 ) )
47		iocleub	⊢ ( ( -∞ ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ 𝑧 ∈ ( -∞ (,] 𝑆 ) ) → 𝑧 ≤ 𝑆 )
48	39 43 46 47	syl3anc	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝑧 ≤ 𝑆 )
49	31 33 34 36 37 48	dmrelrnrel	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐼 ∩ 𝐴 ) ) → ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑆 ) )
50	29 49	chvarvv	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑆 ) )
51		fveq2	⊢ ( 𝑥 = 𝑆 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑆 ) )
52	51	breq1d	⊢ ( 𝑥 = 𝑆 → ( ( 𝐹 ‘ 𝑥 ) < 𝑅 ↔ ( 𝐹 ‘ 𝑆 ) < 𝑅 ) )
53	52 7	elrab2	⊢ ( 𝑆 ∈ 𝑌 ↔ ( 𝑆 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑆 ) < 𝑅 ) )
54	9 53	sylib	⊢ ( 𝜑 → ( 𝑆 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑆 ) < 𝑅 ) )
55	54	simprd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑆 ) < 𝑅 )
56	55	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → ( 𝐹 ‘ 𝑆 ) < 𝑅 )
57	20 23 24 50 56	xrlelttrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) < 𝑅 )
58	18 57	jca	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) < 𝑅 ) )
59	7	reqabi	⊢ ( 𝑥 ∈ 𝑌 ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) < 𝑅 ) )
60	58 59	sylibr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝑥 ∈ 𝑌 )
61	60	ex	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) → 𝑥 ∈ 𝑌 ) )
62	1 61	ralrimi	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) 𝑥 ∈ 𝑌 )
63	30	nfci	⊢ Ⅎ 𝑥 ( 𝐼 ∩ 𝐴 )
64		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑅 }
65	7 64	nfcxfr	⊢ Ⅎ 𝑥 𝑌
66	63 65	dfss3f	⊢ ( ( 𝐼 ∩ 𝐴 ) ⊆ 𝑌 ↔ ∀ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) 𝑥 ∈ 𝑌 )
67	62 66	sylibr	⊢ ( 𝜑 → ( 𝐼 ∩ 𝐴 ) ⊆ 𝑌 )
68	16 67	eqssd	⊢ ( 𝜑 → 𝑌 = ( 𝐼 ∩ 𝐴 ) )