This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rpnnen1lem5

Description: Lemma for rpnnen1 . (Contributed by Mario Carneiro, 12-May-2013) (Revised by NM, 13-Aug-2021) (Proof modification is discouraged.)

Ref Expression
Hypotheses rpnnen1lem.1 ⊢ 𝑇 = { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 }
rpnnen1lem.2 ⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) )
rpnnen1lem.n ⊢ ℕ ∈ V
rpnnen1lem.q ⊢ ℚ ∈ V
Assertion rpnnen1lem5 ( 𝑥 ∈ ℝ → sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) = 𝑥 )

Proof

Step Hyp Ref Expression
1 rpnnen1lem.1 ⊢ 𝑇 = { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 }
2 rpnnen1lem.2 ⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) )
3 rpnnen1lem.n ⊢ ℕ ∈ V
4 rpnnen1lem.q ⊢ ℚ ∈ V
5 1 2 3 4 rpnnen1lem3 ⊢ ( 𝑥 ∈ ℝ → ∀ 𝑛 ∈ ran ( 𝐹 ‘ 𝑥 ) 𝑛 ≤ 𝑥 )
6 1 2 3 4 rpnnen1lem1 ⊢ ( 𝑥 ∈ ℝ → ( 𝐹 ‘ 𝑥 ) ∈ ( ℚ ↑m ℕ ) )
7 4 3 elmap ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( ℚ ↑m ℕ ) ↔ ( 𝐹 ‘ 𝑥 ) : ℕ ⟶ ℚ )
8 6 7 sylib ⊢ ( 𝑥 ∈ ℝ → ( 𝐹 ‘ 𝑥 ) : ℕ ⟶ ℚ )
9 frn ⊢ ( ( 𝐹 ‘ 𝑥 ) : ℕ ⟶ ℚ → ran ( 𝐹 ‘ 𝑥 ) ⊆ ℚ )
10 qssre ⊢ ℚ ⊆ ℝ
11 9 10 sstrdi ⊢ ( ( 𝐹 ‘ 𝑥 ) : ℕ ⟶ ℚ → ran ( 𝐹 ‘ 𝑥 ) ⊆ ℝ )
12 8 11 syl ⊢ ( 𝑥 ∈ ℝ → ran ( 𝐹 ‘ 𝑥 ) ⊆ ℝ )
13 1nn ⊢ 1 ∈ ℕ
14 13 ne0ii ⊢ ℕ ≠ ∅
15 fdm ⊢ ( ( 𝐹 ‘ 𝑥 ) : ℕ ⟶ ℚ → dom ( 𝐹 ‘ 𝑥 ) = ℕ )
16 15 neeq1d ⊢ ( ( 𝐹 ‘ 𝑥 ) : ℕ ⟶ ℚ → ( dom ( 𝐹 ‘ 𝑥 ) ≠ ∅ ↔ ℕ ≠ ∅ ) )
17 14 16 mpbiri ⊢ ( ( 𝐹 ‘ 𝑥 ) : ℕ ⟶ ℚ → dom ( 𝐹 ‘ 𝑥 ) ≠ ∅ )
18 dm0rn0 ⊢ ( dom ( 𝐹 ‘ 𝑥 ) = ∅ ↔ ran ( 𝐹 ‘ 𝑥 ) = ∅ )
19 18 necon3bii ⊢ ( dom ( 𝐹 ‘ 𝑥 ) ≠ ∅ ↔ ran ( 𝐹 ‘ 𝑥 ) ≠ ∅ )
20 17 19 sylib ⊢ ( ( 𝐹 ‘ 𝑥 ) : ℕ ⟶ ℚ → ran ( 𝐹 ‘ 𝑥 ) ≠ ∅ )
21 8 20 syl ⊢ ( 𝑥 ∈ ℝ → ran ( 𝐹 ‘ 𝑥 ) ≠ ∅ )
22 breq2 ⊢ ( 𝑦 = 𝑥 → ( 𝑛 ≤ 𝑦 ↔ 𝑛 ≤ 𝑥 ) )
23 22 ralbidv ⊢ ( 𝑦 = 𝑥 → ( ∀ 𝑛 ∈ ran ( 𝐹 ‘ 𝑥 ) 𝑛 ≤ 𝑦 ↔ ∀ 𝑛 ∈ ran ( 𝐹 ‘ 𝑥 ) 𝑛 ≤ 𝑥 ) )
24 23 rspcev ⊢ ( ( 𝑥 ∈ ℝ ∧ ∀ 𝑛 ∈ ran ( 𝐹 ‘ 𝑥 ) 𝑛 ≤ 𝑥 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ran ( 𝐹 ‘ 𝑥 ) 𝑛 ≤ 𝑦 )
25 5 24 mpdan ⊢ ( 𝑥 ∈ ℝ → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ran ( 𝐹 ‘ 𝑥 ) 𝑛 ≤ 𝑦 )
26 id ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ )
27 suprleub ⊢ ( ( ( ran ( 𝐹 ‘ 𝑥 ) ⊆ ℝ ∧ ran ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ran ( 𝐹 ‘ 𝑥 ) 𝑛 ≤ 𝑦 ) ∧ 𝑥 ∈ ℝ ) → ( sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ≤ 𝑥 ↔ ∀ 𝑛 ∈ ran ( 𝐹 ‘ 𝑥 ) 𝑛 ≤ 𝑥 ) )
28 12 21 25 26 27 syl31anc ⊢ ( 𝑥 ∈ ℝ → ( sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ≤ 𝑥 ↔ ∀ 𝑛 ∈ ran ( 𝐹 ‘ 𝑥 ) 𝑛 ≤ 𝑥 ) )
29 5 28 mpbird ⊢ ( 𝑥 ∈ ℝ → sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ≤ 𝑥 )
30 1 2 3 4 rpnnen1lem4 ⊢ ( 𝑥 ∈ ℝ → sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ∈ ℝ )
31 resubcl ⊢ ( ( 𝑥 ∈ ℝ ∧ sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ∈ ℝ ) → ( 𝑥 − sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ) ∈ ℝ )
32 30 31 mpdan ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 − sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ) ∈ ℝ )
33 32 adantr ⊢ ( ( 𝑥 ∈ ℝ ∧ sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) < 𝑥 ) → ( 𝑥 − sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ) ∈ ℝ )
34 posdif ⊢ ( ( sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) < 𝑥 ↔ 0 < ( 𝑥 − sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ) ) )
35 30 34 mpancom ⊢ ( 𝑥 ∈ ℝ → ( sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) < 𝑥 ↔ 0 < ( 𝑥 − sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ) ) )
36 35 biimpa ⊢ ( ( 𝑥 ∈ ℝ ∧ sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) < 𝑥 ) → 0 < ( 𝑥 − sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ) )
37 36 gt0ne0d ⊢ ( ( 𝑥 ∈ ℝ ∧ sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) < 𝑥 ) → ( 𝑥 − sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ) ≠ 0 )
38 33 37 rereccld ⊢ ( ( 𝑥 ∈ ℝ ∧ sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) < 𝑥 ) → ( 1 / ( 𝑥 − sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ) ) ∈ ℝ )
39 arch ⊢ ( ( 1 / ( 𝑥 − sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ) ) ∈ ℝ → ∃ 𝑘 ∈ ℕ ( 1 / ( 𝑥 − sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ) ) < 𝑘 )
40 38 39 syl ⊢ ( ( 𝑥 ∈ ℝ ∧ sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) < 𝑥 ) → ∃ 𝑘 ∈ ℕ ( 1 / ( 𝑥 − sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ) ) < 𝑘 )
41 40 ex ⊢ ( 𝑥 ∈ ℝ → ( sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) < 𝑥 → ∃ 𝑘 ∈ ℕ ( 1 / ( 𝑥 − sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ) ) < 𝑘 ) )
42 1 2 rpnnen1lem2 ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → sup ( 𝑇 , ℝ , < ) ∈ ℤ )
43 42 zred ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → sup ( 𝑇 , ℝ , < ) ∈ ℝ )
44 43 3adant3 ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ∧ ( 1 / ( 𝑥 − sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ) ) < 𝑘 ) → sup ( 𝑇 , ℝ , < ) ∈ ℝ )
45 44 ltp1d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ∧ ( 1 / ( 𝑥 − sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ) ) < 𝑘 ) → sup ( 𝑇 , ℝ , < ) < ( sup ( 𝑇 , ℝ , < ) + 1 ) )
46 33 36 jca ⊢ ( ( 𝑥 ∈ ℝ ∧ sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) < 𝑥 ) → ( ( 𝑥 − sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ) ∈ ℝ ∧ 0 < ( 𝑥 − sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ) ) )
47 nnre ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ )
48 nngt0 ⊢ ( 𝑘 ∈ ℕ → 0 < 𝑘 )
49 47 48 jca ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) )
50 ltrec1 ⊢ ( ( ( ( 𝑥 − sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ) ∈ ℝ ∧ 0 < ( 𝑥 − sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ) ) ∧ ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) ) → ( ( 1 / ( 𝑥 − sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ) ) < 𝑘 ↔ ( 1 / 𝑘 ) < ( 𝑥 − sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ) ) )
51 46 49 50 syl2an ⊢ ( ( ( 𝑥 ∈ ℝ ∧ sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) < 𝑥 ) ∧ 𝑘 ∈ ℕ ) → ( ( 1 / ( 𝑥 − sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ) ) < 𝑘 ↔ ( 1 / 𝑘 ) < ( 𝑥 − sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ) ) )
52 30 ad2antrr ⊢ ( ( ( 𝑥 ∈ ℝ ∧ sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) < 𝑥 ) ∧ 𝑘 ∈ ℕ ) → sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ∈ ℝ )
53 nnrecre ⊢ ( 𝑘 ∈ ℕ → ( 1 / 𝑘 ) ∈ ℝ )
54 53 adantl ⊢ ( ( ( 𝑥 ∈ ℝ ∧ sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) < 𝑥 ) ∧ 𝑘 ∈ ℕ ) → ( 1 / 𝑘 ) ∈ ℝ )
55 simpll ⊢ ( ( ( 𝑥 ∈ ℝ ∧ sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) < 𝑥 ) ∧ 𝑘 ∈ ℕ ) → 𝑥 ∈ ℝ )
56 52 54 55 ltaddsub2d ⊢ ( ( ( 𝑥 ∈ ℝ ∧ sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) < 𝑥 ) ∧ 𝑘 ∈ ℕ ) → ( ( sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) + ( 1 / 𝑘 ) ) < 𝑥 ↔ ( 1 / 𝑘 ) < ( 𝑥 − sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ) ) )
57 12 adantr ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ran ( 𝐹 ‘ 𝑥 ) ⊆ ℝ )
58 ffn ⊢ ( ( 𝐹 ‘ 𝑥 ) : ℕ ⟶ ℚ → ( 𝐹 ‘ 𝑥 ) Fn ℕ )
59 8 58 syl ⊢ ( 𝑥 ∈ ℝ → ( 𝐹 ‘ 𝑥 ) Fn ℕ )
60 fnfvelrn ⊢ ( ( ( 𝐹 ‘ 𝑥 ) Fn ℕ ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) ∈ ran ( 𝐹 ‘ 𝑥 ) )
61 59 60 sylan ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) ∈ ran ( 𝐹 ‘ 𝑥 ) )
62 57 61 sseldd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) ∈ ℝ )
63 30 adantr ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ∈ ℝ )
64 53 adantl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( 1 / 𝑘 ) ∈ ℝ )
65 12 21 25 3jca ⊢ ( 𝑥 ∈ ℝ → ( ran ( 𝐹 ‘ 𝑥 ) ⊆ ℝ ∧ ran ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ran ( 𝐹 ‘ 𝑥 ) 𝑛 ≤ 𝑦 ) )
66 65 adantr ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( ran ( 𝐹 ‘ 𝑥 ) ⊆ ℝ ∧ ran ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ran ( 𝐹 ‘ 𝑥 ) 𝑛 ≤ 𝑦 ) )
67 suprub ⊢ ( ( ( ran ( 𝐹 ‘ 𝑥 ) ⊆ ℝ ∧ ran ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ran ( 𝐹 ‘ 𝑥 ) 𝑛 ≤ 𝑦 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) ∈ ran ( 𝐹 ‘ 𝑥 ) ) → ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) ≤ sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) )
68 66 61 67 syl2anc ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) ≤ sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) )
69 62 63 64 68 leadd1dd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) + ( 1 / 𝑘 ) ) ≤ ( sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) + ( 1 / 𝑘 ) ) )
70 62 64 readdcld ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) + ( 1 / 𝑘 ) ) ∈ ℝ )
71 readdcl ⊢ ( ( sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ∈ ℝ ∧ ( 1 / 𝑘 ) ∈ ℝ ) → ( sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) + ( 1 / 𝑘 ) ) ∈ ℝ )
72 30 53 71 syl2an ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) + ( 1 / 𝑘 ) ) ∈ ℝ )
73 simpl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → 𝑥 ∈ ℝ )
74 lelttr ⊢ ( ( ( ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) + ( 1 / 𝑘 ) ) ∈ ℝ ∧ ( sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) + ( 1 / 𝑘 ) ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ( ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) + ( 1 / 𝑘 ) ) ≤ ( sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) + ( 1 / 𝑘 ) ) ∧ ( sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) + ( 1 / 𝑘 ) ) < 𝑥 ) → ( ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) + ( 1 / 𝑘 ) ) < 𝑥 ) )
75 74 expd ⊢ ( ( ( ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) + ( 1 / 𝑘 ) ) ∈ ℝ ∧ ( sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) + ( 1 / 𝑘 ) ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) + ( 1 / 𝑘 ) ) ≤ ( sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) + ( 1 / 𝑘 ) ) → ( ( sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) + ( 1 / 𝑘 ) ) < 𝑥 → ( ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) + ( 1 / 𝑘 ) ) < 𝑥 ) ) )
76 70 72 73 75 syl3anc ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( ( ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) + ( 1 / 𝑘 ) ) ≤ ( sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) + ( 1 / 𝑘 ) ) → ( ( sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) + ( 1 / 𝑘 ) ) < 𝑥 → ( ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) + ( 1 / 𝑘 ) ) < 𝑥 ) ) )
77 69 76 mpd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( ( sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) + ( 1 / 𝑘 ) ) < 𝑥 → ( ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) + ( 1 / 𝑘 ) ) < 𝑥 ) )
78 77 adantlr ⊢ ( ( ( 𝑥 ∈ ℝ ∧ sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) < 𝑥 ) ∧ 𝑘 ∈ ℕ ) → ( ( sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) + ( 1 / 𝑘 ) ) < 𝑥 → ( ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) + ( 1 / 𝑘 ) ) < 𝑥 ) )
79 56 78 sylbird ⊢ ( ( ( 𝑥 ∈ ℝ ∧ sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) < 𝑥 ) ∧ 𝑘 ∈ ℕ ) → ( ( 1 / 𝑘 ) < ( 𝑥 − sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ) → ( ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) + ( 1 / 𝑘 ) ) < 𝑥 ) )
80 51 79 sylbid ⊢ ( ( ( 𝑥 ∈ ℝ ∧ sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) < 𝑥 ) ∧ 𝑘 ∈ ℕ ) → ( ( 1 / ( 𝑥 − sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ) ) < 𝑘 → ( ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) + ( 1 / 𝑘 ) ) < 𝑥 ) )
81 42 peano2zd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( sup ( 𝑇 , ℝ , < ) + 1 ) ∈ ℤ )
82 oveq1 ⊢ ( 𝑛 = ( sup ( 𝑇 , ℝ , < ) + 1 ) → ( 𝑛 / 𝑘 ) = ( ( sup ( 𝑇 , ℝ , < ) + 1 ) / 𝑘 ) )
83 82 breq1d ⊢ ( 𝑛 = ( sup ( 𝑇 , ℝ , < ) + 1 ) → ( ( 𝑛 / 𝑘 ) < 𝑥 ↔ ( ( sup ( 𝑇 , ℝ , < ) + 1 ) / 𝑘 ) < 𝑥 ) )
84 83 1 elrab2 ⊢ ( ( sup ( 𝑇 , ℝ , < ) + 1 ) ∈ 𝑇 ↔ ( ( sup ( 𝑇 , ℝ , < ) + 1 ) ∈ ℤ ∧ ( ( sup ( 𝑇 , ℝ , < ) + 1 ) / 𝑘 ) < 𝑥 ) )
85 84 biimpri ⊢ ( ( ( sup ( 𝑇 , ℝ , < ) + 1 ) ∈ ℤ ∧ ( ( sup ( 𝑇 , ℝ , < ) + 1 ) / 𝑘 ) < 𝑥 ) → ( sup ( 𝑇 , ℝ , < ) + 1 ) ∈ 𝑇 )
86 81 85 sylan ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ ( ( sup ( 𝑇 , ℝ , < ) + 1 ) / 𝑘 ) < 𝑥 ) → ( sup ( 𝑇 , ℝ , < ) + 1 ) ∈ 𝑇 )
87 ssrab2 ⊢ { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 } ⊆ ℤ
88 1 87 eqsstri ⊢ 𝑇 ⊆ ℤ
89 zssre ⊢ ℤ ⊆ ℝ
90 88 89 sstri ⊢ 𝑇 ⊆ ℝ
91 90 a1i ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → 𝑇 ⊆ ℝ )
92 remulcl ⊢ ( ( 𝑘 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑘 · 𝑥 ) ∈ ℝ )
93 92 ancoms ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( 𝑘 · 𝑥 ) ∈ ℝ )
94 47 93 sylan2 ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( 𝑘 · 𝑥 ) ∈ ℝ )
95 btwnz ⊢ ( ( 𝑘 · 𝑥 ) ∈ ℝ → ( ∃ 𝑛 ∈ ℤ 𝑛 < ( 𝑘 · 𝑥 ) ∧ ∃ 𝑛 ∈ ℤ ( 𝑘 · 𝑥 ) < 𝑛 ) )
96 95 simpld ⊢ ( ( 𝑘 · 𝑥 ) ∈ ℝ → ∃ 𝑛 ∈ ℤ 𝑛 < ( 𝑘 · 𝑥 ) )
97 94 96 syl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ∃ 𝑛 ∈ ℤ 𝑛 < ( 𝑘 · 𝑥 ) )
98 zre ⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℝ )
99 98 adantl ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → 𝑛 ∈ ℝ )
100 simpll ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → 𝑥 ∈ ℝ )
101 49 ad2antlr ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) )
102 ltdivmul ⊢ ( ( 𝑛 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) ) → ( ( 𝑛 / 𝑘 ) < 𝑥 ↔ 𝑛 < ( 𝑘 · 𝑥 ) ) )
103 99 100 101 102 syl3anc ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → ( ( 𝑛 / 𝑘 ) < 𝑥 ↔ 𝑛 < ( 𝑘 · 𝑥 ) ) )
104 103 rexbidva ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℤ ( 𝑛 / 𝑘 ) < 𝑥 ↔ ∃ 𝑛 ∈ ℤ 𝑛 < ( 𝑘 · 𝑥 ) ) )
105 97 104 mpbird ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ∃ 𝑛 ∈ ℤ ( 𝑛 / 𝑘 ) < 𝑥 )
106 rabn0 ⊢ ( { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 } ≠ ∅ ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 / 𝑘 ) < 𝑥 )
107 105 106 sylibr ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 } ≠ ∅ )
108 1 neeq1i ⊢ ( 𝑇 ≠ ∅ ↔ { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 } ≠ ∅ )
109 107 108 sylibr ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → 𝑇 ≠ ∅ )
110 1 reqabi ⊢ ( 𝑛 ∈ 𝑇 ↔ ( 𝑛 ∈ ℤ ∧ ( 𝑛 / 𝑘 ) < 𝑥 ) )
111 47 ad2antlr ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → 𝑘 ∈ ℝ )
112 111 100 92 syl2anc ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → ( 𝑘 · 𝑥 ) ∈ ℝ )
113 ltle ⊢ ( ( 𝑛 ∈ ℝ ∧ ( 𝑘 · 𝑥 ) ∈ ℝ ) → ( 𝑛 < ( 𝑘 · 𝑥 ) → 𝑛 ≤ ( 𝑘 · 𝑥 ) ) )
114 99 112 113 syl2anc ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → ( 𝑛 < ( 𝑘 · 𝑥 ) → 𝑛 ≤ ( 𝑘 · 𝑥 ) ) )
115 103 114 sylbid ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → ( ( 𝑛 / 𝑘 ) < 𝑥 → 𝑛 ≤ ( 𝑘 · 𝑥 ) ) )
116 115 impr ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑛 ∈ ℤ ∧ ( 𝑛 / 𝑘 ) < 𝑥 ) ) → 𝑛 ≤ ( 𝑘 · 𝑥 ) )
117 110 116 sylan2b ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ 𝑇 ) → 𝑛 ≤ ( 𝑘 · 𝑥 ) )
118 117 ralrimiva ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ∀ 𝑛 ∈ 𝑇 𝑛 ≤ ( 𝑘 · 𝑥 ) )
119 breq2 ⊢ ( 𝑦 = ( 𝑘 · 𝑥 ) → ( 𝑛 ≤ 𝑦 ↔ 𝑛 ≤ ( 𝑘 · 𝑥 ) ) )
120 119 ralbidv ⊢ ( 𝑦 = ( 𝑘 · 𝑥 ) → ( ∀ 𝑛 ∈ 𝑇 𝑛 ≤ 𝑦 ↔ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ ( 𝑘 · 𝑥 ) ) )
121 120 rspcev ⊢ ( ( ( 𝑘 · 𝑥 ) ∈ ℝ ∧ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ ( 𝑘 · 𝑥 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ 𝑦 )
122 94 118 121 syl2anc ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ 𝑦 )
123 91 109 122 3jca ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( 𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ 𝑦 ) )
124 suprub ⊢ ( ( ( 𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ 𝑦 ) ∧ ( sup ( 𝑇 , ℝ , < ) + 1 ) ∈ 𝑇 ) → ( sup ( 𝑇 , ℝ , < ) + 1 ) ≤ sup ( 𝑇 , ℝ , < ) )
125 123 124 sylan ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ ( sup ( 𝑇 , ℝ , < ) + 1 ) ∈ 𝑇 ) → ( sup ( 𝑇 , ℝ , < ) + 1 ) ≤ sup ( 𝑇 , ℝ , < ) )
126 86 125 syldan ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ ( ( sup ( 𝑇 , ℝ , < ) + 1 ) / 𝑘 ) < 𝑥 ) → ( sup ( 𝑇 , ℝ , < ) + 1 ) ≤ sup ( 𝑇 , ℝ , < ) )
127 126 ex ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( ( ( sup ( 𝑇 , ℝ , < ) + 1 ) / 𝑘 ) < 𝑥 → ( sup ( 𝑇 , ℝ , < ) + 1 ) ≤ sup ( 𝑇 , ℝ , < ) ) )
128 42 zcnd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → sup ( 𝑇 , ℝ , < ) ∈ ℂ )
129 1cnd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → 1 ∈ ℂ )
130 nncn ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℂ )
131 nnne0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ≠ 0 )
132 130 131 jca ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 ∈ ℂ ∧ 𝑘 ≠ 0 ) )
133 132 adantl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( 𝑘 ∈ ℂ ∧ 𝑘 ≠ 0 ) )
134 divdir ⊢ ( ( sup ( 𝑇 , ℝ , < ) ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 𝑘 ∈ ℂ ∧ 𝑘 ≠ 0 ) ) → ( ( sup ( 𝑇 , ℝ , < ) + 1 ) / 𝑘 ) = ( ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) + ( 1 / 𝑘 ) ) )
135 128 129 133 134 syl3anc ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( ( sup ( 𝑇 , ℝ , < ) + 1 ) / 𝑘 ) = ( ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) + ( 1 / 𝑘 ) ) )
136 3 mptex ⊢ ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) ∈ V
137 2 fvmpt2 ⊢ ( ( 𝑥 ∈ ℝ ∧ ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) ∈ V ) → ( 𝐹 ‘ 𝑥 ) = ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) )
138 136 137 mpan2 ⊢ ( 𝑥 ∈ ℝ → ( 𝐹 ‘ 𝑥 ) = ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) )
139 138 fveq1d ⊢ ( 𝑥 ∈ ℝ → ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) = ( ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) ‘ 𝑘 ) )
140 ovex ⊢ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ∈ V
141 eqid ⊢ ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) = ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) )
142 141 fvmpt2 ⊢ ( ( 𝑘 ∈ ℕ ∧ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ∈ V ) → ( ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) ‘ 𝑘 ) = ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) )
143 140 142 mpan2 ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) ‘ 𝑘 ) = ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) )
144 139 143 sylan9eq ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) = ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) )
145 144 oveq1d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) + ( 1 / 𝑘 ) ) = ( ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) + ( 1 / 𝑘 ) ) )
146 135 145 eqtr4d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( ( sup ( 𝑇 , ℝ , < ) + 1 ) / 𝑘 ) = ( ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) + ( 1 / 𝑘 ) ) )
147 146 breq1d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( ( ( sup ( 𝑇 , ℝ , < ) + 1 ) / 𝑘 ) < 𝑥 ↔ ( ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) + ( 1 / 𝑘 ) ) < 𝑥 ) )
148 81 zred ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( sup ( 𝑇 , ℝ , < ) + 1 ) ∈ ℝ )
149 148 43 lenltd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( ( sup ( 𝑇 , ℝ , < ) + 1 ) ≤ sup ( 𝑇 , ℝ , < ) ↔ ¬ sup ( 𝑇 , ℝ , < ) < ( sup ( 𝑇 , ℝ , < ) + 1 ) ) )
150 127 147 149 3imtr3d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( ( ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) + ( 1 / 𝑘 ) ) < 𝑥 → ¬ sup ( 𝑇 , ℝ , < ) < ( sup ( 𝑇 , ℝ , < ) + 1 ) ) )
151 150 adantlr ⊢ ( ( ( 𝑥 ∈ ℝ ∧ sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) < 𝑥 ) ∧ 𝑘 ∈ ℕ ) → ( ( ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) + ( 1 / 𝑘 ) ) < 𝑥 → ¬ sup ( 𝑇 , ℝ , < ) < ( sup ( 𝑇 , ℝ , < ) + 1 ) ) )
152 80 151 syld ⊢ ( ( ( 𝑥 ∈ ℝ ∧ sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) < 𝑥 ) ∧ 𝑘 ∈ ℕ ) → ( ( 1 / ( 𝑥 − sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ) ) < 𝑘 → ¬ sup ( 𝑇 , ℝ , < ) < ( sup ( 𝑇 , ℝ , < ) + 1 ) ) )
153 152 exp31 ⊢ ( 𝑥 ∈ ℝ → ( sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) < 𝑥 → ( 𝑘 ∈ ℕ → ( ( 1 / ( 𝑥 − sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ) ) < 𝑘 → ¬ sup ( 𝑇 , ℝ , < ) < ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) )
154 153 com4l ⊢ ( sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) < 𝑥 → ( 𝑘 ∈ ℕ → ( ( 1 / ( 𝑥 − sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ) ) < 𝑘 → ( 𝑥 ∈ ℝ → ¬ sup ( 𝑇 , ℝ , < ) < ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) )
155 154 com14 ⊢ ( 𝑥 ∈ ℝ → ( 𝑘 ∈ ℕ → ( ( 1 / ( 𝑥 − sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ) ) < 𝑘 → ( sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) < 𝑥 → ¬ sup ( 𝑇 , ℝ , < ) < ( sup ( 𝑇 , ℝ , < ) + 1 ) ) ) ) )
156 155 3imp ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ∧ ( 1 / ( 𝑥 − sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ) ) < 𝑘 ) → ( sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) < 𝑥 → ¬ sup ( 𝑇 , ℝ , < ) < ( sup ( 𝑇 , ℝ , < ) + 1 ) ) )
157 45 156 mt2d ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ∧ ( 1 / ( 𝑥 − sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ) ) < 𝑘 ) → ¬ sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) < 𝑥 )
158 157 rexlimdv3a ⊢ ( 𝑥 ∈ ℝ → ( ∃ 𝑘 ∈ ℕ ( 1 / ( 𝑥 − sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ) ) < 𝑘 → ¬ sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) < 𝑥 ) )
159 41 158 syld ⊢ ( 𝑥 ∈ ℝ → ( sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) < 𝑥 → ¬ sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) < 𝑥 ) )
160 159 pm2.01d ⊢ ( 𝑥 ∈ ℝ → ¬ sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) < 𝑥 )
161 eqlelt ⊢ ( ( sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) = 𝑥 ↔ ( sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ≤ 𝑥 ∧ ¬ sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) < 𝑥 ) ) )
162 30 161 mpancom ⊢ ( 𝑥 ∈ ℝ → ( sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) = 𝑥 ↔ ( sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) ≤ 𝑥 ∧ ¬ sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) < 𝑥 ) ) )
163 29 160 162 mpbir2and ⊢ ( 𝑥 ∈ ℝ → sup ( ran ( 𝐹 ‘ 𝑥 ) , ℝ , < ) = 𝑥 )