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 36001
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 12690 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ𝑀))
42, 3ax-mp 5 . . . . . . . . . . . . . . . . . 18 𝑀 ∈ (ℤ𝑀)
5 fdc.3 . . . . . . . . . . . . . . . . . 18 𝑍 = (ℤ𝑀)
64, 5eleqtrri 2836 . . . . . . . . . . . . . . . . 17 𝑀𝑍
7 eqid 2736 . . . . . . . . . . . . . . . . . . . . . 22 {⟨𝑀, 𝑎⟩} = {⟨𝑀, 𝑎⟩}
82elexi 3460 . . . . . . . . . . . . . . . . . . . . . . 23 𝑀 ∈ V
9 vex 3445 . . . . . . . . . . . . . . . . . . . . . . 23 𝑎 ∈ V
108, 9fsn 7057 . . . . . . . . . . . . . . . . . . . . . 22 ({⟨𝑀, 𝑎⟩}:{𝑀}⟶{𝑎} ↔ {⟨𝑀, 𝑎⟩} = {⟨𝑀, 𝑎⟩})
117, 10mpbir 230 . . . . . . . . . . . . . . . . . . . . 21 {⟨𝑀, 𝑎⟩}:{𝑀}⟶{𝑎}
12 snssi 4754 . . . . . . . . . . . . . . . . . . . . 21 (𝑎𝐴 → {𝑎} ⊆ 𝐴)
13 fss 6662 . . . . . . . . . . . . . . . . . . . . 21 (({⟨𝑀, 𝑎⟩}:{𝑀}⟶{𝑎} ∧ {𝑎} ⊆ 𝐴) → {⟨𝑀, 𝑎⟩}:{𝑀}⟶𝐴)
1411, 12, 13sylancr 587 . . . . . . . . . . . . . . . . . . . 20 (𝑎𝐴 → {⟨𝑀, 𝑎⟩}:{𝑀}⟶𝐴)
15 fzsn 13391 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀})
162, 15ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (𝑀...𝑀) = {𝑀}
1716feq2i 6637 . . . . . . . . . . . . . . . . . . . 20 ({⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴 ↔ {⟨𝑀, 𝑎⟩}:{𝑀}⟶𝐴)
1814, 17sylibr 233 . . . . . . . . . . . . . . . . . . 19 (𝑎𝐴 → {⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴)
1918adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝑎𝐴𝜃) → {⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴)
208, 9fvsn 7103 . . . . . . . . . . . . . . . . . . 19 ({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎
2120a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝑎𝐴𝜃) → ({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎)
22 simpr 485 . . . . . . . . . . . . . . . . . 18 ((𝑎𝐴𝜃) → 𝜃)
23 snex 5373 . . . . . . . . . . . . . . . . . . 19 {⟨𝑀, 𝑎⟩} ∈ V
24 feq1 6626 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = {⟨𝑀, 𝑎⟩} → (𝑓:(𝑀...𝑀)⟶𝐴 ↔ {⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴))
25 fveq1 6818 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = {⟨𝑀, 𝑎⟩} → (𝑓𝑀) = ({⟨𝑀, 𝑎⟩}‘𝑀))
2625eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = {⟨𝑀, 𝑎⟩} → ((𝑓𝑀) = 𝑎 ↔ ({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎))
2725, 20eqtrdi 2792 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = {⟨𝑀, 𝑎⟩} → (𝑓𝑀) = 𝑎)
28 sbceq2a 3738 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓𝑀) = 𝑎 → ([(𝑓𝑀) / 𝑎]𝜃𝜃))
2927, 28syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = {⟨𝑀, 𝑎⟩} → ([(𝑓𝑀) / 𝑎]𝜃𝜃))
3026, 29anbi12d 631 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = {⟨𝑀, 𝑎⟩} → (((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃) ↔ (({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎𝜃)))
3124, 30anbi12d 631 . . . . . . . . . . . . . . . . . . 19 (𝑓 = {⟨𝑀, 𝑎⟩} → ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃)) ↔ ({⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴 ∧ (({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎𝜃))))
3223, 31spcev 3554 . . . . . . . . . . . . . . . . . 18 (({⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴 ∧ (({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎𝜃)) → ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃)))
3319, 21, 22, 32syl12anc 834 . . . . . . . . . . . . . . . . 17 ((𝑎𝐴𝜃) → ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃)))
34 oveq2 7337 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑀 → (𝑀...𝑛) = (𝑀...𝑀))
3534feq2d 6631 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑀 → (𝑓:(𝑀...𝑛)⟶𝐴𝑓:(𝑀...𝑀)⟶𝐴))
36 fvex 6832 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓𝑛) ∈ V
37 fdc.7 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = (𝑓𝑛) → (𝜃𝜏))
3836, 37sbcie 3769 . . . . . . . . . . . . . . . . . . . . . . 23 ([(𝑓𝑛) / 𝑎]𝜃𝜏)
39 fveq2 6819 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑀 → (𝑓𝑛) = (𝑓𝑀))
4039sbceq1d 3731 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑀 → ([(𝑓𝑛) / 𝑎]𝜃[(𝑓𝑀) / 𝑎]𝜃))
4138, 40bitr3id 284 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑀 → (𝜏[(𝑓𝑀) / 𝑎]𝜃))
4241anbi2d 629 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑀 → (((𝑓𝑀) = 𝑎𝜏) ↔ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃)))
43 oveq2 7337 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑀 → (𝑁...𝑛) = (𝑁...𝑀))
44 fdc.4 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑁 = (𝑀 + 1)
4544oveq1i 7339 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁...𝑀) = ((𝑀 + 1)...𝑀)
462zrei 12418 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑀 ∈ ℝ
4746ltp1i 11972 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑀 < (𝑀 + 1)
48 peano2z 12454 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑀 ∈ ℤ → (𝑀 + 1) ∈ ℤ)
492, 48ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑀 + 1) ∈ ℤ
50 fzn 13365 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑀 + 1) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 < (𝑀 + 1) ↔ ((𝑀 + 1)...𝑀) = ∅))
5149, 2, 50mp2an 689 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 < (𝑀 + 1) ↔ ((𝑀 + 1)...𝑀) = ∅)
5247, 51mpbi 229 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑀 + 1)...𝑀) = ∅
5345, 52eqtri 2764 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁...𝑀) = ∅
5443, 53eqtrdi 2792 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑀 → (𝑁...𝑛) = ∅)
5554raleqdv 3309 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑀 → (∀𝑘 ∈ (𝑁...𝑛)𝜒 ↔ ∀𝑘 ∈ ∅ 𝜒))
5635, 42, 553anbi123d 1435 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑀 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃) ∧ ∀𝑘 ∈ ∅ 𝜒)))
57 ral0 4456 . . . . . . . . . . . . . . . . . . . . 21 𝑘 ∈ ∅ 𝜒
58 df-3an 1088 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃) ∧ ∀𝑘 ∈ ∅ 𝜒) ↔ ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃)) ∧ ∀𝑘 ∈ ∅ 𝜒))
5957, 58mpbiran2 707 . . . . . . . . . . . . . . . . . . . 20 ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃) ∧ ∀𝑘 ∈ ∅ 𝜒) ↔ (𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃)))
6056, 59bitrdi 286 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑀 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃))))
6160exbidv 1923 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑀 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃))))
6261rspcev 3570 . . . . . . . . . . . . . . . . 17 ((𝑀𝑍 ∧ ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃))) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
636, 33, 62sylancr 587 . . . . . . . . . . . . . . . 16 ((𝑎𝐴𝜃) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
6463adantll 711 . . . . . . . . . . . . . . 15 (((𝜂𝑎𝐴) ∧ 𝜃) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
6564a1d 25 . . . . . . . . . . . . . 14 (((𝜂𝑎𝐴) ∧ 𝜃) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
66 fdc.11 . . . . . . . . . . . . . . . . . . . . 21 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → 𝑏𝑅𝑎)
67 breq1 5092 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑 = 𝑏 → (𝑑𝑅𝑎𝑏𝑅𝑎))
6867rspcev 3570 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∧ 𝑏𝑅𝑎) → ∃𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎)
6968expcom 414 . . . . . . . . . . . . . . . . . . . . 21 (𝑏𝑅𝑎 → (𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎))
7066, 69syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎))
71 dfrex2 3073 . . . . . . . . . . . . . . . . . . . 20 (∃𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎 ↔ ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
7270, 71syl6ib 250 . . . . . . . . . . . . . . . . . . 19 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
7372con2d 134 . . . . . . . . . . . . . . . . . 18 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ¬ 𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
74 eldif 3907 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) ↔ (𝑏𝐴 ∧ ¬ 𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
7574simplbi2 501 . . . . . . . . . . . . . . . . . . . 20 (𝑏𝐴 → (¬ 𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → 𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))))
76 ssrab2 4024 . . . . . . . . . . . . . . . . . . . . . . 23 {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ⊆ 𝐴
77 dfss4 4204 . . . . . . . . . . . . . . . . . . . . . . 23 ({𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ⊆ 𝐴 ↔ (𝐴 ∖ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) = {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})
7876, 77mpbi 229 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴 ∖ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) = {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}
7978eleq2i 2828 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) ↔ 𝑏 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})
80 eqeq2 2748 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 = 𝑏 → ((𝑓𝑀) = 𝑐 ↔ (𝑓𝑀) = 𝑏))
8180anbi1d 630 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = 𝑏 → (((𝑓𝑀) = 𝑐𝜏) ↔ ((𝑓𝑀) = 𝑏𝜏)))
82813anbi2d 1440 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = 𝑏 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
8382exbidv 1923 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 = 𝑏 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
8483rexbidv 3171 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 = 𝑏 → (∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
8584elrab3 3635 . . . . . . . . . . . . . . . . . . . . 21 (𝑏𝐴 → (𝑏 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
8679, 85bitrid 282 . . . . . . . . . . . . . . . . . . . 20 (𝑏𝐴 → (𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
8775, 86sylibd 238 . . . . . . . . . . . . . . . . . . 19 (𝑏𝐴 → (¬ 𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
8887ad2antll 726 . . . . . . . . . . . . . . . . . 18 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (¬ 𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
89 oveq2 7337 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑚 → (𝑀...𝑛) = (𝑀...𝑚))
9089feq2d 6631 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑚 → (𝑓:(𝑀...𝑛)⟶𝐴𝑓:(𝑀...𝑚)⟶𝐴))
91 fveq2 6819 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑚 → (𝑓𝑛) = (𝑓𝑚))
9291sbceq1d 3731 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑚 → ([(𝑓𝑛) / 𝑎]𝜃[(𝑓𝑚) / 𝑎]𝜃))
9338, 92bitr3id 284 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑚 → (𝜏[(𝑓𝑚) / 𝑎]𝜃))
9493anbi2d 629 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑚 → (((𝑓𝑀) = 𝑏𝜏) ↔ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃)))
95 oveq2 7337 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑚 → (𝑁...𝑛) = (𝑁...𝑚))
9695raleqdv 3309 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑚 → (∀𝑘 ∈ (𝑁...𝑛)𝜒 ↔ ∀𝑘 ∈ (𝑁...𝑚)𝜒))
9790, 94, 963anbi123d 1435 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑚 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒)))
9897exbidv 1923 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑚 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒)))
9998cbvrexvw 3222 . . . . . . . . . . . . . . . . . . . 20 (∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑚𝑍𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒))
100 feq1 6626 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = 𝑔 → (𝑓:(𝑀...𝑚)⟶𝐴𝑔:(𝑀...𝑚)⟶𝐴))
101 fveq1 6818 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 = 𝑔 → (𝑓𝑀) = (𝑔𝑀))
102101eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑔 → ((𝑓𝑀) = 𝑏 ↔ (𝑔𝑀) = 𝑏))
103 fveq1 6818 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 = 𝑔 → (𝑓𝑚) = (𝑔𝑚))
104103sbceq1d 3731 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑔 → ([(𝑓𝑚) / 𝑎]𝜃[(𝑔𝑚) / 𝑎]𝜃))
105102, 104anbi12d 631 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = 𝑔 → (((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ↔ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃)))
106 fvex 6832 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓‘(𝑘 − 1)) ∈ V
107 fdc.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 = (𝑓‘(𝑘 − 1)) → (𝜑𝜓))
108107sbcbidv 3785 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = (𝑓‘(𝑘 − 1)) → ([(𝑓𝑘) / 𝑏]𝜑[(𝑓𝑘) / 𝑏]𝜓))
109106, 108sbcie 3769 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓𝑘) / 𝑏]𝜑[(𝑓𝑘) / 𝑏]𝜓)
110 fvex 6832 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓𝑘) ∈ V
111 fdc.6 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 = (𝑓𝑘) → (𝜓𝜒))
112110, 111sbcie 3769 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([(𝑓𝑘) / 𝑏]𝜓𝜒)
113109, 112bitri 274 . . . . . . . . . . . . . . . . . . . . . . . . 25 ([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓𝑘) / 𝑏]𝜑𝜒)
114 fveq1 6818 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 = 𝑔 → (𝑓‘(𝑘 − 1)) = (𝑔‘(𝑘 − 1)))
115 fveq1 6818 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓 = 𝑔 → (𝑓𝑘) = (𝑔𝑘))
116115sbceq1d 3731 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 = 𝑔 → ([(𝑓𝑘) / 𝑏]𝜑[(𝑔𝑘) / 𝑏]𝜑))
117114, 116sbceqbid 3733 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 = 𝑔 → ([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓𝑘) / 𝑏]𝜑[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑))
118113, 117bitr3id 284 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑔 → (𝜒[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑))
119118ralbidv 3170 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = 𝑔 → (∀𝑘 ∈ (𝑁...𝑚)𝜒 ↔ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑))
120100, 105, 1193anbi123d 1435 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = 𝑔 → ((𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒) ↔ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)))
121120cbvexvw 2039 . . . . . . . . . . . . . . . . . . . . 21 (∃𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒) ↔ ∃𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑))
122121rexbii 3093 . . . . . . . . . . . . . . . . . . . 20 (∃𝑚𝑍𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒) ↔ ∃𝑚𝑍𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑))
12399, 122bitri 274 . . . . . . . . . . . . . . . . . . 19 (∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑚𝑍𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑))
1245peano2uzs 12735 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚𝑍 → (𝑚 + 1) ∈ 𝑍)
125124ad2antlr 724 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → (𝑚 + 1) ∈ 𝑍)
126 sbceq2a 3738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑑 = 𝑏 → ([𝑑 / 𝑏]𝜑𝜑))
127126anbi1d 630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑑 = 𝑏 → (([𝑑 / 𝑏]𝜑𝑎𝐴) ↔ (𝜑𝑎𝐴)))
128127anbi1d 630 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑑 = 𝑏 → ((([𝑑 / 𝑏]𝜑𝑎𝐴) ∧ 𝑚𝑍) ↔ ((𝜑𝑎𝐴) ∧ 𝑚𝑍)))
129 eqeq2 2748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑑 = 𝑏 → ((𝑔𝑀) = 𝑑 ↔ (𝑔𝑀) = 𝑏))
130129anbi1d 630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑑 = 𝑏 → (((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ↔ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃)))
1311303anbi2d 1440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑐 = 𝑎 → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑[𝑑 / 𝑏]𝜑))
135 eleq1 2824 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑐 = 𝑎 → (𝑐𝐴𝑎𝐴))
136134, 135anbi12d 631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 = 𝑎 → (([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ↔ ([𝑑 / 𝑏]𝜑𝑎𝐴)))
137136anbi1d 630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = 𝑎 → ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ↔ (([𝑑 / 𝑏]𝜑𝑎𝐴) ∧ 𝑚𝑍)))
138 eqeq2 2748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 = 𝑎 → ((𝑓𝑀) = 𝑐 ↔ (𝑓𝑀) = 𝑎))
139138anbi1d 630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑐 = 𝑎 → (((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ↔ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃)))
1401393anbi2d 1440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑐 = 𝑎 → ((𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒) ↔ (𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
141140exbidv 1923 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑚 ∈ (ℤ𝑀) → (𝑚 + 1) ∈ (ℤ𝑀))
145144, 5eleq2s 2855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑚𝑍 → (𝑚 + 1) ∈ (ℤ𝑀))
146 elfzp12 13428 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑚 + 1) ∈ (ℤ𝑀) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↔ (𝑥 = 𝑀𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)))))
147145, 146syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑚𝑍 → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↔ (𝑥 = 𝑀𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)))))
148147ad2antlr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↔ (𝑥 = 𝑀𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)))))
149 iftrue 4478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑥 = 𝑀 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = 𝑐)
150149eleq1d 2821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑥 = 𝑀 → (if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴𝑐𝐴))
151150biimprcd 249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑐𝐴 → (𝑥 = 𝑀 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
152151ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 = 𝑀 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
153 1re 11068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 1 ∈ ℝ
15446, 153readdcli 11083 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑀 + 1) ∈ ℝ
15546, 154ltnlei 11189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑀 < (𝑀 + 1) ↔ ¬ (𝑀 + 1) ≤ 𝑀)
15647, 155mpbi 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ¬ (𝑀 + 1) ≤ 𝑀
157 eleq1 2824 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑥 = 𝑀 → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) ↔ 𝑀 ∈ ((𝑀 + 1)...(𝑚 + 1))))
158 elfzle1 13352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑚𝑍𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = (𝑔‘(𝑥 − 1)))
164 elfzelz 13349 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → 𝑥 ∈ ℤ)
165164adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → 𝑥 ∈ ℤ)
166 eluzelz 12685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑚 ∈ (ℤ𝑀) → 𝑚 ∈ ℤ)
167166, 5eleq2s 2855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑚𝑍𝑚 ∈ ℤ)
168167peano2zd 12522 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑚𝑍 → (𝑚 + 1) ∈ ℤ)
169 1z 12443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 1 ∈ ℤ
170 fzsubel 13385 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ((((𝑀 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ 𝑥 ∈ ℤ) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))))
17349, 172mpanl1 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11082 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 𝑀 ∈ ℂ
180 ax-1cn 11022 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 1 ∈ ℂ
181179, 180pncan3oi 11330 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑀 + 1) − 1) = 𝑀
182181a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑚𝑍 → ((𝑀 + 1) − 1) = 𝑀)
183167zcnd 12520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑚𝑍𝑚 ∈ ℂ)
184 pncan 11320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑚 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑚 + 1) − 1) = 𝑚)
185183, 180, 184sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑚𝑍 → ((𝑚 + 1) − 1) = 𝑚)
186182, 185oveq12d 7347 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑚𝑍 → (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑀...𝑚))
187186adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑀...𝑚))
188178, 187eleqtrd 2839 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚𝑍𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑥 − 1) ∈ (𝑀...𝑚))
189 ffvelcdm 7009 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ (𝑥 − 1) ∈ (𝑀...𝑚)) → (𝑔‘(𝑥 − 1)) ∈ 𝐴)
190188, 189sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ (𝑚𝑍𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)))) → (𝑔‘(𝑥 − 1)) ∈ 𝐴)
191190anassrs 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑔:(𝑀...𝑚)⟶𝐴𝑚𝑍) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑔‘(𝑥 − 1)) ∈ 𝐴)
192191ancom1s 650 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑚𝑍𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑔‘(𝑥 − 1)) ∈ 𝐴)
193163, 192eqeltrd 2837 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑚𝑍𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴)
194193ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑚𝑍𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
195194adantll 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
196152, 195jaod 856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → ((𝑥 = 𝑀𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
197148, 196sylbid 239 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
198197ralrimiv 3138 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → ∀𝑥 ∈ (𝑀...(𝑚 + 1))if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴)
199 eqid 2736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))
200199fmpt 7034 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (∀𝑥 ∈ (𝑀...(𝑚 + 1))if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴 ↔ (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴)
201198, 200sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴)
202201adantlll 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴)
2032023ad2antr1 1187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴)
204 eluzfz1 13356 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑚 + 1) ∈ (ℤ𝑀) → 𝑀 ∈ (𝑀...(𝑚 + 1)))
205144, 204syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑚 ∈ (ℤ𝑀) → 𝑀 ∈ (𝑀...(𝑚 + 1)))
206205, 5eleq2s 2855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑚𝑍𝑀 ∈ (𝑀...(𝑚 + 1)))
207 vex 3445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑐 ∈ V
208149, 199, 207fvmpt 6925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑀 ∈ (𝑀...(𝑚 + 1)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐)
209206, 208syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑚𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐)
210209ad2antlr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐)
211 eluzfz2 13357 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑚 + 1) ∈ (ℤ𝑀) → (𝑚 + 1) ∈ (𝑀...(𝑚 + 1)))
212144, 211syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑚 ∈ (ℤ𝑀) → (𝑚 + 1) ∈ (𝑀...(𝑚 + 1)))
213212, 5eleq2s 2855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑚𝑍 → (𝑚 + 1) ∈ (𝑀...(𝑚 + 1)))
214 eqeq1 2740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑥 = (𝑚 + 1) → (𝑥 = 𝑀 ↔ (𝑚 + 1) = 𝑀))
215 fvoveq1 7352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑥 = (𝑚 + 1) → (𝑔‘(𝑥 − 1)) = (𝑔‘((𝑚 + 1) − 1)))
216214, 215ifbieq2d 4498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑥 = (𝑚 + 1) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1))))
217 fvex 6832 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑔‘((𝑚 + 1) − 1)) ∈ V
218207, 217ifex 4522 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1))) ∈ V
219216, 199, 218fvmpt 6925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑚 ∈ (ℤ𝑀) → 𝑀𝑚)
222221, 5eleq2s 2855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑚𝑍𝑀𝑚)
223 zleltp1 12464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑀𝑚𝑀 < (𝑚 + 1)))
2242, 167, 223sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑚𝑍 → (𝑀𝑚𝑀 < (𝑚 + 1)))
225222, 224mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑚𝑍𝑀 < (𝑚 + 1))
226 ltne 11165 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑀 ∈ ℝ ∧ 𝑀 < (𝑚 + 1)) → (𝑚 + 1) ≠ 𝑀)
22746, 225, 226sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑚𝑍 → (𝑚 + 1) ≠ 𝑀)
228227neneqd 2945 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑚𝑍 → ¬ (𝑚 + 1) = 𝑀)
229228iffalsed 4483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑚𝑍 → if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1))) = (𝑔‘((𝑚 + 1) − 1)))
230185fveq2d 6823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑚𝑍 → (𝑔‘((𝑚 + 1) − 1)) = (𝑔𝑚))
231220, 229, 2303eqtrd 2780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑚𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) = (𝑔𝑚))
232231sbceq1d 3731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑚𝑍 → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃[(𝑔𝑚) / 𝑎]𝜃))
233232biimpar 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑚𝑍[(𝑔𝑚) / 𝑎]𝜃) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃)
234233ad2ant2l 743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃)) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃)
2352343ad2antr2 1188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃)
236 eluzp1p1 12703 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑚 ∈ (ℤ𝑀) → (𝑚 + 1) ∈ (ℤ‘(𝑀 + 1)))
237236, 5eleq2s 2855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑚𝑍 → (𝑚 + 1) ∈ (ℤ‘(𝑀 + 1)))
23844fveq2i 6822 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (ℤ𝑁) = (ℤ‘(𝑀 + 1))
239237, 238eleqtrrdi 2848 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑚𝑍 → (𝑚 + 1) ∈ (ℤ𝑁))
240 elfzp12 13428 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑚 + 1) ∈ (ℤ𝑁) → (𝑗 ∈ (𝑁...(𝑚 + 1)) ↔ (𝑗 = 𝑁𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)))))
241239, 240syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑚𝑍 → (𝑗 ∈ (𝑁...(𝑚 + 1)) ↔ (𝑗 = 𝑁𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)))))
242241biimpa 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑚𝑍𝑗 ∈ (𝑁...(𝑚 + 1))) → (𝑗 = 𝑁𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))))
243242adantll 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ 𝑗 ∈ (𝑁...(𝑚 + 1))) → (𝑗 = 𝑁𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))))
244243adantlr 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) ∧ 𝑗 ∈ (𝑁...(𝑚 + 1))) → (𝑗 = 𝑁𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))))
245 oveq1 7336 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑗 = 𝑁 → (𝑗 − 1) = (𝑁 − 1))
24644oveq1i 7339 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑁 − 1) = ((𝑀 + 1) − 1)
247246, 181eqtri 2764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑁 − 1) = 𝑀
248245, 247eqtrdi 2792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑗 = 𝑁 → (𝑗 − 1) = 𝑀)
249248fveq2d 6823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑗 = 𝑁 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀))
250249ad2antll 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6819 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑗 = (𝑀 + 1) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)))
255253, 254sylbi 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑗 = 𝑁 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)))
256255ad2antll 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)))
25746, 154, 47ltleii 11191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 𝑀 ≤ (𝑀 + 1)
258 eluz2 12681 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((𝑀 + 1) ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑀 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑀 + 1)))
2592, 49, 257, 258mpbir3an 1340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑀 + 1) ∈ (ℤ𝑀)
260 fzss1 13388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ((𝑀 + 1) ∈ (ℤ𝑀) → ((𝑀 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1)))
261259, 260ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((𝑀 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1))
262 eluzfz1 13356 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (𝑚 ∈ (ℤ𝑀) → 𝑀 ∈ (𝑀...𝑚))
263262, 5eleq2s 2855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑚𝑍𝑀 ∈ (𝑀...𝑚))
264 fzaddel 13383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (((𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑀 ∈ (𝑀...𝑚) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1))))
2652, 169, 264mpanr12 702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑀 ∈ (𝑀...𝑚) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1))))
2662, 167, 265sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑚𝑍 → (𝑀 ∈ (𝑀...𝑚) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1))))
267263, 266mpbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑚𝑍 → (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1)))
268261, 267sselid 3929 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑚𝑍 → (𝑀 + 1) ∈ (𝑀...(𝑚 + 1)))
269 eqeq1 2740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑥 = (𝑀 + 1) → (𝑥 = 𝑀 ↔ (𝑀 + 1) = 𝑀))
270 oveq1 7336 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (𝑥 = (𝑀 + 1) → (𝑥 − 1) = ((𝑀 + 1) − 1))
271270, 181eqtrdi 2792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (𝑥 = (𝑀 + 1) → (𝑥 − 1) = 𝑀)
272271fveq2d 6823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑥 = (𝑀 + 1) → (𝑔‘(𝑥 − 1)) = (𝑔𝑀))
273269, 272ifbieq2d 4498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑥 = (𝑀 + 1) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if((𝑀 + 1) = 𝑀, 𝑐, (𝑔𝑀)))
274 fvex 6832 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑔𝑀) ∈ V
275207, 274ifex 4522 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 if((𝑀 + 1) = 𝑀, 𝑐, (𝑔𝑀)) ∈ V
276273, 199, 275fvmpt 6925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑀 + 1) ∈ (𝑀...(𝑚 + 1)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)) = if((𝑀 + 1) = 𝑀, 𝑐, (𝑔𝑀)))
277268, 276syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑚𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)) = if((𝑀 + 1) = 𝑀, 𝑐, (𝑔𝑀)))
27846, 47gtneii 11180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑀 + 1) ≠ 𝑀
279 ifnefalse 4484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → (𝑔𝑀) = 𝑑)
284256, 282, 2833eqtrd 2780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = 𝑑)
285284sbceq1d 3731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑[𝑑 / 𝑏]𝜑))
286252, 285sbceqbid 3733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) ∧ 𝑗 = 𝑁) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
291 elfzelz 13349 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → 𝑗 ∈ ℤ)
292291adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → 𝑗 ∈ ℤ)
29344, 49eqeltri 2833 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 𝑁 ∈ ℤ
294 peano2z 12454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑁 ∈ ℤ → (𝑁 + 1) ∈ ℤ)
295293, 294ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑁 + 1) ∈ ℤ
296 fzsubel 13385 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 𝑁 ∈ ℝ
305304recni 11082 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 𝑁 ∈ ℂ
306305, 180pncan3oi 11330 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑁 + 1) − 1) = 𝑁
307306a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑚𝑍 → ((𝑁 + 1) − 1) = 𝑁)
308307, 185oveq12d 7347 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑚𝑍 → (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑁...𝑚))
309308adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑁...𝑚))
310303, 309eleqtrd 2839 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 − 1) ∈ (𝑁...𝑚))
311 fvoveq1 7352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑘 = (𝑗 − 1) → (𝑔‘(𝑘 − 1)) = (𝑔‘((𝑗 − 1) − 1)))
312 fveq2 6819 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑘 = (𝑗 − 1) → (𝑔𝑘) = (𝑔‘(𝑗 − 1)))
313312sbceq1d 3731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑘 = (𝑗 − 1) → ([(𝑔𝑘) / 𝑏]𝜑[(𝑔‘(𝑗 − 1)) / 𝑏]𝜑))
314311, 313sbceqbid 3733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑘 = (𝑗 − 1) → ([(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑[(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑))
315314rspcva 3568 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑗 − 1) ∈ (𝑁...𝑚) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → [(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑)
316310, 315sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → [(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑)
31744, 259eqeltri 2833 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 𝑁 ∈ (ℤ𝑀)
318 fzss1 13388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑁 ∈ (ℤ𝑀) → (𝑁...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1)))
319317, 318ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑁...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1))
320 fzssp1 13392 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑁...𝑚) ⊆ (𝑁...(𝑚 + 1))
321320, 310sselid 3929 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 − 1) ∈ (𝑁...(𝑚 + 1)))
322319, 321sselid 3929 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 − 1) ∈ (𝑀...(𝑚 + 1)))
323 eqeq1 2740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑥 = (𝑗 − 1) → (𝑥 = 𝑀 ↔ (𝑗 − 1) = 𝑀))
324 fvoveq1 7352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑥 = (𝑗 − 1) → (𝑔‘(𝑥 − 1)) = (𝑔‘((𝑗 − 1) − 1)))
325323, 324ifbieq2d 4498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑥 = (𝑗 − 1) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1))))
326 fvex 6832 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑔‘((𝑗 − 1) − 1)) ∈ V
327207, 326ifex 4522 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1))) ∈ V
328325, 199, 327fvmpt 6925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11972 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑀 + 1) < ((𝑀 + 1) + 1)
33144oveq1i 7339 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑁 + 1) = ((𝑀 + 1) + 1)
332330, 331breqtrri 5116 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑀 + 1) < (𝑁 + 1)
333304, 153readdcli 11083 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑁 + 1) ∈ ℝ
334154, 333ltnlei 11189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((𝑀 + 1) < (𝑁 + 1) ↔ ¬ (𝑁 + 1) ≤ (𝑀 + 1))
335332, 334mpbi 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ¬ (𝑁 + 1) ≤ (𝑀 + 1)
336291zcnd 12520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → 𝑗 ∈ ℂ)
337 subadd 11317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((𝑗 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑀 ∈ ℂ) → ((𝑗 − 1) = 𝑀 ↔ (1 + 𝑀) = 𝑗))
338180, 179, 337mp3an23 1452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑗 ∈ ℂ → ((𝑗 − 1) = 𝑀 ↔ (1 + 𝑀) = 𝑗))
339336, 338syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ((𝑗 − 1) = 𝑀 ↔ (1 + 𝑀) = 𝑗))
340 eqcom 2743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((1 + 𝑀) = 𝑗𝑗 = (1 + 𝑀))
341180, 179addcomi 11259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (1 + 𝑀) = (𝑀 + 1)
342341eqeq2i 2749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (𝑗 = (1 + 𝑀) ↔ 𝑗 = (𝑀 + 1))
343340, 342bitri 274 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ((1 + 𝑀) = 𝑗𝑗 = (𝑀 + 1))
344 eleq1 2824 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (𝑗 = (𝑀 + 1) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) ↔ (𝑀 + 1) ∈ ((𝑁 + 1)...(𝑚 + 1))))
345 elfzle1 13352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1))) = (𝑔‘((𝑗 − 1) − 1)))
353329, 352eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = (𝑔‘((𝑗 − 1) − 1)))
354 peano2uz 12734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑁 ∈ (ℤ𝑀) → (𝑁 + 1) ∈ (ℤ𝑀))
355 fzss1 13388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((𝑁 + 1) ∈ (ℤ𝑀) → ((𝑁 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1)))
356317, 354, 355mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑁 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1))
357 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)))
358356, 357sselid 3929 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → 𝑗 ∈ (𝑀...(𝑚 + 1)))
359 eqeq1 2740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑥 = 𝑗 → (𝑥 = 𝑀𝑗 = 𝑀))
360 fvoveq1 7352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑥 = 𝑗 → (𝑔‘(𝑥 − 1)) = (𝑔‘(𝑗 − 1)))
361359, 360ifbieq2d 4498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑥 = 𝑗 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))))
362 fvex 6832 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑔‘(𝑗 − 1)) ∈ V
363207, 362ifex 4522 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))) ∈ V
364361, 199, 363fvmpt 6925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑗 ∈ (𝑀...(𝑚 + 1)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))))
365358, 364syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))))
36647, 44breqtrri 5116 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 𝑀 < 𝑁
367304ltp1i 11972 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 𝑁 < (𝑁 + 1)
36846, 304, 333lttri 11194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((𝑀 < 𝑁𝑁 < (𝑁 + 1)) → 𝑀 < (𝑁 + 1))
369366, 367, 368mp2an 689 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 𝑀 < (𝑁 + 1)
37046, 333ltnlei 11189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑀 < (𝑁 + 1) ↔ ¬ (𝑁 + 1) ≤ 𝑀)
371369, 370mpbi 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ¬ (𝑁 + 1) ≤ 𝑀
372 eleq1 2824 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (𝑗 = 𝑀 → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) ↔ 𝑀 ∈ ((𝑁 + 1)...(𝑚 + 1))))
373 elfzle1 13352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))) = (𝑔‘(𝑗 − 1)))
379365, 378eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = (𝑔‘(𝑗 − 1)))
380379sbceq1d 3731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑[(𝑔‘(𝑗 − 1)) / 𝑏]𝜑))
381353, 380sbceqbid 3733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑚𝑍 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
385384adantlrl 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
386385adantlll 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
387290, 386jaodan 955 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3139 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∀𝑗 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
390 fvoveq1 7352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 = 𝑘 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)))
391 fveq2 6819 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑗 = 𝑘 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘))
392391sbceq1d 3731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 = 𝑘 → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
393390, 392sbceqbid 3733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑗 = 𝑘 → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
394393cbvralvw 3221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
397396adantrlr 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ (((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
3983973adantr1 1168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
399 ovex 7362 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑀...(𝑚 + 1)) ∈ V
400399mptex 7149 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) ∈ V
401 feq1 6626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ↔ (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴))
402 fveq1 6818 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓𝑀) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀))
403402eqeq1d 2738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ((𝑓𝑀) = 𝑐 ↔ ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐))
404 fveq1 6818 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓‘(𝑚 + 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)))
405404sbceq1d 3731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6818 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓‘(𝑘 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)))
408 fveq1 6818 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓𝑘) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘))
409408sbceq1d 3731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ([(𝑓𝑘) / 𝑏]𝜑[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
410407, 409sbceqbid 3733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3170 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒 ↔ ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
413401, 406, 4123anbi123d 1435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))
416415ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
417143, 416chvarvv 2001 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((([𝑑 / 𝑏]𝜑𝑎𝐴) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
418133, 417chvarvv 2001 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑎𝐴) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
419418adantlrr 718 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
420419adantlll 715 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
421420imp 407 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))
422 oveq2 7337 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = (𝑚 + 1) → (𝑀...𝑛) = (𝑀...(𝑚 + 1)))
423422feq2d 6631 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = (𝑚 + 1) → (𝑓:(𝑀...𝑛)⟶𝐴𝑓:(𝑀...(𝑚 + 1))⟶𝐴))
424 fveq2 6819 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = (𝑚 + 1) → (𝑓𝑛) = (𝑓‘(𝑚 + 1)))
425424sbceq1d 3731 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = (𝑚 + 1) → ([(𝑓𝑛) / 𝑎]𝜃[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃))
42638, 425bitr3id 284 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = (𝑚 + 1) → (𝜏[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃))
427426anbi2d 629 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = (𝑚 + 1) → (((𝑓𝑀) = 𝑎𝜏) ↔ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃)))
428 oveq2 7337 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = (𝑚 + 1) → (𝑁...𝑛) = (𝑁...(𝑚 + 1)))
429428raleqdv 3309 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = (𝑚 + 1) → (∀𝑘 ∈ (𝑁...𝑛)𝜒 ↔ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))
430423, 427, 4293anbi123d 1435 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = (𝑚 + 1) → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
431430exbidv 1923 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = (𝑚 + 1) → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
432431rspcev 3570 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑚 + 1) ∈ 𝑍 ∧ ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
433125, 421, 432syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
434433ex 413 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
435434exlimdv 1935 . . . . . . . . . . . . . . . . . . . 20 ((((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) → (∃𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
436435rexlimdva 3148 . . . . . . . . . . . . . . . . . . 19 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (∃𝑚𝑍𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
437123, 436biimtrid 241 . . . . . . . . . . . . . . . . . 18 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
43873, 88, 4373syld 60 . . . . . . . . . . . . . . . . 17 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
439438an42s 658 . . . . . . . . . . . . . . . 16 (((𝜂𝑎𝐴) ∧ (𝑏𝐴𝜑)) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
440439rexlimdvaa 3149 . . . . . . . . . . . . . . 15 ((𝜂𝑎𝐴) → (∃𝑏𝐴 𝜑 → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))))
441440imp 407 . . . . . . . . . . . . . 14 (((𝜂𝑎𝐴) ∧ ∃𝑏𝐴 𝜑) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
442 fdc.10 . . . . . . . . . . . . . 14 ((𝜂𝑎𝐴) → (𝜃 ∨ ∃𝑏𝐴 𝜑))
44365, 441, 442mpjaodan 956 . . . . . . . . . . . . 13 ((𝜂𝑎𝐴) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
444138anbi1d 630 . . . . . . . . . . . . . . . . . 18 (𝑐 = 𝑎 → (((𝑓𝑀) = 𝑐𝜏) ↔ ((𝑓𝑀) = 𝑎𝜏)))
4454443anbi2d 1440 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑎 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
446445exbidv 1923 . . . . . . . . . . . . . . . 16 (𝑐 = 𝑎 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
447446rexbidv 3171 . . . . . . . . . . . . . . 15 (𝑐 = 𝑎 → (∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
448447elrab3 3635 . . . . . . . . . . . . . 14 (𝑎𝐴 → (𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
449448adantl 482 . . . . . . . . . . . . 13 ((𝜂𝑎𝐴) → (𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
450443, 449sylibrd 258 . . . . . . . . . . . 12 ((𝜂𝑎𝐴) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
451450ex 413 . . . . . . . . . . 11 (𝜂 → (𝑎𝐴 → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
452451com23 86 . . . . . . . . . 10 (𝜂 → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → (𝑎𝐴𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
453 eldif 3907 . . . . . . . . . . . 12 (𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ↔ (𝑎𝐴 ∧ ¬ 𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
454453notbii 319 . . . . . . . . . . 11 𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ↔ ¬ (𝑎𝐴 ∧ ¬ 𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
455 iman 402 . . . . . . . . . . 11 ((𝑎𝐴𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ↔ ¬ (𝑎𝐴 ∧ ¬ 𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
456454, 455bitr4i 277 . . . . . . . . . 10 𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ↔ (𝑎𝐴𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
457452, 456syl6ibr 251 . . . . . . . . 9 (𝜂 → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ¬ 𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
458457con2d 134 . . . . . . . 8 (𝜂 → (𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
459458imp 407 . . . . . . 7 ((𝜂𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) → ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
460459nrexdv 3142 . . . . . 6 (𝜂 → ¬ ∃𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
461 df-ne 2941 . . . . . . 7 ((𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅ ↔ ¬ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅)
462 fdc.9 . . . . . . . 8 (𝜂𝑅 Fr 𝐴)
463 difss 4077 . . . . . . . 8 (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴
464 fdc.1 . . . . . . . . . . 11 𝐴 ∈ V
465 difexg 5268 . . . . . . . . . . 11 (𝐴 ∈ V → (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∈ V)
466464, 465ax-mp 5 . . . . . . . . . 10 (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∈ V
467 fri 5574 . . . . . . . . . 10 ((((𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∈ V ∧ 𝑅 Fr 𝐴) ∧ ((𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴 ∧ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅)) → ∃𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
468466, 467mpanl1 697 . . . . . . . . 9 ((𝑅 Fr 𝐴 ∧ ((𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴 ∧ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅)) → ∃𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
469468expr 457 . . . . . . . 8 ((𝑅 Fr 𝐴 ∧ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴) → ((𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅ → ∃𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
470462, 463, 469sylancl 586 . . . . . . 7 (𝜂 → ((𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅ → ∃𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
471461, 470syl5bir 242 . . . . . 6 (𝜂 → (¬ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅ → ∃𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
472460, 471mt3d 148 . . . . 5 (𝜂 → (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅)
473 ssdif0 4309 . . . . 5 (𝐴 ⊆ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅)
474472, 473sylibr 233 . . . 4 (𝜂𝐴 ⊆ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})
47576a1i 11 . . . 4 (𝜂 → {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ⊆ 𝐴)
476474, 475eqssd 3948 . . 3 (𝜂𝐴 = {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})
477 rabid2 3432 . . 3 (𝐴 = {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∀𝑐𝐴𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
478476, 477sylib 217 . 2 (𝜂 → ∀𝑐𝐴𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
479 eqeq2 2748 . . . . . . 7 (𝑐 = 𝐶 → ((𝑓𝑀) = 𝑐 ↔ (𝑓𝑀) = 𝐶))
480479anbi1d 630 . . . . . 6 (𝑐 = 𝐶 → (((𝑓𝑀) = 𝑐𝜏) ↔ ((𝑓𝑀) = 𝐶𝜏)))
4814803anbi2d 1440 . . . . 5 (𝑐 = 𝐶 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝐶𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
482481exbidv 1923 . . . 4 (𝑐 = 𝐶 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝐶𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
483482rexbidv 3171 . . 3 (𝑐 = 𝐶 → (∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝐶𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
484483rspcva 3568 . 2 ((𝐶𝐴 ∧ ∀𝑐𝐴𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝐶𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
4851, 478, 484syl2anc 584 1 (𝜂 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝐶𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 844  w3a 1086   = wceq 1540  wex 1780  wcel 2105  wne 2940  wral 3061  wrex 3070  {crab 3403  Vcvv 3441  [wsbc 3726  cdif 3894  wss 3897  c0 4268  ifcif 4472  {csn 4572  cop 4578   class class class wbr 5089  cmpt 5172   Fr wfr 5566  wf 6469  cfv 6473  (class class class)co 7329  cc 10962  cr 10963  1c1 10965   + caddc 10967   < clt 11102  cle 11103  cmin 11298  cz 12412  cuz 12675  ...cfz 13332
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5226  ax-sep 5240  ax-nul 5247  ax-pow 5305  ax-pr 5369  ax-un 7642  ax-cnex 11020  ax-resscn 11021  ax-1cn 11022  ax-icn 11023  ax-addcl 11024  ax-addrcl 11025  ax-mulcl 11026  ax-mulrcl 11027  ax-mulcom 11028  ax-addass 11029  ax-mulass 11030  ax-distr 11031  ax-i2m1 11032  ax-1ne0 11033  ax-1rid 11034  ax-rnegex 11035  ax-rrecex 11036  ax-cnre 11037  ax-pre-lttri 11038  ax-pre-lttrn 11039  ax-pre-ltadd 11040  ax-pre-mulgt0 11041
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4269  df-if 4473  df-pw 4548  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4852  df-iun 4940  df-br 5090  df-opab 5152  df-mpt 5173  df-tr 5207  df-id 5512  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5569  df-we 5571  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6232  df-ord 6299  df-on 6300  df-lim 6301  df-suc 6302  df-iota 6425  df-fun 6475  df-fn 6476  df-f 6477  df-f1 6478  df-fo 6479  df-f1o 6480  df-fv 6481  df-riota 7286  df-ov 7332  df-oprab 7333  df-mpo 7334  df-om 7773  df-1st 7891  df-2nd 7892  df-frecs 8159  df-wrecs 8190  df-recs 8264  df-rdg 8303  df-er 8561  df-en 8797  df-dom 8798  df-sdom 8799  df-pnf 11104  df-mnf 11105  df-xr 11106  df-ltxr 11107  df-le 11108  df-sub 11300  df-neg 11301  df-nn 12067  df-n0 12327  df-z 12413  df-uz 12676  df-fz 13333
This theorem is referenced by:  fdc1  36002
  Copyright terms: Public domain W3C validator