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 33854
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 11894 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ𝑀))
42, 3ax-mp 5 . . . . . . . . . . . . . . . . . 18 𝑀 ∈ (ℤ𝑀)
5 fdc.3 . . . . . . . . . . . . . . . . . 18 𝑍 = (ℤ𝑀)
64, 5eleqtrri 2838 . . . . . . . . . . . . . . . . 17 𝑀𝑍
7 eqid 2760 . . . . . . . . . . . . . . . . . . . . . 22 {⟨𝑀, 𝑎⟩} = {⟨𝑀, 𝑎⟩}
82elexi 3353 . . . . . . . . . . . . . . . . . . . . . . 23 𝑀 ∈ V
9 vex 3343 . . . . . . . . . . . . . . . . . . . . . . 23 𝑎 ∈ V
108, 9fsn 6565 . . . . . . . . . . . . . . . . . . . . . 22 ({⟨𝑀, 𝑎⟩}:{𝑀}⟶{𝑎} ↔ {⟨𝑀, 𝑎⟩} = {⟨𝑀, 𝑎⟩})
117, 10mpbir 221 . . . . . . . . . . . . . . . . . . . . 21 {⟨𝑀, 𝑎⟩}:{𝑀}⟶{𝑎}
12 snssi 4484 . . . . . . . . . . . . . . . . . . . . 21 (𝑎𝐴 → {𝑎} ⊆ 𝐴)
13 fss 6217 . . . . . . . . . . . . . . . . . . . . 21 (({⟨𝑀, 𝑎⟩}:{𝑀}⟶{𝑎} ∧ {𝑎} ⊆ 𝐴) → {⟨𝑀, 𝑎⟩}:{𝑀}⟶𝐴)
1411, 12, 13sylancr 698 . . . . . . . . . . . . . . . . . . . 20 (𝑎𝐴 → {⟨𝑀, 𝑎⟩}:{𝑀}⟶𝐴)
15 fzsn 12576 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀})
162, 15ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (𝑀...𝑀) = {𝑀}
1716feq2i 6198 . . . . . . . . . . . . . . . . . . . 20 ({⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴 ↔ {⟨𝑀, 𝑎⟩}:{𝑀}⟶𝐴)
1814, 17sylibr 224 . . . . . . . . . . . . . . . . . . 19 (𝑎𝐴 → {⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴)
1918adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝑎𝐴𝜃) → {⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴)
208, 9fvsn 6610 . . . . . . . . . . . . . . . . . . 19 ({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎
2120a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝑎𝐴𝜃) → ({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎)
22 simpr 479 . . . . . . . . . . . . . . . . . 18 ((𝑎𝐴𝜃) → 𝜃)
23 snex 5057 . . . . . . . . . . . . . . . . . . 19 {⟨𝑀, 𝑎⟩} ∈ V
24 feq1 6187 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = {⟨𝑀, 𝑎⟩} → (𝑓:(𝑀...𝑀)⟶𝐴 ↔ {⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴))
25 fveq1 6351 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = {⟨𝑀, 𝑎⟩} → (𝑓𝑀) = ({⟨𝑀, 𝑎⟩}‘𝑀))
2625eqeq1d 2762 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = {⟨𝑀, 𝑎⟩} → ((𝑓𝑀) = 𝑎 ↔ ({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎))
2725, 20syl6eq 2810 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = {⟨𝑀, 𝑎⟩} → (𝑓𝑀) = 𝑎)
28 sbceq2a 3588 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓𝑀) = 𝑎 → ([(𝑓𝑀) / 𝑎]𝜃𝜃))
2927, 28syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = {⟨𝑀, 𝑎⟩} → ([(𝑓𝑀) / 𝑎]𝜃𝜃))
3026, 29anbi12d 749 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = {⟨𝑀, 𝑎⟩} → (((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃) ↔ (({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎𝜃)))
3124, 30anbi12d 749 . . . . . . . . . . . . . . . . . . 19 (𝑓 = {⟨𝑀, 𝑎⟩} → ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃)) ↔ ({⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴 ∧ (({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎𝜃))))
3223, 31spcev 3440 . . . . . . . . . . . . . . . . . 18 (({⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴 ∧ (({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎𝜃)) → ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃)))
3319, 21, 22, 32syl12anc 1475 . . . . . . . . . . . . . . . . 17 ((𝑎𝐴𝜃) → ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃)))
34 oveq2 6821 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑀 → (𝑀...𝑛) = (𝑀...𝑀))
3534feq2d 6192 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑀 → (𝑓:(𝑀...𝑛)⟶𝐴𝑓:(𝑀...𝑀)⟶𝐴))
36 fvex 6362 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓𝑛) ∈ V
37 fdc.7 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = (𝑓𝑛) → (𝜃𝜏))
3836, 37sbcie 3611 . . . . . . . . . . . . . . . . . . . . . . 23 ([(𝑓𝑛) / 𝑎]𝜃𝜏)
39 fveq2 6352 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑀 → (𝑓𝑛) = (𝑓𝑀))
4039sbceq1d 3581 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑀 → ([(𝑓𝑛) / 𝑎]𝜃[(𝑓𝑀) / 𝑎]𝜃))
4138, 40syl5bbr 274 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑀 → (𝜏[(𝑓𝑀) / 𝑎]𝜃))
4241anbi2d 742 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑀 → (((𝑓𝑀) = 𝑎𝜏) ↔ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃)))
43 oveq2 6821 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑀 → (𝑁...𝑛) = (𝑁...𝑀))
44 fdc.4 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑁 = (𝑀 + 1)
4544oveq1i 6823 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁...𝑀) = ((𝑀 + 1)...𝑀)
462zrei 11575 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑀 ∈ ℝ
4746ltp1i 11119 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑀 < (𝑀 + 1)
48 peano2z 11610 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑀 ∈ ℤ → (𝑀 + 1) ∈ ℤ)
492, 48ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑀 + 1) ∈ ℤ
50 fzn 12550 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑀 + 1) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 < (𝑀 + 1) ↔ ((𝑀 + 1)...𝑀) = ∅))
5149, 2, 50mp2an 710 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 < (𝑀 + 1) ↔ ((𝑀 + 1)...𝑀) = ∅)
5247, 51mpbi 220 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑀 + 1)...𝑀) = ∅
5345, 52eqtri 2782 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁...𝑀) = ∅
5443, 53syl6eq 2810 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑀 → (𝑁...𝑛) = ∅)
5554raleqdv 3283 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑀 → (∀𝑘 ∈ (𝑁...𝑛)𝜒 ↔ ∀𝑘 ∈ ∅ 𝜒))
5635, 42, 553anbi123d 1548 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑀 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃) ∧ ∀𝑘 ∈ ∅ 𝜒)))
57 ral0 4220 . . . . . . . . . . . . . . . . . . . . 21 𝑘 ∈ ∅ 𝜒
58 df-3an 1074 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃) ∧ ∀𝑘 ∈ ∅ 𝜒) ↔ ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃)) ∧ ∀𝑘 ∈ ∅ 𝜒))
5957, 58mpbiran2 992 . . . . . . . . . . . . . . . . . . . 20 ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃) ∧ ∀𝑘 ∈ ∅ 𝜒) ↔ (𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃)))
6056, 59syl6bb 276 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑀 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃))))
6160exbidv 1999 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑀 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃))))
6261rspcev 3449 . . . . . . . . . . . . . . . . 17 ((𝑀𝑍 ∧ ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃))) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
636, 33, 62sylancr 698 . . . . . . . . . . . . . . . 16 ((𝑎𝐴𝜃) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
6463adantll 752 . . . . . . . . . . . . . . 15 (((𝜂𝑎𝐴) ∧ 𝜃) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
6564a1d 25 . . . . . . . . . . . . . 14 (((𝜂𝑎𝐴) ∧ 𝜃) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
66 fdc.11 . . . . . . . . . . . . . . . . . . . . 21 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → 𝑏𝑅𝑎)
67 breq1 4807 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑 = 𝑏 → (𝑑𝑅𝑎𝑏𝑅𝑎))
6867rspcev 3449 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∧ 𝑏𝑅𝑎) → ∃𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎)
6968expcom 450 . . . . . . . . . . . . . . . . . . . . 21 (𝑏𝑅𝑎 → (𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎))
7066, 69syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎))
71 dfrex2 3134 . . . . . . . . . . . . . . . . . . . 20 (∃𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎 ↔ ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
7270, 71syl6ib 241 . . . . . . . . . . . . . . . . . . 19 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
7372con2d 129 . . . . . . . . . . . . . . . . . 18 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ¬ 𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
74 eldif 3725 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) ↔ (𝑏𝐴 ∧ ¬ 𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
7574simplbi2 656 . . . . . . . . . . . . . . . . . . . 20 (𝑏𝐴 → (¬ 𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → 𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))))
76 ssrab2 3828 . . . . . . . . . . . . . . . . . . . . . . 23 {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ⊆ 𝐴
77 dfss4 4001 . . . . . . . . . . . . . . . . . . . . . . 23 ({𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ⊆ 𝐴 ↔ (𝐴 ∖ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) = {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})
7876, 77mpbi 220 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴 ∖ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) = {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}
7978eleq2i 2831 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) ↔ 𝑏 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})
80 eqeq2 2771 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 = 𝑏 → ((𝑓𝑀) = 𝑐 ↔ (𝑓𝑀) = 𝑏))
8180anbi1d 743 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = 𝑏 → (((𝑓𝑀) = 𝑐𝜏) ↔ ((𝑓𝑀) = 𝑏𝜏)))
82813anbi2d 1553 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = 𝑏 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
8382exbidv 1999 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 = 𝑏 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
8483rexbidv 3190 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 = 𝑏 → (∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
8584elrab3 3505 . . . . . . . . . . . . . . . . . . . . 21 (𝑏𝐴 → (𝑏 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
8679, 85syl5bb 272 . . . . . . . . . . . . . . . . . . . 20 (𝑏𝐴 → (𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
8775, 86sylibd 229 . . . . . . . . . . . . . . . . . . 19 (𝑏𝐴 → (¬ 𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
8887ad2antll 767 . . . . . . . . . . . . . . . . . 18 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (¬ 𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
89 oveq2 6821 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑚 → (𝑀...𝑛) = (𝑀...𝑚))
9089feq2d 6192 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑚 → (𝑓:(𝑀...𝑛)⟶𝐴𝑓:(𝑀...𝑚)⟶𝐴))
91 fveq2 6352 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑚 → (𝑓𝑛) = (𝑓𝑚))
9291sbceq1d 3581 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑚 → ([(𝑓𝑛) / 𝑎]𝜃[(𝑓𝑚) / 𝑎]𝜃))
9338, 92syl5bbr 274 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑚 → (𝜏[(𝑓𝑚) / 𝑎]𝜃))
9493anbi2d 742 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑚 → (((𝑓𝑀) = 𝑏𝜏) ↔ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃)))
95 oveq2 6821 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑚 → (𝑁...𝑛) = (𝑁...𝑚))
9695raleqdv 3283 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑚 → (∀𝑘 ∈ (𝑁...𝑛)𝜒 ↔ ∀𝑘 ∈ (𝑁...𝑚)𝜒))
9790, 94, 963anbi123d 1548 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑚 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒)))
9897exbidv 1999 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑚 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒)))
9998cbvrexv 3311 . . . . . . . . . . . . . . . . . . . 20 (∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑚𝑍𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒))
100 feq1 6187 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = 𝑔 → (𝑓:(𝑀...𝑚)⟶𝐴𝑔:(𝑀...𝑚)⟶𝐴))
101 fveq1 6351 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 = 𝑔 → (𝑓𝑀) = (𝑔𝑀))
102101eqeq1d 2762 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑔 → ((𝑓𝑀) = 𝑏 ↔ (𝑔𝑀) = 𝑏))
103 fveq1 6351 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 = 𝑔 → (𝑓𝑚) = (𝑔𝑚))
104103sbceq1d 3581 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑔 → ([(𝑓𝑚) / 𝑎]𝜃[(𝑔𝑚) / 𝑎]𝜃))
105102, 104anbi12d 749 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = 𝑔 → (((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ↔ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃)))
106 fvex 6362 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓‘(𝑘 − 1)) ∈ V
107 fdc.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 = (𝑓‘(𝑘 − 1)) → (𝜑𝜓))
108107sbcbidv 3631 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = (𝑓‘(𝑘 − 1)) → ([(𝑓𝑘) / 𝑏]𝜑[(𝑓𝑘) / 𝑏]𝜓))
109106, 108sbcie 3611 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓𝑘) / 𝑏]𝜑[(𝑓𝑘) / 𝑏]𝜓)
110 fvex 6362 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓𝑘) ∈ V
111 fdc.6 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 = (𝑓𝑘) → (𝜓𝜒))
112110, 111sbcie 3611 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([(𝑓𝑘) / 𝑏]𝜓𝜒)
113109, 112bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . 25 ([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓𝑘) / 𝑏]𝜑𝜒)
114 fveq1 6351 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 = 𝑔 → (𝑓‘(𝑘 − 1)) = (𝑔‘(𝑘 − 1)))
115 fveq1 6351 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓 = 𝑔 → (𝑓𝑘) = (𝑔𝑘))
116115sbceq1d 3581 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 = 𝑔 → ([(𝑓𝑘) / 𝑏]𝜑[(𝑔𝑘) / 𝑏]𝜑))
117114, 116sbceqbid 3583 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 = 𝑔 → ([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓𝑘) / 𝑏]𝜑[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑))
118113, 117syl5bbr 274 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑔 → (𝜒[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑))
119118ralbidv 3124 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = 𝑔 → (∀𝑘 ∈ (𝑁...𝑚)𝜒 ↔ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑))
120100, 105, 1193anbi123d 1548 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = 𝑔 → ((𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒) ↔ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)))
121120cbvexv 2420 . . . . . . . . . . . . . . . . . . . . 21 (∃𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒) ↔ ∃𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑))
122121rexbii 3179 . . . . . . . . . . . . . . . . . . . 20 (∃𝑚𝑍𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒) ↔ ∃𝑚𝑍𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑))
12399, 122bitri 264 . . . . . . . . . . . . . . . . . . 19 (∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑚𝑍𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑))
1245peano2uzs 11935 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚𝑍 → (𝑚 + 1) ∈ 𝑍)
125124ad2antlr 765 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → (𝑚 + 1) ∈ 𝑍)
126 sbceq2a 3588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑑 = 𝑏 → ([𝑑 / 𝑏]𝜑𝜑))
127126anbi1d 743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑑 = 𝑏 → (([𝑑 / 𝑏]𝜑𝑎𝐴) ↔ (𝜑𝑎𝐴)))
128127anbi1d 743 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑑 = 𝑏 → ((([𝑑 / 𝑏]𝜑𝑎𝐴) ∧ 𝑚𝑍) ↔ ((𝜑𝑎𝐴) ∧ 𝑚𝑍)))
129 eqeq2 2771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑑 = 𝑏 → ((𝑔𝑀) = 𝑑 ↔ (𝑔𝑀) = 𝑏))
130129anbi1d 743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑑 = 𝑏 → (((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ↔ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃)))
1311303anbi2d 1553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑑 = 𝑏 → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) ↔ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)))
132131imbi1d 330 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑑 = 𝑏 → (((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)) ↔ ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))))
133128, 132imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑑 = 𝑏 → (((([𝑑 / 𝑏]𝜑𝑎𝐴) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))) ↔ (((𝜑𝑎𝐴) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))))
134 sbceq2a 3588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑐 = 𝑎 → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑[𝑑 / 𝑏]𝜑))
135 eleq1 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑐 = 𝑎 → (𝑐𝐴𝑎𝐴))
136134, 135anbi12d 749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 = 𝑎 → (([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ↔ ([𝑑 / 𝑏]𝜑𝑎𝐴)))
137136anbi1d 743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = 𝑎 → ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ↔ (([𝑑 / 𝑏]𝜑𝑎𝐴) ∧ 𝑚𝑍)))
138 eqeq2 2771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 = 𝑎 → ((𝑓𝑀) = 𝑐 ↔ (𝑓𝑀) = 𝑎))
139138anbi1d 743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑐 = 𝑎 → (((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ↔ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃)))
1401393anbi2d 1553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑐 = 𝑎 → ((𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒) ↔ (𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
141140exbidv 1999 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 = 𝑎 → (∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒) ↔ ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
142141imbi2d 329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = 𝑎 → (((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)) ↔ ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))))
143137, 142imbi12d 333 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 = 𝑎 → (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))) ↔ ((([𝑑 / 𝑏]𝜑𝑎𝐴) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))))
144 peano2uz 11934 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑚 ∈ (ℤ𝑀) → (𝑚 + 1) ∈ (ℤ𝑀))
145144, 5eleq2s 2857 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑚𝑍 → (𝑚 + 1) ∈ (ℤ𝑀))
146 elfzp12 12612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑚 + 1) ∈ (ℤ𝑀) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↔ (𝑥 = 𝑀𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)))))
147145, 146syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑚𝑍 → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↔ (𝑥 = 𝑀𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)))))
148147ad2antlr 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↔ (𝑥 = 𝑀𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)))))
149 iftrue 4236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑥 = 𝑀 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = 𝑐)
150149eleq1d 2824 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑥 = 𝑀 → (if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴𝑐𝐴))
151150biimprcd 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑐𝐴 → (𝑥 = 𝑀 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
152151ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 = 𝑀 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
153 1re 10231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 1 ∈ ℝ
15446, 153readdcli 10245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑀 + 1) ∈ ℝ
15546, 154ltnlei 10350 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑀 < (𝑀 + 1) ↔ ¬ (𝑀 + 1) ≤ 𝑀)
15647, 155mpbi 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ¬ (𝑀 + 1) ≤ 𝑀
157 eleq1 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑥 = 𝑀 → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) ↔ 𝑀 ∈ ((𝑀 + 1)...(𝑚 + 1))))
158 elfzle1 12537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑀 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑀 + 1) ≤ 𝑀)
159157, 158syl6bi 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑥 = 𝑀 → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑀 + 1) ≤ 𝑀))
160159com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 = 𝑀 → (𝑀 + 1) ≤ 𝑀))
161156, 160mtoi 190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → ¬ 𝑥 = 𝑀)
162161adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑚𝑍𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → ¬ 𝑥 = 𝑀)
163162iffalsed 4241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑚𝑍𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = (𝑔‘(𝑥 − 1)))
164 elfzelz 12535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → 𝑥 ∈ ℤ)
165164adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → 𝑥 ∈ ℤ)
166 eluzelz 11889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑚 ∈ (ℤ𝑀) → 𝑚 ∈ ℤ)
167166, 5eleq2s 2857 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑚𝑍𝑚 ∈ ℤ)
168167peano2zd 11677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑚𝑍 → (𝑚 + 1) ∈ ℤ)
169 1z 11599 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 1 ∈ ℤ
170 fzsubel 12570 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ((((𝑀 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ (𝑥 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) ↔ (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))))
171170biimpd 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((((𝑀 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ (𝑥 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))))
172169, 171mpanr2 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ((((𝑀 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ 𝑥 ∈ ℤ) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))))
17349, 172mpanl1 718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (((𝑚 + 1) ∈ ℤ ∧ 𝑥 ∈ ℤ) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))))
174173ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑥 ∈ ℤ → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))))
178165, 177mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)))
17946recni 10244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 𝑀 ∈ ℂ
180 ax-1cn 10186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 1 ∈ ℂ
181179, 180pncan3oi 10489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑀 + 1) − 1) = 𝑀
182181a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑚𝑍 → ((𝑀 + 1) − 1) = 𝑀)
183167zcnd 11675 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑚𝑍𝑚 ∈ ℂ)
184 pncan 10479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑚 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑚 + 1) − 1) = 𝑚)
185183, 180, 184sylancl 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑚𝑍 → ((𝑚 + 1) − 1) = 𝑚)
186182, 185oveq12d 6831 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑚𝑍 → (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑀...𝑚))
187186adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑀...𝑚))
188178, 187eleqtrd 2841 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚𝑍𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑥 − 1) ∈ (𝑀...𝑚))
189 ffvelrn 6520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ (𝑥 − 1) ∈ (𝑀...𝑚)) → (𝑔‘(𝑥 − 1)) ∈ 𝐴)
190188, 189sylan2 492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ (𝑚𝑍𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)))) → (𝑔‘(𝑥 − 1)) ∈ 𝐴)
191190anassrs 683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑔:(𝑀...𝑚)⟶𝐴𝑚𝑍) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑔‘(𝑥 − 1)) ∈ 𝐴)
192191ancom1s 882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑚𝑍𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑔‘(𝑥 − 1)) ∈ 𝐴)
193163, 192eqeltrd 2839 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑚𝑍𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴)
194193ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑚𝑍𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
195194adantll 752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
196152, 195jaod 394 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → ((𝑥 = 𝑀𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
197148, 196sylbid 230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
198197ralrimiv 3103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → ∀𝑥 ∈ (𝑀...(𝑚 + 1))if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴)
199 eqid 2760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))
200199fmpt 6544 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (∀𝑥 ∈ (𝑀...(𝑚 + 1))if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴 ↔ (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴)
201198, 200sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴)
202201adantlll 756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴)
2032023ad2antr1 1204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴)
204 eluzfz1 12541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑚 + 1) ∈ (ℤ𝑀) → 𝑀 ∈ (𝑀...(𝑚 + 1)))
205144, 204syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑚 ∈ (ℤ𝑀) → 𝑀 ∈ (𝑀...(𝑚 + 1)))
206205, 5eleq2s 2857 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑚𝑍𝑀 ∈ (𝑀...(𝑚 + 1)))
207 vex 3343 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑐 ∈ V
208149, 199, 207fvmpt 6444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑀 ∈ (𝑀...(𝑚 + 1)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐)
209206, 208syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑚𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐)
210209ad2antlr 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐)
211 eluzfz2 12542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑚 + 1) ∈ (ℤ𝑀) → (𝑚 + 1) ∈ (𝑀...(𝑚 + 1)))
212144, 211syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑚 ∈ (ℤ𝑀) → (𝑚 + 1) ∈ (𝑀...(𝑚 + 1)))
213212, 5eleq2s 2857 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑚𝑍 → (𝑚 + 1) ∈ (𝑀...(𝑚 + 1)))
214 eqeq1 2764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑥 = (𝑚 + 1) → (𝑥 = 𝑀 ↔ (𝑚 + 1) = 𝑀))
215 oveq1 6820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑥 = (𝑚 + 1) → (𝑥 − 1) = ((𝑚 + 1) − 1))
216215fveq2d 6356 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑥 = (𝑚 + 1) → (𝑔‘(𝑥 − 1)) = (𝑔‘((𝑚 + 1) − 1)))
217214, 216ifbieq2d 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑥 = (𝑚 + 1) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1))))
218 fvex 6362 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑔‘((𝑚 + 1) − 1)) ∈ V
219207, 218ifex 4300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1))) ∈ V
220217, 199, 219fvmpt 6444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑚 + 1) ∈ (𝑀...(𝑚 + 1)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) = if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1))))
221213, 220syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑚𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) = if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1))))
222 eluzle 11892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑚 ∈ (ℤ𝑀) → 𝑀𝑚)
223222, 5eleq2s 2857 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑚𝑍𝑀𝑚)
224 zleltp1 11620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑀𝑚𝑀 < (𝑚 + 1)))
2252, 167, 224sylancr 698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑚𝑍 → (𝑀𝑚𝑀 < (𝑚 + 1)))
226223, 225mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑚𝑍𝑀 < (𝑚 + 1))
227 ltne 10326 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑀 ∈ ℝ ∧ 𝑀 < (𝑚 + 1)) → (𝑚 + 1) ≠ 𝑀)
22846, 226, 227sylancr 698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑚𝑍 → (𝑚 + 1) ≠ 𝑀)
229228neneqd 2937 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑚𝑍 → ¬ (𝑚 + 1) = 𝑀)
230229iffalsed 4241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑚𝑍 → if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1))) = (𝑔‘((𝑚 + 1) − 1)))
231185fveq2d 6356 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑚𝑍 → (𝑔‘((𝑚 + 1) − 1)) = (𝑔𝑚))
232221, 230, 2313eqtrd 2798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑚𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) = (𝑔𝑚))
233232sbceq1d 3581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑚𝑍 → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃[(𝑔𝑚) / 𝑎]𝜃))
234233biimpar 503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑚𝑍[(𝑔𝑚) / 𝑎]𝜃) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃)
235234ad2ant2l 799 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃)) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃)
2362353ad2antr2 1205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃)
237 eluzp1p1 11905 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑚 ∈ (ℤ𝑀) → (𝑚 + 1) ∈ (ℤ‘(𝑀 + 1)))
238237, 5eleq2s 2857 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑚𝑍 → (𝑚 + 1) ∈ (ℤ‘(𝑀 + 1)))
23944fveq2i 6355 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (ℤ𝑁) = (ℤ‘(𝑀 + 1))
240238, 239syl6eleqr 2850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑚𝑍 → (𝑚 + 1) ∈ (ℤ𝑁))
241 elfzp12 12612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑚 + 1) ∈ (ℤ𝑁) → (𝑗 ∈ (𝑁...(𝑚 + 1)) ↔ (𝑗 = 𝑁𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)))))
242240, 241syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑚𝑍 → (𝑗 ∈ (𝑁...(𝑚 + 1)) ↔ (𝑗 = 𝑁𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)))))
243242biimpa 502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑚𝑍𝑗 ∈ (𝑁...(𝑚 + 1))) → (𝑗 = 𝑁𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))))
244243adantll 752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ 𝑗 ∈ (𝑁...(𝑚 + 1))) → (𝑗 = 𝑁𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))))
245244adantlr 753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) ∧ 𝑗 ∈ (𝑁...(𝑚 + 1))) → (𝑗 = 𝑁𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))))
246 oveq1 6820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑗 = 𝑁 → (𝑗 − 1) = (𝑁 − 1))
24744oveq1i 6823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑁 − 1) = ((𝑀 + 1) − 1)
248247, 181eqtri 2782 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑁 − 1) = 𝑀
249246, 248syl6eq 2810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑗 = 𝑁 → (𝑗 − 1) = 𝑀)
250249fveq2d 6356 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑗 = 𝑁 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀))
251250ad2antll 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀))
252209adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐)
253251, 252eqtrd 2794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = 𝑐)
25444eqeq2i 2772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑗 = 𝑁𝑗 = (𝑀 + 1))
255 fveq2 6352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑗 = (𝑀 + 1) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)))
256254, 255sylbi 207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑗 = 𝑁 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)))
257256ad2antll 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)))
25846, 154, 47ltleii 10352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 𝑀 ≤ (𝑀 + 1)
259 eluz2 11885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((𝑀 + 1) ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑀 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑀 + 1)))
2602, 49, 258, 259mpbir3an 1427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑀 + 1) ∈ (ℤ𝑀)
261 fzss1 12573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ((𝑀 + 1) ∈ (ℤ𝑀) → ((𝑀 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1)))
262260, 261ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((𝑀 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1))
263 eluzfz1 12541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (𝑚 ∈ (ℤ𝑀) → 𝑀 ∈ (𝑀...𝑚))
264263, 5eleq2s 2857 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑚𝑍𝑀 ∈ (𝑀...𝑚))
265 fzaddel 12568 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (((𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑀 ∈ (𝑀...𝑚) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1))))
2662, 169, 265mpanr12 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑀 ∈ (𝑀...𝑚) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1))))
2672, 167, 266sylancr 698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑚𝑍 → (𝑀 ∈ (𝑀...𝑚) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1))))
268264, 267mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑚𝑍 → (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1)))
269262, 268sseldi 3742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑚𝑍 → (𝑀 + 1) ∈ (𝑀...(𝑚 + 1)))
270 eqeq1 2764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑥 = (𝑀 + 1) → (𝑥 = 𝑀 ↔ (𝑀 + 1) = 𝑀))
271 oveq1 6820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (𝑥 = (𝑀 + 1) → (𝑥 − 1) = ((𝑀 + 1) − 1))
272271, 181syl6eq 2810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (𝑥 = (𝑀 + 1) → (𝑥 − 1) = 𝑀)
273272fveq2d 6356 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑥 = (𝑀 + 1) → (𝑔‘(𝑥 − 1)) = (𝑔𝑀))
274270, 273ifbieq2d 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑥 = (𝑀 + 1) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if((𝑀 + 1) = 𝑀, 𝑐, (𝑔𝑀)))
275 fvex 6362 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑔𝑀) ∈ V
276207, 275ifex 4300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 if((𝑀 + 1) = 𝑀, 𝑐, (𝑔𝑀)) ∈ V
277274, 199, 276fvmpt 6444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑀 + 1) ∈ (𝑀...(𝑚 + 1)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)) = if((𝑀 + 1) = 𝑀, 𝑐, (𝑔𝑀)))
278269, 277syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑚𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)) = if((𝑀 + 1) = 𝑀, 𝑐, (𝑔𝑀)))
27946, 47gtneii 10341 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑀 + 1) ≠ 𝑀
280 ifnefalse 4242 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑀 + 1) ≠ 𝑀 → if((𝑀 + 1) = 𝑀, 𝑐, (𝑔𝑀)) = (𝑔𝑀))
281279, 280ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 if((𝑀 + 1) = 𝑀, 𝑐, (𝑔𝑀)) = (𝑔𝑀)
282278, 281syl6eq 2810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑚𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)) = (𝑔𝑀))
283282adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)) = (𝑔𝑀))
284 simprl 811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → (𝑔𝑀) = 𝑑)
285257, 283, 2843eqtrd 2798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = 𝑑)
286285sbceq1d 3581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑[𝑑 / 𝑏]𝜑))
287253, 286sbceqbid 3583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑[𝑐 / 𝑎][𝑑 / 𝑏]𝜑))
288287biimparc 505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ (𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
289288anassrs 683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
290289anassrs 683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ (𝑔𝑀) = 𝑑) ∧ 𝑗 = 𝑁) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
291290adantlrr 759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) ∧ 𝑗 = 𝑁) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
292 elfzelz 12535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → 𝑗 ∈ ℤ)
293292adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → 𝑗 ∈ ℤ)
29444, 49eqeltri 2835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 𝑁 ∈ ℤ
295 peano2z 11610 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑁 ∈ ℤ → (𝑁 + 1) ∈ ℤ)
296294, 295ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑁 + 1) ∈ ℤ
297 fzsubel 12570 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((((𝑁 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ (𝑗 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) ↔ (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1))))
298297biimpd 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ((((𝑁 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ (𝑗 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1))))
299169, 298mpanr2 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((((𝑁 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ 𝑗 ∈ ℤ) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1))))
300299ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (((𝑁 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) → (𝑗 ∈ ℤ → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)))))
301296, 168, 300sylancr 698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑚𝑍 → (𝑗 ∈ ℤ → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)))))
302301com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑚𝑍 → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 ∈ ℤ → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)))))
303302imp 444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 ∈ ℤ → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1))))
304293, 303mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)))
305294zrei 11575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 𝑁 ∈ ℝ
306305recni 10244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 𝑁 ∈ ℂ
307306, 180pncan3oi 10489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑁 + 1) − 1) = 𝑁
308307a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑚𝑍 → ((𝑁 + 1) − 1) = 𝑁)
309308, 185oveq12d 6831 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑚𝑍 → (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑁...𝑚))
310309adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑁...𝑚))
311304, 310eleqtrd 2841 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 − 1) ∈ (𝑁...𝑚))
312 oveq1 6820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑘 = (𝑗 − 1) → (𝑘 − 1) = ((𝑗 − 1) − 1))
313312fveq2d 6356 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑘 = (𝑗 − 1) → (𝑔‘(𝑘 − 1)) = (𝑔‘((𝑗 − 1) − 1)))
314 fveq2 6352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑘 = (𝑗 − 1) → (𝑔𝑘) = (𝑔‘(𝑗 − 1)))
315314sbceq1d 3581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑘 = (𝑗 − 1) → ([(𝑔𝑘) / 𝑏]𝜑[(𝑔‘(𝑗 − 1)) / 𝑏]𝜑))
316313, 315sbceqbid 3583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑘 = (𝑗 − 1) → ([(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑[(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑))
317316rspcva 3447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑗 − 1) ∈ (𝑁...𝑚) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → [(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑)
318311, 317sylan 489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → [(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑)
31944, 260eqeltri 2835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 𝑁 ∈ (ℤ𝑀)
320 fzss1 12573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑁 ∈ (ℤ𝑀) → (𝑁...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1)))
321319, 320ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑁...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1))
322 fzssp1 12577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑁...𝑚) ⊆ (𝑁...(𝑚 + 1))
323322, 311sseldi 3742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 − 1) ∈ (𝑁...(𝑚 + 1)))
324321, 323sseldi 3742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 − 1) ∈ (𝑀...(𝑚 + 1)))
325 eqeq1 2764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑥 = (𝑗 − 1) → (𝑥 = 𝑀 ↔ (𝑗 − 1) = 𝑀))
326 oveq1 6820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑥 = (𝑗 − 1) → (𝑥 − 1) = ((𝑗 − 1) − 1))
327326fveq2d 6356 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑥 = (𝑗 − 1) → (𝑔‘(𝑥 − 1)) = (𝑔‘((𝑗 − 1) − 1)))
328325, 327ifbieq2d 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑥 = (𝑗 − 1) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1))))
329 fvex 6362 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑔‘((𝑗 − 1) − 1)) ∈ V
330207, 329ifex 4300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1))) ∈ V
331328, 199, 330fvmpt 6444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑗 − 1) ∈ (𝑀...(𝑚 + 1)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1))))
332324, 331syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1))))
333154ltp1i 11119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑀 + 1) < ((𝑀 + 1) + 1)
33444oveq1i 6823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑁 + 1) = ((𝑀 + 1) + 1)
335333, 334breqtrri 4831 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑀 + 1) < (𝑁 + 1)
336305, 153readdcli 10245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑁 + 1) ∈ ℝ
337154, 336ltnlei 10350 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((𝑀 + 1) < (𝑁 + 1) ↔ ¬ (𝑁 + 1) ≤ (𝑀 + 1))
338335, 337mpbi 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ¬ (𝑁 + 1) ≤ (𝑀 + 1)
339292zcnd 11675 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → 𝑗 ∈ ℂ)
340 subadd 10476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((𝑗 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑀 ∈ ℂ) → ((𝑗 − 1) = 𝑀 ↔ (1 + 𝑀) = 𝑗))
341180, 179, 340mp3an23 1565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑗 ∈ ℂ → ((𝑗 − 1) = 𝑀 ↔ (1 + 𝑀) = 𝑗))
342339, 341syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ((𝑗 − 1) = 𝑀 ↔ (1 + 𝑀) = 𝑗))
343 eqcom 2767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((1 + 𝑀) = 𝑗𝑗 = (1 + 𝑀))
344180, 179addcomi 10419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (1 + 𝑀) = (𝑀 + 1)
345344eqeq2i 2772 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (𝑗 = (1 + 𝑀) ↔ 𝑗 = (𝑀 + 1))
346343, 345bitri 264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ((1 + 𝑀) = 𝑗𝑗 = (𝑀 + 1))
347 eleq1 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (𝑗 = (𝑀 + 1) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) ↔ (𝑀 + 1) ∈ ((𝑁 + 1)...(𝑚 + 1))))
348 elfzle1 12537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ((𝑀 + 1) ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑁 + 1) ≤ (𝑀 + 1))
349347, 348syl6bi 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (𝑗 = (𝑀 + 1) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑁 + 1) ≤ (𝑀 + 1)))
350349com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 = (𝑀 + 1) → (𝑁 + 1) ≤ (𝑀 + 1)))
351346, 350syl5bi 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ((1 + 𝑀) = 𝑗 → (𝑁 + 1) ≤ (𝑀 + 1)))
352342, 351sylbid 230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ((𝑗 − 1) = 𝑀 → (𝑁 + 1) ≤ (𝑀 + 1)))
353338, 352mtoi 190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ¬ (𝑗 − 1) = 𝑀)
354353adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ¬ (𝑗 − 1) = 𝑀)
355354iffalsed 4241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1))) = (𝑔‘((𝑗 − 1) − 1)))
356332, 355eqtrd 2794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = (𝑔‘((𝑗 − 1) − 1)))
357 peano2uz 11934 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑁 ∈ (ℤ𝑀) → (𝑁 + 1) ∈ (ℤ𝑀))
358 fzss1 12573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((𝑁 + 1) ∈ (ℤ𝑀) → ((𝑁 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1)))
359319, 357, 358mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑁 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1))
360 simpr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)))
361359, 360sseldi 3742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → 𝑗 ∈ (𝑀...(𝑚 + 1)))
362 eqeq1 2764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑥 = 𝑗 → (𝑥 = 𝑀𝑗 = 𝑀))
363 oveq1 6820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑥 = 𝑗 → (𝑥 − 1) = (𝑗 − 1))
364363fveq2d 6356 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑥 = 𝑗 → (𝑔‘(𝑥 − 1)) = (𝑔‘(𝑗 − 1)))
365362, 364ifbieq2d 4255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑥 = 𝑗 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))))
366 fvex 6362 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑔‘(𝑗 − 1)) ∈ V
367207, 366ifex 4300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))) ∈ V
368365, 199, 367fvmpt 6444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑗 ∈ (𝑀...(𝑚 + 1)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))))
369361, 368syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))))
37047, 44breqtrri 4831 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 𝑀 < 𝑁
371305ltp1i 11119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 𝑁 < (𝑁 + 1)
37246, 305, 336lttri 10355 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((𝑀 < 𝑁𝑁 < (𝑁 + 1)) → 𝑀 < (𝑁 + 1))
373370, 371, 372mp2an 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 𝑀 < (𝑁 + 1)
37446, 336ltnlei 10350 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑀 < (𝑁 + 1) ↔ ¬ (𝑁 + 1) ≤ 𝑀)
375373, 374mpbi 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ¬ (𝑁 + 1) ≤ 𝑀
376 eleq1 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (𝑗 = 𝑀 → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) ↔ 𝑀 ∈ ((𝑁 + 1)...(𝑚 + 1))))
377 elfzle1 12537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (𝑀 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑁 + 1) ≤ 𝑀)
378376, 377syl6bi 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑗 = 𝑀 → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑁 + 1) ≤ 𝑀))
379378com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 = 𝑀 → (𝑁 + 1) ≤ 𝑀))
380375, 379mtoi 190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ¬ 𝑗 = 𝑀)
381380adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ¬ 𝑗 = 𝑀)
382381iffalsed 4241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))) = (𝑔‘(𝑗 − 1)))
383369, 382eqtrd 2794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = (𝑔‘(𝑗 − 1)))
384383sbceq1d 3581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑[(𝑔‘(𝑗 − 1)) / 𝑏]𝜑))
385356, 384sbceqbid 3583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑[(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑))
386385biimpar 503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) ∧ [(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
387318, 386syldan 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
388387an32s 881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑚𝑍 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
389388adantlrl 758 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
390389adantlll 756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
391291, 390jaodan 861 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) ∧ (𝑗 = 𝑁𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
392245, 391syldan 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) ∧ 𝑗 ∈ (𝑁...(𝑚 + 1))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
393392ralrimiva 3104 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∀𝑗 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
394 oveq1 6820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑗 = 𝑘 → (𝑗 − 1) = (𝑘 − 1))
395394fveq2d 6356 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 = 𝑘 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)))
396 fveq2 6352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑗 = 𝑘 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘))
397396sbceq1d 3581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 = 𝑘 → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
398395, 397sbceqbid 3583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑗 = 𝑘 → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
399398cbvralv 3310 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (∀𝑗 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑 ↔ ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
400393, 399sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
401400adantllr 757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
402401adantrlr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ (((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
4034023adantr1 1175 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
404 ovex 6841 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑀...(𝑚 + 1)) ∈ V
405404mptex 6650 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) ∈ V
406 feq1 6187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ↔ (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴))
407 fveq1 6351 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓𝑀) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀))
408407eqeq1d 2762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ((𝑓𝑀) = 𝑐 ↔ ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐))
409 fveq1 6351 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓‘(𝑚 + 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)))
410409sbceq1d 3581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ([(𝑓‘(𝑚 + 1)) / 𝑎]𝜃[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃))
411408, 410anbi12d 749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ↔ (((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃)))
412 fveq1 6351 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓‘(𝑘 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)))
413 fveq1 6351 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓𝑘) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘))
414413sbceq1d 3581 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ([(𝑓𝑘) / 𝑏]𝜑[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
415412, 414sbceqbid 3583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓𝑘) / 𝑏]𝜑[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
416113, 415syl5bbr 274 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝜒[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
417416ralbidv 3124 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒 ↔ ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
418406, 411, 4173anbi123d 1548 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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))))‘𝑘) / 𝑏]𝜑)))
419405, 418spcev 3440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴 ∧ (((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))
420203, 210, 236, 403, 419syl121anc 1482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))
421420ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
422143, 421chvarv 2408 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((([𝑑 / 𝑏]𝜑𝑎𝐴) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
423133, 422chvarv 2408 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑎𝐴) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
424423adantlrr 759 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
425424adantlll 756 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
426425imp 444 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))
427 oveq2 6821 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = (𝑚 + 1) → (𝑀...𝑛) = (𝑀...(𝑚 + 1)))
428427feq2d 6192 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = (𝑚 + 1) → (𝑓:(𝑀...𝑛)⟶𝐴𝑓:(𝑀...(𝑚 + 1))⟶𝐴))
429 fveq2 6352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = (𝑚 + 1) → (𝑓𝑛) = (𝑓‘(𝑚 + 1)))
430429sbceq1d 3581 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = (𝑚 + 1) → ([(𝑓𝑛) / 𝑎]𝜃[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃))
43138, 430syl5bbr 274 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = (𝑚 + 1) → (𝜏[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃))
432431anbi2d 742 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = (𝑚 + 1) → (((𝑓𝑀) = 𝑎𝜏) ↔ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃)))
433 oveq2 6821 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = (𝑚 + 1) → (𝑁...𝑛) = (𝑁...(𝑚 + 1)))
434433raleqdv 3283 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = (𝑚 + 1) → (∀𝑘 ∈ (𝑁...𝑛)𝜒 ↔ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))
435428, 432, 4343anbi123d 1548 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = (𝑚 + 1) → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
436435exbidv 1999 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = (𝑚 + 1) → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
437436rspcev 3449 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑚 + 1) ∈ 𝑍 ∧ ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
438125, 426, 437syl2anc 696 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
439438ex 449 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
440439exlimdv 2010 . . . . . . . . . . . . . . . . . . . 20 ((((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) → (∃𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
441440rexlimdva 3169 . . . . . . . . . . . . . . . . . . 19 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (∃𝑚𝑍𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
442123, 441syl5bi 232 . . . . . . . . . . . . . . . . . 18 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
44373, 88, 4423syld 60 . . . . . . . . . . . . . . . . 17 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
444443an42s 905 . . . . . . . . . . . . . . . 16 (((𝜂𝑎𝐴) ∧ (𝑏𝐴𝜑)) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
445444rexlimdvaa 3170 . . . . . . . . . . . . . . 15 ((𝜂𝑎𝐴) → (∃𝑏𝐴 𝜑 → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))))
446445imp 444 . . . . . . . . . . . . . 14 (((𝜂𝑎𝐴) ∧ ∃𝑏𝐴 𝜑) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
447 fdc.10 . . . . . . . . . . . . . 14 ((𝜂𝑎𝐴) → (𝜃 ∨ ∃𝑏𝐴 𝜑))
44865, 446, 447mpjaodan 862 . . . . . . . . . . . . 13 ((𝜂𝑎𝐴) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
449138anbi1d 743 . . . . . . . . . . . . . . . . . 18 (𝑐 = 𝑎 → (((𝑓𝑀) = 𝑐𝜏) ↔ ((𝑓𝑀) = 𝑎𝜏)))
4504493anbi2d 1553 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑎 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
451450exbidv 1999 . . . . . . . . . . . . . . . 16 (𝑐 = 𝑎 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
452451rexbidv 3190 . . . . . . . . . . . . . . 15 (𝑐 = 𝑎 → (∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
453452elrab3 3505 . . . . . . . . . . . . . 14 (𝑎𝐴 → (𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
454453adantl 473 . . . . . . . . . . . . 13 ((𝜂𝑎𝐴) → (𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
455448, 454sylibrd 249 . . . . . . . . . . . 12 ((𝜂𝑎𝐴) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
456455ex 449 . . . . . . . . . . 11 (𝜂 → (𝑎𝐴 → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
457456com23 86 . . . . . . . . . 10 (𝜂 → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → (𝑎𝐴𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
458 eldif 3725 . . . . . . . . . . . 12 (𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ↔ (𝑎𝐴 ∧ ¬ 𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
459458notbii 309 . . . . . . . . . . 11 𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ↔ ¬ (𝑎𝐴 ∧ ¬ 𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
460 iman 439 . . . . . . . . . . 11 ((𝑎𝐴𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ↔ ¬ (𝑎𝐴 ∧ ¬ 𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
461459, 460bitr4i 267 . . . . . . . . . 10 𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ↔ (𝑎𝐴𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
462457, 461syl6ibr 242 . . . . . . . . 9 (𝜂 → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ¬ 𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
463462con2d 129 . . . . . . . 8 (𝜂 → (𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
464463imp 444 . . . . . . 7 ((𝜂𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) → ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
465464nrexdv 3139 . . . . . 6 (𝜂 → ¬ ∃𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
466 df-ne 2933 . . . . . . 7 ((𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅ ↔ ¬ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅)
467 fdc.9 . . . . . . . 8 (𝜂𝑅 Fr 𝐴)
468 difss 3880 . . . . . . . 8 (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴
469 fdc.1 . . . . . . . . . . 11 𝐴 ∈ V
470 difexg 4960 . . . . . . . . . . 11 (𝐴 ∈ V → (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∈ V)
471469, 470ax-mp 5 . . . . . . . . . 10 (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∈ V
472 fri 5228 . . . . . . . . . 10 ((((𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∈ V ∧ 𝑅 Fr 𝐴) ∧ ((𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴 ∧ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅)) → ∃𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
473471, 472mpanl1 718 . . . . . . . . 9 ((𝑅 Fr 𝐴 ∧ ((𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴 ∧ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅)) → ∃𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
474473expr 644 . . . . . . . 8 ((𝑅 Fr 𝐴 ∧ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴) → ((𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅ → ∃𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
475467, 468, 474sylancl 697 . . . . . . 7 (𝜂 → ((𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅ → ∃𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
476466, 475syl5bir 233 . . . . . 6 (𝜂 → (¬ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅ → ∃𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
477465, 476mt3d 140 . . . . 5 (𝜂 → (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅)
478 ssdif0 4085 . . . . 5 (𝐴 ⊆ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅)
479477, 478sylibr 224 . . . 4 (𝜂𝐴 ⊆ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})
48076a1i 11 . . . 4 (𝜂 → {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ⊆ 𝐴)
481479, 480eqssd 3761 . . 3 (𝜂𝐴 = {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})
482 rabid2 3257 . . 3 (𝐴 = {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∀𝑐𝐴𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
483481, 482sylib 208 . 2 (𝜂 → ∀𝑐𝐴𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
484 eqeq2 2771 . . . . . . 7 (𝑐 = 𝐶 → ((𝑓𝑀) = 𝑐 ↔ (𝑓𝑀) = 𝐶))
485484anbi1d 743 . . . . . 6 (𝑐 = 𝐶 → (((𝑓𝑀) = 𝑐𝜏) ↔ ((𝑓𝑀) = 𝐶𝜏)))
4864853anbi2d 1553 . . . . 5 (𝑐 = 𝐶 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝐶𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
487486exbidv 1999 . . . 4 (𝑐 = 𝐶 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝐶𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
488487rexbidv 3190 . . 3 (𝑐 = 𝐶 → (∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝐶𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
489488rspcva 3447 . 2 ((𝐶𝐴 ∧ ∀𝑐𝐴𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝐶𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
4901, 483, 489syl2anc 696 1 (𝜂 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝐶𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1072   = wceq 1632  wex 1853  wcel 2139  wne 2932  wral 3050  wrex 3051  {crab 3054  Vcvv 3340  [wsbc 3576  cdif 3712  wss 3715  c0 4058  ifcif 4230  {csn 4321  cop 4327   class class class wbr 4804  cmpt 4881   Fr wfr 5222  wf 6045  cfv 6049  (class class class)co 6813  cc 10126  cr 10127  1c1 10129   + caddc 10131   < clt 10266  cle 10267  cmin 10458  cz 11569  cuz 11879  ...cfz 12519
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-1st 7333  df-2nd 7334  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-er 7911  df-en 8122  df-dom 8123  df-sdom 8124  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-nn 11213  df-n0 11485  df-z 11570  df-uz 11880  df-fz 12520
This theorem is referenced by:  fdc1  33855
  Copyright terms: Public domain W3C validator