ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nninfdclemp1 GIF version

Theorem nninfdclemp1 12667
Description: Lemma for nninfdc 12670. Each element of the sequence 𝐹 is greater than the previous element. (Contributed by Jim Kingdon, 26-Sep-2024.)
Hypotheses
Ref Expression
nninfdclemf.a (𝜑𝐴 ⊆ ℕ)
nninfdclemf.dc (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥𝐴)
nninfdclemf.nb (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛𝐴 𝑚 < 𝑛)
nninfdclemf.j (𝜑 → (𝐽𝐴 ∧ 1 < 𝐽))
nninfdclemf.f 𝐹 = seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))
nninfdclemp1.u (𝜑𝑈 ∈ ℕ)
Assertion
Ref Expression
nninfdclemp1 (𝜑 → (𝐹𝑈) < (𝐹‘(𝑈 + 1)))
Distinct variable groups:   𝐴,𝑚,𝑛   𝑦,𝐴,𝑧   𝑥,𝐴   𝑚,𝐹,𝑛   𝑥,𝐹   𝑦,𝐹,𝑧   𝑖,𝐽   𝑦,𝐽,𝑧   𝑈,𝑖   𝑈,𝑚,𝑛   𝑥,𝑈   𝑦,𝑈,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑖,𝑚,𝑛)   𝐴(𝑖)   𝐹(𝑖)   𝐽(𝑥,𝑚,𝑛)

Proof of Theorem nninfdclemp1
Dummy variables 𝑎 𝑏 𝑟 𝑝 𝑞 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nninfdclemf.a . . . 4 (𝜑𝐴 ⊆ ℕ)
2 nninfdclemf.dc . . . . . 6 (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥𝐴)
3 nninfdclemf.nb . . . . . 6 (𝜑 → ∀𝑚 ∈ ℕ ∃𝑛𝐴 𝑚 < 𝑛)
4 nninfdclemf.j . . . . . 6 (𝜑 → (𝐽𝐴 ∧ 1 < 𝐽))
5 nninfdclemf.f . . . . . 6 𝐹 = seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))
61, 2, 3, 4, 5nninfdclemf 12666 . . . . 5 (𝜑𝐹:ℕ⟶𝐴)
7 nninfdclemp1.u . . . . 5 (𝜑𝑈 ∈ ℕ)
86, 7ffvelcdmd 5698 . . . 4 (𝜑 → (𝐹𝑈) ∈ 𝐴)
91, 8sseldd 3184 . . 3 (𝜑 → (𝐹𝑈) ∈ ℕ)
109nnred 9003 . 2 (𝜑 → (𝐹𝑈) ∈ ℝ)
119nnzd 9447 . . . 4 (𝜑 → (𝐹𝑈) ∈ ℤ)
1211peano2zd 9451 . . 3 (𝜑 → ((𝐹𝑈) + 1) ∈ ℤ)
1312zred 9448 . 2 (𝜑 → ((𝐹𝑈) + 1) ∈ ℝ)
147peano2nnd 9005 . . . . 5 (𝜑 → (𝑈 + 1) ∈ ℕ)
156, 14ffvelcdmd 5698 . . . 4 (𝜑 → (𝐹‘(𝑈 + 1)) ∈ 𝐴)
161, 15sseldd 3184 . . 3 (𝜑 → (𝐹‘(𝑈 + 1)) ∈ ℕ)
1716nnred 9003 . 2 (𝜑 → (𝐹‘(𝑈 + 1)) ∈ ℝ)
1810ltp1d 8957 . 2 (𝜑 → (𝐹𝑈) < ((𝐹𝑈) + 1))
19 simpr 110 . . . . . . 7 ((𝜑𝑟 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1)))) → 𝑟 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))))
2019elin2d 3353 . . . . . 6 ((𝜑𝑟 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1)))) → 𝑟 ∈ (ℤ‘((𝐹𝑈) + 1)))
21 eluzle 9613 . . . . . 6 (𝑟 ∈ (ℤ‘((𝐹𝑈) + 1)) → ((𝐹𝑈) + 1) ≤ 𝑟)
2220, 21syl 14 . . . . 5 ((𝜑𝑟 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1)))) → ((𝐹𝑈) + 1) ≤ 𝑟)
2322ralrimiva 2570 . . . 4 (𝜑 → ∀𝑟 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1)))((𝐹𝑈) + 1) ≤ 𝑟)
24 inss1 3383 . . . . . . 7 (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))) ⊆ 𝐴
2524, 1sstrid 3194 . . . . . 6 (𝜑 → (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))) ⊆ ℕ)
26 eleq1w 2257 . . . . . . . . . . 11 (𝑥 = 𝑎 → (𝑥𝐴𝑎𝐴))
2726dcbid 839 . . . . . . . . . 10 (𝑥 = 𝑎 → (DECID 𝑥𝐴DECID 𝑎𝐴))
282adantr 276 . . . . . . . . . 10 ((𝜑𝑎 ∈ ℕ) → ∀𝑥 ∈ ℕ DECID 𝑥𝐴)
29 simpr 110 . . . . . . . . . 10 ((𝜑𝑎 ∈ ℕ) → 𝑎 ∈ ℕ)
3027, 28, 29rspcdva 2873 . . . . . . . . 9 ((𝜑𝑎 ∈ ℕ) → DECID 𝑎𝐴)
3129nnzd 9447 . . . . . . . . . 10 ((𝜑𝑎 ∈ ℕ) → 𝑎 ∈ ℤ)
32 eluzdc 9684 . . . . . . . . . 10 ((((𝐹𝑈) + 1) ∈ ℤ ∧ 𝑎 ∈ ℤ) → DECID 𝑎 ∈ (ℤ‘((𝐹𝑈) + 1)))
3312, 31, 32syl2an2r 595 . . . . . . . . 9 ((𝜑𝑎 ∈ ℕ) → DECID 𝑎 ∈ (ℤ‘((𝐹𝑈) + 1)))
34 dcan2 936 . . . . . . . . 9 (DECID 𝑎𝐴 → (DECID 𝑎 ∈ (ℤ‘((𝐹𝑈) + 1)) → DECID (𝑎𝐴𝑎 ∈ (ℤ‘((𝐹𝑈) + 1)))))
3530, 33, 34sylc 62 . . . . . . . 8 ((𝜑𝑎 ∈ ℕ) → DECID (𝑎𝐴𝑎 ∈ (ℤ‘((𝐹𝑈) + 1))))
36 elin 3346 . . . . . . . . 9 (𝑎 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))) ↔ (𝑎𝐴𝑎 ∈ (ℤ‘((𝐹𝑈) + 1))))
3736dcbii 841 . . . . . . . 8 (DECID 𝑎 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))) ↔ DECID (𝑎𝐴𝑎 ∈ (ℤ‘((𝐹𝑈) + 1))))
3835, 37sylibr 134 . . . . . . 7 ((𝜑𝑎 ∈ ℕ) → DECID 𝑎 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))))
3938ralrimiva 2570 . . . . . 6 (𝜑 → ∀𝑎 ∈ ℕ DECID 𝑎 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))))
40 breq1 4036 . . . . . . . . . . 11 (𝑚 = (𝐹𝑈) → (𝑚 < 𝑛 ↔ (𝐹𝑈) < 𝑛))
4140rexbidv 2498 . . . . . . . . . 10 (𝑚 = (𝐹𝑈) → (∃𝑛𝐴 𝑚 < 𝑛 ↔ ∃𝑛𝐴 (𝐹𝑈) < 𝑛))
4241, 3, 9rspcdva 2873 . . . . . . . . 9 (𝜑 → ∃𝑛𝐴 (𝐹𝑈) < 𝑛)
43 breq2 4037 . . . . . . . . . 10 (𝑛 = 𝑏 → ((𝐹𝑈) < 𝑛 ↔ (𝐹𝑈) < 𝑏))
4443cbvrexv 2730 . . . . . . . . 9 (∃𝑛𝐴 (𝐹𝑈) < 𝑛 ↔ ∃𝑏𝐴 (𝐹𝑈) < 𝑏)
4542, 44sylib 122 . . . . . . . 8 (𝜑 → ∃𝑏𝐴 (𝐹𝑈) < 𝑏)
46 df-rex 2481 . . . . . . . 8 (∃𝑏𝐴 (𝐹𝑈) < 𝑏 ↔ ∃𝑏(𝑏𝐴 ∧ (𝐹𝑈) < 𝑏))
4745, 46sylib 122 . . . . . . 7 (𝜑 → ∃𝑏(𝑏𝐴 ∧ (𝐹𝑈) < 𝑏))
48 simprl 529 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐴 ∧ (𝐹𝑈) < 𝑏)) → 𝑏𝐴)
4912adantr 276 . . . . . . . . . . 11 ((𝜑 ∧ (𝑏𝐴 ∧ (𝐹𝑈) < 𝑏)) → ((𝐹𝑈) + 1) ∈ ℤ)
501adantr 276 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑏𝐴 ∧ (𝐹𝑈) < 𝑏)) → 𝐴 ⊆ ℕ)
5150, 48sseldd 3184 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑏𝐴 ∧ (𝐹𝑈) < 𝑏)) → 𝑏 ∈ ℕ)
5251nnzd 9447 . . . . . . . . . . 11 ((𝜑 ∧ (𝑏𝐴 ∧ (𝐹𝑈) < 𝑏)) → 𝑏 ∈ ℤ)
53 simprr 531 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑏𝐴 ∧ (𝐹𝑈) < 𝑏)) → (𝐹𝑈) < 𝑏)
54 nnltp1le 9386 . . . . . . . . . . . . 13 (((𝐹𝑈) ∈ ℕ ∧ 𝑏 ∈ ℕ) → ((𝐹𝑈) < 𝑏 ↔ ((𝐹𝑈) + 1) ≤ 𝑏))
559, 51, 54syl2an2r 595 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑏𝐴 ∧ (𝐹𝑈) < 𝑏)) → ((𝐹𝑈) < 𝑏 ↔ ((𝐹𝑈) + 1) ≤ 𝑏))
5653, 55mpbid 147 . . . . . . . . . . 11 ((𝜑 ∧ (𝑏𝐴 ∧ (𝐹𝑈) < 𝑏)) → ((𝐹𝑈) + 1) ≤ 𝑏)
57 eluz2 9607 . . . . . . . . . . 11 (𝑏 ∈ (ℤ‘((𝐹𝑈) + 1)) ↔ (((𝐹𝑈) + 1) ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ ((𝐹𝑈) + 1) ≤ 𝑏))
5849, 52, 56, 57syl3anbrc 1183 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐴 ∧ (𝐹𝑈) < 𝑏)) → 𝑏 ∈ (ℤ‘((𝐹𝑈) + 1)))
5948, 58elind 3348 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐴 ∧ (𝐹𝑈) < 𝑏)) → 𝑏 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))))
6059ex 115 . . . . . . . 8 (𝜑 → ((𝑏𝐴 ∧ (𝐹𝑈) < 𝑏) → 𝑏 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1)))))
6160eximdv 1894 . . . . . . 7 (𝜑 → (∃𝑏(𝑏𝐴 ∧ (𝐹𝑈) < 𝑏) → ∃𝑏 𝑏 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1)))))
6247, 61mpd 13 . . . . . 6 (𝜑 → ∃𝑏 𝑏 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))))
6325, 39, 62nninfdcex 10327 . . . . 5 (𝜑 → ∃𝑎 ∈ ℝ (∀𝑏 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))) ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑟 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1)))𝑟 < 𝑏)))
64 nnssre 8994 . . . . . 6 ℕ ⊆ ℝ
6525, 64sstrdi 3195 . . . . 5 (𝜑 → (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))) ⊆ ℝ)
6663, 65, 13infregelbex 9672 . . . 4 (𝜑 → (((𝐹𝑈) + 1) ≤ inf((𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))), ℝ, < ) ↔ ∀𝑟 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1)))((𝐹𝑈) + 1) ≤ 𝑟))
6723, 66mpbird 167 . . 3 (𝜑 → ((𝐹𝑈) + 1) ≤ inf((𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))), ℝ, < ))
685fveq1i 5559 . . . . 5 (𝐹‘(𝑈 + 1)) = (seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))‘(𝑈 + 1))
69 nnuz 9637 . . . . . . 7 ℕ = (ℤ‘1)
707, 69eleqtrdi 2289 . . . . . 6 (𝜑𝑈 ∈ (ℤ‘1))
71 eqid 2196 . . . . . . . 8 (𝑖 ∈ ℕ ↦ 𝐽) = (𝑖 ∈ ℕ ↦ 𝐽)
72 eqidd 2197 . . . . . . . 8 (𝑖 = 𝑝𝐽 = 𝐽)
73 elnnuz 9638 . . . . . . . . . 10 (𝑝 ∈ ℕ ↔ 𝑝 ∈ (ℤ‘1))
7473biimpri 133 . . . . . . . . 9 (𝑝 ∈ (ℤ‘1) → 𝑝 ∈ ℕ)
7574adantl 277 . . . . . . . 8 ((𝜑𝑝 ∈ (ℤ‘1)) → 𝑝 ∈ ℕ)
764simpld 112 . . . . . . . . 9 (𝜑𝐽𝐴)
7776adantr 276 . . . . . . . 8 ((𝜑𝑝 ∈ (ℤ‘1)) → 𝐽𝐴)
7871, 72, 75, 77fvmptd3 5655 . . . . . . 7 ((𝜑𝑝 ∈ (ℤ‘1)) → ((𝑖 ∈ ℕ ↦ 𝐽)‘𝑝) = 𝐽)
7978, 77eqeltrd 2273 . . . . . 6 ((𝜑𝑝 ∈ (ℤ‘1)) → ((𝑖 ∈ ℕ ↦ 𝐽)‘𝑝) ∈ 𝐴)
801adantr 276 . . . . . . 7 ((𝜑 ∧ (𝑝𝐴𝑞𝐴)) → 𝐴 ⊆ ℕ)
812adantr 276 . . . . . . 7 ((𝜑 ∧ (𝑝𝐴𝑞𝐴)) → ∀𝑥 ∈ ℕ DECID 𝑥𝐴)
823adantr 276 . . . . . . 7 ((𝜑 ∧ (𝑝𝐴𝑞𝐴)) → ∀𝑚 ∈ ℕ ∃𝑛𝐴 𝑚 < 𝑛)
83 simprl 529 . . . . . . 7 ((𝜑 ∧ (𝑝𝐴𝑞𝐴)) → 𝑝𝐴)
84 simprr 531 . . . . . . 7 ((𝜑 ∧ (𝑝𝐴𝑞𝐴)) → 𝑞𝐴)
8580, 81, 82, 83, 84nninfdclemcl 12665 . . . . . 6 ((𝜑 ∧ (𝑝𝐴𝑞𝐴)) → (𝑝(𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < ))𝑞) ∈ 𝐴)
8670, 79, 85seq3p1 10557 . . . . 5 (𝜑 → (seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))‘(𝑈 + 1)) = ((seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))‘𝑈)(𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < ))((𝑖 ∈ ℕ ↦ 𝐽)‘(𝑈 + 1))))
8768, 86eqtrid 2241 . . . 4 (𝜑 → (𝐹‘(𝑈 + 1)) = ((seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))‘𝑈)(𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < ))((𝑖 ∈ ℕ ↦ 𝐽)‘(𝑈 + 1))))
885fveq1i 5559 . . . . . . 7 (𝐹𝑈) = (seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))‘𝑈)
8988eqcomi 2200 . . . . . 6 (seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))‘𝑈) = (𝐹𝑈)
9089a1i 9 . . . . 5 (𝜑 → (seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))‘𝑈) = (𝐹𝑈))
91 eqidd 2197 . . . . . 6 (𝑖 = (𝑈 + 1) → 𝐽 = 𝐽)
9271, 91, 14, 76fvmptd3 5655 . . . . 5 (𝜑 → ((𝑖 ∈ ℕ ↦ 𝐽)‘(𝑈 + 1)) = 𝐽)
9390, 92oveq12d 5940 . . . 4 (𝜑 → ((seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))‘𝑈)(𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < ))((𝑖 ∈ ℕ ↦ 𝐽)‘(𝑈 + 1))) = ((𝐹𝑈)(𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < ))𝐽))
941, 76sseldd 3184 . . . . 5 (𝜑𝐽 ∈ ℕ)
95 eleq1w 2257 . . . . . . . . . . . . 13 (𝑥 = 𝑠 → (𝑥𝐴𝑠𝐴))
9695dcbid 839 . . . . . . . . . . . 12 (𝑥 = 𝑠 → (DECID 𝑥𝐴DECID 𝑠𝐴))
972adantr 276 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ ℕ) → ∀𝑥 ∈ ℕ DECID 𝑥𝐴)
98 simpr 110 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ ℕ) → 𝑠 ∈ ℕ)
9996, 97, 98rspcdva 2873 . . . . . . . . . . 11 ((𝜑𝑠 ∈ ℕ) → DECID 𝑠𝐴)
10098nnzd 9447 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ ℕ) → 𝑠 ∈ ℤ)
101 eluzdc 9684 . . . . . . . . . . . 12 ((((𝐹𝑈) + 1) ∈ ℤ ∧ 𝑠 ∈ ℤ) → DECID 𝑠 ∈ (ℤ‘((𝐹𝑈) + 1)))
10212, 100, 101syl2an2r 595 . . . . . . . . . . 11 ((𝜑𝑠 ∈ ℕ) → DECID 𝑠 ∈ (ℤ‘((𝐹𝑈) + 1)))
103 dcan2 936 . . . . . . . . . . 11 (DECID 𝑠𝐴 → (DECID 𝑠 ∈ (ℤ‘((𝐹𝑈) + 1)) → DECID (𝑠𝐴𝑠 ∈ (ℤ‘((𝐹𝑈) + 1)))))
10499, 102, 103sylc 62 . . . . . . . . . 10 ((𝜑𝑠 ∈ ℕ) → DECID (𝑠𝐴𝑠 ∈ (ℤ‘((𝐹𝑈) + 1))))
105 elin 3346 . . . . . . . . . . 11 (𝑠 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))) ↔ (𝑠𝐴𝑠 ∈ (ℤ‘((𝐹𝑈) + 1))))
106105dcbii 841 . . . . . . . . . 10 (DECID 𝑠 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))) ↔ DECID (𝑠𝐴𝑠 ∈ (ℤ‘((𝐹𝑈) + 1))))
107104, 106sylibr 134 . . . . . . . . 9 ((𝜑𝑠 ∈ ℕ) → DECID 𝑠 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))))
108107ralrimiva 2570 . . . . . . . 8 (𝜑 → ∀𝑠 ∈ ℕ DECID 𝑠 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))))
109 eleq1w 2257 . . . . . . . . . 10 (𝑠 = 𝑥 → (𝑠 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))) ↔ 𝑥 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1)))))
110109dcbid 839 . . . . . . . . 9 (𝑠 = 𝑥 → (DECID 𝑠 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))) ↔ DECID 𝑥 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1)))))
111110cbvralv 2729 . . . . . . . 8 (∀𝑠 ∈ ℕ DECID 𝑠 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))) ↔ ∀𝑥 ∈ ℕ DECID 𝑥 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))))
112108, 111sylib 122 . . . . . . 7 (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))))
113 nnmindc 12201 . . . . . . 7 (((𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))) ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))) ∧ ∃𝑏 𝑏 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1)))) → inf((𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))), ℝ, < ) ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))))
11425, 112, 62, 113syl3anc 1249 . . . . . 6 (𝜑 → inf((𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))), ℝ, < ) ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))))
115114elin1d 3352 . . . . 5 (𝜑 → inf((𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))), ℝ, < ) ∈ 𝐴)
116 fvoveq1 5945 . . . . . . . 8 (𝑦 = (𝐹𝑈) → (ℤ‘(𝑦 + 1)) = (ℤ‘((𝐹𝑈) + 1)))
117116ineq2d 3364 . . . . . . 7 (𝑦 = (𝐹𝑈) → (𝐴 ∩ (ℤ‘(𝑦 + 1))) = (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))))
118117infeq1d 7078 . . . . . 6 (𝑦 = (𝐹𝑈) → inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < ) = inf((𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))), ℝ, < ))
119 eqidd 2197 . . . . . 6 (𝑧 = 𝐽 → inf((𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))), ℝ, < ) = inf((𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))), ℝ, < ))
120 eqid 2196 . . . . . 6 (𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < )) = (𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < ))
121118, 119, 120ovmpog 6057 . . . . 5 (((𝐹𝑈) ∈ ℕ ∧ 𝐽 ∈ ℕ ∧ inf((𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))), ℝ, < ) ∈ 𝐴) → ((𝐹𝑈)(𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < ))𝐽) = inf((𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))), ℝ, < ))
1229, 94, 115, 121syl3anc 1249 . . . 4 (𝜑 → ((𝐹𝑈)(𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < ))𝐽) = inf((𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))), ℝ, < ))
12387, 93, 1223eqtrd 2233 . . 3 (𝜑 → (𝐹‘(𝑈 + 1)) = inf((𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))), ℝ, < ))
12467, 123breqtrrd 4061 . 2 (𝜑 → ((𝐹𝑈) + 1) ≤ (𝐹‘(𝑈 + 1)))
12510, 13, 17, 18, 124ltletrd 8450 1 (𝜑 → (𝐹𝑈) < (𝐹‘(𝑈 + 1)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  DECID wdc 835   = wceq 1364  wex 1506  wcel 2167  wral 2475  wrex 2476  cin 3156  wss 3157   class class class wbr 4033  cmpt 4094  cfv 5258  (class class class)co 5922  cmpo 5924  infcinf 7049  cr 7878  1c1 7880   + caddc 7882   < clt 8061  cle 8062  cn 8990  cz 9326  cuz 9601  seqcseq 10539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-coll 4148  ax-sep 4151  ax-nul 4159  ax-pow 4207  ax-pr 4242  ax-un 4468  ax-setind 4573  ax-iinf 4624  ax-cnex 7970  ax-resscn 7971  ax-1cn 7972  ax-1re 7973  ax-icn 7974  ax-addcl 7975  ax-addrcl 7976  ax-mulcl 7977  ax-addcom 7979  ax-addass 7981  ax-distr 7983  ax-i2m1 7984  ax-0lt1 7985  ax-0id 7987  ax-rnegex 7988  ax-cnre 7990  ax-pre-ltirr 7991  ax-pre-ltwlin 7992  ax-pre-lttrn 7993  ax-pre-apti 7994  ax-pre-ltadd 7995
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-nel 2463  df-ral 2480  df-rex 2481  df-reu 2482  df-rmo 2483  df-rab 2484  df-v 2765  df-sbc 2990  df-csb 3085  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-nul 3451  df-pw 3607  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-int 3875  df-iun 3918  df-br 4034  df-opab 4095  df-mpt 4096  df-tr 4132  df-id 4328  df-po 4331  df-iso 4332  df-iord 4401  df-on 4403  df-ilim 4404  df-suc 4406  df-iom 4627  df-xp 4669  df-rel 4670  df-cnv 4671  df-co 4672  df-dm 4673  df-rn 4674  df-res 4675  df-ima 4676  df-iota 5219  df-fun 5260  df-fn 5261  df-f 5262  df-f1 5263  df-fo 5264  df-f1o 5265  df-fv 5266  df-isom 5267  df-riota 5877  df-ov 5925  df-oprab 5926  df-mpo 5927  df-1st 6198  df-2nd 6199  df-recs 6363  df-frec 6449  df-sup 7050  df-inf 7051  df-pnf 8063  df-mnf 8064  df-xr 8065  df-ltxr 8066  df-le 8067  df-sub 8199  df-neg 8200  df-inn 8991  df-n0 9250  df-z 9327  df-uz 9602  df-fz 10084  df-fzo 10218  df-seqfrec 10540
This theorem is referenced by:  nninfdclemlt  12668
  Copyright terms: Public domain W3C validator