Metamath Proof Explorer

Theorem iunhoiioolem

Description: A n-dimensional open interval expressed as the indexed union of half-open intervals. One side of the double inclusion. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses iunhoiioolem.K ⊢ Ⅎ 𝑘 𝜑
iunhoiioolem.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
iunhoiioolem.n ⊢ ( 𝜑 → 𝑋 ≠ ∅ )
iunhoiioolem.a ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ )
iunhoiioolem.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐵 ∈ ℝ* )
iunhoiioolem.f ⊢ ( 𝜑 → 𝐹 ∈ X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) )
iunhoiioolem.c ⊢ 𝐶 = inf ( ran ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) , ℝ , < )
Assertion iunhoiioolem ( 𝜑 → 𝐹 ∈ ∪ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) )

Proof

Step Hyp Ref Expression
1 iunhoiioolem.K ⊢ Ⅎ 𝑘 𝜑
2 iunhoiioolem.x ⊢ ( 𝜑 → 𝑋 ∈ Fin )
3 iunhoiioolem.n ⊢ ( 𝜑 → 𝑋 ≠ ∅ )
4 iunhoiioolem.a ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ )
5 iunhoiioolem.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐵 ∈ ℝ* )
6 iunhoiioolem.f ⊢ ( 𝜑 → 𝐹 ∈ X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) )
7 iunhoiioolem.c ⊢ 𝐶 = inf ( ran ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) , ℝ , < )
8 eqid ⊢ ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) = ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) )
9 ixpf ⊢ ( 𝐹 ∈ X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) → 𝐹 : 𝑋 ⟶ ∪ 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) )
10 6 9 syl ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ∪ 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) )
11 ioossre ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ
12 11 rgenw ⊢ ∀ 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) ⊆ ℝ
13 12 a1i ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) ⊆ ℝ )
14 iunss ⊢ ( ∪ 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) ⊆ ℝ ↔ ∀ 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) ⊆ ℝ )
15 13 14 sylibr ⊢ ( 𝜑 → ∪ 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) ⊆ ℝ )
16 10 15 fssd ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℝ )
17 16 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
18 17 4 resubcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ∈ ℝ )
19 4 rexrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ* )
20 6 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐹 ∈ X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) )
21 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝑘 ∈ 𝑋 )
22 fvixp2 ⊢ ( ( 𝐹 ∈ X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝐴 (,) 𝐵 ) )
23 20 21 22 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝐴 (,) 𝐵 ) )
24 ioogtlb ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝐴 (,) 𝐵 ) ) → 𝐴 < ( 𝐹 ‘ 𝑘 ) )
25 19 5 23 24 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐴 < ( 𝐹 ‘ 𝑘 ) )
26 4 17 posdifd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 < ( 𝐹 ‘ 𝑘 ) ↔ 0 < ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) )
27 25 26 mpbid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 0 < ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) )
28 18 27 elrpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ∈ ℝ+ )
29 1 8 28 rnmptssd ⊢ ( 𝜑 → ran ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ⊆ ℝ+ )
30 ltso ⊢ < Or ℝ
31 30 a1i ⊢ ( 𝜑 → < Or ℝ )
32 8 rnmptfi ⊢ ( 𝑋 ∈ Fin → ran ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ∈ Fin )
33 2 32 syl ⊢ ( 𝜑 → ran ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ∈ Fin )
34 1 28 8 3 rnmptn0 ⊢ ( 𝜑 → ran ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ≠ ∅ )
35 1 8 18 rnmptssd ⊢ ( 𝜑 → ran ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ⊆ ℝ )
36 fiinfcl ⊢ ( ( < Or ℝ ∧ ( ran ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ∈ Fin ∧ ran ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ≠ ∅ ∧ ran ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ⊆ ℝ ) ) → inf ( ran ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) , ℝ , < ) ∈ ran ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) )
37 31 33 34 35 36 syl13anc ⊢ ( 𝜑 → inf ( ran ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) , ℝ , < ) ∈ ran ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) )
38 7 37 eqeltrid ⊢ ( 𝜑 → 𝐶 ∈ ran ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) )
39 29 38 sseldd ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
40 rpgtrecnn ⊢ ( 𝐶 ∈ ℝ+ → ∃ 𝑛 ∈ ℕ ( 1 / 𝑛 ) < 𝐶 )
41 39 40 syl ⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ ( 1 / 𝑛 ) < 𝐶 )
42 6 elexd ⊢ ( 𝜑 → 𝐹 ∈ V )
43 42 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝐶 ) → 𝐹 ∈ V )
44 10 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝑋 )
45 44 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝐶 ) → 𝐹 Fn 𝑋 )
46 nfv ⊢ Ⅎ 𝑘 𝑛 ∈ ℕ
47 1 46 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑛 ∈ ℕ )
48 nfcv ⊢ Ⅎ 𝑘 ( 1 / 𝑛 )
49 nfcv ⊢ Ⅎ 𝑘 <
50 nfmpt1 ⊢ Ⅎ 𝑘 ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) )
51 50 nfrn ⊢ Ⅎ 𝑘 ran ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) )
52 nfcv ⊢ Ⅎ 𝑘 ℝ
53 51 52 49 nfinf ⊢ Ⅎ 𝑘 inf ( ran ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) , ℝ , < )
54 7 53 nfcxfr ⊢ Ⅎ 𝑘 𝐶
55 48 49 54 nfbr ⊢ Ⅎ 𝑘 ( 1 / 𝑛 ) < 𝐶
56 47 55 nfan ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝐶 )
57 4 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ )
58 nnrecre ⊢ ( 𝑛 ∈ ℕ → ( 1 / 𝑛 ) ∈ ℝ )
59 58 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 1 / 𝑛 ) ∈ ℝ )
60 57 59 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 + ( 1 / 𝑛 ) ) ∈ ℝ )
61 60 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 + ( 1 / 𝑛 ) ) ∈ ℝ* )
62 61 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝐶 ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 + ( 1 / 𝑛 ) ) ∈ ℝ* )
63 5 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → 𝐵 ∈ ℝ* )
64 63 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝐶 ) ∧ 𝑘 ∈ 𝑋 ) → 𝐵 ∈ ℝ* )
65 ressxr ⊢ ℝ ⊆ ℝ*
66 65 a1i ⊢ ( 𝜑 → ℝ ⊆ ℝ* )
67 16 66 fssd ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℝ* )
68 67 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝐶 ) → 𝐹 : 𝑋 ⟶ ℝ* )
69 68 ffvelrnda ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝐶 ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
70 60 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝐶 ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 + ( 1 / 𝑛 ) ) ∈ ℝ )
71 17 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝐶 ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
72 59 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝐶 ) ∧ 𝑘 ∈ 𝑋 ) → ( 1 / 𝑛 ) ∈ ℝ )
73 35 38 sseldd ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
74 73 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝐶 ) ∧ 𝑘 ∈ 𝑋 ) → 𝐶 ∈ ℝ )
75 18 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝐶 ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ∈ ℝ )
76 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝐶 ) ∧ 𝑘 ∈ 𝑋 ) → ( 1 / 𝑛 ) < 𝐶 )
77 35 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ran ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ⊆ ℝ )
78 33 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ran ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ∈ Fin )
79 id ⊢ ( 𝑘 ∈ 𝑋 → 𝑘 ∈ 𝑋 )
80 ovexd ⊢ ( 𝑘 ∈ 𝑋 → ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ∈ V )
81 8 elrnmpt1 ⊢ ( ( 𝑘 ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ∈ V ) → ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ∈ ran ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) )
82 79 80 81 syl2anc ⊢ ( 𝑘 ∈ 𝑋 → ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ∈ ran ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) )
83 82 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ∈ ran ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) )
84 infrefilb ⊢ ( ( ran ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ⊆ ℝ ∧ ran ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ∈ Fin ∧ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ∈ ran ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) ) → inf ( ran ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) , ℝ , < ) ≤ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) )
85 77 78 83 84 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → inf ( ran ( 𝑘 ∈ 𝑋 ↦ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) , ℝ , < ) ≤ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) )
86 7 85 eqbrtrid ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → 𝐶 ≤ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) )
87 86 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝐶 ) ∧ 𝑘 ∈ 𝑋 ) → 𝐶 ≤ ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) )
88 72 74 75 76 87 ltletrd ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝐶 ) ∧ 𝑘 ∈ 𝑋 ) → ( 1 / 𝑛 ) < ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) )
89 57 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝐶 ) ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ )
90 89 72 71 ltaddsub2d ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝐶 ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐴 + ( 1 / 𝑛 ) ) < ( 𝐹 ‘ 𝑘 ) ↔ ( 1 / 𝑛 ) < ( ( 𝐹 ‘ 𝑘 ) − 𝐴 ) ) )
91 88 90 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝐶 ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 + ( 1 / 𝑛 ) ) < ( 𝐹 ‘ 𝑘 ) )
92 70 71 91 ltled ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝐶 ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐴 + ( 1 / 𝑛 ) ) ≤ ( 𝐹 ‘ 𝑘 ) )
93 iooltub ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑘 ) < 𝐵 )
94 19 5 23 93 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑘 ) < 𝐵 )
95 94 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝐶 ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑘 ) < 𝐵 )
96 62 64 69 92 95 elicod ⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝐶 ) ∧ 𝑘 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) )
97 96 ex ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝐶 ) → ( 𝑘 ∈ 𝑋 → ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) ) )
98 56 97 ralrimi ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝐶 ) → ∀ 𝑘 ∈ 𝑋 ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) )
99 43 45 98 3jca ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝐶 ) → ( 𝐹 ∈ V ∧ 𝐹 Fn 𝑋 ∧ ∀ 𝑘 ∈ 𝑋 ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) ) )
100 elixp2 ⊢ ( 𝐹 ∈ X 𝑘 ∈ 𝑋 ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) ↔ ( 𝐹 ∈ V ∧ 𝐹 Fn 𝑋 ∧ ∀ 𝑘 ∈ 𝑋 ( 𝐹 ‘ 𝑘 ) ∈ ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) ) )
101 99 100 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ ( 1 / 𝑛 ) < 𝐶 ) → 𝐹 ∈ X 𝑘 ∈ 𝑋 ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) )
102 101 ex ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 1 / 𝑛 ) < 𝐶 → 𝐹 ∈ X 𝑘 ∈ 𝑋 ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) ) )
103 102 reximdva ⊢ ( 𝜑 → ( ∃ 𝑛 ∈ ℕ ( 1 / 𝑛 ) < 𝐶 → ∃ 𝑛 ∈ ℕ 𝐹 ∈ X 𝑘 ∈ 𝑋 ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) ) )
104 41 103 mpd ⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ 𝐹 ∈ X 𝑘 ∈ 𝑋 ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) )
105 eliun ⊢ ( 𝐹 ∈ ∪ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) ↔ ∃ 𝑛 ∈ ℕ 𝐹 ∈ X 𝑘 ∈ 𝑋 ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) )
106 104 105 sylibr ⊢ ( 𝜑 → 𝐹 ∈ ∪ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) )