Theorem pimdecfgtioc

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

	Ref	Expression
Hypotheses	pimdecfgtioc.x	⊢ Ⅎ 𝑥 𝜑
	pimdecfgtioc.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	pimdecfgtioc.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
	pimdecfgtioc.i	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
	pimdecfgtioc.r	⊢ ( 𝜑 → 𝑅 ∈ ℝ* )
	pimdecfgtioc.y	⊢ 𝑌 = { 𝑥 ∈ 𝐴 ∣ 𝑅 < ( 𝐹 ‘ 𝑥 ) }
	pimdecfgtioc.c	⊢ 𝑆 = sup ( 𝑌 , ℝ* , < )
	pimdecfgtioc.e	⊢ ( 𝜑 → 𝑆 ∈ 𝑌 )
	pimdecfgtioc.d	⊢ 𝐼 = ( -∞ (,] 𝑆 )
Assertion	pimdecfgtioc	⊢ ( 𝜑 → 𝑌 = ( 𝐼 ∩ 𝐴 ) )

Proof

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