Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fdc Structured version   Visualization version   GIF version

Theorem fdc 33852
Description: Finite version of dependent choice. Construct a function whose value depends on the previous function value, except at a final point at which no new value can be chosen. The final hypothesis ensures that the process will terminate. The proof does not use the Axiom of Choice. (Contributed by Jeff Madsen, 18-Jun-2010.)
Hypotheses
Ref Expression
fdc.1 𝐴 ∈ V
fdc.2 𝑀 ∈ ℤ
fdc.3 𝑍 = (ℤ𝑀)
fdc.4 𝑁 = (𝑀 + 1)
fdc.5 (𝑎 = (𝑓‘(𝑘 − 1)) → (𝜑𝜓))
fdc.6 (𝑏 = (𝑓𝑘) → (𝜓𝜒))
fdc.7 (𝑎 = (𝑓𝑛) → (𝜃𝜏))
fdc.8 (𝜂𝐶𝐴)
fdc.9 (𝜂𝑅 Fr 𝐴)
fdc.10 ((𝜂𝑎𝐴) → (𝜃 ∨ ∃𝑏𝐴 𝜑))
fdc.11 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → 𝑏𝑅𝑎)
Assertion
Ref Expression
fdc (𝜂 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝐶𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
Distinct variable groups:   𝐶,𝑓,𝑛   𝐴,𝑎,𝑏,𝑓,𝑛   𝑀,𝑎,𝑏,𝑓,𝑘,𝑛   𝑍,𝑎,𝑏,𝑛   𝑁,𝑎,𝑏,𝑓,𝑘,𝑛   𝑅,𝑎,𝑏   𝜑,𝑓,𝑘   𝜓,𝑎   𝜒,𝑎,𝑏,𝑛   𝜃,𝑓,𝑛   𝜏,𝑎,𝑏   𝜂,𝑎,𝑏
Allowed substitution hints:   𝜑(𝑛,𝑎,𝑏)   𝜓(𝑓,𝑘,𝑛,𝑏)   𝜒(𝑓,𝑘)   𝜃(𝑘,𝑎,𝑏)   𝜏(𝑓,𝑘,𝑛)   𝜂(𝑓,𝑘,𝑛)   𝐴(𝑘)   𝐶(𝑘,𝑎,𝑏)   𝑅(𝑓,𝑘,𝑛)   𝑍(𝑓,𝑘)

Proof of Theorem fdc
Dummy variables 𝑐 𝑑 𝑔 𝑚 𝑥 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fdc.8 . 2 (𝜂𝐶𝐴)
2 fdc.2 . . . . . . . . . . . . . . . . . . 19 𝑀 ∈ ℤ
3 uzid 11919 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ𝑀))
42, 3ax-mp 5 . . . . . . . . . . . . . . . . . 18 𝑀 ∈ (ℤ𝑀)
5 fdc.3 . . . . . . . . . . . . . . . . . 18 𝑍 = (ℤ𝑀)
64, 5eleqtrri 2884 . . . . . . . . . . . . . . . . 17 𝑀𝑍
7 eqid 2806 . . . . . . . . . . . . . . . . . . . . . 22 {⟨𝑀, 𝑎⟩} = {⟨𝑀, 𝑎⟩}
82elexi 3407 . . . . . . . . . . . . . . . . . . . . . . 23 𝑀 ∈ V
9 vex 3394 . . . . . . . . . . . . . . . . . . . . . . 23 𝑎 ∈ V
108, 9fsn 6625 . . . . . . . . . . . . . . . . . . . . . 22 ({⟨𝑀, 𝑎⟩}:{𝑀}⟶{𝑎} ↔ {⟨𝑀, 𝑎⟩} = {⟨𝑀, 𝑎⟩})
117, 10mpbir 222 . . . . . . . . . . . . . . . . . . . . 21 {⟨𝑀, 𝑎⟩}:{𝑀}⟶{𝑎}
12 snssi 4529 . . . . . . . . . . . . . . . . . . . . 21 (𝑎𝐴 → {𝑎} ⊆ 𝐴)
13 fss 6269 . . . . . . . . . . . . . . . . . . . . 21 (({⟨𝑀, 𝑎⟩}:{𝑀}⟶{𝑎} ∧ {𝑎} ⊆ 𝐴) → {⟨𝑀, 𝑎⟩}:{𝑀}⟶𝐴)
1411, 12, 13sylancr 577 . . . . . . . . . . . . . . . . . . . 20 (𝑎𝐴 → {⟨𝑀, 𝑎⟩}:{𝑀}⟶𝐴)
15 fzsn 12606 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀})
162, 15ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (𝑀...𝑀) = {𝑀}
1716feq2i 6248 . . . . . . . . . . . . . . . . . . . 20 ({⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴 ↔ {⟨𝑀, 𝑎⟩}:{𝑀}⟶𝐴)
1814, 17sylibr 225 . . . . . . . . . . . . . . . . . . 19 (𝑎𝐴 → {⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴)
1918adantr 468 . . . . . . . . . . . . . . . . . 18 ((𝑎𝐴𝜃) → {⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴)
208, 9fvsn 6671 . . . . . . . . . . . . . . . . . . 19 ({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎
2120a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝑎𝐴𝜃) → ({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎)
22 simpr 473 . . . . . . . . . . . . . . . . . 18 ((𝑎𝐴𝜃) → 𝜃)
23 snex 5098 . . . . . . . . . . . . . . . . . . 19 {⟨𝑀, 𝑎⟩} ∈ V
24 feq1 6237 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = {⟨𝑀, 𝑎⟩} → (𝑓:(𝑀...𝑀)⟶𝐴 ↔ {⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴))
25 fveq1 6407 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = {⟨𝑀, 𝑎⟩} → (𝑓𝑀) = ({⟨𝑀, 𝑎⟩}‘𝑀))
2625eqeq1d 2808 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = {⟨𝑀, 𝑎⟩} → ((𝑓𝑀) = 𝑎 ↔ ({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎))
2725, 20syl6eq 2856 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = {⟨𝑀, 𝑎⟩} → (𝑓𝑀) = 𝑎)
28 sbceq2a 3645 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓𝑀) = 𝑎 → ([(𝑓𝑀) / 𝑎]𝜃𝜃))
2927, 28syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = {⟨𝑀, 𝑎⟩} → ([(𝑓𝑀) / 𝑎]𝜃𝜃))
3026, 29anbi12d 618 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = {⟨𝑀, 𝑎⟩} → (((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃) ↔ (({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎𝜃)))
3124, 30anbi12d 618 . . . . . . . . . . . . . . . . . . 19 (𝑓 = {⟨𝑀, 𝑎⟩} → ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃)) ↔ ({⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴 ∧ (({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎𝜃))))
3223, 31spcev 3493 . . . . . . . . . . . . . . . . . 18 (({⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴 ∧ (({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎𝜃)) → ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃)))
3319, 21, 22, 32syl12anc 856 . . . . . . . . . . . . . . . . 17 ((𝑎𝐴𝜃) → ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃)))
34 oveq2 6882 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑀 → (𝑀...𝑛) = (𝑀...𝑀))
3534feq2d 6242 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑀 → (𝑓:(𝑀...𝑛)⟶𝐴𝑓:(𝑀...𝑀)⟶𝐴))
36 fvex 6421 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓𝑛) ∈ V
37 fdc.7 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = (𝑓𝑛) → (𝜃𝜏))
3836, 37sbcie 3668 . . . . . . . . . . . . . . . . . . . . . . 23 ([(𝑓𝑛) / 𝑎]𝜃𝜏)
39 fveq2 6408 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑀 → (𝑓𝑛) = (𝑓𝑀))
4039sbceq1d 3638 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑀 → ([(𝑓𝑛) / 𝑎]𝜃[(𝑓𝑀) / 𝑎]𝜃))
4138, 40syl5bbr 276 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑀 → (𝜏[(𝑓𝑀) / 𝑎]𝜃))
4241anbi2d 616 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑀 → (((𝑓𝑀) = 𝑎𝜏) ↔ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃)))
43 oveq2 6882 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑀 → (𝑁...𝑛) = (𝑁...𝑀))
44 fdc.4 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑁 = (𝑀 + 1)
4544oveq1i 6884 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁...𝑀) = ((𝑀 + 1)...𝑀)
462zrei 11649 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑀 ∈ ℝ
4746ltp1i 11212 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑀 < (𝑀 + 1)
48 peano2z 11684 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑀 ∈ ℤ → (𝑀 + 1) ∈ ℤ)
492, 48ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑀 + 1) ∈ ℤ
50 fzn 12580 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑀 + 1) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 < (𝑀 + 1) ↔ ((𝑀 + 1)...𝑀) = ∅))
5149, 2, 50mp2an 675 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 < (𝑀 + 1) ↔ ((𝑀 + 1)...𝑀) = ∅)
5247, 51mpbi 221 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑀 + 1)...𝑀) = ∅
5345, 52eqtri 2828 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁...𝑀) = ∅
5443, 53syl6eq 2856 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑀 → (𝑁...𝑛) = ∅)
5554raleqdv 3333 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑀 → (∀𝑘 ∈ (𝑁...𝑛)𝜒 ↔ ∀𝑘 ∈ ∅ 𝜒))
5635, 42, 553anbi123d 1553 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑀 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃) ∧ ∀𝑘 ∈ ∅ 𝜒)))
57 ral0 4271 . . . . . . . . . . . . . . . . . . . . 21 𝑘 ∈ ∅ 𝜒
58 df-3an 1102 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃) ∧ ∀𝑘 ∈ ∅ 𝜒) ↔ ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃)) ∧ ∀𝑘 ∈ ∅ 𝜒))
5957, 58mpbiran2 692 . . . . . . . . . . . . . . . . . . . 20 ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃) ∧ ∀𝑘 ∈ ∅ 𝜒) ↔ (𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃)))
6056, 59syl6bb 278 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑀 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃))))
6160exbidv 2012 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑀 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃))))
6261rspcev 3502 . . . . . . . . . . . . . . . . 17 ((𝑀𝑍 ∧ ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃))) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
636, 33, 62sylancr 577 . . . . . . . . . . . . . . . 16 ((𝑎𝐴𝜃) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
6463adantll 696 . . . . . . . . . . . . . . 15 (((𝜂𝑎𝐴) ∧ 𝜃) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
6564a1d 25 . . . . . . . . . . . . . 14 (((𝜂𝑎𝐴) ∧ 𝜃) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
66 fdc.11 . . . . . . . . . . . . . . . . . . . . 21 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → 𝑏𝑅𝑎)
67 breq1 4847 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑 = 𝑏 → (𝑑𝑅𝑎𝑏𝑅𝑎))
6867rspcev 3502 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∧ 𝑏𝑅𝑎) → ∃𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎)
6968expcom 400 . . . . . . . . . . . . . . . . . . . . 21 (𝑏𝑅𝑎 → (𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎))
7066, 69syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎))
71 dfrex2 3183 . . . . . . . . . . . . . . . . . . . 20 (∃𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎 ↔ ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
7270, 71syl6ib 242 . . . . . . . . . . . . . . . . . . 19 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
7372con2d 131 . . . . . . . . . . . . . . . . . 18 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ¬ 𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
74 eldif 3779 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) ↔ (𝑏𝐴 ∧ ¬ 𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
7574simplbi2 490 . . . . . . . . . . . . . . . . . . . 20 (𝑏𝐴 → (¬ 𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → 𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))))
76 ssrab2 3884 . . . . . . . . . . . . . . . . . . . . . . 23 {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ⊆ 𝐴
77 dfss4 4060 . . . . . . . . . . . . . . . . . . . . . . 23 ({𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ⊆ 𝐴 ↔ (𝐴 ∖ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) = {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})
7876, 77mpbi 221 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴 ∖ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) = {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}
7978eleq2i 2877 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) ↔ 𝑏 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})
80 eqeq2 2817 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 = 𝑏 → ((𝑓𝑀) = 𝑐 ↔ (𝑓𝑀) = 𝑏))
8180anbi1d 617 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = 𝑏 → (((𝑓𝑀) = 𝑐𝜏) ↔ ((𝑓𝑀) = 𝑏𝜏)))
82813anbi2d 1558 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = 𝑏 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
8382exbidv 2012 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 = 𝑏 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
8483rexbidv 3240 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 = 𝑏 → (∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
8584elrab3 3560 . . . . . . . . . . . . . . . . . . . . 21 (𝑏𝐴 → (𝑏 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
8679, 85syl5bb 274 . . . . . . . . . . . . . . . . . . . 20 (𝑏𝐴 → (𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
8775, 86sylibd 230 . . . . . . . . . . . . . . . . . . 19 (𝑏𝐴 → (¬ 𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
8887ad2antll 711 . . . . . . . . . . . . . . . . . 18 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (¬ 𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
89 oveq2 6882 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑚 → (𝑀...𝑛) = (𝑀...𝑚))
9089feq2d 6242 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑚 → (𝑓:(𝑀...𝑛)⟶𝐴𝑓:(𝑀...𝑚)⟶𝐴))
91 fveq2 6408 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑚 → (𝑓𝑛) = (𝑓𝑚))
9291sbceq1d 3638 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑚 → ([(𝑓𝑛) / 𝑎]𝜃[(𝑓𝑚) / 𝑎]𝜃))
9338, 92syl5bbr 276 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑚 → (𝜏[(𝑓𝑚) / 𝑎]𝜃))
9493anbi2d 616 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑚 → (((𝑓𝑀) = 𝑏𝜏) ↔ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃)))
95 oveq2 6882 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑚 → (𝑁...𝑛) = (𝑁...𝑚))
9695raleqdv 3333 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑚 → (∀𝑘 ∈ (𝑁...𝑛)𝜒 ↔ ∀𝑘 ∈ (𝑁...𝑚)𝜒))
9790, 94, 963anbi123d 1553 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑚 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒)))
9897exbidv 2012 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑚 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒)))
9998cbvrexv 3361 . . . . . . . . . . . . . . . . . . . 20 (∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑚𝑍𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒))
100 feq1 6237 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = 𝑔 → (𝑓:(𝑀...𝑚)⟶𝐴𝑔:(𝑀...𝑚)⟶𝐴))
101 fveq1 6407 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 = 𝑔 → (𝑓𝑀) = (𝑔𝑀))
102101eqeq1d 2808 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑔 → ((𝑓𝑀) = 𝑏 ↔ (𝑔𝑀) = 𝑏))
103 fveq1 6407 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 = 𝑔 → (𝑓𝑚) = (𝑔𝑚))
104103sbceq1d 3638 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑔 → ([(𝑓𝑚) / 𝑎]𝜃[(𝑔𝑚) / 𝑎]𝜃))
105102, 104anbi12d 618 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = 𝑔 → (((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ↔ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃)))
106 fvex 6421 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓‘(𝑘 − 1)) ∈ V
107 fdc.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 = (𝑓‘(𝑘 − 1)) → (𝜑𝜓))
108107sbcbidv 3688 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = (𝑓‘(𝑘 − 1)) → ([(𝑓𝑘) / 𝑏]𝜑[(𝑓𝑘) / 𝑏]𝜓))
109106, 108sbcie 3668 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓𝑘) / 𝑏]𝜑[(𝑓𝑘) / 𝑏]𝜓)
110 fvex 6421 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓𝑘) ∈ V
111 fdc.6 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 = (𝑓𝑘) → (𝜓𝜒))
112110, 111sbcie 3668 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([(𝑓𝑘) / 𝑏]𝜓𝜒)
113109, 112bitri 266 . . . . . . . . . . . . . . . . . . . . . . . . 25 ([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓𝑘) / 𝑏]𝜑𝜒)
114 fveq1 6407 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 = 𝑔 → (𝑓‘(𝑘 − 1)) = (𝑔‘(𝑘 − 1)))
115 fveq1 6407 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓 = 𝑔 → (𝑓𝑘) = (𝑔𝑘))
116115sbceq1d 3638 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 = 𝑔 → ([(𝑓𝑘) / 𝑏]𝜑[(𝑔𝑘) / 𝑏]𝜑))
117114, 116sbceqbid 3640 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 = 𝑔 → ([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓𝑘) / 𝑏]𝜑[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑))
118113, 117syl5bbr 276 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑔 → (𝜒[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑))
119118ralbidv 3174 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = 𝑔 → (∀𝑘 ∈ (𝑁...𝑚)𝜒 ↔ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑))
120100, 105, 1193anbi123d 1553 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = 𝑔 → ((𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒) ↔ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)))
121120cbvexvw 2137 . . . . . . . . . . . . . . . . . . . . 21 (∃𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒) ↔ ∃𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑))
122121rexbii 3229 . . . . . . . . . . . . . . . . . . . 20 (∃𝑚𝑍𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒) ↔ ∃𝑚𝑍𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑))
12399, 122bitri 266 . . . . . . . . . . . . . . . . . . 19 (∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑚𝑍𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑))
1245peano2uzs 11960 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚𝑍 → (𝑚 + 1) ∈ 𝑍)
125124ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → (𝑚 + 1) ∈ 𝑍)
126 sbceq2a 3645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑑 = 𝑏 → ([𝑑 / 𝑏]𝜑𝜑))
127126anbi1d 617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑑 = 𝑏 → (([𝑑 / 𝑏]𝜑𝑎𝐴) ↔ (𝜑𝑎𝐴)))
128127anbi1d 617 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑑 = 𝑏 → ((([𝑑 / 𝑏]𝜑𝑎𝐴) ∧ 𝑚𝑍) ↔ ((𝜑𝑎𝐴) ∧ 𝑚𝑍)))
129 eqeq2 2817 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑑 = 𝑏 → ((𝑔𝑀) = 𝑑 ↔ (𝑔𝑀) = 𝑏))
130129anbi1d 617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑑 = 𝑏 → (((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ↔ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃)))
1311303anbi2d 1558 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑑 = 𝑏 → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) ↔ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)))
132131imbi1d 332 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑑 = 𝑏 → (((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)) ↔ ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))))
133128, 132imbi12d 335 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑑 = 𝑏 → (((([𝑑 / 𝑏]𝜑𝑎𝐴) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))) ↔ (((𝜑𝑎𝐴) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))))
134 sbceq2a 3645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑐 = 𝑎 → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑[𝑑 / 𝑏]𝜑))
135 eleq1 2873 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑐 = 𝑎 → (𝑐𝐴𝑎𝐴))
136134, 135anbi12d 618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 = 𝑎 → (([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ↔ ([𝑑 / 𝑏]𝜑𝑎𝐴)))
137136anbi1d 617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = 𝑎 → ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ↔ (([𝑑 / 𝑏]𝜑𝑎𝐴) ∧ 𝑚𝑍)))
138 eqeq2 2817 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 = 𝑎 → ((𝑓𝑀) = 𝑐 ↔ (𝑓𝑀) = 𝑎))
139138anbi1d 617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑐 = 𝑎 → (((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ↔ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃)))
1401393anbi2d 1558 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑐 = 𝑎 → ((𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒) ↔ (𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
141140exbidv 2012 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 = 𝑎 → (∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒) ↔ ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
142141imbi2d 331 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = 𝑎 → (((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)) ↔ ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))))
143137, 142imbi12d 335 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 = 𝑎 → (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))) ↔ ((([𝑑 / 𝑏]𝜑𝑎𝐴) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))))
144 peano2uz 11959 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑚 ∈ (ℤ𝑀) → (𝑚 + 1) ∈ (ℤ𝑀))
145144, 5eleq2s 2903 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑚𝑍 → (𝑚 + 1) ∈ (ℤ𝑀))
146 elfzp12 12642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑚 + 1) ∈ (ℤ𝑀) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↔ (𝑥 = 𝑀𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)))))
147145, 146syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑚𝑍 → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↔ (𝑥 = 𝑀𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)))))
148147ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↔ (𝑥 = 𝑀𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)))))
149 iftrue 4285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑥 = 𝑀 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = 𝑐)
150149eleq1d 2870 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑥 = 𝑀 → (if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴𝑐𝐴))
151150biimprcd 241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑐𝐴 → (𝑥 = 𝑀 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
152151ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 = 𝑀 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
153 1re 10325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 1 ∈ ℝ
15446, 153readdcli 10340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑀 + 1) ∈ ℝ
15546, 154ltnlei 10443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑀 < (𝑀 + 1) ↔ ¬ (𝑀 + 1) ≤ 𝑀)
15647, 155mpbi 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ¬ (𝑀 + 1) ≤ 𝑀
157 eleq1 2873 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑥 = 𝑀 → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) ↔ 𝑀 ∈ ((𝑀 + 1)...(𝑚 + 1))))
158 elfzle1 12567 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑀 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑀 + 1) ≤ 𝑀)
159157, 158syl6bi 244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑥 = 𝑀 → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑀 + 1) ≤ 𝑀))
160159com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 = 𝑀 → (𝑀 + 1) ≤ 𝑀))
161156, 160mtoi 190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → ¬ 𝑥 = 𝑀)
162161adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑚𝑍𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → ¬ 𝑥 = 𝑀)
163162iffalsed 4290 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑚𝑍𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = (𝑔‘(𝑥 − 1)))
164 elfzelz 12565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → 𝑥 ∈ ℤ)
165164adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → 𝑥 ∈ ℤ)
166 eluzelz 11914 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑚 ∈ (ℤ𝑀) → 𝑚 ∈ ℤ)
167166, 5eleq2s 2903 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑚𝑍𝑚 ∈ ℤ)
168167peano2zd 11751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑚𝑍 → (𝑚 + 1) ∈ ℤ)
169 1z 11673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 1 ∈ ℤ
170 fzsubel 12600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ((((𝑀 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ (𝑥 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) ↔ (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))))
171170biimpd 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((((𝑀 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ (𝑥 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))))
172169, 171mpanr2 687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ((((𝑀 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ 𝑥 ∈ ℤ) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))))
17349, 172mpanl1 683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (((𝑚 + 1) ∈ ℤ ∧ 𝑥 ∈ ℤ) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))))
174173ex 399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑚 + 1) ∈ ℤ → (𝑥 ∈ ℤ → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)))))
175168, 174syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑚𝑍 → (𝑥 ∈ ℤ → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)))))
176175com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑚𝑍 → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 ∈ ℤ → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)))))
177176imp 395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑥 ∈ ℤ → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))))
178165, 177mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)))
17946recni 10339 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 𝑀 ∈ ℂ
180 ax-1cn 10279 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 1 ∈ ℂ
181179, 180pncan3oi 10582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑀 + 1) − 1) = 𝑀
182181a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑚𝑍 → ((𝑀 + 1) − 1) = 𝑀)
183167zcnd 11749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑚𝑍𝑚 ∈ ℂ)
184 pncan 10572 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑚 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑚 + 1) − 1) = 𝑚)
185183, 180, 184sylancl 576 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑚𝑍 → ((𝑚 + 1) − 1) = 𝑚)
186182, 185oveq12d 6892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑚𝑍 → (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑀...𝑚))
187186adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑀...𝑚))
188178, 187eleqtrd 2887 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚𝑍𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑥 − 1) ∈ (𝑀...𝑚))
189 ffvelrn 6579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ (𝑥 − 1) ∈ (𝑀...𝑚)) → (𝑔‘(𝑥 − 1)) ∈ 𝐴)
190188, 189sylan2 582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ (𝑚𝑍𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)))) → (𝑔‘(𝑥 − 1)) ∈ 𝐴)
191190anassrs 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑔:(𝑀...𝑚)⟶𝐴𝑚𝑍) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑔‘(𝑥 − 1)) ∈ 𝐴)
192191ancom1s 635 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑚𝑍𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑔‘(𝑥 − 1)) ∈ 𝐴)
193163, 192eqeltrd 2885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑚𝑍𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴)
194193ex 399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑚𝑍𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
195194adantll 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
196152, 195jaod 877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → ((𝑥 = 𝑀𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
197148, 196sylbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
198197ralrimiv 3153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → ∀𝑥 ∈ (𝑀...(𝑚 + 1))if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴)
199 eqid 2806 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))
200199fmpt 6602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (∀𝑥 ∈ (𝑀...(𝑚 + 1))if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴 ↔ (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴)
201198, 200sylib 209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴)
202201adantlll 700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴)
2032023ad2antr1 1232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴)
204 eluzfz1 12571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑚 + 1) ∈ (ℤ𝑀) → 𝑀 ∈ (𝑀...(𝑚 + 1)))
205144, 204syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑚 ∈ (ℤ𝑀) → 𝑀 ∈ (𝑀...(𝑚 + 1)))
206205, 5eleq2s 2903 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑚𝑍𝑀 ∈ (𝑀...(𝑚 + 1)))
207 vex 3394 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑐 ∈ V
208149, 199, 207fvmpt 6503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑀 ∈ (𝑀...(𝑚 + 1)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐)
209206, 208syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑚𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐)
210209ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐)
211 eluzfz2 12572 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑚 + 1) ∈ (ℤ𝑀) → (𝑚 + 1) ∈ (𝑀...(𝑚 + 1)))
212144, 211syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑚 ∈ (ℤ𝑀) → (𝑚 + 1) ∈ (𝑀...(𝑚 + 1)))
213212, 5eleq2s 2903 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑚𝑍 → (𝑚 + 1) ∈ (𝑀...(𝑚 + 1)))
214 eqeq1 2810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑥 = (𝑚 + 1) → (𝑥 = 𝑀 ↔ (𝑚 + 1) = 𝑀))
215 fvoveq1 6897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑥 = (𝑚 + 1) → (𝑔‘(𝑥 − 1)) = (𝑔‘((𝑚 + 1) − 1)))
216214, 215ifbieq2d 4304 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑥 = (𝑚 + 1) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1))))
217 fvex 6421 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑔‘((𝑚 + 1) − 1)) ∈ V
218207, 217ifex 4327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1))) ∈ V
219216, 199, 218fvmpt 6503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑚 + 1) ∈ (𝑀...(𝑚 + 1)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) = if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1))))
220213, 219syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑚𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) = if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1))))
221 eluzle 11917 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑚 ∈ (ℤ𝑀) → 𝑀𝑚)
222221, 5eleq2s 2903 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑚𝑍𝑀𝑚)
223 zleltp1 11694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑀𝑚𝑀 < (𝑚 + 1)))
2242, 167, 223sylancr 577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑚𝑍 → (𝑀𝑚𝑀 < (𝑚 + 1)))
225222, 224mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑚𝑍𝑀 < (𝑚 + 1))
226 ltne 10419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑀 ∈ ℝ ∧ 𝑀 < (𝑚 + 1)) → (𝑚 + 1) ≠ 𝑀)
22746, 225, 226sylancr 577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑚𝑍 → (𝑚 + 1) ≠ 𝑀)
228227neneqd 2983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑚𝑍 → ¬ (𝑚 + 1) = 𝑀)
229228iffalsed 4290 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑚𝑍 → if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1))) = (𝑔‘((𝑚 + 1) − 1)))
230185fveq2d 6412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑚𝑍 → (𝑔‘((𝑚 + 1) − 1)) = (𝑔𝑚))
231220, 229, 2303eqtrd 2844 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑚𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) = (𝑔𝑚))
232231sbceq1d 3638 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑚𝑍 → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃[(𝑔𝑚) / 𝑎]𝜃))
233232biimpar 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑚𝑍[(𝑔𝑚) / 𝑎]𝜃) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃)
234233ad2ant2l 743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃)) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃)
2352343ad2antr2 1233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃)
236 eluzp1p1 11930 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑚 ∈ (ℤ𝑀) → (𝑚 + 1) ∈ (ℤ‘(𝑀 + 1)))
237236, 5eleq2s 2903 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑚𝑍 → (𝑚 + 1) ∈ (ℤ‘(𝑀 + 1)))
23844fveq2i 6411 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (ℤ𝑁) = (ℤ‘(𝑀 + 1))
239237, 238syl6eleqr 2896 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑚𝑍 → (𝑚 + 1) ∈ (ℤ𝑁))
240 elfzp12 12642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑚 + 1) ∈ (ℤ𝑁) → (𝑗 ∈ (𝑁...(𝑚 + 1)) ↔ (𝑗 = 𝑁𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)))))
241239, 240syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑚𝑍 → (𝑗 ∈ (𝑁...(𝑚 + 1)) ↔ (𝑗 = 𝑁𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)))))
242241biimpa 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑚𝑍𝑗 ∈ (𝑁...(𝑚 + 1))) → (𝑗 = 𝑁𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))))
243242adantll 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ 𝑗 ∈ (𝑁...(𝑚 + 1))) → (𝑗 = 𝑁𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))))
244243adantlr 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) ∧ 𝑗 ∈ (𝑁...(𝑚 + 1))) → (𝑗 = 𝑁𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))))
245 oveq1 6881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑗 = 𝑁 → (𝑗 − 1) = (𝑁 − 1))
24644oveq1i 6884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑁 − 1) = ((𝑀 + 1) − 1)
247246, 181eqtri 2828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑁 − 1) = 𝑀
248245, 247syl6eq 2856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑗 = 𝑁 → (𝑗 − 1) = 𝑀)
249248fveq2d 6412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑗 = 𝑁 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀))
250249ad2antll 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀))
251209adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐)
252250, 251eqtrd 2840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = 𝑐)
25344eqeq2i 2818 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑗 = 𝑁𝑗 = (𝑀 + 1))
254 fveq2 6408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑗 = (𝑀 + 1) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)))
255253, 254sylbi 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑗 = 𝑁 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)))
256255ad2antll 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)))
25746, 154, 47ltleii 10445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 𝑀 ≤ (𝑀 + 1)
258 eluz2 11910 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((𝑀 + 1) ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑀 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑀 + 1)))
2592, 49, 257, 258mpbir3an 1434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑀 + 1) ∈ (ℤ𝑀)
260 fzss1 12603 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ((𝑀 + 1) ∈ (ℤ𝑀) → ((𝑀 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1)))
261259, 260ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((𝑀 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1))
262 eluzfz1 12571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (𝑚 ∈ (ℤ𝑀) → 𝑀 ∈ (𝑀...𝑚))
263262, 5eleq2s 2903 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑚𝑍𝑀 ∈ (𝑀...𝑚))
264 fzaddel 12598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (((𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑀 ∈ (𝑀...𝑚) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1))))
2652, 169, 264mpanr12 688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑀 ∈ (𝑀...𝑚) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1))))
2662, 167, 265sylancr 577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑚𝑍 → (𝑀 ∈ (𝑀...𝑚) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1))))
267263, 266mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑚𝑍 → (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1)))
268261, 267sseldi 3796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑚𝑍 → (𝑀 + 1) ∈ (𝑀...(𝑚 + 1)))
269 eqeq1 2810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑥 = (𝑀 + 1) → (𝑥 = 𝑀 ↔ (𝑀 + 1) = 𝑀))
270 oveq1 6881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (𝑥 = (𝑀 + 1) → (𝑥 − 1) = ((𝑀 + 1) − 1))
271270, 181syl6eq 2856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (𝑥 = (𝑀 + 1) → (𝑥 − 1) = 𝑀)
272271fveq2d 6412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑥 = (𝑀 + 1) → (𝑔‘(𝑥 − 1)) = (𝑔𝑀))
273269, 272ifbieq2d 4304 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑥 = (𝑀 + 1) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if((𝑀 + 1) = 𝑀, 𝑐, (𝑔𝑀)))
274 fvex 6421 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑔𝑀) ∈ V
275207, 274ifex 4327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 if((𝑀 + 1) = 𝑀, 𝑐, (𝑔𝑀)) ∈ V
276273, 199, 275fvmpt 6503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑀 + 1) ∈ (𝑀...(𝑚 + 1)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)) = if((𝑀 + 1) = 𝑀, 𝑐, (𝑔𝑀)))
277268, 276syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑚𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)) = if((𝑀 + 1) = 𝑀, 𝑐, (𝑔𝑀)))
27846, 47gtneii 10434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑀 + 1) ≠ 𝑀
279 ifnefalse 4291 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑀 + 1) ≠ 𝑀 → if((𝑀 + 1) = 𝑀, 𝑐, (𝑔𝑀)) = (𝑔𝑀))
280278, 279ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 if((𝑀 + 1) = 𝑀, 𝑐, (𝑔𝑀)) = (𝑔𝑀)
281277, 280syl6eq 2856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑚𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)) = (𝑔𝑀))
282281adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)) = (𝑔𝑀))
283 simprl 778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → (𝑔𝑀) = 𝑑)
284256, 282, 2833eqtrd 2844 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = 𝑑)
285284sbceq1d 3638 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑[𝑑 / 𝑏]𝜑))
286252, 285sbceqbid 3640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑))
287286biimparc 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ (𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
288287anassrs 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
289288anassrs 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ (𝑔𝑀) = 𝑑) ∧ 𝑗 = 𝑁) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
290289adantlrr 703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) ∧ 𝑗 = 𝑁) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
291 elfzelz 12565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → 𝑗 ∈ ℤ)
292291adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → 𝑗 ∈ ℤ)
29344, 49eqeltri 2881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 𝑁 ∈ ℤ
294 peano2z 11684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑁 ∈ ℤ → (𝑁 + 1) ∈ ℤ)
295293, 294ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑁 + 1) ∈ ℤ
296 fzsubel 12600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((((𝑁 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ (𝑗 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) ↔ (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1))))
297296biimpd 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ((((𝑁 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ (𝑗 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1))))
298169, 297mpanr2 687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((((𝑁 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ 𝑗 ∈ ℤ) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1))))
299298ex 399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (((𝑁 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) → (𝑗 ∈ ℤ → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)))))
300295, 168, 299sylancr 577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑚𝑍 → (𝑗 ∈ ℤ → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)))))
301300com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑚𝑍 → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 ∈ ℤ → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)))))
302301imp 395 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 ∈ ℤ → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1))))
303292, 302mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)))
304293zrei 11649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 𝑁 ∈ ℝ
305304recni 10339 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 𝑁 ∈ ℂ
306305, 180pncan3oi 10582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑁 + 1) − 1) = 𝑁
307306a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑚𝑍 → ((𝑁 + 1) − 1) = 𝑁)
308307, 185oveq12d 6892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑚𝑍 → (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑁...𝑚))
309308adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑁...𝑚))
310303, 309eleqtrd 2887 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 − 1) ∈ (𝑁...𝑚))
311 fvoveq1 6897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑘 = (𝑗 − 1) → (𝑔‘(𝑘 − 1)) = (𝑔‘((𝑗 − 1) − 1)))
312 fveq2 6408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑘 = (𝑗 − 1) → (𝑔𝑘) = (𝑔‘(𝑗 − 1)))
313312sbceq1d 3638 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑘 = (𝑗 − 1) → ([(𝑔𝑘) / 𝑏]𝜑[(𝑔‘(𝑗 − 1)) / 𝑏]𝜑))
314311, 313sbceqbid 3640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑘 = (𝑗 − 1) → ([(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑[(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑))
315314rspcva 3500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑗 − 1) ∈ (𝑁...𝑚) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → [(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑)
316310, 315sylan 571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → [(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑)
31744, 259eqeltri 2881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 𝑁 ∈ (ℤ𝑀)
318 fzss1 12603 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑁 ∈ (ℤ𝑀) → (𝑁...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1)))
319317, 318ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑁...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1))
320 fzssp1 12607 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑁...𝑚) ⊆ (𝑁...(𝑚 + 1))
321320, 310sseldi 3796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 − 1) ∈ (𝑁...(𝑚 + 1)))
322319, 321sseldi 3796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 − 1) ∈ (𝑀...(𝑚 + 1)))
323 eqeq1 2810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑥 = (𝑗 − 1) → (𝑥 = 𝑀 ↔ (𝑗 − 1) = 𝑀))
324 fvoveq1 6897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑥 = (𝑗 − 1) → (𝑔‘(𝑥 − 1)) = (𝑔‘((𝑗 − 1) − 1)))
325323, 324ifbieq2d 4304 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑥 = (𝑗 − 1) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1))))
326 fvex 6421 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑔‘((𝑗 − 1) − 1)) ∈ V
327207, 326ifex 4327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1))) ∈ V
328325, 199, 327fvmpt 6503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑗 − 1) ∈ (𝑀...(𝑚 + 1)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1))))
329322, 328syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1))))
330154ltp1i 11212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑀 + 1) < ((𝑀 + 1) + 1)
33144oveq1i 6884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑁 + 1) = ((𝑀 + 1) + 1)
332330, 331breqtrri 4871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑀 + 1) < (𝑁 + 1)
333304, 153readdcli 10340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑁 + 1) ∈ ℝ
334154, 333ltnlei 10443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((𝑀 + 1) < (𝑁 + 1) ↔ ¬ (𝑁 + 1) ≤ (𝑀 + 1))
335332, 334mpbi 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ¬ (𝑁 + 1) ≤ (𝑀 + 1)
336291zcnd 11749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → 𝑗 ∈ ℂ)
337 subadd 10569 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((𝑗 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑀 ∈ ℂ) → ((𝑗 − 1) = 𝑀 ↔ (1 + 𝑀) = 𝑗))
338180, 179, 337mp3an23 1570 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑗 ∈ ℂ → ((𝑗 − 1) = 𝑀 ↔ (1 + 𝑀) = 𝑗))
339336, 338syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ((𝑗 − 1) = 𝑀 ↔ (1 + 𝑀) = 𝑗))
340 eqcom 2813 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((1 + 𝑀) = 𝑗𝑗 = (1 + 𝑀))
341180, 179addcomi 10512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (1 + 𝑀) = (𝑀 + 1)
342341eqeq2i 2818 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (𝑗 = (1 + 𝑀) ↔ 𝑗 = (𝑀 + 1))
343340, 342bitri 266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ((1 + 𝑀) = 𝑗𝑗 = (𝑀 + 1))
344 eleq1 2873 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (𝑗 = (𝑀 + 1) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) ↔ (𝑀 + 1) ∈ ((𝑁 + 1)...(𝑚 + 1))))
345 elfzle1 12567 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ((𝑀 + 1) ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑁 + 1) ≤ (𝑀 + 1))
346344, 345syl6bi 244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (𝑗 = (𝑀 + 1) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑁 + 1) ≤ (𝑀 + 1)))
347346com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 = (𝑀 + 1) → (𝑁 + 1) ≤ (𝑀 + 1)))
348343, 347syl5bi 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ((1 + 𝑀) = 𝑗 → (𝑁 + 1) ≤ (𝑀 + 1)))
349339, 348sylbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ((𝑗 − 1) = 𝑀 → (𝑁 + 1) ≤ (𝑀 + 1)))
350335, 349mtoi 190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ¬ (𝑗 − 1) = 𝑀)
351350adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ¬ (𝑗 − 1) = 𝑀)
352351iffalsed 4290 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1))) = (𝑔‘((𝑗 − 1) − 1)))
353329, 352eqtrd 2840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = (𝑔‘((𝑗 − 1) − 1)))
354 peano2uz 11959 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑁 ∈ (ℤ𝑀) → (𝑁 + 1) ∈ (ℤ𝑀))
355 fzss1 12603 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((𝑁 + 1) ∈ (ℤ𝑀) → ((𝑁 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1)))
356317, 354, 355mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑁 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1))
357 simpr 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)))
358356, 357sseldi 3796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → 𝑗 ∈ (𝑀...(𝑚 + 1)))
359 eqeq1 2810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑥 = 𝑗 → (𝑥 = 𝑀𝑗 = 𝑀))
360 fvoveq1 6897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑥 = 𝑗 → (𝑔‘(𝑥 − 1)) = (𝑔‘(𝑗 − 1)))
361359, 360ifbieq2d 4304 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑥 = 𝑗 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))))
362 fvex 6421 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑔‘(𝑗 − 1)) ∈ V
363207, 362ifex 4327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))) ∈ V
364361, 199, 363fvmpt 6503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑗 ∈ (𝑀...(𝑚 + 1)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))))
365358, 364syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))))
36647, 44breqtrri 4871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 𝑀 < 𝑁
367304ltp1i 11212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 𝑁 < (𝑁 + 1)
36846, 304, 333lttri 10448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((𝑀 < 𝑁𝑁 < (𝑁 + 1)) → 𝑀 < (𝑁 + 1))
369366, 367, 368mp2an 675 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 𝑀 < (𝑁 + 1)
37046, 333ltnlei 10443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑀 < (𝑁 + 1) ↔ ¬ (𝑁 + 1) ≤ 𝑀)
371369, 370mpbi 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ¬ (𝑁 + 1) ≤ 𝑀
372 eleq1 2873 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (𝑗 = 𝑀 → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) ↔ 𝑀 ∈ ((𝑁 + 1)...(𝑚 + 1))))
373 elfzle1 12567 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (𝑀 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑁 + 1) ≤ 𝑀)
374372, 373syl6bi 244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑗 = 𝑀 → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑁 + 1) ≤ 𝑀))
375374com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 = 𝑀 → (𝑁 + 1) ≤ 𝑀))
376371, 375mtoi 190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ¬ 𝑗 = 𝑀)
377376adantl 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ¬ 𝑗 = 𝑀)
378377iffalsed 4290 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))) = (𝑔‘(𝑗 − 1)))
379365, 378eqtrd 2840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = (𝑔‘(𝑗 − 1)))
380379sbceq1d 3638 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑[(𝑔‘(𝑗 − 1)) / 𝑏]𝜑))
381353, 380sbceqbid 3640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑[(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑))
382381biimpar 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) ∧ [(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
383316, 382syldan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
384383an32s 634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑚𝑍 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
385384adantlrl 702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
386385adantlll 700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
387290, 386jaodan 971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) ∧ (𝑗 = 𝑁𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
388244, 387syldan 581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) ∧ 𝑗 ∈ (𝑁...(𝑚 + 1))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
389388ralrimiva 3154 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∀𝑗 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
390 fvoveq1 6897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 = 𝑘 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)))
391 fveq2 6408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑗 = 𝑘 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘))
392391sbceq1d 3638 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 = 𝑘 → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
393390, 392sbceqbid 3640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑗 = 𝑘 → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
394393cbvralv 3360 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (∀𝑗 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑 ↔ ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
395389, 394sylib 209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
396395adantllr 701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
397396adantrlr 705 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ (((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
3983973adantr1 1203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
399 ovex 6906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑀...(𝑚 + 1)) ∈ V
400399mptex 6711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) ∈ V
401 feq1 6237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ↔ (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴))
402 fveq1 6407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓𝑀) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀))
403402eqeq1d 2808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ((𝑓𝑀) = 𝑐 ↔ ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐))
404 fveq1 6407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓‘(𝑚 + 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)))
405404sbceq1d 3638 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ([(𝑓‘(𝑚 + 1)) / 𝑎]𝜃[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃))
406403, 405anbi12d 618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ↔ (((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃)))
407 fveq1 6407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓‘(𝑘 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)))
408 fveq1 6407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓𝑘) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘))
409408sbceq1d 3638 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ([(𝑓𝑘) / 𝑏]𝜑[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
410407, 409sbceqbid 3640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓𝑘) / 𝑏]𝜑[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
411113, 410syl5bbr 276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝜒[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
412411ralbidv 3174 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒 ↔ ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
413401, 406, 4123anbi123d 1553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ((𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒) ↔ ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴 ∧ (((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)))
414400, 413spcev 3493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴 ∧ (((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))
415203, 210, 235, 398, 414syl121anc 1487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))
416415ex 399 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
417143, 416chvarv 2437 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((([𝑑 / 𝑏]𝜑𝑎𝐴) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
418133, 417chvarv 2437 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑎𝐴) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
419418adantlrr 703 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
420419adantlll 700 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
421420imp 395 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))
422 oveq2 6882 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = (𝑚 + 1) → (𝑀...𝑛) = (𝑀...(𝑚 + 1)))
423422feq2d 6242 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = (𝑚 + 1) → (𝑓:(𝑀...𝑛)⟶𝐴𝑓:(𝑀...(𝑚 + 1))⟶𝐴))
424 fveq2 6408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = (𝑚 + 1) → (𝑓𝑛) = (𝑓‘(𝑚 + 1)))
425424sbceq1d 3638 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = (𝑚 + 1) → ([(𝑓𝑛) / 𝑎]𝜃[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃))
42638, 425syl5bbr 276 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = (𝑚 + 1) → (𝜏[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃))
427426anbi2d 616 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = (𝑚 + 1) → (((𝑓𝑀) = 𝑎𝜏) ↔ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃)))
428 oveq2 6882 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = (𝑚 + 1) → (𝑁...𝑛) = (𝑁...(𝑚 + 1)))
429428raleqdv 3333 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = (𝑚 + 1) → (∀𝑘 ∈ (𝑁...𝑛)𝜒 ↔ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))
430423, 427, 4293anbi123d 1553 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = (𝑚 + 1) → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
431430exbidv 2012 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = (𝑚 + 1) → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
432431rspcev 3502 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑚 + 1) ∈ 𝑍 ∧ ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
433125, 421, 432syl2anc 575 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
434433ex 399 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
435434exlimdv 2024 . . . . . . . . . . . . . . . . . . . 20 ((((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) → (∃𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
436435rexlimdva 3219 . . . . . . . . . . . . . . . . . . 19 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (∃𝑚𝑍𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
437123, 436syl5bi 233 . . . . . . . . . . . . . . . . . 18 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
43873, 88, 4373syld 60 . . . . . . . . . . . . . . . . 17 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
439438an42s 643 . . . . . . . . . . . . . . . 16 (((𝜂𝑎𝐴) ∧ (𝑏𝐴𝜑)) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
440439rexlimdvaa 3220 . . . . . . . . . . . . . . 15 ((𝜂𝑎𝐴) → (∃𝑏𝐴 𝜑 → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))))
441440imp 395 . . . . . . . . . . . . . 14 (((𝜂𝑎𝐴) ∧ ∃𝑏𝐴 𝜑) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
442 fdc.10 . . . . . . . . . . . . . 14 ((𝜂𝑎𝐴) → (𝜃 ∨ ∃𝑏𝐴 𝜑))
44365, 441, 442mpjaodan 972 . . . . . . . . . . . . 13 ((𝜂𝑎𝐴) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
444138anbi1d 617 . . . . . . . . . . . . . . . . . 18 (𝑐 = 𝑎 → (((𝑓𝑀) = 𝑐𝜏) ↔ ((𝑓𝑀) = 𝑎𝜏)))
4454443anbi2d 1558 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑎 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
446445exbidv 2012 . . . . . . . . . . . . . . . 16 (𝑐 = 𝑎 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
447446rexbidv 3240 . . . . . . . . . . . . . . 15 (𝑐 = 𝑎 → (∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
448447elrab3 3560 . . . . . . . . . . . . . 14 (𝑎𝐴 → (𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
449448adantl 469 . . . . . . . . . . . . 13 ((𝜂𝑎𝐴) → (𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
450443, 449sylibrd 250 . . . . . . . . . . . 12 ((𝜂𝑎𝐴) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
451450ex 399 . . . . . . . . . . 11 (𝜂 → (𝑎𝐴 → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
452451com23 86 . . . . . . . . . 10 (𝜂 → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → (𝑎𝐴𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
453 eldif 3779 . . . . . . . . . . . 12 (𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ↔ (𝑎𝐴 ∧ ¬ 𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
454453notbii 311 . . . . . . . . . . 11 𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ↔ ¬ (𝑎𝐴 ∧ ¬ 𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
455 iman 390 . . . . . . . . . . 11 ((𝑎𝐴𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ↔ ¬ (𝑎𝐴 ∧ ¬ 𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
456454, 455bitr4i 269 . . . . . . . . . 10 𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ↔ (𝑎𝐴𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
457452, 456syl6ibr 243 . . . . . . . . 9 (𝜂 → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ¬ 𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
458457con2d 131 . . . . . . . 8 (𝜂 → (𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
459458imp 395 . . . . . . 7 ((𝜂𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) → ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
460459nrexdv 3188 . . . . . 6 (𝜂 → ¬ ∃𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
461 df-ne 2979 . . . . . . 7 ((𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅ ↔ ¬ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅)
462 fdc.9 . . . . . . . 8 (𝜂𝑅 Fr 𝐴)
463 difss 3936 . . . . . . . 8 (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴
464 fdc.1 . . . . . . . . . . 11 𝐴 ∈ V
465 difexg 5003 . . . . . . . . . . 11 (𝐴 ∈ V → (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∈ V)
466464, 465ax-mp 5 . . . . . . . . . 10 (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∈ V
467 fri 5273 . . . . . . . . . 10 ((((𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∈ V ∧ 𝑅 Fr 𝐴) ∧ ((𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴 ∧ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅)) → ∃𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
468466, 467mpanl1 683 . . . . . . . . 9 ((𝑅 Fr 𝐴 ∧ ((𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴 ∧ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅)) → ∃𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
469468expr 446 . . . . . . . 8 ((𝑅 Fr 𝐴 ∧ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴) → ((𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅ → ∃𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
470462, 463, 469sylancl 576 . . . . . . 7 (𝜂 → ((𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅ → ∃𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
471461, 470syl5bir 234 . . . . . 6 (𝜂 → (¬ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅ → ∃𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
472460, 471mt3d 142 . . . . 5 (𝜂 → (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅)
473 ssdif0 4143 . . . . 5 (𝐴 ⊆ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅)
474472, 473sylibr 225 . . . 4 (𝜂𝐴 ⊆ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})
47576a1i 11 . . . 4 (𝜂 → {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ⊆ 𝐴)
476474, 475eqssd 3815 . . 3 (𝜂𝐴 = {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})
477 rabid2 3307 . . 3 (𝐴 = {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∀𝑐𝐴𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
478476, 477sylib 209 . 2 (𝜂 → ∀𝑐𝐴𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
479 eqeq2 2817 . . . . . . 7 (𝑐 = 𝐶 → ((𝑓𝑀) = 𝑐 ↔ (𝑓𝑀) = 𝐶))
480479anbi1d 617 . . . . . 6 (𝑐 = 𝐶 → (((𝑓𝑀) = 𝑐𝜏) ↔ ((𝑓𝑀) = 𝐶𝜏)))
4814803anbi2d 1558 . . . . 5 (𝑐 = 𝐶 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝐶𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
482481exbidv 2012 . . . 4 (𝑐 = 𝐶 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝐶𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
483482rexbidv 3240 . . 3 (𝑐 = 𝐶 → (∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝐶𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
484483rspcva 3500 . 2 ((𝐶𝐴 ∧ ∀𝑐𝐴𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝐶𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
4851, 478, 484syl2anc 575 1 (𝜂 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝐶𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865  w3a 1100   = wceq 1637  wex 1859  wcel 2156  wne 2978  wral 3096  wrex 3097  {crab 3100  Vcvv 3391  [wsbc 3633  cdif 3766  wss 3769  c0 4116  ifcif 4279  {csn 4370  cop 4376   class class class wbr 4844  cmpt 4923   Fr wfr 5267  wf 6097  cfv 6101  (class class class)co 6874  cc 10219  cr 10220  1c1 10222   + caddc 10224   < clt 10359  cle 10360  cmin 10551  cz 11643  cuz 11904  ...cfz 12549
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179  ax-cnex 10277  ax-resscn 10278  ax-1cn 10279  ax-icn 10280  ax-addcl 10281  ax-addrcl 10282  ax-mulcl 10283  ax-mulrcl 10284  ax-mulcom 10285  ax-addass 10286  ax-mulass 10287  ax-distr 10288  ax-i2m1 10289  ax-1ne0 10290  ax-1rid 10291  ax-rnegex 10292  ax-rrecex 10293  ax-cnre 10294  ax-pre-lttri 10295  ax-pre-lttrn 10296  ax-pre-ltadd 10297  ax-pre-mulgt0 10298
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-riota 6835  df-ov 6877  df-oprab 6878  df-mpt2 6879  df-om 7296  df-1st 7398  df-2nd 7399  df-wrecs 7642  df-recs 7704  df-rdg 7742  df-er 7979  df-en 8193  df-dom 8194  df-sdom 8195  df-pnf 10361  df-mnf 10362  df-xr 10363  df-ltxr 10364  df-le 10365  df-sub 10553  df-neg 10554  df-nn 11306  df-n0 11560  df-z 11644  df-uz 11905  df-fz 12550
This theorem is referenced by:  fdc1  33853
  Copyright terms: Public domain W3C validator