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

Theorem axcaucvglemval 7028
 Description: Lemma for axcaucvg 7031. Value of sequence when mapping to N and R. (Contributed by Jim Kingdon, 10-Jul-2021.)
Hypotheses
Ref Expression
axcaucvg.n 𝑁 = {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}
axcaucvg.f (𝜑𝐹:𝑁⟶ℝ)
axcaucvg.cau (𝜑 → ∀𝑛𝑁𝑘𝑁 (𝑛 < 𝑘 → ((𝐹𝑛) < ((𝐹𝑘) + (𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)) ∧ (𝐹𝑘) < ((𝐹𝑛) + (𝑟 ∈ ℝ (𝑛 · 𝑟) = 1)))))
axcaucvg.g 𝐺 = (𝑗N ↦ (𝑧R (𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑗, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑗, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩))
Assertion
Ref Expression
axcaucvglemval ((𝜑𝐽N) → (𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨(𝐺𝐽), 0R⟩)
Distinct variable groups:   𝑗,𝐹,𝑧   𝑧,𝐺   𝑗,𝐽,𝑙,𝑢,𝑧   𝜑,𝑗   𝑦,𝑙,𝑢   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑢,𝑘,𝑛,𝑟,𝑙)   𝐹(𝑥,𝑦,𝑢,𝑘,𝑛,𝑟,𝑙)   𝐺(𝑥,𝑦,𝑢,𝑗,𝑘,𝑛,𝑟,𝑙)   𝐽(𝑥,𝑦,𝑘,𝑛,𝑟)   𝑁(𝑥,𝑦,𝑧,𝑢,𝑗,𝑘,𝑛,𝑟,𝑙)

Proof of Theorem axcaucvglemval
StepHypRef Expression
1 axcaucvg.g . . . . 5 𝐺 = (𝑗N ↦ (𝑧R (𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑗, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑗, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩))
21a1i 9 . . . 4 ((𝜑𝐽N) → 𝐺 = (𝑗N ↦ (𝑧R (𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑗, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑗, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩)))
3 opeq1 3576 . . . . . . . . . . . . . . . 16 (𝑗 = 𝐽 → ⟨𝑗, 1𝑜⟩ = ⟨𝐽, 1𝑜⟩)
43eceq1d 6172 . . . . . . . . . . . . . . 15 (𝑗 = 𝐽 → [⟨𝑗, 1𝑜⟩] ~Q = [⟨𝐽, 1𝑜⟩] ~Q )
54breq2d 3803 . . . . . . . . . . . . . 14 (𝑗 = 𝐽 → (𝑙 <Q [⟨𝑗, 1𝑜⟩] ~Q𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q ))
65abbidv 2171 . . . . . . . . . . . . 13 (𝑗 = 𝐽 → {𝑙𝑙 <Q [⟨𝑗, 1𝑜⟩] ~Q } = {𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q })
74breq1d 3801 . . . . . . . . . . . . . 14 (𝑗 = 𝐽 → ([⟨𝑗, 1𝑜⟩] ~Q <Q 𝑢 ↔ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢))
87abbidv 2171 . . . . . . . . . . . . 13 (𝑗 = 𝐽 → {𝑢 ∣ [⟨𝑗, 1𝑜⟩] ~Q <Q 𝑢} = {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢})
96, 8opeq12d 3584 . . . . . . . . . . . 12 (𝑗 = 𝐽 → ⟨{𝑙𝑙 <Q [⟨𝑗, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑗, 1𝑜⟩] ~Q <Q 𝑢}⟩ = ⟨{𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩)
109oveq1d 5554 . . . . . . . . . . 11 (𝑗 = 𝐽 → (⟨{𝑙𝑙 <Q [⟨𝑗, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑗, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P) = (⟨{𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P))
1110opeq1d 3582 . . . . . . . . . 10 (𝑗 = 𝐽 → ⟨(⟨{𝑙𝑙 <Q [⟨𝑗, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑗, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩ = ⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩)
1211eceq1d 6172 . . . . . . . . 9 (𝑗 = 𝐽 → [⟨(⟨{𝑙𝑙 <Q [⟨𝑗, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑗, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R = [⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R )
1312opeq1d 3582 . . . . . . . 8 (𝑗 = 𝐽 → ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑗, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑗, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ = ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩)
1413fveq2d 5209 . . . . . . 7 (𝑗 = 𝐽 → (𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑗, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑗, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = (𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩))
1514eqeq1d 2064 . . . . . 6 (𝑗 = 𝐽 → ((𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑗, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑗, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩ ↔ (𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩))
1615riotabidv 5497 . . . . 5 (𝑗 = 𝐽 → (𝑧R (𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑗, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑗, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩) = (𝑧R (𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩))
1716adantl 266 . . . 4 (((𝜑𝐽N) ∧ 𝑗 = 𝐽) → (𝑧R (𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝑗, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝑗, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩) = (𝑧R (𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩))
18 simpr 107 . . . 4 ((𝜑𝐽N) → 𝐽N)
19 axcaucvg.n . . . . 5 𝑁 = {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}
20 axcaucvg.f . . . . 5 (𝜑𝐹:𝑁⟶ℝ)
2119, 20axcaucvglemcl 7026 . . . 4 ((𝜑𝐽N) → (𝑧R (𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩) ∈ R)
222, 17, 18, 21fvmptd 5280 . . 3 ((𝜑𝐽N) → (𝐺𝐽) = (𝑧R (𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩))
2322eqcomd 2061 . 2 ((𝜑𝐽N) → (𝑧R (𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩) = (𝐺𝐽))
2422, 21eqeltrd 2130 . . 3 ((𝜑𝐽N) → (𝐺𝐽) ∈ R)
2520adantr 265 . . . . . 6 ((𝜑𝐽N) → 𝐹:𝑁⟶ℝ)
26 pitonn 6981 . . . . . . . 8 (𝐽N → ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)})
2726, 19syl6eleqr 2147 . . . . . . 7 (𝐽N → ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ ∈ 𝑁)
2827adantl 266 . . . . . 6 ((𝜑𝐽N) → ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ ∈ 𝑁)
2925, 28ffvelrnd 5330 . . . . 5 ((𝜑𝐽N) → (𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) ∈ ℝ)
30 elrealeu 6963 . . . . 5 ((𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) ∈ ℝ ↔ ∃!𝑧R𝑧, 0R⟩ = (𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩))
3129, 30sylib 131 . . . 4 ((𝜑𝐽N) → ∃!𝑧R𝑧, 0R⟩ = (𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩))
32 eqcom 2058 . . . . 5 (⟨𝑧, 0R⟩ = (𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) ↔ (𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩)
3332reubii 2512 . . . 4 (∃!𝑧R𝑧, 0R⟩ = (𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) ↔ ∃!𝑧R (𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩)
3431, 33sylib 131 . . 3 ((𝜑𝐽N) → ∃!𝑧R (𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩)
35 opeq1 3576 . . . . 5 (𝑧 = (𝐺𝐽) → ⟨𝑧, 0R⟩ = ⟨(𝐺𝐽), 0R⟩)
3635eqeq2d 2067 . . . 4 (𝑧 = (𝐺𝐽) → ((𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩ ↔ (𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨(𝐺𝐽), 0R⟩))
3736riota2 5517 . . 3 (((𝐺𝐽) ∈ R ∧ ∃!𝑧R (𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩) → ((𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨(𝐺𝐽), 0R⟩ ↔ (𝑧R (𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩) = (𝐺𝐽)))
3824, 34, 37syl2anc 397 . 2 ((𝜑𝐽N) → ((𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨(𝐺𝐽), 0R⟩ ↔ (𝑧R (𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨𝑧, 0R⟩) = (𝐺𝐽)))
3923, 38mpbird 160 1 ((𝜑𝐽N) → (𝐹‘⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1𝑜⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1𝑜⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩) = ⟨(𝐺𝐽), 0R⟩)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   ↔ wb 102   = wceq 1259   ∈ wcel 1409  {cab 2042  ∀wral 2323  ∃!wreu 2325  ⟨cop 3405  ∩ cint 3642   class class class wbr 3791   ↦ cmpt 3845  ⟶wf 4925  ‘cfv 4929  ℩crio 5494  (class class class)co 5539  1𝑜c1o 6024  [cec 6134  Ncnpi 6427   ~Q ceq 6434
 Copyright terms: Public domain W3C validator