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

Theorem nninfdclemp1 12377
Description: Lemma for nninfdc 12380. 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 12376 . . . . 5 (𝜑𝐹:ℕ⟶𝐴)
7 nninfdclemp1.u . . . . 5 (𝜑𝑈 ∈ ℕ)
86, 7ffvelrnd 5618 . . . 4 (𝜑 → (𝐹𝑈) ∈ 𝐴)
91, 8sseldd 3141 . . 3 (𝜑 → (𝐹𝑈) ∈ ℕ)
109nnred 8864 . 2 (𝜑 → (𝐹𝑈) ∈ ℝ)
119nnzd 9306 . . . 4 (𝜑 → (𝐹𝑈) ∈ ℤ)
1211peano2zd 9310 . . 3 (𝜑 → ((𝐹𝑈) + 1) ∈ ℤ)
1312zred 9307 . 2 (𝜑 → ((𝐹𝑈) + 1) ∈ ℝ)
147peano2nnd 8866 . . . . 5 (𝜑 → (𝑈 + 1) ∈ ℕ)
156, 14ffvelrnd 5618 . . . 4 (𝜑 → (𝐹‘(𝑈 + 1)) ∈ 𝐴)
161, 15sseldd 3141 . . 3 (𝜑 → (𝐹‘(𝑈 + 1)) ∈ ℕ)
1716nnred 8864 . 2 (𝜑 → (𝐹‘(𝑈 + 1)) ∈ ℝ)
1810ltp1d 8819 . 2 (𝜑 → (𝐹𝑈) < ((𝐹𝑈) + 1))
19 simpr 109 . . . . . . 7 ((𝜑𝑟 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1)))) → 𝑟 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))))
2019elin2d 3310 . . . . . 6 ((𝜑𝑟 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1)))) → 𝑟 ∈ (ℤ‘((𝐹𝑈) + 1)))
21 eluzle 9472 . . . . . 6 (𝑟 ∈ (ℤ‘((𝐹𝑈) + 1)) → ((𝐹𝑈) + 1) ≤ 𝑟)
2220, 21syl 14 . . . . 5 ((𝜑𝑟 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1)))) → ((𝐹𝑈) + 1) ≤ 𝑟)
2322ralrimiva 2537 . . . 4 (𝜑 → ∀𝑟 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1)))((𝐹𝑈) + 1) ≤ 𝑟)
24 inss1 3340 . . . . . . 7 (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))) ⊆ 𝐴
2524, 1sstrid 3151 . . . . . 6 (𝜑 → (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))) ⊆ ℕ)
26 eleq1w 2225 . . . . . . . . . . 11 (𝑥 = 𝑎 → (𝑥𝐴𝑎𝐴))
2726dcbid 828 . . . . . . . . . 10 (𝑥 = 𝑎 → (DECID 𝑥𝐴DECID 𝑎𝐴))
282adantr 274 . . . . . . . . . 10 ((𝜑𝑎 ∈ ℕ) → ∀𝑥 ∈ ℕ DECID 𝑥𝐴)
29 simpr 109 . . . . . . . . . 10 ((𝜑𝑎 ∈ ℕ) → 𝑎 ∈ ℕ)
3027, 28, 29rspcdva 2833 . . . . . . . . 9 ((𝜑𝑎 ∈ ℕ) → DECID 𝑎𝐴)
3129nnzd 9306 . . . . . . . . . 10 ((𝜑𝑎 ∈ ℕ) → 𝑎 ∈ ℤ)
32 eluzdc 9542 . . . . . . . . . 10 ((((𝐹𝑈) + 1) ∈ ℤ ∧ 𝑎 ∈ ℤ) → DECID 𝑎 ∈ (ℤ‘((𝐹𝑈) + 1)))
3312, 31, 32syl2an2r 585 . . . . . . . . 9 ((𝜑𝑎 ∈ ℕ) → DECID 𝑎 ∈ (ℤ‘((𝐹𝑈) + 1)))
34 dcan 923 . . . . . . . . 9 (DECID 𝑎𝐴 → (DECID 𝑎 ∈ (ℤ‘((𝐹𝑈) + 1)) → DECID (𝑎𝐴𝑎 ∈ (ℤ‘((𝐹𝑈) + 1)))))
3530, 33, 34sylc 62 . . . . . . . 8 ((𝜑𝑎 ∈ ℕ) → DECID (𝑎𝐴𝑎 ∈ (ℤ‘((𝐹𝑈) + 1))))
36 elin 3303 . . . . . . . . 9 (𝑎 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))) ↔ (𝑎𝐴𝑎 ∈ (ℤ‘((𝐹𝑈) + 1))))
3736dcbii 830 . . . . . . . 8 (DECID 𝑎 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))) ↔ DECID (𝑎𝐴𝑎 ∈ (ℤ‘((𝐹𝑈) + 1))))
3835, 37sylibr 133 . . . . . . 7 ((𝜑𝑎 ∈ ℕ) → DECID 𝑎 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))))
3938ralrimiva 2537 . . . . . 6 (𝜑 → ∀𝑎 ∈ ℕ DECID 𝑎 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))))
40 breq1 3982 . . . . . . . . . . 11 (𝑚 = (𝐹𝑈) → (𝑚 < 𝑛 ↔ (𝐹𝑈) < 𝑛))
4140rexbidv 2465 . . . . . . . . . 10 (𝑚 = (𝐹𝑈) → (∃𝑛𝐴 𝑚 < 𝑛 ↔ ∃𝑛𝐴 (𝐹𝑈) < 𝑛))
4241, 3, 9rspcdva 2833 . . . . . . . . 9 (𝜑 → ∃𝑛𝐴 (𝐹𝑈) < 𝑛)
43 breq2 3983 . . . . . . . . . 10 (𝑛 = 𝑏 → ((𝐹𝑈) < 𝑛 ↔ (𝐹𝑈) < 𝑏))
4443cbvrexv 2691 . . . . . . . . 9 (∃𝑛𝐴 (𝐹𝑈) < 𝑛 ↔ ∃𝑏𝐴 (𝐹𝑈) < 𝑏)
4542, 44sylib 121 . . . . . . . 8 (𝜑 → ∃𝑏𝐴 (𝐹𝑈) < 𝑏)
46 df-rex 2448 . . . . . . . 8 (∃𝑏𝐴 (𝐹𝑈) < 𝑏 ↔ ∃𝑏(𝑏𝐴 ∧ (𝐹𝑈) < 𝑏))
4745, 46sylib 121 . . . . . . 7 (𝜑 → ∃𝑏(𝑏𝐴 ∧ (𝐹𝑈) < 𝑏))
48 simprl 521 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐴 ∧ (𝐹𝑈) < 𝑏)) → 𝑏𝐴)
4912adantr 274 . . . . . . . . . . 11 ((𝜑 ∧ (𝑏𝐴 ∧ (𝐹𝑈) < 𝑏)) → ((𝐹𝑈) + 1) ∈ ℤ)
501adantr 274 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑏𝐴 ∧ (𝐹𝑈) < 𝑏)) → 𝐴 ⊆ ℕ)
5150, 48sseldd 3141 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑏𝐴 ∧ (𝐹𝑈) < 𝑏)) → 𝑏 ∈ ℕ)
5251nnzd 9306 . . . . . . . . . . 11 ((𝜑 ∧ (𝑏𝐴 ∧ (𝐹𝑈) < 𝑏)) → 𝑏 ∈ ℤ)
53 simprr 522 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑏𝐴 ∧ (𝐹𝑈) < 𝑏)) → (𝐹𝑈) < 𝑏)
54 nnltp1le 9245 . . . . . . . . . . . . 13 (((𝐹𝑈) ∈ ℕ ∧ 𝑏 ∈ ℕ) → ((𝐹𝑈) < 𝑏 ↔ ((𝐹𝑈) + 1) ≤ 𝑏))
559, 51, 54syl2an2r 585 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑏𝐴 ∧ (𝐹𝑈) < 𝑏)) → ((𝐹𝑈) < 𝑏 ↔ ((𝐹𝑈) + 1) ≤ 𝑏))
5653, 55mpbid 146 . . . . . . . . . . 11 ((𝜑 ∧ (𝑏𝐴 ∧ (𝐹𝑈) < 𝑏)) → ((𝐹𝑈) + 1) ≤ 𝑏)
57 eluz2 9466 . . . . . . . . . . 11 (𝑏 ∈ (ℤ‘((𝐹𝑈) + 1)) ↔ (((𝐹𝑈) + 1) ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ ((𝐹𝑈) + 1) ≤ 𝑏))
5849, 52, 56, 57syl3anbrc 1170 . . . . . . . . . 10 ((𝜑 ∧ (𝑏𝐴 ∧ (𝐹𝑈) < 𝑏)) → 𝑏 ∈ (ℤ‘((𝐹𝑈) + 1)))
5948, 58elind 3305 . . . . . . . . 9 ((𝜑 ∧ (𝑏𝐴 ∧ (𝐹𝑈) < 𝑏)) → 𝑏 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))))
6059ex 114 . . . . . . . 8 (𝜑 → ((𝑏𝐴 ∧ (𝐹𝑈) < 𝑏) → 𝑏 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1)))))
6160eximdv 1867 . . . . . . 7 (𝜑 → (∃𝑏(𝑏𝐴 ∧ (𝐹𝑈) < 𝑏) → ∃𝑏 𝑏 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1)))))
6247, 61mpd 13 . . . . . 6 (𝜑 → ∃𝑏 𝑏 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))))
6325, 39, 62nninfdcex 11880 . . . . 5 (𝜑 → ∃𝑎 ∈ ℝ (∀𝑏 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))) ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑟 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1)))𝑟 < 𝑏)))
64 nnssre 8855 . . . . . 6 ℕ ⊆ ℝ
6525, 64sstrdi 3152 . . . . 5 (𝜑 → (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))) ⊆ ℝ)
6663, 65, 13infregelbex 9530 . . . 4 (𝜑 → (((𝐹𝑈) + 1) ≤ inf((𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))), ℝ, < ) ↔ ∀𝑟 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1)))((𝐹𝑈) + 1) ≤ 𝑟))
6723, 66mpbird 166 . . 3 (𝜑 → ((𝐹𝑈) + 1) ≤ inf((𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))), ℝ, < ))
685fveq1i 5484 . . . . 5 (𝐹‘(𝑈 + 1)) = (seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))‘(𝑈 + 1))
69 nnuz 9495 . . . . . . 7 ℕ = (ℤ‘1)
707, 69eleqtrdi 2257 . . . . . 6 (𝜑𝑈 ∈ (ℤ‘1))
71 eqid 2164 . . . . . . . 8 (𝑖 ∈ ℕ ↦ 𝐽) = (𝑖 ∈ ℕ ↦ 𝐽)
72 eqidd 2165 . . . . . . . 8 (𝑖 = 𝑝𝐽 = 𝐽)
73 elnnuz 9496 . . . . . . . . . 10 (𝑝 ∈ ℕ ↔ 𝑝 ∈ (ℤ‘1))
7473biimpri 132 . . . . . . . . 9 (𝑝 ∈ (ℤ‘1) → 𝑝 ∈ ℕ)
7574adantl 275 . . . . . . . 8 ((𝜑𝑝 ∈ (ℤ‘1)) → 𝑝 ∈ ℕ)
764simpld 111 . . . . . . . . 9 (𝜑𝐽𝐴)
7776adantr 274 . . . . . . . 8 ((𝜑𝑝 ∈ (ℤ‘1)) → 𝐽𝐴)
7871, 72, 75, 77fvmptd3 5576 . . . . . . 7 ((𝜑𝑝 ∈ (ℤ‘1)) → ((𝑖 ∈ ℕ ↦ 𝐽)‘𝑝) = 𝐽)
7978, 77eqeltrd 2241 . . . . . 6 ((𝜑𝑝 ∈ (ℤ‘1)) → ((𝑖 ∈ ℕ ↦ 𝐽)‘𝑝) ∈ 𝐴)
801adantr 274 . . . . . . 7 ((𝜑 ∧ (𝑝𝐴𝑞𝐴)) → 𝐴 ⊆ ℕ)
812adantr 274 . . . . . . 7 ((𝜑 ∧ (𝑝𝐴𝑞𝐴)) → ∀𝑥 ∈ ℕ DECID 𝑥𝐴)
823adantr 274 . . . . . . 7 ((𝜑 ∧ (𝑝𝐴𝑞𝐴)) → ∀𝑚 ∈ ℕ ∃𝑛𝐴 𝑚 < 𝑛)
83 simprl 521 . . . . . . 7 ((𝜑 ∧ (𝑝𝐴𝑞𝐴)) → 𝑝𝐴)
84 simprr 522 . . . . . . 7 ((𝜑 ∧ (𝑝𝐴𝑞𝐴)) → 𝑞𝐴)
8580, 81, 82, 83, 84nninfdclemcl 12375 . . . . . 6 ((𝜑 ∧ (𝑝𝐴𝑞𝐴)) → (𝑝(𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < ))𝑞) ∈ 𝐴)
8670, 79, 85seq3p1 10391 . . . . 5 (𝜑 → (seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))‘(𝑈 + 1)) = ((seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))‘𝑈)(𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < ))((𝑖 ∈ ℕ ↦ 𝐽)‘(𝑈 + 1))))
8768, 86syl5eq 2209 . . . 4 (𝜑 → (𝐹‘(𝑈 + 1)) = ((seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))‘𝑈)(𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < ))((𝑖 ∈ ℕ ↦ 𝐽)‘(𝑈 + 1))))
885fveq1i 5484 . . . . . . 7 (𝐹𝑈) = (seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))‘𝑈)
8988eqcomi 2168 . . . . . 6 (seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))‘𝑈) = (𝐹𝑈)
9089a1i 9 . . . . 5 (𝜑 → (seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))‘𝑈) = (𝐹𝑈))
91 eqidd 2165 . . . . . 6 (𝑖 = (𝑈 + 1) → 𝐽 = 𝐽)
9271, 91, 14, 76fvmptd3 5576 . . . . 5 (𝜑 → ((𝑖 ∈ ℕ ↦ 𝐽)‘(𝑈 + 1)) = 𝐽)
9390, 92oveq12d 5857 . . . 4 (𝜑 → ((seq1((𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < )), (𝑖 ∈ ℕ ↦ 𝐽))‘𝑈)(𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < ))((𝑖 ∈ ℕ ↦ 𝐽)‘(𝑈 + 1))) = ((𝐹𝑈)(𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < ))𝐽))
941, 76sseldd 3141 . . . . 5 (𝜑𝐽 ∈ ℕ)
95 eleq1w 2225 . . . . . . . . . . . . 13 (𝑥 = 𝑠 → (𝑥𝐴𝑠𝐴))
9695dcbid 828 . . . . . . . . . . . 12 (𝑥 = 𝑠 → (DECID 𝑥𝐴DECID 𝑠𝐴))
972adantr 274 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ ℕ) → ∀𝑥 ∈ ℕ DECID 𝑥𝐴)
98 simpr 109 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ ℕ) → 𝑠 ∈ ℕ)
9996, 97, 98rspcdva 2833 . . . . . . . . . . 11 ((𝜑𝑠 ∈ ℕ) → DECID 𝑠𝐴)
10098nnzd 9306 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ ℕ) → 𝑠 ∈ ℤ)
101 eluzdc 9542 . . . . . . . . . . . 12 ((((𝐹𝑈) + 1) ∈ ℤ ∧ 𝑠 ∈ ℤ) → DECID 𝑠 ∈ (ℤ‘((𝐹𝑈) + 1)))
10212, 100, 101syl2an2r 585 . . . . . . . . . . 11 ((𝜑𝑠 ∈ ℕ) → DECID 𝑠 ∈ (ℤ‘((𝐹𝑈) + 1)))
103 dcan 923 . . . . . . . . . . 11 (DECID 𝑠𝐴 → (DECID 𝑠 ∈ (ℤ‘((𝐹𝑈) + 1)) → DECID (𝑠𝐴𝑠 ∈ (ℤ‘((𝐹𝑈) + 1)))))
10499, 102, 103sylc 62 . . . . . . . . . 10 ((𝜑𝑠 ∈ ℕ) → DECID (𝑠𝐴𝑠 ∈ (ℤ‘((𝐹𝑈) + 1))))
105 elin 3303 . . . . . . . . . . 11 (𝑠 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))) ↔ (𝑠𝐴𝑠 ∈ (ℤ‘((𝐹𝑈) + 1))))
106105dcbii 830 . . . . . . . . . 10 (DECID 𝑠 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))) ↔ DECID (𝑠𝐴𝑠 ∈ (ℤ‘((𝐹𝑈) + 1))))
107104, 106sylibr 133 . . . . . . . . 9 ((𝜑𝑠 ∈ ℕ) → DECID 𝑠 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))))
108107ralrimiva 2537 . . . . . . . 8 (𝜑 → ∀𝑠 ∈ ℕ DECID 𝑠 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))))
109 eleq1w 2225 . . . . . . . . . 10 (𝑠 = 𝑥 → (𝑠 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))) ↔ 𝑥 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1)))))
110109dcbid 828 . . . . . . . . 9 (𝑠 = 𝑥 → (DECID 𝑠 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))) ↔ DECID 𝑥 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1)))))
111110cbvralv 2690 . . . . . . . 8 (∀𝑠 ∈ ℕ DECID 𝑠 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))) ↔ ∀𝑥 ∈ ℕ DECID 𝑥 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))))
112108, 111sylib 121 . . . . . . 7 (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))))
113 nnmindc 11961 . . . . . . 7 (((𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))) ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))) ∧ ∃𝑏 𝑏 ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1)))) → inf((𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))), ℝ, < ) ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))))
11425, 112, 62, 113syl3anc 1227 . . . . . 6 (𝜑 → inf((𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))), ℝ, < ) ∈ (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))))
115114elin1d 3309 . . . . 5 (𝜑 → inf((𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))), ℝ, < ) ∈ 𝐴)
116 fvoveq1 5862 . . . . . . . 8 (𝑦 = (𝐹𝑈) → (ℤ‘(𝑦 + 1)) = (ℤ‘((𝐹𝑈) + 1)))
117116ineq2d 3321 . . . . . . 7 (𝑦 = (𝐹𝑈) → (𝐴 ∩ (ℤ‘(𝑦 + 1))) = (𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))))
118117infeq1d 6971 . . . . . 6 (𝑦 = (𝐹𝑈) → inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < ) = inf((𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))), ℝ, < ))
119 eqidd 2165 . . . . . 6 (𝑧 = 𝐽 → inf((𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))), ℝ, < ) = inf((𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))), ℝ, < ))
120 eqid 2164 . . . . . 6 (𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < )) = (𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < ))
121118, 119, 120ovmpog 5970 . . . . 5 (((𝐹𝑈) ∈ ℕ ∧ 𝐽 ∈ ℕ ∧ inf((𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))), ℝ, < ) ∈ 𝐴) → ((𝐹𝑈)(𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < ))𝐽) = inf((𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))), ℝ, < ))
1229, 94, 115, 121syl3anc 1227 . . . 4 (𝜑 → ((𝐹𝑈)(𝑦 ∈ ℕ, 𝑧 ∈ ℕ ↦ inf((𝐴 ∩ (ℤ‘(𝑦 + 1))), ℝ, < ))𝐽) = inf((𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))), ℝ, < ))
12387, 93, 1223eqtrd 2201 . . 3 (𝜑 → (𝐹‘(𝑈 + 1)) = inf((𝐴 ∩ (ℤ‘((𝐹𝑈) + 1))), ℝ, < ))
12467, 123breqtrrd 4007 . 2 (𝜑 → ((𝐹𝑈) + 1) ≤ (𝐹‘(𝑈 + 1)))
12510, 13, 17, 18, 124ltletrd 8315 1 (𝜑 → (𝐹𝑈) < (𝐹‘(𝑈 + 1)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  DECID wdc 824   = wceq 1342  wex 1479  wcel 2135  wral 2442  wrex 2443  cin 3113  wss 3114   class class class wbr 3979  cmpt 4040  cfv 5185  (class class class)co 5839  cmpo 5841  infcinf 6942  cr 7746  1c1 7748   + caddc 7750   < clt 7927  cle 7928  cn 8851  cz 9185  cuz 9460  seqcseq 10374
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-13 2137  ax-14 2138  ax-ext 2146  ax-coll 4094  ax-sep 4097  ax-nul 4105  ax-pow 4150  ax-pr 4184  ax-un 4408  ax-setind 4511  ax-iinf 4562  ax-cnex 7838  ax-resscn 7839  ax-1cn 7840  ax-1re 7841  ax-icn 7842  ax-addcl 7843  ax-addrcl 7844  ax-mulcl 7845  ax-addcom 7847  ax-addass 7849  ax-distr 7851  ax-i2m1 7852  ax-0lt1 7853  ax-0id 7855  ax-rnegex 7856  ax-cnre 7858  ax-pre-ltirr 7859  ax-pre-ltwlin 7860  ax-pre-lttrn 7861  ax-pre-apti 7862  ax-pre-ltadd 7863
This theorem depends on definitions:  df-bi 116  df-dc 825  df-3or 968  df-3an 969  df-tru 1345  df-fal 1348  df-nf 1448  df-sb 1750  df-eu 2016  df-mo 2017  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ne 2335  df-nel 2430  df-ral 2447  df-rex 2448  df-reu 2449  df-rmo 2450  df-rab 2451  df-v 2726  df-sbc 2950  df-csb 3044  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-nul 3408  df-pw 3558  df-sn 3579  df-pr 3580  df-op 3582  df-uni 3787  df-int 3822  df-iun 3865  df-br 3980  df-opab 4041  df-mpt 4042  df-tr 4078  df-id 4268  df-po 4271  df-iso 4272  df-iord 4341  df-on 4343  df-ilim 4344  df-suc 4346  df-iom 4565  df-xp 4607  df-rel 4608  df-cnv 4609  df-co 4610  df-dm 4611  df-rn 4612  df-res 4613  df-ima 4614  df-iota 5150  df-fun 5187  df-fn 5188  df-f 5189  df-f1 5190  df-fo 5191  df-f1o 5192  df-fv 5193  df-isom 5194  df-riota 5795  df-ov 5842  df-oprab 5843  df-mpo 5844  df-1st 6103  df-2nd 6104  df-recs 6267  df-frec 6353  df-sup 6943  df-inf 6944  df-pnf 7929  df-mnf 7930  df-xr 7931  df-ltxr 7932  df-le 7933  df-sub 8065  df-neg 8066  df-inn 8852  df-n0 9109  df-z 9186  df-uz 9461  df-fz 9939  df-fzo 10072  df-seqfrec 10375
This theorem is referenced by:  nninfdclemlt  12378
  Copyright terms: Public domain W3C validator