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 36204
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 12778 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ𝑀))
42, 3ax-mp 5 . . . . . . . . . . . . . . . . . 18 𝑀 ∈ (ℤ𝑀)
5 fdc.3 . . . . . . . . . . . . . . . . . 18 𝑍 = (ℤ𝑀)
64, 5eleqtrri 2837 . . . . . . . . . . . . . . . . 17 𝑀𝑍
7 eqid 2736 . . . . . . . . . . . . . . . . . . . . . 22 {⟨𝑀, 𝑎⟩} = {⟨𝑀, 𝑎⟩}
82elexi 3464 . . . . . . . . . . . . . . . . . . . . . . 23 𝑀 ∈ V
9 vex 3449 . . . . . . . . . . . . . . . . . . . . . . 23 𝑎 ∈ V
108, 9fsn 7081 . . . . . . . . . . . . . . . . . . . . . 22 ({⟨𝑀, 𝑎⟩}:{𝑀}⟶{𝑎} ↔ {⟨𝑀, 𝑎⟩} = {⟨𝑀, 𝑎⟩})
117, 10mpbir 230 . . . . . . . . . . . . . . . . . . . . 21 {⟨𝑀, 𝑎⟩}:{𝑀}⟶{𝑎}
12 snssi 4768 . . . . . . . . . . . . . . . . . . . . 21 (𝑎𝐴 → {𝑎} ⊆ 𝐴)
13 fss 6685 . . . . . . . . . . . . . . . . . . . . 21 (({⟨𝑀, 𝑎⟩}:{𝑀}⟶{𝑎} ∧ {𝑎} ⊆ 𝐴) → {⟨𝑀, 𝑎⟩}:{𝑀}⟶𝐴)
1411, 12, 13sylancr 587 . . . . . . . . . . . . . . . . . . . 20 (𝑎𝐴 → {⟨𝑀, 𝑎⟩}:{𝑀}⟶𝐴)
15 fzsn 13483 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀})
162, 15ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (𝑀...𝑀) = {𝑀}
1716feq2i 6660 . . . . . . . . . . . . . . . . . . . 20 ({⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴 ↔ {⟨𝑀, 𝑎⟩}:{𝑀}⟶𝐴)
1814, 17sylibr 233 . . . . . . . . . . . . . . . . . . 19 (𝑎𝐴 → {⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴)
1918adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝑎𝐴𝜃) → {⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴)
208, 9fvsn 7127 . . . . . . . . . . . . . . . . . . 19 ({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎
2120a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝑎𝐴𝜃) → ({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎)
22 simpr 485 . . . . . . . . . . . . . . . . . 18 ((𝑎𝐴𝜃) → 𝜃)
23 snex 5388 . . . . . . . . . . . . . . . . . . 19 {⟨𝑀, 𝑎⟩} ∈ V
24 feq1 6649 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = {⟨𝑀, 𝑎⟩} → (𝑓:(𝑀...𝑀)⟶𝐴 ↔ {⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴))
25 fveq1 6841 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = {⟨𝑀, 𝑎⟩} → (𝑓𝑀) = ({⟨𝑀, 𝑎⟩}‘𝑀))
2625eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = {⟨𝑀, 𝑎⟩} → ((𝑓𝑀) = 𝑎 ↔ ({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎))
2725, 20eqtrdi 2792 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = {⟨𝑀, 𝑎⟩} → (𝑓𝑀) = 𝑎)
28 sbceq2a 3751 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓𝑀) = 𝑎 → ([(𝑓𝑀) / 𝑎]𝜃𝜃))
2927, 28syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = {⟨𝑀, 𝑎⟩} → ([(𝑓𝑀) / 𝑎]𝜃𝜃))
3026, 29anbi12d 631 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = {⟨𝑀, 𝑎⟩} → (((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃) ↔ (({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎𝜃)))
3124, 30anbi12d 631 . . . . . . . . . . . . . . . . . . 19 (𝑓 = {⟨𝑀, 𝑎⟩} → ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃)) ↔ ({⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴 ∧ (({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎𝜃))))
3223, 31spcev 3565 . . . . . . . . . . . . . . . . . 18 (({⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴 ∧ (({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎𝜃)) → ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃)))
3319, 21, 22, 32syl12anc 835 . . . . . . . . . . . . . . . . 17 ((𝑎𝐴𝜃) → ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃)))
34 oveq2 7365 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑀 → (𝑀...𝑛) = (𝑀...𝑀))
3534feq2d 6654 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑀 → (𝑓:(𝑀...𝑛)⟶𝐴𝑓:(𝑀...𝑀)⟶𝐴))
36 fvex 6855 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓𝑛) ∈ V
37 fdc.7 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = (𝑓𝑛) → (𝜃𝜏))
3836, 37sbcie 3782 . . . . . . . . . . . . . . . . . . . . . . 23 ([(𝑓𝑛) / 𝑎]𝜃𝜏)
39 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑀 → (𝑓𝑛) = (𝑓𝑀))
4039sbceq1d 3744 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑀 → ([(𝑓𝑛) / 𝑎]𝜃[(𝑓𝑀) / 𝑎]𝜃))
4138, 40bitr3id 284 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑀 → (𝜏[(𝑓𝑀) / 𝑎]𝜃))
4241anbi2d 629 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑀 → (((𝑓𝑀) = 𝑎𝜏) ↔ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃)))
43 oveq2 7365 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑀 → (𝑁...𝑛) = (𝑁...𝑀))
44 fdc.4 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑁 = (𝑀 + 1)
4544oveq1i 7367 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁...𝑀) = ((𝑀 + 1)...𝑀)
462zrei 12505 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑀 ∈ ℝ
4746ltp1i 12059 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑀 < (𝑀 + 1)
48 peano2z 12544 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑀 ∈ ℤ → (𝑀 + 1) ∈ ℤ)
492, 48ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑀 + 1) ∈ ℤ
50 fzn 13457 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑀 + 1) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 < (𝑀 + 1) ↔ ((𝑀 + 1)...𝑀) = ∅))
5149, 2, 50mp2an 690 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 < (𝑀 + 1) ↔ ((𝑀 + 1)...𝑀) = ∅)
5247, 51mpbi 229 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑀 + 1)...𝑀) = ∅
5345, 52eqtri 2764 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁...𝑀) = ∅
5443, 53eqtrdi 2792 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑀 → (𝑁...𝑛) = ∅)
5554raleqdv 3313 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑀 → (∀𝑘 ∈ (𝑁...𝑛)𝜒 ↔ ∀𝑘 ∈ ∅ 𝜒))
5635, 42, 553anbi123d 1436 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑀 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃) ∧ ∀𝑘 ∈ ∅ 𝜒)))
57 ral0 4470 . . . . . . . . . . . . . . . . . . . . 21 𝑘 ∈ ∅ 𝜒
58 df-3an 1089 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃) ∧ ∀𝑘 ∈ ∅ 𝜒) ↔ ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃)) ∧ ∀𝑘 ∈ ∅ 𝜒))
5957, 58mpbiran2 708 . . . . . . . . . . . . . . . . . . . 20 ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃) ∧ ∀𝑘 ∈ ∅ 𝜒) ↔ (𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃)))
6056, 59bitrdi 286 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑀 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃))))
6160exbidv 1924 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑀 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃))))
6261rspcev 3581 . . . . . . . . . . . . . . . . 17 ((𝑀𝑍 ∧ ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃))) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
636, 33, 62sylancr 587 . . . . . . . . . . . . . . . 16 ((𝑎𝐴𝜃) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
6463adantll 712 . . . . . . . . . . . . . . 15 (((𝜂𝑎𝐴) ∧ 𝜃) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
6564a1d 25 . . . . . . . . . . . . . 14 (((𝜂𝑎𝐴) ∧ 𝜃) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
66 fdc.11 . . . . . . . . . . . . . . . . . . . . 21 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → 𝑏𝑅𝑎)
67 breq1 5108 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑 = 𝑏 → (𝑑𝑅𝑎𝑏𝑅𝑎))
6867rspcev 3581 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∧ 𝑏𝑅𝑎) → ∃𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎)
6968expcom 414 . . . . . . . . . . . . . . . . . . . . 21 (𝑏𝑅𝑎 → (𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎))
7066, 69syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎))
71 dfrex2 3076 . . . . . . . . . . . . . . . . . . . 20 (∃𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎 ↔ ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
7270, 71syl6ib 250 . . . . . . . . . . . . . . . . . . 19 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
7372con2d 134 . . . . . . . . . . . . . . . . . 18 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ¬ 𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
74 eldif 3920 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) ↔ (𝑏𝐴 ∧ ¬ 𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
7574simplbi2 501 . . . . . . . . . . . . . . . . . . . 20 (𝑏𝐴 → (¬ 𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → 𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))))
76 ssrab2 4037 . . . . . . . . . . . . . . . . . . . . . . 23 {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ⊆ 𝐴
77 dfss4 4218 . . . . . . . . . . . . . . . . . . . . . . 23 ({𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ⊆ 𝐴 ↔ (𝐴 ∖ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) = {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})
7876, 77mpbi 229 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴 ∖ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) = {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}
7978eleq2i 2829 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) ↔ 𝑏 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})
80 eqeq2 2748 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 = 𝑏 → ((𝑓𝑀) = 𝑐 ↔ (𝑓𝑀) = 𝑏))
8180anbi1d 630 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = 𝑏 → (((𝑓𝑀) = 𝑐𝜏) ↔ ((𝑓𝑀) = 𝑏𝜏)))
82813anbi2d 1441 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = 𝑏 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
8382exbidv 1924 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 = 𝑏 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
8483rexbidv 3175 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 = 𝑏 → (∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
8584elrab3 3646 . . . . . . . . . . . . . . . . . . . . 21 (𝑏𝐴 → (𝑏 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
8679, 85bitrid 282 . . . . . . . . . . . . . . . . . . . 20 (𝑏𝐴 → (𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
8775, 86sylibd 238 . . . . . . . . . . . . . . . . . . 19 (𝑏𝐴 → (¬ 𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
8887ad2antll 727 . . . . . . . . . . . . . . . . . 18 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (¬ 𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
89 oveq2 7365 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑚 → (𝑀...𝑛) = (𝑀...𝑚))
9089feq2d 6654 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑚 → (𝑓:(𝑀...𝑛)⟶𝐴𝑓:(𝑀...𝑚)⟶𝐴))
91 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑚 → (𝑓𝑛) = (𝑓𝑚))
9291sbceq1d 3744 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑚 → ([(𝑓𝑛) / 𝑎]𝜃[(𝑓𝑚) / 𝑎]𝜃))
9338, 92bitr3id 284 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑚 → (𝜏[(𝑓𝑚) / 𝑎]𝜃))
9493anbi2d 629 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑚 → (((𝑓𝑀) = 𝑏𝜏) ↔ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃)))
95 oveq2 7365 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑚 → (𝑁...𝑛) = (𝑁...𝑚))
9695raleqdv 3313 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑚 → (∀𝑘 ∈ (𝑁...𝑛)𝜒 ↔ ∀𝑘 ∈ (𝑁...𝑚)𝜒))
9790, 94, 963anbi123d 1436 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑚 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒)))
9897exbidv 1924 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑚 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒)))
9998cbvrexvw 3226 . . . . . . . . . . . . . . . . . . . 20 (∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑚𝑍𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒))
100 feq1 6649 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = 𝑔 → (𝑓:(𝑀...𝑚)⟶𝐴𝑔:(𝑀...𝑚)⟶𝐴))
101 fveq1 6841 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 = 𝑔 → (𝑓𝑀) = (𝑔𝑀))
102101eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑔 → ((𝑓𝑀) = 𝑏 ↔ (𝑔𝑀) = 𝑏))
103 fveq1 6841 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 = 𝑔 → (𝑓𝑚) = (𝑔𝑚))
104103sbceq1d 3744 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑔 → ([(𝑓𝑚) / 𝑎]𝜃[(𝑔𝑚) / 𝑎]𝜃))
105102, 104anbi12d 631 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = 𝑔 → (((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ↔ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃)))
106 fvex 6855 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓‘(𝑘 − 1)) ∈ V
107 fdc.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 = (𝑓‘(𝑘 − 1)) → (𝜑𝜓))
108107sbcbidv 3798 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = (𝑓‘(𝑘 − 1)) → ([(𝑓𝑘) / 𝑏]𝜑[(𝑓𝑘) / 𝑏]𝜓))
109106, 108sbcie 3782 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓𝑘) / 𝑏]𝜑[(𝑓𝑘) / 𝑏]𝜓)
110 fvex 6855 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓𝑘) ∈ V
111 fdc.6 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 = (𝑓𝑘) → (𝜓𝜒))
112110, 111sbcie 3782 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([(𝑓𝑘) / 𝑏]𝜓𝜒)
113109, 112bitri 274 . . . . . . . . . . . . . . . . . . . . . . . . 25 ([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓𝑘) / 𝑏]𝜑𝜒)
114 fveq1 6841 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 = 𝑔 → (𝑓‘(𝑘 − 1)) = (𝑔‘(𝑘 − 1)))
115 fveq1 6841 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓 = 𝑔 → (𝑓𝑘) = (𝑔𝑘))
116115sbceq1d 3744 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 = 𝑔 → ([(𝑓𝑘) / 𝑏]𝜑[(𝑔𝑘) / 𝑏]𝜑))
117114, 116sbceqbid 3746 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 = 𝑔 → ([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓𝑘) / 𝑏]𝜑[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑))
118113, 117bitr3id 284 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑔 → (𝜒[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑))
119118ralbidv 3174 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = 𝑔 → (∀𝑘 ∈ (𝑁...𝑚)𝜒 ↔ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑))
120100, 105, 1193anbi123d 1436 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = 𝑔 → ((𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒) ↔ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)))
121120cbvexvw 2040 . . . . . . . . . . . . . . . . . . . . 21 (∃𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒) ↔ ∃𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑))
122121rexbii 3097 . . . . . . . . . . . . . . . . . . . 20 (∃𝑚𝑍𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒) ↔ ∃𝑚𝑍𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑))
12399, 122bitri 274 . . . . . . . . . . . . . . . . . . 19 (∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑚𝑍𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑))
1245peano2uzs 12827 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚𝑍 → (𝑚 + 1) ∈ 𝑍)
125124ad2antlr 725 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → (𝑚 + 1) ∈ 𝑍)
126 sbceq2a 3751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑑 = 𝑏 → ([𝑑 / 𝑏]𝜑𝜑))
127126anbi1d 630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑑 = 𝑏 → (([𝑑 / 𝑏]𝜑𝑎𝐴) ↔ (𝜑𝑎𝐴)))
128127anbi1d 630 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑑 = 𝑏 → ((([𝑑 / 𝑏]𝜑𝑎𝐴) ∧ 𝑚𝑍) ↔ ((𝜑𝑎𝐴) ∧ 𝑚𝑍)))
129 eqeq2 2748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑑 = 𝑏 → ((𝑔𝑀) = 𝑑 ↔ (𝑔𝑀) = 𝑏))
130129anbi1d 630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑑 = 𝑏 → (((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ↔ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃)))
1311303anbi2d 1441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑑 = 𝑏 → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) ↔ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)))
132131imbi1d 341 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑑 = 𝑏 → (((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)) ↔ ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))))
133128, 132imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑑 = 𝑏 → (((([𝑑 / 𝑏]𝜑𝑎𝐴) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))) ↔ (((𝜑𝑎𝐴) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))))
134 sbceq2a 3751 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑐 = 𝑎 → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑[𝑑 / 𝑏]𝜑))
135 eleq1 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑐 = 𝑎 → (𝑐𝐴𝑎𝐴))
136134, 135anbi12d 631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 = 𝑎 → (([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ↔ ([𝑑 / 𝑏]𝜑𝑎𝐴)))
137136anbi1d 630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = 𝑎 → ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ↔ (([𝑑 / 𝑏]𝜑𝑎𝐴) ∧ 𝑚𝑍)))
138 eqeq2 2748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 = 𝑎 → ((𝑓𝑀) = 𝑐 ↔ (𝑓𝑀) = 𝑎))
139138anbi1d 630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑐 = 𝑎 → (((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ↔ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃)))
1401393anbi2d 1441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑐 = 𝑎 → ((𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒) ↔ (𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
141140exbidv 1924 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 = 𝑎 → (∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒) ↔ ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
142141imbi2d 340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = 𝑎 → (((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)) ↔ ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))))
143137, 142imbi12d 344 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 = 𝑎 → (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))) ↔ ((([𝑑 / 𝑏]𝜑𝑎𝐴) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))))
144 peano2uz 12826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑚 ∈ (ℤ𝑀) → (𝑚 + 1) ∈ (ℤ𝑀))
145144, 5eleq2s 2856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑚𝑍 → (𝑚 + 1) ∈ (ℤ𝑀))
146 elfzp12 13520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑚 + 1) ∈ (ℤ𝑀) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↔ (𝑥 = 𝑀𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)))))
147145, 146syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑚𝑍 → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↔ (𝑥 = 𝑀𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)))))
148147ad2antlr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↔ (𝑥 = 𝑀𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)))))
149 iftrue 4492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑥 = 𝑀 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = 𝑐)
150149eleq1d 2822 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑥 = 𝑀 → (if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴𝑐𝐴))
151150biimprcd 249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑐𝐴 → (𝑥 = 𝑀 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
152151ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 = 𝑀 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
153 1re 11155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 1 ∈ ℝ
15446, 153readdcli 11170 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑀 + 1) ∈ ℝ
15546, 154ltnlei 11276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑀 < (𝑀 + 1) ↔ ¬ (𝑀 + 1) ≤ 𝑀)
15647, 155mpbi 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ¬ (𝑀 + 1) ≤ 𝑀
157 eleq1 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑥 = 𝑀 → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) ↔ 𝑀 ∈ ((𝑀 + 1)...(𝑚 + 1))))
158 elfzle1 13444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑀 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑀 + 1) ≤ 𝑀)
159157, 158syl6bi 252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑥 = 𝑀 → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑀 + 1) ≤ 𝑀))
160159com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 = 𝑀 → (𝑀 + 1) ≤ 𝑀))
161156, 160mtoi 198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → ¬ 𝑥 = 𝑀)
162161adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑚𝑍𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → ¬ 𝑥 = 𝑀)
163162iffalsed 4497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑚𝑍𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = (𝑔‘(𝑥 − 1)))
164 elfzelz 13441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → 𝑥 ∈ ℤ)
165164adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → 𝑥 ∈ ℤ)
166 eluzelz 12773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑚 ∈ (ℤ𝑀) → 𝑚 ∈ ℤ)
167166, 5eleq2s 2856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑚𝑍𝑚 ∈ ℤ)
168167peano2zd 12610 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑚𝑍 → (𝑚 + 1) ∈ ℤ)
169 1z 12533 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 1 ∈ ℤ
170 fzsubel 13477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ((((𝑀 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ (𝑥 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) ↔ (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))))
171170biimpd 228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((((𝑀 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ (𝑥 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))))
172169, 171mpanr2 702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ((((𝑀 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ 𝑥 ∈ ℤ) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))))
17349, 172mpanl1 698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (((𝑚 + 1) ∈ ℤ ∧ 𝑥 ∈ ℤ) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))))
174173ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑥 ∈ ℤ → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))))
178165, 177mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)))
17946recni 11169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 𝑀 ∈ ℂ
180 ax-1cn 11109 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 1 ∈ ℂ
181179, 180pncan3oi 11417 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑀 + 1) − 1) = 𝑀
182181a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑚𝑍 → ((𝑀 + 1) − 1) = 𝑀)
183167zcnd 12608 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑚𝑍𝑚 ∈ ℂ)
184 pncan 11407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑚 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑚 + 1) − 1) = 𝑚)
185183, 180, 184sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑚𝑍 → ((𝑚 + 1) − 1) = 𝑚)
186182, 185oveq12d 7375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑚𝑍 → (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑀...𝑚))
187186adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑀...𝑚))
188178, 187eleqtrd 2840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚𝑍𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑥 − 1) ∈ (𝑀...𝑚))
189 ffvelcdm 7032 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ (𝑥 − 1) ∈ (𝑀...𝑚)) → (𝑔‘(𝑥 − 1)) ∈ 𝐴)
190188, 189sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ (𝑚𝑍𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)))) → (𝑔‘(𝑥 − 1)) ∈ 𝐴)
191190anassrs 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑔:(𝑀...𝑚)⟶𝐴𝑚𝑍) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑔‘(𝑥 − 1)) ∈ 𝐴)
192191ancom1s 651 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑚𝑍𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑔‘(𝑥 − 1)) ∈ 𝐴)
193163, 192eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑚𝑍𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴)
194193ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑚𝑍𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
195194adantll 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
196152, 195jaod 857 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → ((𝑥 = 𝑀𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
197148, 196sylbid 239 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
198197ralrimiv 3142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → ∀𝑥 ∈ (𝑀...(𝑚 + 1))if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴)
199 eqid 2736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))
200199fmpt 7058 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (∀𝑥 ∈ (𝑀...(𝑚 + 1))if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴 ↔ (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴)
201198, 200sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴)
202201adantlll 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴)
2032023ad2antr1 1188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴)
204 eluzfz1 13448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑚 + 1) ∈ (ℤ𝑀) → 𝑀 ∈ (𝑀...(𝑚 + 1)))
205144, 204syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑚 ∈ (ℤ𝑀) → 𝑀 ∈ (𝑀...(𝑚 + 1)))
206205, 5eleq2s 2856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑚𝑍𝑀 ∈ (𝑀...(𝑚 + 1)))
207 vex 3449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑐 ∈ V
208149, 199, 207fvmpt 6948 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑀 ∈ (𝑀...(𝑚 + 1)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐)
209206, 208syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑚𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐)
210209ad2antlr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐)
211 eluzfz2 13449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑚 + 1) ∈ (ℤ𝑀) → (𝑚 + 1) ∈ (𝑀...(𝑚 + 1)))
212144, 211syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑚 ∈ (ℤ𝑀) → (𝑚 + 1) ∈ (𝑀...(𝑚 + 1)))
213212, 5eleq2s 2856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑚𝑍 → (𝑚 + 1) ∈ (𝑀...(𝑚 + 1)))
214 eqeq1 2740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑥 = (𝑚 + 1) → (𝑥 = 𝑀 ↔ (𝑚 + 1) = 𝑀))
215 fvoveq1 7380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑥 = (𝑚 + 1) → (𝑔‘(𝑥 − 1)) = (𝑔‘((𝑚 + 1) − 1)))
216214, 215ifbieq2d 4512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑥 = (𝑚 + 1) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1))))
217 fvex 6855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑔‘((𝑚 + 1) − 1)) ∈ V
218207, 217ifex 4536 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1))) ∈ V
219216, 199, 218fvmpt 6948 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑚 ∈ (ℤ𝑀) → 𝑀𝑚)
222221, 5eleq2s 2856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑚𝑍𝑀𝑚)
223 zleltp1 12554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑀𝑚𝑀 < (𝑚 + 1)))
2242, 167, 223sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑚𝑍 → (𝑀𝑚𝑀 < (𝑚 + 1)))
225222, 224mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑚𝑍𝑀 < (𝑚 + 1))
226 ltne 11252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑀 ∈ ℝ ∧ 𝑀 < (𝑚 + 1)) → (𝑚 + 1) ≠ 𝑀)
22746, 225, 226sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑚𝑍 → (𝑚 + 1) ≠ 𝑀)
228227neneqd 2948 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑚𝑍 → ¬ (𝑚 + 1) = 𝑀)
229228iffalsed 4497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑚𝑍 → if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1))) = (𝑔‘((𝑚 + 1) − 1)))
230185fveq2d 6846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑚𝑍 → (𝑔‘((𝑚 + 1) − 1)) = (𝑔𝑚))
231220, 229, 2303eqtrd 2780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑚𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) = (𝑔𝑚))
232231sbceq1d 3744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑚𝑍 → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃[(𝑔𝑚) / 𝑎]𝜃))
233232biimpar 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑚𝑍[(𝑔𝑚) / 𝑎]𝜃) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃)
234233ad2ant2l 744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃)) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃)
2352343ad2antr2 1189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃)
236 eluzp1p1 12791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑚 ∈ (ℤ𝑀) → (𝑚 + 1) ∈ (ℤ‘(𝑀 + 1)))
237236, 5eleq2s 2856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑚𝑍 → (𝑚 + 1) ∈ (ℤ‘(𝑀 + 1)))
23844fveq2i 6845 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (ℤ𝑁) = (ℤ‘(𝑀 + 1))
239237, 238eleqtrrdi 2849 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑚𝑍 → (𝑚 + 1) ∈ (ℤ𝑁))
240 elfzp12 13520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑚 + 1) ∈ (ℤ𝑁) → (𝑗 ∈ (𝑁...(𝑚 + 1)) ↔ (𝑗 = 𝑁𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)))))
241239, 240syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑚𝑍 → (𝑗 ∈ (𝑁...(𝑚 + 1)) ↔ (𝑗 = 𝑁𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)))))
242241biimpa 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑚𝑍𝑗 ∈ (𝑁...(𝑚 + 1))) → (𝑗 = 𝑁𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))))
243242adantll 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ 𝑗 ∈ (𝑁...(𝑚 + 1))) → (𝑗 = 𝑁𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))))
244243adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) ∧ 𝑗 ∈ (𝑁...(𝑚 + 1))) → (𝑗 = 𝑁𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))))
245 oveq1 7364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑗 = 𝑁 → (𝑗 − 1) = (𝑁 − 1))
24644oveq1i 7367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑁 − 1) = ((𝑀 + 1) − 1)
247246, 181eqtri 2764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑁 − 1) = 𝑀
248245, 247eqtrdi 2792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑗 = 𝑁 → (𝑗 − 1) = 𝑀)
249248fveq2d 6846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑗 = 𝑁 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀))
250249ad2antll 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀))
251209adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐)
252250, 251eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = 𝑐)
25344eqeq2i 2749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑗 = 𝑁𝑗 = (𝑀 + 1))
254 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑗 = (𝑀 + 1) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)))
255253, 254sylbi 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑗 = 𝑁 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)))
256255ad2antll 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)))
25746, 154, 47ltleii 11278 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 𝑀 ≤ (𝑀 + 1)
258 eluz2 12769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((𝑀 + 1) ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑀 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑀 + 1)))
2592, 49, 257, 258mpbir3an 1341 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑀 + 1) ∈ (ℤ𝑀)
260 fzss1 13480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ((𝑀 + 1) ∈ (ℤ𝑀) → ((𝑀 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1)))
261259, 260ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((𝑀 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1))
262 eluzfz1 13448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (𝑚 ∈ (ℤ𝑀) → 𝑀 ∈ (𝑀...𝑚))
263262, 5eleq2s 2856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑚𝑍𝑀 ∈ (𝑀...𝑚))
264 fzaddel 13475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (((𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑀 ∈ (𝑀...𝑚) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1))))
2652, 169, 264mpanr12 703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑀 ∈ (𝑀...𝑚) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1))))
2662, 167, 265sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑚𝑍 → (𝑀 ∈ (𝑀...𝑚) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1))))
267263, 266mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑚𝑍 → (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1)))
268261, 267sselid 3942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑚𝑍 → (𝑀 + 1) ∈ (𝑀...(𝑚 + 1)))
269 eqeq1 2740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑥 = (𝑀 + 1) → (𝑥 = 𝑀 ↔ (𝑀 + 1) = 𝑀))
270 oveq1 7364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (𝑥 = (𝑀 + 1) → (𝑥 − 1) = ((𝑀 + 1) − 1))
271270, 181eqtrdi 2792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (𝑥 = (𝑀 + 1) → (𝑥 − 1) = 𝑀)
272271fveq2d 6846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑥 = (𝑀 + 1) → (𝑔‘(𝑥 − 1)) = (𝑔𝑀))
273269, 272ifbieq2d 4512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑥 = (𝑀 + 1) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if((𝑀 + 1) = 𝑀, 𝑐, (𝑔𝑀)))
274 fvex 6855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑔𝑀) ∈ V
275207, 274ifex 4536 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 if((𝑀 + 1) = 𝑀, 𝑐, (𝑔𝑀)) ∈ V
276273, 199, 275fvmpt 6948 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑀 + 1) ∈ (𝑀...(𝑚 + 1)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)) = if((𝑀 + 1) = 𝑀, 𝑐, (𝑔𝑀)))
277268, 276syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑚𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)) = if((𝑀 + 1) = 𝑀, 𝑐, (𝑔𝑀)))
27846, 47gtneii 11267 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑀 + 1) ≠ 𝑀
279 ifnefalse 4498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑀 + 1) ≠ 𝑀 → if((𝑀 + 1) = 𝑀, 𝑐, (𝑔𝑀)) = (𝑔𝑀))
280278, 279ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 if((𝑀 + 1) = 𝑀, 𝑐, (𝑔𝑀)) = (𝑔𝑀)
281277, 280eqtrdi 2792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑚𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)) = (𝑔𝑀))
282281adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)) = (𝑔𝑀))
283 simprl 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → (𝑔𝑀) = 𝑑)
284256, 282, 2833eqtrd 2780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = 𝑑)
285284sbceq1d 3744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑[𝑑 / 𝑏]𝜑))
286252, 285sbceqbid 3746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑))
287286biimparc 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ (𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
288287anassrs 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
289288anassrs 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ (𝑔𝑀) = 𝑑) ∧ 𝑗 = 𝑁) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
290289adantlrr 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) ∧ 𝑗 = 𝑁) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
291 elfzelz 13441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → 𝑗 ∈ ℤ)
292291adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → 𝑗 ∈ ℤ)
29344, 49eqeltri 2834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 𝑁 ∈ ℤ
294 peano2z 12544 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑁 ∈ ℤ → (𝑁 + 1) ∈ ℤ)
295293, 294ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑁 + 1) ∈ ℤ
296 fzsubel 13477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((((𝑁 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ (𝑗 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) ↔ (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1))))
297296biimpd 228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ((((𝑁 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ (𝑗 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1))))
298169, 297mpanr2 702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((((𝑁 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ 𝑗 ∈ ℤ) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1))))
299298ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (((𝑁 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) → (𝑗 ∈ ℤ → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)))))
300295, 168, 299sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑚𝑍 → (𝑗 ∈ ℤ → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)))))
301300com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑚𝑍 → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 ∈ ℤ → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)))))
302301imp 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 ∈ ℤ → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1))))
303292, 302mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)))
304293zrei 12505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 𝑁 ∈ ℝ
305304recni 11169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 𝑁 ∈ ℂ
306305, 180pncan3oi 11417 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑁 + 1) − 1) = 𝑁
307306a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑚𝑍 → ((𝑁 + 1) − 1) = 𝑁)
308307, 185oveq12d 7375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑚𝑍 → (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑁...𝑚))
309308adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑁...𝑚))
310303, 309eleqtrd 2840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 − 1) ∈ (𝑁...𝑚))
311 fvoveq1 7380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑘 = (𝑗 − 1) → (𝑔‘(𝑘 − 1)) = (𝑔‘((𝑗 − 1) − 1)))
312 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑘 = (𝑗 − 1) → (𝑔𝑘) = (𝑔‘(𝑗 − 1)))
313312sbceq1d 3744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑘 = (𝑗 − 1) → ([(𝑔𝑘) / 𝑏]𝜑[(𝑔‘(𝑗 − 1)) / 𝑏]𝜑))
314311, 313sbceqbid 3746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑘 = (𝑗 − 1) → ([(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑[(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑))
315314rspcva 3579 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑗 − 1) ∈ (𝑁...𝑚) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → [(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑)
316310, 315sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → [(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑)
31744, 259eqeltri 2834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 𝑁 ∈ (ℤ𝑀)
318 fzss1 13480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑁 ∈ (ℤ𝑀) → (𝑁...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1)))
319317, 318ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑁...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1))
320 fzssp1 13484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑁...𝑚) ⊆ (𝑁...(𝑚 + 1))
321320, 310sselid 3942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 − 1) ∈ (𝑁...(𝑚 + 1)))
322319, 321sselid 3942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 − 1) ∈ (𝑀...(𝑚 + 1)))
323 eqeq1 2740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑥 = (𝑗 − 1) → (𝑥 = 𝑀 ↔ (𝑗 − 1) = 𝑀))
324 fvoveq1 7380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑥 = (𝑗 − 1) → (𝑔‘(𝑥 − 1)) = (𝑔‘((𝑗 − 1) − 1)))
325323, 324ifbieq2d 4512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑥 = (𝑗 − 1) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1))))
326 fvex 6855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑔‘((𝑗 − 1) − 1)) ∈ V
327207, 326ifex 4536 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1))) ∈ V
328325, 199, 327fvmpt 6948 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑀 + 1) < ((𝑀 + 1) + 1)
33144oveq1i 7367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑁 + 1) = ((𝑀 + 1) + 1)
332330, 331breqtrri 5132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑀 + 1) < (𝑁 + 1)
333304, 153readdcli 11170 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑁 + 1) ∈ ℝ
334154, 333ltnlei 11276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((𝑀 + 1) < (𝑁 + 1) ↔ ¬ (𝑁 + 1) ≤ (𝑀 + 1))
335332, 334mpbi 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ¬ (𝑁 + 1) ≤ (𝑀 + 1)
336291zcnd 12608 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → 𝑗 ∈ ℂ)
337 subadd 11404 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((𝑗 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑀 ∈ ℂ) → ((𝑗 − 1) = 𝑀 ↔ (1 + 𝑀) = 𝑗))
338180, 179, 337mp3an23 1453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑗 ∈ ℂ → ((𝑗 − 1) = 𝑀 ↔ (1 + 𝑀) = 𝑗))
339336, 338syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ((𝑗 − 1) = 𝑀 ↔ (1 + 𝑀) = 𝑗))
340 eqcom 2743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((1 + 𝑀) = 𝑗𝑗 = (1 + 𝑀))
341180, 179addcomi 11346 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (1 + 𝑀) = (𝑀 + 1)
342341eqeq2i 2749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (𝑗 = (1 + 𝑀) ↔ 𝑗 = (𝑀 + 1))
343340, 342bitri 274 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ((1 + 𝑀) = 𝑗𝑗 = (𝑀 + 1))
344 eleq1 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (𝑗 = (𝑀 + 1) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) ↔ (𝑀 + 1) ∈ ((𝑁 + 1)...(𝑚 + 1))))
345 elfzle1 13444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ((𝑀 + 1) ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑁 + 1) ≤ (𝑀 + 1))
346344, 345syl6bi 252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (𝑗 = (𝑀 + 1) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑁 + 1) ≤ (𝑀 + 1)))
347346com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 = (𝑀 + 1) → (𝑁 + 1) ≤ (𝑀 + 1)))
348343, 347biimtrid 241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ((1 + 𝑀) = 𝑗 → (𝑁 + 1) ≤ (𝑀 + 1)))
349339, 348sylbid 239 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ((𝑗 − 1) = 𝑀 → (𝑁 + 1) ≤ (𝑀 + 1)))
350335, 349mtoi 198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ¬ (𝑗 − 1) = 𝑀)
351350adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ¬ (𝑗 − 1) = 𝑀)
352351iffalsed 4497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1))) = (𝑔‘((𝑗 − 1) − 1)))
353329, 352eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = (𝑔‘((𝑗 − 1) − 1)))
354 peano2uz 12826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑁 ∈ (ℤ𝑀) → (𝑁 + 1) ∈ (ℤ𝑀))
355 fzss1 13480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((𝑁 + 1) ∈ (ℤ𝑀) → ((𝑁 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1)))
356317, 354, 355mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑁 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1))
357 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)))
358356, 357sselid 3942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → 𝑗 ∈ (𝑀...(𝑚 + 1)))
359 eqeq1 2740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑥 = 𝑗 → (𝑥 = 𝑀𝑗 = 𝑀))
360 fvoveq1 7380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑥 = 𝑗 → (𝑔‘(𝑥 − 1)) = (𝑔‘(𝑗 − 1)))
361359, 360ifbieq2d 4512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑥 = 𝑗 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))))
362 fvex 6855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑔‘(𝑗 − 1)) ∈ V
363207, 362ifex 4536 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))) ∈ V
364361, 199, 363fvmpt 6948 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑗 ∈ (𝑀...(𝑚 + 1)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))))
365358, 364syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))))
36647, 44breqtrri 5132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 𝑀 < 𝑁
367304ltp1i 12059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 𝑁 < (𝑁 + 1)
36846, 304, 333lttri 11281 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((𝑀 < 𝑁𝑁 < (𝑁 + 1)) → 𝑀 < (𝑁 + 1))
369366, 367, 368mp2an 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 𝑀 < (𝑁 + 1)
37046, 333ltnlei 11276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑀 < (𝑁 + 1) ↔ ¬ (𝑁 + 1) ≤ 𝑀)
371369, 370mpbi 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ¬ (𝑁 + 1) ≤ 𝑀
372 eleq1 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (𝑗 = 𝑀 → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) ↔ 𝑀 ∈ ((𝑁 + 1)...(𝑚 + 1))))
373 elfzle1 13444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (𝑀 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑁 + 1) ≤ 𝑀)
374372, 373syl6bi 252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑗 = 𝑀 → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑁 + 1) ≤ 𝑀))
375374com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 = 𝑀 → (𝑁 + 1) ≤ 𝑀))
376371, 375mtoi 198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ¬ 𝑗 = 𝑀)
377376adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ¬ 𝑗 = 𝑀)
378377iffalsed 4497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))) = (𝑔‘(𝑗 − 1)))
379365, 378eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = (𝑔‘(𝑗 − 1)))
380379sbceq1d 3744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑[(𝑔‘(𝑗 − 1)) / 𝑏]𝜑))
381353, 380sbceqbid 3746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑[(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑))
382381biimpar 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) ∧ [(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
383316, 382syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
384383an32s 650 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑚𝑍 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
385384adantlrl 718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
386385adantlll 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
387290, 386jaodan 956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) ∧ (𝑗 = 𝑁𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
388244, 387syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) ∧ 𝑗 ∈ (𝑁...(𝑚 + 1))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
389388ralrimiva 3143 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∀𝑗 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
390 fvoveq1 7380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 = 𝑘 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)))
391 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑗 = 𝑘 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘))
392391sbceq1d 3744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 = 𝑘 → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
393390, 392sbceqbid 3746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑗 = 𝑘 → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
394393cbvralvw 3225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (∀𝑗 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑 ↔ ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
395389, 394sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
396395adantllr 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
397396adantrlr 721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ (((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
3983973adantr1 1169 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
399 ovex 7390 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑀...(𝑚 + 1)) ∈ V
400399mptex 7173 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) ∈ V
401 feq1 6649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ↔ (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴))
402 fveq1 6841 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓𝑀) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀))
403402eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ((𝑓𝑀) = 𝑐 ↔ ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐))
404 fveq1 6841 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓‘(𝑚 + 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)))
405404sbceq1d 3744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ([(𝑓‘(𝑚 + 1)) / 𝑎]𝜃[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃))
406403, 405anbi12d 631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ↔ (((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃)))
407 fveq1 6841 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓‘(𝑘 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)))
408 fveq1 6841 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓𝑘) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘))
409408sbceq1d 3744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ([(𝑓𝑘) / 𝑏]𝜑[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
410407, 409sbceqbid 3746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓𝑘) / 𝑏]𝜑[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
411113, 410bitr3id 284 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))
416415ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
417143, 416chvarvv 2002 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((([𝑑 / 𝑏]𝜑𝑎𝐴) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
418133, 417chvarvv 2002 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑎𝐴) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
419418adantlrr 719 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
420419adantlll 716 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
421420imp 407 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))
422 oveq2 7365 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = (𝑚 + 1) → (𝑀...𝑛) = (𝑀...(𝑚 + 1)))
423422feq2d 6654 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = (𝑚 + 1) → (𝑓:(𝑀...𝑛)⟶𝐴𝑓:(𝑀...(𝑚 + 1))⟶𝐴))
424 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = (𝑚 + 1) → (𝑓𝑛) = (𝑓‘(𝑚 + 1)))
425424sbceq1d 3744 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = (𝑚 + 1) → ([(𝑓𝑛) / 𝑎]𝜃[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃))
42638, 425bitr3id 284 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = (𝑚 + 1) → (𝜏[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃))
427426anbi2d 629 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = (𝑚 + 1) → (((𝑓𝑀) = 𝑎𝜏) ↔ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃)))
428 oveq2 7365 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = (𝑚 + 1) → (𝑁...𝑛) = (𝑁...(𝑚 + 1)))
429428raleqdv 3313 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = (𝑚 + 1) → (∀𝑘 ∈ (𝑁...𝑛)𝜒 ↔ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))
430423, 427, 4293anbi123d 1436 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = (𝑚 + 1) → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
431430exbidv 1924 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = (𝑚 + 1) → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
432431rspcev 3581 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑚 + 1) ∈ 𝑍 ∧ ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
433125, 421, 432syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
434433ex 413 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
435434exlimdv 1936 . . . . . . . . . . . . . . . . . . . 20 ((((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) → (∃𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
436435rexlimdva 3152 . . . . . . . . . . . . . . . . . . 19 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (∃𝑚𝑍𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
437123, 436biimtrid 241 . . . . . . . . . . . . . . . . . 18 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
43873, 88, 4373syld 60 . . . . . . . . . . . . . . . . 17 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
439438an42s 659 . . . . . . . . . . . . . . . 16 (((𝜂𝑎𝐴) ∧ (𝑏𝐴𝜑)) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
440439rexlimdvaa 3153 . . . . . . . . . . . . . . 15 ((𝜂𝑎𝐴) → (∃𝑏𝐴 𝜑 → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))))
441440imp 407 . . . . . . . . . . . . . 14 (((𝜂𝑎𝐴) ∧ ∃𝑏𝐴 𝜑) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
442 fdc.10 . . . . . . . . . . . . . 14 ((𝜂𝑎𝐴) → (𝜃 ∨ ∃𝑏𝐴 𝜑))
44365, 441, 442mpjaodan 957 . . . . . . . . . . . . 13 ((𝜂𝑎𝐴) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
444138anbi1d 630 . . . . . . . . . . . . . . . . . 18 (𝑐 = 𝑎 → (((𝑓𝑀) = 𝑐𝜏) ↔ ((𝑓𝑀) = 𝑎𝜏)))
4454443anbi2d 1441 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑎 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
446445exbidv 1924 . . . . . . . . . . . . . . . 16 (𝑐 = 𝑎 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
447446rexbidv 3175 . . . . . . . . . . . . . . 15 (𝑐 = 𝑎 → (∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
448447elrab3 3646 . . . . . . . . . . . . . 14 (𝑎𝐴 → (𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
449448adantl 482 . . . . . . . . . . . . 13 ((𝜂𝑎𝐴) → (𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
450443, 449sylibrd 258 . . . . . . . . . . . 12 ((𝜂𝑎𝐴) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
451450ex 413 . . . . . . . . . . 11 (𝜂 → (𝑎𝐴 → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
452451com23 86 . . . . . . . . . 10 (𝜂 → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → (𝑎𝐴𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
453 eldif 3920 . . . . . . . . . . . 12 (𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ↔ (𝑎𝐴 ∧ ¬ 𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
454453notbii 319 . . . . . . . . . . 11 𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ↔ ¬ (𝑎𝐴 ∧ ¬ 𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
455 iman 402 . . . . . . . . . . 11 ((𝑎𝐴𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ↔ ¬ (𝑎𝐴 ∧ ¬ 𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
456454, 455bitr4i 277 . . . . . . . . . 10 𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ↔ (𝑎𝐴𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
457452, 456syl6ibr 251 . . . . . . . . 9 (𝜂 → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ¬ 𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
458457con2d 134 . . . . . . . 8 (𝜂 → (𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
459458imp 407 . . . . . . 7 ((𝜂𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) → ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
460459nrexdv 3146 . . . . . 6 (𝜂 → ¬ ∃𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
461 df-ne 2944 . . . . . . 7 ((𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅ ↔ ¬ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅)
462 fdc.9 . . . . . . . 8 (𝜂𝑅 Fr 𝐴)
463 difss 4091 . . . . . . . 8 (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴
464 fdc.1 . . . . . . . . . . 11 𝐴 ∈ V
465 difexg 5284 . . . . . . . . . . 11 (𝐴 ∈ V → (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∈ V)
466464, 465ax-mp 5 . . . . . . . . . 10 (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∈ V
467 fri 5593 . . . . . . . . . 10 ((((𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∈ V ∧ 𝑅 Fr 𝐴) ∧ ((𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴 ∧ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅)) → ∃𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
468466, 467mpanl1 698 . . . . . . . . 9 ((𝑅 Fr 𝐴 ∧ ((𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴 ∧ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅)) → ∃𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
469468expr 457 . . . . . . . 8 ((𝑅 Fr 𝐴 ∧ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴) → ((𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅ → ∃𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
470462, 463, 469sylancl 586 . . . . . . 7 (𝜂 → ((𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅ → ∃𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
471461, 470biimtrrid 242 . . . . . 6 (𝜂 → (¬ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅ → ∃𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
472460, 471mt3d 148 . . . . 5 (𝜂 → (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅)
473 ssdif0 4323 . . . . 5 (𝐴 ⊆ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅)
474472, 473sylibr 233 . . . 4 (𝜂𝐴 ⊆ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})
47576a1i 11 . . . 4 (𝜂 → {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ⊆ 𝐴)
476474, 475eqssd 3961 . . 3 (𝜂𝐴 = {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})
477 rabid2 3436 . . 3 (𝐴 = {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∀𝑐𝐴𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
478476, 477sylib 217 . 2 (𝜂 → ∀𝑐𝐴𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
479 eqeq2 2748 . . . . . . 7 (𝑐 = 𝐶 → ((𝑓𝑀) = 𝑐 ↔ (𝑓𝑀) = 𝐶))
480479anbi1d 630 . . . . . 6 (𝑐 = 𝐶 → (((𝑓𝑀) = 𝑐𝜏) ↔ ((𝑓𝑀) = 𝐶𝜏)))
4814803anbi2d 1441 . . . . 5 (𝑐 = 𝐶 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝐶𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
482481exbidv 1924 . . . 4 (𝑐 = 𝐶 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝐶𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
483482rexbidv 3175 . . 3 (𝑐 = 𝐶 → (∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝐶𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
484483rspcva 3579 . 2 ((𝐶𝐴 ∧ ∀𝑐𝐴𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝐶𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
4851, 478, 484syl2anc 584 1 (𝜂 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝐶𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  w3a 1087   = wceq 1541  wex 1781  wcel 2106  wne 2943  wral 3064  wrex 3073  {crab 3407  Vcvv 3445  [wsbc 3739  cdif 3907  wss 3910  c0 4282  ifcif 4486  {csn 4586  cop 4592   class class class wbr 5105  cmpt 5188   Fr wfr 5585  wf 6492  cfv 6496  (class class class)co 7357  cc 11049  cr 11050  1c1 11052   + caddc 11054   < clt 11189  cle 11190  cmin 11385  cz 12499  cuz 12763  ...cfz 13424
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-nn 12154  df-n0 12414  df-z 12500  df-uz 12764  df-fz 13425
This theorem is referenced by:  fdc1  36205
  Copyright terms: Public domain W3C validator