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

Proof

Step	Hyp	Ref	Expression
1		pimdecfgtioo.x	⊢ Ⅎ 𝑥 𝜑
2		pimdecfgtioo.h	⊢ Ⅎ 𝑦 𝜑
3		pimdecfgtioo.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
4		pimdecfgtioo.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
5		pimdecfgtioo.d	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
6		pimdecfgtioo.r	⊢ ( 𝜑 → 𝑅 ∈ ℝ* )
7		pimdecfgtioo.y	⊢ 𝑌 = { 𝑥 ∈ 𝐴 ∣ 𝑅 < ( 𝐹 ‘ 𝑥 ) }
8		pimdecfgtioo.c	⊢ 𝑆 = sup ( 𝑌 , ℝ* , < )
9		pimdecfgtioo.e	⊢ ( 𝜑 → ¬ 𝑆 ∈ 𝑌 )
10		pimdecfgtioo.i	⊢ 𝐼 = ( -∞ (,) 𝑆 )
11		ssrab2	⊢ { 𝑥 ∈ 𝐴 ∣ 𝑅 < ( 𝐹 ‘ 𝑥 ) } ⊆ 𝐴
12	7 11	eqsstri	⊢ 𝑌 ⊆ 𝐴
13	12	a1i	⊢ ( 𝜑 → 𝑌 ⊆ 𝐴 )
14	13 3	sstrd	⊢ ( 𝜑 → 𝑌 ⊆ ℝ )
15	14 8 9 10	ressioosup	⊢ ( 𝜑 → 𝑌 ⊆ 𝐼 )
16	15 13	ssind	⊢ ( 𝜑 → 𝑌 ⊆ ( 𝐼 ∩ 𝐴 ) )
17		elinel2	⊢ ( 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) → 𝑥 ∈ 𝐴 )
18	17	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝑥 ∈ 𝐴 )
19		mnfxr	⊢ -∞ ∈ ℝ*
20	19	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → -∞ ∈ ℝ* )
21		ressxr	⊢ ℝ ⊆ ℝ*
22	14 21	sstrdi	⊢ ( 𝜑 → 𝑌 ⊆ ℝ* )
23	22	supxrcld	⊢ ( 𝜑 → sup ( 𝑌 , ℝ* , < ) ∈ ℝ* )
24	8 23	eqeltrid	⊢ ( 𝜑 → 𝑆 ∈ ℝ* )
25	24	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝑆 ∈ ℝ* )
26		elinel1	⊢ ( 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) → 𝑥 ∈ 𝐼 )
27	26 10	eleqtrdi	⊢ ( 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) → 𝑥 ∈ ( -∞ (,) 𝑆 ) )
28	27	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝑥 ∈ ( -∞ (,) 𝑆 ) )
29		iooltub	⊢ ( ( -∞ ∈ ℝ* ∧ 𝑆 ∈ ℝ* ∧ 𝑥 ∈ ( -∞ (,) 𝑆 ) ) → 𝑥 < 𝑆 )
30	20 25 28 29	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝑥 < 𝑆 )
31	30	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ¬ 𝑅 < ( 𝐹 ‘ 𝑥 ) ) → 𝑥 < 𝑆 )
32		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ¬ 𝑅 < ( 𝐹 ‘ 𝑥 ) ) → ¬ 𝑅 < ( 𝐹 ‘ 𝑥 ) )
33	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝐹 : 𝐴 ⟶ ℝ* )
34	33 18	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ* )
35	34	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ¬ 𝑅 < ( 𝐹 ‘ 𝑥 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ* )
36	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝑅 ∈ ℝ* )
37	36	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ¬ 𝑅 < ( 𝐹 ‘ 𝑥 ) ) → 𝑅 ∈ ℝ* )
38	35 37	xrlenltd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ¬ 𝑅 < ( 𝐹 ‘ 𝑥 ) ) → ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑅 ↔ ¬ 𝑅 < ( 𝐹 ‘ 𝑥 ) ) )
39	32 38	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ¬ 𝑅 < ( 𝐹 ‘ 𝑥 ) ) → ( 𝐹 ‘ 𝑥 ) ≤ 𝑅 )
40		nfv	⊢ Ⅎ 𝑦 𝑥 ∈ ( 𝐼 ∩ 𝐴 )
41	2 40	nfan	⊢ Ⅎ 𝑦 ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) )
42		nfv	⊢ Ⅎ 𝑦 ( 𝐹 ‘ 𝑥 ) ≤ 𝑅
43	41 42	nfan	⊢ Ⅎ 𝑦 ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑥 ) ≤ 𝑅 )
44		fveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
45	44	breq2d	⊢ ( 𝑥 = 𝑦 → ( 𝑅 < ( 𝐹 ‘ 𝑥 ) ↔ 𝑅 < ( 𝐹 ‘ 𝑦 ) ) )
46	45 7	elrab2	⊢ ( 𝑦 ∈ 𝑌 ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑅 < ( 𝐹 ‘ 𝑦 ) ) )
47	46	biimpi	⊢ ( 𝑦 ∈ 𝑌 → ( 𝑦 ∈ 𝐴 ∧ 𝑅 < ( 𝐹 ‘ 𝑦 ) ) )
48	47	simprd	⊢ ( 𝑦 ∈ 𝑌 → 𝑅 < ( 𝐹 ‘ 𝑦 ) )
49	48	ad2antlr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑥 ) ≤ 𝑅 ) ∧ 𝑦 ∈ 𝑌 ) ∧ ¬ 𝑦 ≤ 𝑥 ) → 𝑅 < ( 𝐹 ‘ 𝑦 ) )
50	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝐴 ⊆ ℝ )
51	50 18	sseldd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝑥 ∈ ℝ )
52	51	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ ¬ 𝑦 ≤ 𝑥 ) → 𝑥 ∈ ℝ )
53	14	sselda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝑦 ∈ ℝ )
54	53	ad4ant13	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ ¬ 𝑦 ≤ 𝑥 ) → 𝑦 ∈ ℝ )
55		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ ¬ 𝑦 ≤ 𝑥 ) → ¬ 𝑦 ≤ 𝑥 )
56	52 54	ltnled	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ ¬ 𝑦 ≤ 𝑥 ) → ( 𝑥 < 𝑦 ↔ ¬ 𝑦 ≤ 𝑥 ) )
57	55 56	mpbird	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ ¬ 𝑦 ≤ 𝑥 ) → 𝑥 < 𝑦 )
58	52 54 57	ltled	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ ¬ 𝑦 ≤ 𝑥 ) → 𝑥 ≤ 𝑦 )
59	58	adantllr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑥 ) ≤ 𝑅 ) ∧ 𝑦 ∈ 𝑌 ) ∧ ¬ 𝑦 ≤ 𝑥 ) → 𝑥 ≤ 𝑦 )
60	4	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝐹 : 𝐴 ⟶ ℝ* )
61	13	sselda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝑦 ∈ 𝐴 )
62	60 61	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ* )
63	62	ad5ant14	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑥 ) ≤ 𝑅 ) ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑥 ≤ 𝑦 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ* )
64	34	ad3antrrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑥 ) ≤ 𝑅 ) ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑥 ≤ 𝑦 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ* )
65	36	ad3antrrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑥 ) ≤ 𝑅 ) ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑥 ≤ 𝑦 ) → 𝑅 ∈ ℝ* )
66		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑥 ≤ 𝑦 ) → 𝑥 ≤ 𝑦 )
67		rspa	⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
68	5 17 67	syl2an	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
69	68	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑥 ≤ 𝑦 ) → ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
70	61	ad4ant13	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑥 ≤ 𝑦 ) → 𝑦 ∈ 𝐴 )
71		rspa	⊢ ( ( ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
72	69 70 71	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑥 ≤ 𝑦 ) → ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
73	66 72	mpd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑥 ≤ 𝑦 ) → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) )
74	73	adantllr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑥 ) ≤ 𝑅 ) ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑥 ≤ 𝑦 ) → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑥 ) )
75		simpllr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑥 ) ≤ 𝑅 ) ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑥 ≤ 𝑦 ) → ( 𝐹 ‘ 𝑥 ) ≤ 𝑅 )
76	63 64 65 74 75	xrletrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑥 ) ≤ 𝑅 ) ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑥 ≤ 𝑦 ) → ( 𝐹 ‘ 𝑦 ) ≤ 𝑅 )
77	63 65	xrlenltd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑥 ) ≤ 𝑅 ) ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑥 ≤ 𝑦 ) → ( ( 𝐹 ‘ 𝑦 ) ≤ 𝑅 ↔ ¬ 𝑅 < ( 𝐹 ‘ 𝑦 ) ) )
78	76 77	mpbid	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑥 ) ≤ 𝑅 ) ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑥 ≤ 𝑦 ) → ¬ 𝑅 < ( 𝐹 ‘ 𝑦 ) )
79	59 78	syldan	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑥 ) ≤ 𝑅 ) ∧ 𝑦 ∈ 𝑌 ) ∧ ¬ 𝑦 ≤ 𝑥 ) → ¬ 𝑅 < ( 𝐹 ‘ 𝑦 ) )
80	49 79	condan	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑥 ) ≤ 𝑅 ) ∧ 𝑦 ∈ 𝑌 ) → 𝑦 ≤ 𝑥 )
81	80	ex	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑥 ) ≤ 𝑅 ) → ( 𝑦 ∈ 𝑌 → 𝑦 ≤ 𝑥 ) )
82	43 81	ralrimi	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑥 ) ≤ 𝑅 ) → ∀ 𝑦 ∈ 𝑌 𝑦 ≤ 𝑥 )
83	39 82	syldan	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ¬ 𝑅 < ( 𝐹 ‘ 𝑥 ) ) → ∀ 𝑦 ∈ 𝑌 𝑦 ≤ 𝑥 )
84	22	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝑌 ⊆ ℝ* )
85	21 51	sselid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝑥 ∈ ℝ* )
86		supxrleub	⊢ ( ( 𝑌 ⊆ ℝ* ∧ 𝑥 ∈ ℝ* ) → ( sup ( 𝑌 , ℝ* , < ) ≤ 𝑥 ↔ ∀ 𝑦 ∈ 𝑌 𝑦 ≤ 𝑥 ) )
87	84 85 86	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → ( sup ( 𝑌 , ℝ* , < ) ≤ 𝑥 ↔ ∀ 𝑦 ∈ 𝑌 𝑦 ≤ 𝑥 ) )
88	87	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ¬ 𝑅 < ( 𝐹 ‘ 𝑥 ) ) → ( sup ( 𝑌 , ℝ* , < ) ≤ 𝑥 ↔ ∀ 𝑦 ∈ 𝑌 𝑦 ≤ 𝑥 ) )
89	83 88	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ¬ 𝑅 < ( 𝐹 ‘ 𝑥 ) ) → sup ( 𝑌 , ℝ* , < ) ≤ 𝑥 )
90	8 89	eqbrtrid	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ¬ 𝑅 < ( 𝐹 ‘ 𝑥 ) ) → 𝑆 ≤ 𝑥 )
91	25	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ¬ 𝑅 < ( 𝐹 ‘ 𝑥 ) ) → 𝑆 ∈ ℝ* )
92	85	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ¬ 𝑅 < ( 𝐹 ‘ 𝑥 ) ) → 𝑥 ∈ ℝ* )
93	91 92	xrlenltd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ¬ 𝑅 < ( 𝐹 ‘ 𝑥 ) ) → ( 𝑆 ≤ 𝑥 ↔ ¬ 𝑥 < 𝑆 ) )
94	90 93	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ¬ 𝑅 < ( 𝐹 ‘ 𝑥 ) ) → ¬ 𝑥 < 𝑆 )
95	31 94	condan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝑅 < ( 𝐹 ‘ 𝑥 ) )
96	18 95	jca	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑅 < ( 𝐹 ‘ 𝑥 ) ) )
97	7	rabeq2i	⊢ ( 𝑥 ∈ 𝑌 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑅 < ( 𝐹 ‘ 𝑥 ) ) )
98	96 97	sylibr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝑥 ∈ 𝑌 )
99	98	ex	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) → 𝑥 ∈ 𝑌 ) )
100	1 99	ralrimi	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) 𝑥 ∈ 𝑌 )
101		nfcv	⊢ Ⅎ 𝑥 ( 𝐼 ∩ 𝐴 )
102		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ 𝑅 < ( 𝐹 ‘ 𝑥 ) }
103	7 102	nfcxfr	⊢ Ⅎ 𝑥 𝑌
104	101 103	dfss3f	⊢ ( ( 𝐼 ∩ 𝐴 ) ⊆ 𝑌 ↔ ∀ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) 𝑥 ∈ 𝑌 )
105	100 104	sylibr	⊢ ( 𝜑 → ( 𝐼 ∩ 𝐴 ) ⊆ 𝑌 )
106	16 105	eqssd	⊢ ( 𝜑 → 𝑌 = ( 𝐼 ∩ 𝐴 ) )