Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 pimincfltioo.x ⊢ Ⅎ 𝑥 𝜑
2 pimincfltioo.h ⊢ Ⅎ 𝑦 𝜑
3 pimincfltioo.a ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
4 pimincfltioo.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )
5 pimincfltioo.i ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
6 pimincfltioo.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ* )
7 pimincfltioo.y ⊢ 𝑌 = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑅 }
8 pimincfltioo.c ⊢ 𝑆 = sup ( 𝑌 , ℝ* , < )
9 pimincfltioo.e ⊢ ( 𝜑 → ¬ 𝑆 ∈ 𝑌 )
10 pimincfltioo.d ⊢ 𝐼 = ( -∞ (,) 𝑆 )
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 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝑅 ∈ ℝ* )
34 33 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) < 𝑅 ) → 𝑅 ∈ ℝ* )
35 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝐹 : 𝐴 ⟶ ℝ* )
36 35 18 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ* )
37 36 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) < 𝑅 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ* )
38 34 37 xrlenltd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) < 𝑅 ) → ( 𝑅 ≤ ( 𝐹 ‘ 𝑥 ) ↔ ¬ ( 𝐹 ‘ 𝑥 ) < 𝑅 ) )
39 32 38 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) < 𝑅 ) → 𝑅 ≤ ( 𝐹 ‘ 𝑥 ) )
40 nfv ⊢ Ⅎ 𝑦 𝑥 ∈ ( 𝐼 ∩ 𝐴 )
41 2 40 nfan ⊢ Ⅎ 𝑦 ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) )
42 nfv ⊢ Ⅎ 𝑦 𝑅 ≤ ( 𝐹 ‘ 𝑥 )
43 41 42 nfan ⊢ Ⅎ 𝑦 ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑅 ≤ ( 𝐹 ‘ 𝑥 ) )
44 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
45 44 breq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) < 𝑅 ↔ ( 𝐹 ‘ 𝑦 ) < 𝑅 ) )
46 45 7 elrab2 ⊢ ( 𝑦 ∈ 𝑌 ↔ ( 𝑦 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑦 ) < 𝑅 ) )
47 46 biimpi ⊢ ( 𝑦 ∈ 𝑌 → ( 𝑦 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑦 ) < 𝑅 ) )
48 47 simprd ⊢ ( 𝑦 ∈ 𝑌 → ( 𝐹 ‘ 𝑦 ) < 𝑅 )
49 48 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝐹 ‘ 𝑦 ) < 𝑅 )
50 49 ad5ant14 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑅 ≤ ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ ¬ 𝑦 ≤ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) < 𝑅 )
51 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝐴 ⊆ ℝ )
52 51 18 sseldd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝑥 ∈ ℝ )
53 52 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑅 ≤ ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ ¬ 𝑦 ≤ 𝑥 ) → 𝑥 ∈ ℝ )
54 14 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝑦 ∈ ℝ )
55 54 ad5ant14 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑅 ≤ ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ ¬ 𝑦 ≤ 𝑥 ) → 𝑦 ∈ ℝ )
56 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ ¬ 𝑦 ≤ 𝑥 ) → ¬ 𝑦 ≤ 𝑥 )
57 52 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ ¬ 𝑦 ≤ 𝑥 ) → 𝑥 ∈ ℝ )
58 54 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ ¬ 𝑦 ≤ 𝑥 ) → 𝑦 ∈ ℝ )
59 57 58 ltnled ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ ¬ 𝑦 ≤ 𝑥 ) → ( 𝑥 < 𝑦 ↔ ¬ 𝑦 ≤ 𝑥 ) )
60 56 59 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ ¬ 𝑦 ≤ 𝑥 ) → 𝑥 < 𝑦 )
61 60 adantllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑅 ≤ ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ ¬ 𝑦 ≤ 𝑥 ) → 𝑥 < 𝑦 )
62 53 55 61 ltled ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑅 ≤ ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ ¬ 𝑦 ≤ 𝑥 ) → 𝑥 ≤ 𝑦 )
63 33 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑅 ≤ ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑥 ≤ 𝑦 ) → 𝑅 ∈ ℝ* )
64 36 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑅 ≤ ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑥 ≤ 𝑦 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ* )
65 4 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝐹 : 𝐴 ⟶ ℝ* )
66 13 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝑦 ∈ 𝐴 )
67 65 66 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ* )
68 67 ad5ant14 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑅 ≤ ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑥 ≤ 𝑦 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ* )
69 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑅 ≤ ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑥 ≤ 𝑦 ) → 𝑅 ≤ ( 𝐹 ‘ 𝑥 ) )
70 nfv ⊢ Ⅎ 𝑤 ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑥 ≤ 𝑦 )
71 nfv ⊢ Ⅎ 𝑧 ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑥 ≤ 𝑦 )
72 breq1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 ≤ 𝑧 ↔ 𝑥 ≤ 𝑧 ) )
73 fveq2 ⊢ ( 𝑤 = 𝑥 → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑥 ) )
74 73 breq1d ⊢ ( 𝑤 = 𝑥 → ( ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑧 ) ) )
75 72 74 imbi12d ⊢ ( 𝑤 = 𝑥 → ( ( 𝑤 ≤ 𝑧 → ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ↔ ( 𝑥 ≤ 𝑧 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ) )
76 breq2 ⊢ ( 𝑧 = 𝑦 → ( 𝑥 ≤ 𝑧 ↔ 𝑥 ≤ 𝑦 ) )
77 fveq2 ⊢ ( 𝑧 = 𝑦 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑦 ) )
78 77 breq2d ⊢ ( 𝑧 = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
79 76 78 imbi12d ⊢ ( 𝑧 = 𝑦 → ( ( 𝑥 ≤ 𝑧 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ↔ ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) ) )
80 75 79 cbvral2vw ⊢ ( ∀ 𝑤 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑤 ≤ 𝑧 → ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
81 5 80 sylibr ⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑤 ≤ 𝑧 → ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) )
82 81 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑥 ≤ 𝑦 ) → ∀ 𝑤 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑤 ≤ 𝑧 → ( 𝐹 ‘ 𝑤 ) ≤ ( 𝐹 ‘ 𝑧 ) ) )
83 18 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑥 ≤ 𝑦 ) → 𝑥 ∈ 𝐴 )
84 66 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑥 ≤ 𝑦 ) → 𝑦 ∈ 𝐴 )
85 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑥 ≤ 𝑦 ) → 𝑥 ≤ 𝑦 )
86 70 71 82 83 84 85 dmrelrnrel ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑥 ≤ 𝑦 ) → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) )
87 86 adantllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑅 ≤ ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑥 ≤ 𝑦 ) → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) )
88 63 64 68 69 87 xrletrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑅 ≤ ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑥 ≤ 𝑦 ) → 𝑅 ≤ ( 𝐹 ‘ 𝑦 ) )
89 63 68 xrlenltd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑅 ≤ ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑥 ≤ 𝑦 ) → ( 𝑅 ≤ ( 𝐹 ‘ 𝑦 ) ↔ ¬ ( 𝐹 ‘ 𝑦 ) < 𝑅 ) )
90 88 89 mpbid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑅 ≤ ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑥 ≤ 𝑦 ) → ¬ ( 𝐹 ‘ 𝑦 ) < 𝑅 )
91 62 90 syldan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑅 ≤ ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑌 ) ∧ ¬ 𝑦 ≤ 𝑥 ) → ¬ ( 𝐹 ‘ 𝑦 ) < 𝑅 )
92 50 91 condan ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑅 ≤ ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑌 ) → 𝑦 ≤ 𝑥 )
93 92 ex ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑅 ≤ ( 𝐹 ‘ 𝑥 ) ) → ( 𝑦 ∈ 𝑌 → 𝑦 ≤ 𝑥 ) )
94 43 93 ralrimi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ 𝑅 ≤ ( 𝐹 ‘ 𝑥 ) ) → ∀ 𝑦 ∈ 𝑌 𝑦 ≤ 𝑥 )
95 39 94 syldan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) < 𝑅 ) → ∀ 𝑦 ∈ 𝑌 𝑦 ≤ 𝑥 )
96 22 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝑌 ⊆ ℝ* )
97 21 52 sselid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝑥 ∈ ℝ* )
98 supxrleub ⊢ ( ( 𝑌 ⊆ ℝ* ∧ 𝑥 ∈ ℝ* ) → ( sup ( 𝑌 , ℝ* , < ) ≤ 𝑥 ↔ ∀ 𝑦 ∈ 𝑌 𝑦 ≤ 𝑥 ) )
99 96 97 98 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → ( sup ( 𝑌 , ℝ* , < ) ≤ 𝑥 ↔ ∀ 𝑦 ∈ 𝑌 𝑦 ≤ 𝑥 ) )
100 99 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) < 𝑅 ) → ( sup ( 𝑌 , ℝ* , < ) ≤ 𝑥 ↔ ∀ 𝑦 ∈ 𝑌 𝑦 ≤ 𝑥 ) )
101 95 100 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) < 𝑅 ) → sup ( 𝑌 , ℝ* , < ) ≤ 𝑥 )
102 8 101 eqbrtrid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) < 𝑅 ) → 𝑆 ≤ 𝑥 )
103 25 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) < 𝑅 ) → 𝑆 ∈ ℝ* )
104 97 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) < 𝑅 ) → 𝑥 ∈ ℝ* )
105 103 104 xrlenltd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) < 𝑅 ) → ( 𝑆 ≤ 𝑥 ↔ ¬ 𝑥 < 𝑆 ) )
106 102 105 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) < 𝑅 ) → ¬ 𝑥 < 𝑆 )
107 31 106 condan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → ( 𝐹 ‘ 𝑥 ) < 𝑅 )
108 18 107 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) < 𝑅 ) )
109 7 rabeq2i ⊢ ( 𝑥 ∈ 𝑌 ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) < 𝑅 ) )
110 108 109 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) ) → 𝑥 ∈ 𝑌 )
111 110 ex ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) → 𝑥 ∈ 𝑌 ) )
112 1 111 ralrimi ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) 𝑥 ∈ 𝑌 )
113 nfcv ⊢ Ⅎ 𝑥 ( 𝐼 ∩ 𝐴 )
114 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) < 𝑅 }
115 7 114 nfcxfr ⊢ Ⅎ 𝑥 𝑌
116 113 115 dfss3f ⊢ ( ( 𝐼 ∩ 𝐴 ) ⊆ 𝑌 ↔ ∀ 𝑥 ∈ ( 𝐼 ∩ 𝐴 ) 𝑥 ∈ 𝑌 )
117 112 116 sylibr ⊢ ( 𝜑 → ( 𝐼 ∩ 𝐴 ) ⊆ 𝑌 )
118 16 117 eqssd ⊢ ( 𝜑 → 𝑌 = ( 𝐼 ∩ 𝐴 ) )