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 34903
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 12247 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ𝑀))
42, 3ax-mp 5 . . . . . . . . . . . . . . . . . 18 𝑀 ∈ (ℤ𝑀)
5 fdc.3 . . . . . . . . . . . . . . . . . 18 𝑍 = (ℤ𝑀)
64, 5eleqtrri 2912 . . . . . . . . . . . . . . . . 17 𝑀𝑍
7 eqid 2821 . . . . . . . . . . . . . . . . . . . . . 22 {⟨𝑀, 𝑎⟩} = {⟨𝑀, 𝑎⟩}
82elexi 3514 . . . . . . . . . . . . . . . . . . . . . . 23 𝑀 ∈ V
9 vex 3498 . . . . . . . . . . . . . . . . . . . . . . 23 𝑎 ∈ V
108, 9fsn 6890 . . . . . . . . . . . . . . . . . . . . . 22 ({⟨𝑀, 𝑎⟩}:{𝑀}⟶{𝑎} ↔ {⟨𝑀, 𝑎⟩} = {⟨𝑀, 𝑎⟩})
117, 10mpbir 232 . . . . . . . . . . . . . . . . . . . . 21 {⟨𝑀, 𝑎⟩}:{𝑀}⟶{𝑎}
12 snssi 4735 . . . . . . . . . . . . . . . . . . . . 21 (𝑎𝐴 → {𝑎} ⊆ 𝐴)
13 fss 6521 . . . . . . . . . . . . . . . . . . . . 21 (({⟨𝑀, 𝑎⟩}:{𝑀}⟶{𝑎} ∧ {𝑎} ⊆ 𝐴) → {⟨𝑀, 𝑎⟩}:{𝑀}⟶𝐴)
1411, 12, 13sylancr 587 . . . . . . . . . . . . . . . . . . . 20 (𝑎𝐴 → {⟨𝑀, 𝑎⟩}:{𝑀}⟶𝐴)
15 fzsn 12939 . . . . . . . . . . . . . . . . . . . . . 22 (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀})
162, 15ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (𝑀...𝑀) = {𝑀}
1716feq2i 6500 . . . . . . . . . . . . . . . . . . . 20 ({⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴 ↔ {⟨𝑀, 𝑎⟩}:{𝑀}⟶𝐴)
1814, 17sylibr 235 . . . . . . . . . . . . . . . . . . 19 (𝑎𝐴 → {⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴)
1918adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝑎𝐴𝜃) → {⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴)
208, 9fvsn 6936 . . . . . . . . . . . . . . . . . . 19 ({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎
2120a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝑎𝐴𝜃) → ({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎)
22 simpr 485 . . . . . . . . . . . . . . . . . 18 ((𝑎𝐴𝜃) → 𝜃)
23 snex 5323 . . . . . . . . . . . . . . . . . . 19 {⟨𝑀, 𝑎⟩} ∈ V
24 feq1 6489 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = {⟨𝑀, 𝑎⟩} → (𝑓:(𝑀...𝑀)⟶𝐴 ↔ {⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴))
25 fveq1 6663 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = {⟨𝑀, 𝑎⟩} → (𝑓𝑀) = ({⟨𝑀, 𝑎⟩}‘𝑀))
2625eqeq1d 2823 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = {⟨𝑀, 𝑎⟩} → ((𝑓𝑀) = 𝑎 ↔ ({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎))
2725, 20syl6eq 2872 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = {⟨𝑀, 𝑎⟩} → (𝑓𝑀) = 𝑎)
28 sbceq2a 3783 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓𝑀) = 𝑎 → ([(𝑓𝑀) / 𝑎]𝜃𝜃))
2927, 28syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = {⟨𝑀, 𝑎⟩} → ([(𝑓𝑀) / 𝑎]𝜃𝜃))
3026, 29anbi12d 630 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = {⟨𝑀, 𝑎⟩} → (((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃) ↔ (({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎𝜃)))
3124, 30anbi12d 630 . . . . . . . . . . . . . . . . . . 19 (𝑓 = {⟨𝑀, 𝑎⟩} → ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃)) ↔ ({⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴 ∧ (({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎𝜃))))
3223, 31spcev 3606 . . . . . . . . . . . . . . . . . 18 (({⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴 ∧ (({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎𝜃)) → ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃)))
3319, 21, 22, 32syl12anc 832 . . . . . . . . . . . . . . . . 17 ((𝑎𝐴𝜃) → ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃)))
34 oveq2 7153 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑀 → (𝑀...𝑛) = (𝑀...𝑀))
3534feq2d 6494 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑀 → (𝑓:(𝑀...𝑛)⟶𝐴𝑓:(𝑀...𝑀)⟶𝐴))
36 fvex 6677 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓𝑛) ∈ V
37 fdc.7 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 = (𝑓𝑛) → (𝜃𝜏))
3836, 37sbcie 3811 . . . . . . . . . . . . . . . . . . . . . . 23 ([(𝑓𝑛) / 𝑎]𝜃𝜏)
39 fveq2 6664 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑀 → (𝑓𝑛) = (𝑓𝑀))
4039sbceq1d 3776 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑀 → ([(𝑓𝑛) / 𝑎]𝜃[(𝑓𝑀) / 𝑎]𝜃))
4138, 40syl5bbr 286 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑀 → (𝜏[(𝑓𝑀) / 𝑎]𝜃))
4241anbi2d 628 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑀 → (((𝑓𝑀) = 𝑎𝜏) ↔ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃)))
43 oveq2 7153 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑀 → (𝑁...𝑛) = (𝑁...𝑀))
44 fdc.4 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑁 = (𝑀 + 1)
4544oveq1i 7155 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁...𝑀) = ((𝑀 + 1)...𝑀)
462zrei 11976 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑀 ∈ ℝ
4746ltp1i 11533 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑀 < (𝑀 + 1)
48 peano2z 12012 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑀 ∈ ℤ → (𝑀 + 1) ∈ ℤ)
492, 48ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑀 + 1) ∈ ℤ
50 fzn 12913 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑀 + 1) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 < (𝑀 + 1) ↔ ((𝑀 + 1)...𝑀) = ∅))
5149, 2, 50mp2an 688 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 < (𝑀 + 1) ↔ ((𝑀 + 1)...𝑀) = ∅)
5247, 51mpbi 231 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑀 + 1)...𝑀) = ∅
5345, 52eqtri 2844 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁...𝑀) = ∅
5443, 53syl6eq 2872 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑀 → (𝑁...𝑛) = ∅)
5554raleqdv 3416 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑀 → (∀𝑘 ∈ (𝑁...𝑛)𝜒 ↔ ∀𝑘 ∈ ∅ 𝜒))
5635, 42, 553anbi123d 1427 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑀 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃) ∧ ∀𝑘 ∈ ∅ 𝜒)))
57 ral0 4454 . . . . . . . . . . . . . . . . . . . . 21 𝑘 ∈ ∅ 𝜒
58 df-3an 1081 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃) ∧ ∀𝑘 ∈ ∅ 𝜒) ↔ ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃)) ∧ ∀𝑘 ∈ ∅ 𝜒))
5957, 58mpbiran2 706 . . . . . . . . . . . . . . . . . . . 20 ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃) ∧ ∀𝑘 ∈ ∅ 𝜒) ↔ (𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃)))
6056, 59syl6bb 288 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑀 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃))))
6160exbidv 1913 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑀 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃))))
6261rspcev 3622 . . . . . . . . . . . . . . . . 17 ((𝑀𝑍 ∧ ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓𝑀) / 𝑎]𝜃))) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
636, 33, 62sylancr 587 . . . . . . . . . . . . . . . 16 ((𝑎𝐴𝜃) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
6463adantll 710 . . . . . . . . . . . . . . 15 (((𝜂𝑎𝐴) ∧ 𝜃) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
6564a1d 25 . . . . . . . . . . . . . 14 (((𝜂𝑎𝐴) ∧ 𝜃) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
66 fdc.11 . . . . . . . . . . . . . . . . . . . . 21 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → 𝑏𝑅𝑎)
67 breq1 5061 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑 = 𝑏 → (𝑑𝑅𝑎𝑏𝑅𝑎))
6867rspcev 3622 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∧ 𝑏𝑅𝑎) → ∃𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎)
6968expcom 414 . . . . . . . . . . . . . . . . . . . . 21 (𝑏𝑅𝑎 → (𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎))
7066, 69syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎))
71 dfrex2 3239 . . . . . . . . . . . . . . . . . . . 20 (∃𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎 ↔ ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
7270, 71syl6ib 252 . . . . . . . . . . . . . . . . . . 19 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
7372con2d 136 . . . . . . . . . . . . . . . . . 18 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ¬ 𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
74 eldif 3945 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) ↔ (𝑏𝐴 ∧ ¬ 𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
7574simplbi2 501 . . . . . . . . . . . . . . . . . . . 20 (𝑏𝐴 → (¬ 𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → 𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))))
76 ssrab2 4055 . . . . . . . . . . . . . . . . . . . . . . 23 {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ⊆ 𝐴
77 dfss4 4234 . . . . . . . . . . . . . . . . . . . . . . 23 ({𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ⊆ 𝐴 ↔ (𝐴 ∖ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) = {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})
7876, 77mpbi 231 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴 ∖ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) = {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}
7978eleq2i 2904 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) ↔ 𝑏 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})
80 eqeq2 2833 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 = 𝑏 → ((𝑓𝑀) = 𝑐 ↔ (𝑓𝑀) = 𝑏))
8180anbi1d 629 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = 𝑏 → (((𝑓𝑀) = 𝑐𝜏) ↔ ((𝑓𝑀) = 𝑏𝜏)))
82813anbi2d 1432 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = 𝑏 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
8382exbidv 1913 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 = 𝑏 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
8483rexbidv 3297 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 = 𝑏 → (∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
8584elrab3 3680 . . . . . . . . . . . . . . . . . . . . 21 (𝑏𝐴 → (𝑏 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
8679, 85syl5bb 284 . . . . . . . . . . . . . . . . . . . 20 (𝑏𝐴 → (𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
8775, 86sylibd 240 . . . . . . . . . . . . . . . . . . 19 (𝑏𝐴 → (¬ 𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
8887ad2antll 725 . . . . . . . . . . . . . . . . . 18 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (¬ 𝑏 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
89 oveq2 7153 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑚 → (𝑀...𝑛) = (𝑀...𝑚))
9089feq2d 6494 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑚 → (𝑓:(𝑀...𝑛)⟶𝐴𝑓:(𝑀...𝑚)⟶𝐴))
91 fveq2 6664 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = 𝑚 → (𝑓𝑛) = (𝑓𝑚))
9291sbceq1d 3776 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑚 → ([(𝑓𝑛) / 𝑎]𝜃[(𝑓𝑚) / 𝑎]𝜃))
9338, 92syl5bbr 286 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑚 → (𝜏[(𝑓𝑚) / 𝑎]𝜃))
9493anbi2d 628 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑚 → (((𝑓𝑀) = 𝑏𝜏) ↔ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃)))
95 oveq2 7153 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑚 → (𝑁...𝑛) = (𝑁...𝑚))
9695raleqdv 3416 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑚 → (∀𝑘 ∈ (𝑁...𝑛)𝜒 ↔ ∀𝑘 ∈ (𝑁...𝑚)𝜒))
9790, 94, 963anbi123d 1427 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑚 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒)))
9897exbidv 1913 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑚 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒)))
9998cbvrexvw 3451 . . . . . . . . . . . . . . . . . . . 20 (∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑚𝑍𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒))
100 feq1 6489 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = 𝑔 → (𝑓:(𝑀...𝑚)⟶𝐴𝑔:(𝑀...𝑚)⟶𝐴))
101 fveq1 6663 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 = 𝑔 → (𝑓𝑀) = (𝑔𝑀))
102101eqeq1d 2823 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑔 → ((𝑓𝑀) = 𝑏 ↔ (𝑔𝑀) = 𝑏))
103 fveq1 6663 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 = 𝑔 → (𝑓𝑚) = (𝑔𝑚))
104103sbceq1d 3776 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑔 → ([(𝑓𝑚) / 𝑎]𝜃[(𝑔𝑚) / 𝑎]𝜃))
105102, 104anbi12d 630 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = 𝑔 → (((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ↔ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃)))
106 fvex 6677 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓‘(𝑘 − 1)) ∈ V
107 fdc.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑎 = (𝑓‘(𝑘 − 1)) → (𝜑𝜓))
108107sbcbidv 3826 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑎 = (𝑓‘(𝑘 − 1)) → ([(𝑓𝑘) / 𝑏]𝜑[(𝑓𝑘) / 𝑏]𝜓))
109106, 108sbcie 3811 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓𝑘) / 𝑏]𝜑[(𝑓𝑘) / 𝑏]𝜓)
110 fvex 6677 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓𝑘) ∈ V
111 fdc.6 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏 = (𝑓𝑘) → (𝜓𝜒))
112110, 111sbcie 3811 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ([(𝑓𝑘) / 𝑏]𝜓𝜒)
113109, 112bitri 276 . . . . . . . . . . . . . . . . . . . . . . . . 25 ([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓𝑘) / 𝑏]𝜑𝜒)
114 fveq1 6663 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 = 𝑔 → (𝑓‘(𝑘 − 1)) = (𝑔‘(𝑘 − 1)))
115 fveq1 6663 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓 = 𝑔 → (𝑓𝑘) = (𝑔𝑘))
116115sbceq1d 3776 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 = 𝑔 → ([(𝑓𝑘) / 𝑏]𝜑[(𝑔𝑘) / 𝑏]𝜑))
117114, 116sbceqbid 3778 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 = 𝑔 → ([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓𝑘) / 𝑏]𝜑[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑))
118113, 117syl5bbr 286 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑔 → (𝜒[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑))
119118ralbidv 3197 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = 𝑔 → (∀𝑘 ∈ (𝑁...𝑚)𝜒 ↔ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑))
120100, 105, 1193anbi123d 1427 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = 𝑔 → ((𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒) ↔ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)))
121120cbvexvw 2035 . . . . . . . . . . . . . . . . . . . . 21 (∃𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒) ↔ ∃𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑))
122121rexbii 3247 . . . . . . . . . . . . . . . . . . . 20 (∃𝑚𝑍𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏[(𝑓𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒) ↔ ∃𝑚𝑍𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑))
12399, 122bitri 276 . . . . . . . . . . . . . . . . . . 19 (∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑚𝑍𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑))
1245peano2uzs 12291 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚𝑍 → (𝑚 + 1) ∈ 𝑍)
125124ad2antlr 723 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → (𝑚 + 1) ∈ 𝑍)
126 sbceq2a 3783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑑 = 𝑏 → ([𝑑 / 𝑏]𝜑𝜑))
127126anbi1d 629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑑 = 𝑏 → (([𝑑 / 𝑏]𝜑𝑎𝐴) ↔ (𝜑𝑎𝐴)))
128127anbi1d 629 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑑 = 𝑏 → ((([𝑑 / 𝑏]𝜑𝑎𝐴) ∧ 𝑚𝑍) ↔ ((𝜑𝑎𝐴) ∧ 𝑚𝑍)))
129 eqeq2 2833 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑑 = 𝑏 → ((𝑔𝑀) = 𝑑 ↔ (𝑔𝑀) = 𝑏))
130129anbi1d 629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑑 = 𝑏 → (((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ↔ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃)))
1311303anbi2d 1432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑑 = 𝑏 → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) ↔ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)))
132131imbi1d 343 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑑 = 𝑏 → (((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)) ↔ ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))))
133128, 132imbi12d 346 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑑 = 𝑏 → (((([𝑑 / 𝑏]𝜑𝑎𝐴) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))) ↔ (((𝜑𝑎𝐴) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))))
134 sbceq2a 3783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑐 = 𝑎 → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑[𝑑 / 𝑏]𝜑))
135 eleq1 2900 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑐 = 𝑎 → (𝑐𝐴𝑎𝐴))
136134, 135anbi12d 630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 = 𝑎 → (([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ↔ ([𝑑 / 𝑏]𝜑𝑎𝐴)))
137136anbi1d 629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = 𝑎 → ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ↔ (([𝑑 / 𝑏]𝜑𝑎𝐴) ∧ 𝑚𝑍)))
138 eqeq2 2833 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑐 = 𝑎 → ((𝑓𝑀) = 𝑐 ↔ (𝑓𝑀) = 𝑎))
139138anbi1d 629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑐 = 𝑎 → (((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ↔ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃)))
1401393anbi2d 1432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑐 = 𝑎 → ((𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒) ↔ (𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
141140exbidv 1913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑐 = 𝑎 → (∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒) ↔ ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
142141imbi2d 342 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑐 = 𝑎 → (((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)) ↔ ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))))
143137, 142imbi12d 346 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑐 = 𝑎 → (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))) ↔ ((([𝑑 / 𝑏]𝜑𝑎𝐴) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))))
144 peano2uz 12290 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑚 ∈ (ℤ𝑀) → (𝑚 + 1) ∈ (ℤ𝑀))
145144, 5eleq2s 2931 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑚𝑍 → (𝑚 + 1) ∈ (ℤ𝑀))
146 elfzp12 12976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑚 + 1) ∈ (ℤ𝑀) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↔ (𝑥 = 𝑀𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)))))
147145, 146syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑚𝑍 → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↔ (𝑥 = 𝑀𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)))))
148147ad2antlr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↔ (𝑥 = 𝑀𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)))))
149 iftrue 4471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑥 = 𝑀 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = 𝑐)
150149eleq1d 2897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑥 = 𝑀 → (if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴𝑐𝐴))
151150biimprcd 251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑐𝐴 → (𝑥 = 𝑀 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
152151ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 = 𝑀 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
153 1re 10630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 1 ∈ ℝ
15446, 153readdcli 10645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑀 + 1) ∈ ℝ
15546, 154ltnlei 10750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑀 < (𝑀 + 1) ↔ ¬ (𝑀 + 1) ≤ 𝑀)
15647, 155mpbi 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ¬ (𝑀 + 1) ≤ 𝑀
157 eleq1 2900 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑥 = 𝑀 → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) ↔ 𝑀 ∈ ((𝑀 + 1)...(𝑚 + 1))))
158 elfzle1 12900 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑀 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑀 + 1) ≤ 𝑀)
159157, 158syl6bi 254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑥 = 𝑀 → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑀 + 1) ≤ 𝑀))
160159com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 = 𝑀 → (𝑀 + 1) ≤ 𝑀))
161156, 160mtoi 200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → ¬ 𝑥 = 𝑀)
162161adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑚𝑍𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → ¬ 𝑥 = 𝑀)
163162iffalsed 4476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑚𝑍𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = (𝑔‘(𝑥 − 1)))
164 elfzelz 12898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → 𝑥 ∈ ℤ)
165164adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → 𝑥 ∈ ℤ)
166 eluzelz 12242 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑚 ∈ (ℤ𝑀) → 𝑚 ∈ ℤ)
167166, 5eleq2s 2931 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑚𝑍𝑚 ∈ ℤ)
168167peano2zd 12079 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑚𝑍 → (𝑚 + 1) ∈ ℤ)
169 1z 12001 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 1 ∈ ℤ
170 fzsubel 12933 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ((((𝑀 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ (𝑥 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) ↔ (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))))
171170biimpd 230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((((𝑀 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ (𝑥 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))))
172169, 171mpanr2 700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ((((𝑀 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ 𝑥 ∈ ℤ) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))))
17349, 172mpanl1 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 𝑀 ∈ ℂ
180 ax-1cn 10584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 1 ∈ ℂ
181179, 180pncan3oi 10891 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑀 + 1) − 1) = 𝑀
182181a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑚𝑍 → ((𝑀 + 1) − 1) = 𝑀)
183167zcnd 12077 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑚𝑍𝑚 ∈ ℂ)
184 pncan 10881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑚 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑚 + 1) − 1) = 𝑚)
185183, 180, 184sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑚𝑍 → ((𝑚 + 1) − 1) = 𝑚)
186182, 185oveq12d 7163 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑚𝑍 → (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑀...𝑚))
187186adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑀...𝑚))
188178, 187eleqtrd 2915 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚𝑍𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑥 − 1) ∈ (𝑀...𝑚))
189 ffvelrn 6842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ (𝑥 − 1) ∈ (𝑀...𝑚)) → (𝑔‘(𝑥 − 1)) ∈ 𝐴)
190188, 189sylan2 592 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ (𝑚𝑍𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)))) → (𝑔‘(𝑥 − 1)) ∈ 𝐴)
191190anassrs 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (((𝑔:(𝑀...𝑚)⟶𝐴𝑚𝑍) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑔‘(𝑥 − 1)) ∈ 𝐴)
192191ancom1s 649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑚𝑍𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑔‘(𝑥 − 1)) ∈ 𝐴)
193163, 192eqeltrd 2913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑚𝑍𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴)
194193ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑚𝑍𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
195194adantll 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
196152, 195jaod 853 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → ((𝑥 = 𝑀𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
197148, 196sylbid 241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
198197ralrimiv 3181 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → ∀𝑥 ∈ (𝑀...(𝑚 + 1))if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴)
199 eqid 2821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))
200199fmpt 6867 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (∀𝑥 ∈ (𝑀...(𝑚 + 1))if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴 ↔ (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴)
201198, 200sylib 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝑐𝐴𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴)
202201adantlll 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴)
2032023ad2antr1 1180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴)
204 eluzfz1 12904 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑚 + 1) ∈ (ℤ𝑀) → 𝑀 ∈ (𝑀...(𝑚 + 1)))
205144, 204syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑚 ∈ (ℤ𝑀) → 𝑀 ∈ (𝑀...(𝑚 + 1)))
206205, 5eleq2s 2931 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑚𝑍𝑀 ∈ (𝑀...(𝑚 + 1)))
207 vex 3498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑐 ∈ V
208149, 199, 207fvmpt 6762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑀 ∈ (𝑀...(𝑚 + 1)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐)
209206, 208syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑚𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐)
210209ad2antlr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐)
211 eluzfz2 12905 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑚 + 1) ∈ (ℤ𝑀) → (𝑚 + 1) ∈ (𝑀...(𝑚 + 1)))
212144, 211syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑚 ∈ (ℤ𝑀) → (𝑚 + 1) ∈ (𝑀...(𝑚 + 1)))
213212, 5eleq2s 2931 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑚𝑍 → (𝑚 + 1) ∈ (𝑀...(𝑚 + 1)))
214 eqeq1 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑥 = (𝑚 + 1) → (𝑥 = 𝑀 ↔ (𝑚 + 1) = 𝑀))
215 fvoveq1 7168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑥 = (𝑚 + 1) → (𝑔‘(𝑥 − 1)) = (𝑔‘((𝑚 + 1) − 1)))
216214, 215ifbieq2d 4490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑥 = (𝑚 + 1) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1))))
217 fvex 6677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑔‘((𝑚 + 1) − 1)) ∈ V
218207, 217ifex 4513 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1))) ∈ V
219216, 199, 218fvmpt 6762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑚 ∈ (ℤ𝑀) → 𝑀𝑚)
222221, 5eleq2s 2931 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑚𝑍𝑀𝑚)
223 zleltp1 12022 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑀𝑚𝑀 < (𝑚 + 1)))
2242, 167, 223sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑚𝑍 → (𝑀𝑚𝑀 < (𝑚 + 1)))
225222, 224mpbid 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑚𝑍𝑀 < (𝑚 + 1))
226 ltne 10726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑀 ∈ ℝ ∧ 𝑀 < (𝑚 + 1)) → (𝑚 + 1) ≠ 𝑀)
22746, 225, 226sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑚𝑍 → (𝑚 + 1) ≠ 𝑀)
228227neneqd 3021 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑚𝑍 → ¬ (𝑚 + 1) = 𝑀)
229228iffalsed 4476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑚𝑍 → if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1))) = (𝑔‘((𝑚 + 1) − 1)))
230185fveq2d 6668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑚𝑍 → (𝑔‘((𝑚 + 1) − 1)) = (𝑔𝑚))
231220, 229, 2303eqtrd 2860 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑚𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) = (𝑔𝑚))
232231sbceq1d 3776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑚𝑍 → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃[(𝑔𝑚) / 𝑎]𝜃))
233232biimpar 478 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑚𝑍[(𝑔𝑚) / 𝑎]𝜃) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃)
234233ad2ant2l 742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃)) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃)
2352343ad2antr2 1181 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃)
236 eluzp1p1 12259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑚 ∈ (ℤ𝑀) → (𝑚 + 1) ∈ (ℤ‘(𝑀 + 1)))
237236, 5eleq2s 2931 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑚𝑍 → (𝑚 + 1) ∈ (ℤ‘(𝑀 + 1)))
23844fveq2i 6667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (ℤ𝑁) = (ℤ‘(𝑀 + 1))
239237, 238eleqtrrdi 2924 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑚𝑍 → (𝑚 + 1) ∈ (ℤ𝑁))
240 elfzp12 12976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑚 + 1) ∈ (ℤ𝑁) → (𝑗 ∈ (𝑁...(𝑚 + 1)) ↔ (𝑗 = 𝑁𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)))))
241239, 240syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝑚𝑍 → (𝑗 ∈ (𝑁...(𝑚 + 1)) ↔ (𝑗 = 𝑁𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)))))
242241biimpa 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((𝑚𝑍𝑗 ∈ (𝑁...(𝑚 + 1))) → (𝑗 = 𝑁𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))))
243242adantll 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ 𝑗 ∈ (𝑁...(𝑚 + 1))) → (𝑗 = 𝑁𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))))
244243adantlr 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) ∧ 𝑗 ∈ (𝑁...(𝑚 + 1))) → (𝑗 = 𝑁𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))))
245 oveq1 7152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑗 = 𝑁 → (𝑗 − 1) = (𝑁 − 1))
24644oveq1i 7155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑁 − 1) = ((𝑀 + 1) − 1)
247246, 181eqtri 2844 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑁 − 1) = 𝑀
248245, 247syl6eq 2872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑗 = 𝑁 → (𝑗 − 1) = 𝑀)
249248fveq2d 6668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑗 = 𝑁 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀))
250249ad2antll 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀))
251209adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐)
252250, 251eqtrd 2856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = 𝑐)
25344eqeq2i 2834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑗 = 𝑁𝑗 = (𝑀 + 1))
254 fveq2 6664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑗 = (𝑀 + 1) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)))
255253, 254sylbi 218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑗 = 𝑁 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)))
256255ad2antll 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)))
25746, 154, 47ltleii 10752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 𝑀 ≤ (𝑀 + 1)
258 eluz2 12238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((𝑀 + 1) ∈ (ℤ𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑀 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑀 + 1)))
2592, 49, 257, 258mpbir3an 1333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑀 + 1) ∈ (ℤ𝑀)
260 fzss1 12936 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ((𝑀 + 1) ∈ (ℤ𝑀) → ((𝑀 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1)))
261259, 260ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((𝑀 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1))
262 eluzfz1 12904 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (𝑚 ∈ (ℤ𝑀) → 𝑀 ∈ (𝑀...𝑚))
263262, 5eleq2s 2931 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑚𝑍𝑀 ∈ (𝑀...𝑚))
264 fzaddel 12931 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (((𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑀 ∈ (𝑀...𝑚) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1))))
2652, 169, 264mpanr12 701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑀 ∈ (𝑀...𝑚) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1))))
2662, 167, 265sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑚𝑍 → (𝑀 ∈ (𝑀...𝑚) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1))))
267263, 266mpbid 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑚𝑍 → (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1)))
268261, 267sseldi 3964 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑚𝑍 → (𝑀 + 1) ∈ (𝑀...(𝑚 + 1)))
269 eqeq1 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑥 = (𝑀 + 1) → (𝑥 = 𝑀 ↔ (𝑀 + 1) = 𝑀))
270 oveq1 7152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (𝑥 = (𝑀 + 1) → (𝑥 − 1) = ((𝑀 + 1) − 1))
271270, 181syl6eq 2872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (𝑥 = (𝑀 + 1) → (𝑥 − 1) = 𝑀)
272271fveq2d 6668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑥 = (𝑀 + 1) → (𝑔‘(𝑥 − 1)) = (𝑔𝑀))
273269, 272ifbieq2d 4490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑥 = (𝑀 + 1) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if((𝑀 + 1) = 𝑀, 𝑐, (𝑔𝑀)))
274 fvex 6677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑔𝑀) ∈ V
275207, 274ifex 4513 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 if((𝑀 + 1) = 𝑀, 𝑐, (𝑔𝑀)) ∈ V
276273, 199, 275fvmpt 6762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑀 + 1) ∈ (𝑀...(𝑚 + 1)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)) = if((𝑀 + 1) = 𝑀, 𝑐, (𝑔𝑀)))
277268, 276syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑚𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)) = if((𝑀 + 1) = 𝑀, 𝑐, (𝑔𝑀)))
27846, 47gtneii 10741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑀 + 1) ≠ 𝑀
279 ifnefalse 4477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑀 + 1) ≠ 𝑀 → if((𝑀 + 1) = 𝑀, 𝑐, (𝑔𝑀)) = (𝑔𝑀))
280278, 279ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 if((𝑀 + 1) = 𝑀, 𝑐, (𝑔𝑀)) = (𝑔𝑀)
281277, 280syl6eq 2872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑚𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)) = (𝑔𝑀))
282281adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)) = (𝑔𝑀))
283 simprl 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → (𝑔𝑀) = 𝑑)
284256, 282, 2833eqtrd 2860 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = 𝑑)
285284sbceq1d 3776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑𝑗 = 𝑁)) → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑[𝑑 / 𝑏]𝜑))
286252, 285sbceqbid 3778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) ∧ 𝑗 = 𝑁) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
291 elfzelz 12898 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → 𝑗 ∈ ℤ)
292291adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → 𝑗 ∈ ℤ)
29344, 49eqeltri 2909 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 𝑁 ∈ ℤ
294 peano2z 12012 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑁 ∈ ℤ → (𝑁 + 1) ∈ ℤ)
295293, 294ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑁 + 1) ∈ ℤ
296 fzsubel 12933 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((((𝑁 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ (𝑗 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) ↔ (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1))))
297296biimpd 230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ((((𝑁 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ (𝑗 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1))))
298169, 297mpanr2 700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 𝑁 ∈ ℝ
305304recni 10644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 𝑁 ∈ ℂ
306305, 180pncan3oi 10891 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑁 + 1) − 1) = 𝑁
307306a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑚𝑍 → ((𝑁 + 1) − 1) = 𝑁)
308307, 185oveq12d 7163 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑚𝑍 → (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑁...𝑚))
309308adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑁...𝑚))
310303, 309eleqtrd 2915 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 − 1) ∈ (𝑁...𝑚))
311 fvoveq1 7168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑘 = (𝑗 − 1) → (𝑔‘(𝑘 − 1)) = (𝑔‘((𝑗 − 1) − 1)))
312 fveq2 6664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑘 = (𝑗 − 1) → (𝑔𝑘) = (𝑔‘(𝑗 − 1)))
313312sbceq1d 3776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (𝑘 = (𝑗 − 1) → ([(𝑔𝑘) / 𝑏]𝜑[(𝑔‘(𝑗 − 1)) / 𝑏]𝜑))
314311, 313sbceqbid 3778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (𝑘 = (𝑗 − 1) → ([(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑[(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑))
315314rspcva 3620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑗 − 1) ∈ (𝑁...𝑚) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → [(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑)
316310, 315sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → [(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑)
31744, 259eqeltri 2909 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 𝑁 ∈ (ℤ𝑀)
318 fzss1 12936 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑁 ∈ (ℤ𝑀) → (𝑁...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1)))
319317, 318ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑁...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1))
320 fzssp1 12940 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑁...𝑚) ⊆ (𝑁...(𝑚 + 1))
321320, 310sseldi 3964 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 − 1) ∈ (𝑁...(𝑚 + 1)))
322319, 321sseldi 3964 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 − 1) ∈ (𝑀...(𝑚 + 1)))
323 eqeq1 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑥 = (𝑗 − 1) → (𝑥 = 𝑀 ↔ (𝑗 − 1) = 𝑀))
324 fvoveq1 7168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑥 = (𝑗 − 1) → (𝑔‘(𝑥 − 1)) = (𝑔‘((𝑗 − 1) − 1)))
325323, 324ifbieq2d 4490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑥 = (𝑗 − 1) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1))))
326 fvex 6677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑔‘((𝑗 − 1) − 1)) ∈ V
327207, 326ifex 4513 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1))) ∈ V
328325, 199, 327fvmpt 6762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11533 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑀 + 1) < ((𝑀 + 1) + 1)
33144oveq1i 7155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑁 + 1) = ((𝑀 + 1) + 1)
332330, 331breqtrri 5085 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑀 + 1) < (𝑁 + 1)
333304, 153readdcli 10645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑁 + 1) ∈ ℝ
334154, 333ltnlei 10750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((𝑀 + 1) < (𝑁 + 1) ↔ ¬ (𝑁 + 1) ≤ (𝑀 + 1))
335332, 334mpbi 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ¬ (𝑁 + 1) ≤ (𝑀 + 1)
336291zcnd 12077 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → 𝑗 ∈ ℂ)
337 subadd 10878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((𝑗 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑀 ∈ ℂ) → ((𝑗 − 1) = 𝑀 ↔ (1 + 𝑀) = 𝑗))
338180, 179, 337mp3an23 1444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑗 ∈ ℂ → ((𝑗 − 1) = 𝑀 ↔ (1 + 𝑀) = 𝑗))
339336, 338syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ((𝑗 − 1) = 𝑀 ↔ (1 + 𝑀) = 𝑗))
340 eqcom 2828 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((1 + 𝑀) = 𝑗𝑗 = (1 + 𝑀))
341180, 179addcomi 10820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (1 + 𝑀) = (𝑀 + 1)
342341eqeq2i 2834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (𝑗 = (1 + 𝑀) ↔ 𝑗 = (𝑀 + 1))
343340, 342bitri 276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ((1 + 𝑀) = 𝑗𝑗 = (𝑀 + 1))
344 eleq1 2900 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 (𝑗 = (𝑀 + 1) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) ↔ (𝑀 + 1) ∈ ((𝑁 + 1)...(𝑚 + 1))))
345 elfzle1 12900 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ((𝑀 + 1) ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑁 + 1) ≤ (𝑀 + 1))
346344, 345syl6bi 254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (𝑗 = (𝑀 + 1) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑁 + 1) ≤ (𝑀 + 1)))
347346com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 = (𝑀 + 1) → (𝑁 + 1) ≤ (𝑀 + 1)))
348343, 347syl5bi 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ((1 + 𝑀) = 𝑗 → (𝑁 + 1) ≤ (𝑀 + 1)))
349339, 348sylbid 241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ((𝑗 − 1) = 𝑀 → (𝑁 + 1) ≤ (𝑀 + 1)))
350335, 349mtoi 200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ¬ (𝑗 − 1) = 𝑀)
351350adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ¬ (𝑗 − 1) = 𝑀)
352351iffalsed 4476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1))) = (𝑔‘((𝑗 − 1) − 1)))
353329, 352eqtrd 2856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = (𝑔‘((𝑗 − 1) − 1)))
354 peano2uz 12290 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑁 ∈ (ℤ𝑀) → (𝑁 + 1) ∈ (ℤ𝑀))
355 fzss1 12936 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ((𝑁 + 1) ∈ (ℤ𝑀) → ((𝑁 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1)))
356317, 354, 355mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑁 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1))
357 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)))
358356, 357sseldi 3964 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → 𝑗 ∈ (𝑀...(𝑚 + 1)))
359 eqeq1 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑥 = 𝑗 → (𝑥 = 𝑀𝑗 = 𝑀))
360 fvoveq1 7168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑥 = 𝑗 → (𝑔‘(𝑥 − 1)) = (𝑔‘(𝑗 − 1)))
361359, 360ifbieq2d 4490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑥 = 𝑗 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))))
362 fvex 6677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑔‘(𝑗 − 1)) ∈ V
363207, 362ifex 4513 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))) ∈ V
364361, 199, 363fvmpt 6762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑗 ∈ (𝑀...(𝑚 + 1)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))))
365358, 364syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))))
36647, 44breqtrri 5085 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 𝑀 < 𝑁
367304ltp1i 11533 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 𝑁 < (𝑁 + 1)
36846, 304, 333lttri 10755 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ((𝑀 < 𝑁𝑁 < (𝑁 + 1)) → 𝑀 < (𝑁 + 1))
369366, 367, 368mp2an 688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 𝑀 < (𝑁 + 1)
37046, 333ltnlei 10750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑀 < (𝑁 + 1) ↔ ¬ (𝑁 + 1) ≤ 𝑀)
371369, 370mpbi 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ¬ (𝑁 + 1) ≤ 𝑀
372 eleq1 2900 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (𝑗 = 𝑀 → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) ↔ 𝑀 ∈ ((𝑁 + 1)...(𝑚 + 1))))
373 elfzle1 12900 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 (𝑀 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑁 + 1) ≤ 𝑀)
374372, 373syl6bi 254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 (𝑗 = 𝑀 → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑁 + 1) ≤ 𝑀))
375374com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 = 𝑀 → (𝑁 + 1) ≤ 𝑀))
376371, 375mtoi 200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ¬ 𝑗 = 𝑀)
377376adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ¬ 𝑗 = 𝑀)
378377iffalsed 4476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))) = (𝑔‘(𝑗 − 1)))
379365, 378eqtrd 2856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = (𝑔‘(𝑗 − 1)))
380379sbceq1d 3776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ((𝑚𝑍𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑[(𝑔‘(𝑗 − 1)) / 𝑏]𝜑))
381353, 380sbceqbid 3778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (((𝑚𝑍 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
385384adantlrl 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (((𝑚𝑍 ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
386385adantlll 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
387290, 386jaodan 951 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∀𝑗 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
390 fvoveq1 7168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 = 𝑘 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)))
391 fveq2 6664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑗 = 𝑘 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘))
392391sbceq1d 3776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑗 = 𝑘 → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
393390, 392sbceqbid 3778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑗 = 𝑘 → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
394393cbvralvw 3450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (∀𝑗 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑 ↔ ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
395389, 394sylib 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
396395adantllr 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ ((𝑔𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
397396adantrlr 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ (((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
3983973adantr1 1161 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
399 ovex 7178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑀...(𝑚 + 1)) ∈ V
400399mptex 6978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) ∈ V
401 feq1 6489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ↔ (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴))
402 fveq1 6663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓𝑀) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀))
403402eqeq1d 2823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ((𝑓𝑀) = 𝑐 ↔ ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐))
404 fveq1 6663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓‘(𝑚 + 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)))
405404sbceq1d 3776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ([(𝑓‘(𝑚 + 1)) / 𝑎]𝜃[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃))
406403, 405anbi12d 630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ↔ (((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃)))
407 fveq1 6663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓‘(𝑘 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)))
408 fveq1 6663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓𝑘) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘))
409408sbceq1d 3776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ([(𝑓𝑘) / 𝑏]𝜑[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
410407, 409sbceqbid 3778 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓𝑘) / 𝑏]𝜑[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
411113, 410syl5bbr 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝜒[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
412411ralbidv 3197 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒 ↔ ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
413401, 406, 4123anbi123d 1427 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3606 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))
416415ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑𝑐𝐴) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑐[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
417143, 416chvarvv 1996 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((([𝑑 / 𝑏]𝜑𝑎𝐴) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑑[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
418133, 417chvarvv 1996 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑎𝐴) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
419418adantlrr 717 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
420419adantlll 714 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
421420imp 407 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))
422 oveq2 7153 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = (𝑚 + 1) → (𝑀...𝑛) = (𝑀...(𝑚 + 1)))
423422feq2d 6494 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = (𝑚 + 1) → (𝑓:(𝑀...𝑛)⟶𝐴𝑓:(𝑀...(𝑚 + 1))⟶𝐴))
424 fveq2 6664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = (𝑚 + 1) → (𝑓𝑛) = (𝑓‘(𝑚 + 1)))
425424sbceq1d 3776 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = (𝑚 + 1) → ([(𝑓𝑛) / 𝑎]𝜃[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃))
42638, 425syl5bbr 286 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = (𝑚 + 1) → (𝜏[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃))
427426anbi2d 628 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = (𝑚 + 1) → (((𝑓𝑀) = 𝑎𝜏) ↔ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃)))
428 oveq2 7153 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = (𝑚 + 1) → (𝑁...𝑛) = (𝑁...(𝑚 + 1)))
429428raleqdv 3416 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = (𝑚 + 1) → (∀𝑘 ∈ (𝑁...𝑛)𝜒 ↔ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))
430423, 427, 4293anbi123d 1427 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = (𝑚 + 1) → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
431430exbidv 1913 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = (𝑚 + 1) → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
432431rspcev 3622 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑚 + 1) ∈ 𝑍 ∧ ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓𝑀) = 𝑎[(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
433125, 421, 432syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑)) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
434433ex 413 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
435434exlimdv 1925 . . . . . . . . . . . . . . . . . . . 20 ((((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑚𝑍) → (∃𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
436435rexlimdva 3284 . . . . . . . . . . . . . . . . . . 19 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (∃𝑚𝑍𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔𝑀) = 𝑏[(𝑔𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔𝑘) / 𝑏]𝜑) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
437123, 436syl5bi 243 . . . . . . . . . . . . . . . . . 18 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑏𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
43873, 88, 4373syld 60 . . . . . . . . . . . . . . . . 17 (((𝜂𝜑) ∧ (𝑎𝐴𝑏𝐴)) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
439438an42s 657 . . . . . . . . . . . . . . . 16 (((𝜂𝑎𝐴) ∧ (𝑏𝐴𝜑)) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
440439rexlimdvaa 3285 . . . . . . . . . . . . . . 15 ((𝜂𝑎𝐴) → (∃𝑏𝐴 𝜑 → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))))
441440imp 407 . . . . . . . . . . . . . 14 (((𝜂𝑎𝐴) ∧ ∃𝑏𝐴 𝜑) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
442 fdc.10 . . . . . . . . . . . . . 14 ((𝜂𝑎𝐴) → (𝜃 ∨ ∃𝑏𝐴 𝜑))
44365, 441, 442mpjaodan 952 . . . . . . . . . . . . 13 ((𝜂𝑎𝐴) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
444138anbi1d 629 . . . . . . . . . . . . . . . . . 18 (𝑐 = 𝑎 → (((𝑓𝑀) = 𝑐𝜏) ↔ ((𝑓𝑀) = 𝑎𝜏)))
4454443anbi2d 1432 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝑎 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
446445exbidv 1913 . . . . . . . . . . . . . . . 16 (𝑐 = 𝑎 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
447446rexbidv 3297 . . . . . . . . . . . . . . 15 (𝑐 = 𝑎 → (∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
448447elrab3 3680 . . . . . . . . . . . . . 14 (𝑎𝐴 → (𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
449448adantl 482 . . . . . . . . . . . . 13 ((𝜂𝑎𝐴) → (𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑎𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
450443, 449sylibrd 260 . . . . . . . . . . . 12 ((𝜂𝑎𝐴) → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
451450ex 413 . . . . . . . . . . 11 (𝜂 → (𝑎𝐴 → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
452451com23 86 . . . . . . . . . 10 (𝜂 → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → (𝑎𝐴𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
453 eldif 3945 . . . . . . . . . . . 12 (𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ↔ (𝑎𝐴 ∧ ¬ 𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
454453notbii 321 . . . . . . . . . . 11 𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ↔ ¬ (𝑎𝐴 ∧ ¬ 𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
455 iman 402 . . . . . . . . . . 11 ((𝑎𝐴𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ↔ ¬ (𝑎𝐴 ∧ ¬ 𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
456454, 455bitr4i 279 . . . . . . . . . 10 𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ↔ (𝑎𝐴𝑎 ∈ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
457452, 456syl6ibr 253 . . . . . . . . 9 (𝜂 → (∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ¬ 𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
458457con2d 136 . . . . . . . 8 (𝜂 → (𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
459458imp 407 . . . . . . 7 ((𝜂𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) → ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
460459nrexdv 3270 . . . . . 6 (𝜂 → ¬ ∃𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
461 df-ne 3017 . . . . . . 7 ((𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅ ↔ ¬ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅)
462 fdc.9 . . . . . . . 8 (𝜂𝑅 Fr 𝐴)
463 difss 4107 . . . . . . . 8 (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴
464 fdc.1 . . . . . . . . . . 11 𝐴 ∈ V
465 difexg 5223 . . . . . . . . . . 11 (𝐴 ∈ V → (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∈ V)
466464, 465ax-mp 5 . . . . . . . . . 10 (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∈ V
467 fri 5511 . . . . . . . . . 10 ((((𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∈ V ∧ 𝑅 Fr 𝐴) ∧ ((𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴 ∧ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅)) → ∃𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
468466, 467mpanl1 696 . . . . . . . . 9 ((𝑅 Fr 𝐴 ∧ ((𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴 ∧ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅)) → ∃𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
469468expr 457 . . . . . . . 8 ((𝑅 Fr 𝐴 ∧ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴) → ((𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅ → ∃𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
470462, 463, 469sylancl 586 . . . . . . 7 (𝜂 → ((𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅ → ∃𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
471461, 470syl5bir 244 . . . . . 6 (𝜂 → (¬ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅ → ∃𝑎 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
472460, 471mt3d 150 . . . . 5 (𝜂 → (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅)
473 ssdif0 4322 . . . . 5 (𝐴 ⊆ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ (𝐴 ∖ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅)
474472, 473sylibr 235 . . . 4 (𝜂𝐴 ⊆ {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})
47576a1i 11 . . . 4 (𝜂 → {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ⊆ 𝐴)
476474, 475eqssd 3983 . . 3 (𝜂𝐴 = {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})
477 rabid2 3382 . . 3 (𝐴 = {𝑐𝐴 ∣ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∀𝑐𝐴𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
478476, 477sylib 219 . 2 (𝜂 → ∀𝑐𝐴𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
479 eqeq2 2833 . . . . . . 7 (𝑐 = 𝐶 → ((𝑓𝑀) = 𝑐 ↔ (𝑓𝑀) = 𝐶))
480479anbi1d 629 . . . . . 6 (𝑐 = 𝐶 → (((𝑓𝑀) = 𝑐𝜏) ↔ ((𝑓𝑀) = 𝐶𝜏)))
4814803anbi2d 1432 . . . . 5 (𝑐 = 𝐶 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝐶𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
482481exbidv 1913 . . . 4 (𝑐 = 𝐶 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝐶𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
483482rexbidv 3297 . . 3 (𝑐 = 𝐶 → (∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝐶𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
484483rspcva 3620 . 2 ((𝐶𝐴 ∧ ∀𝑐𝐴𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝑐𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)) → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝐶𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
4851, 478, 484syl2anc 584 1 (𝜂 → ∃𝑛𝑍𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓𝑀) = 𝐶𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 841  w3a 1079   = wceq 1528  wex 1771  wcel 2105  wne 3016  wral 3138  wrex 3139  {crab 3142  Vcvv 3495  [wsbc 3771  cdif 3932  wss 3935  c0 4290  ifcif 4465  {csn 4559  cop 4565   class class class wbr 5058  cmpt 5138   Fr wfr 5505  wf 6345  cfv 6349  (class class class)co 7145  cc 10524  cr 10525  1c1 10527   + caddc 10529   < clt 10664  cle 10665  cmin 10859  cz 11970  cuz 12232  ...cfz 12882
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4833  df-iun 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7569  df-1st 7680  df-2nd 7681  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-er 8279  df-en 8499  df-dom 8500  df-sdom 8501  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11628  df-n0 11887  df-z 11971  df-uz 12233  df-fz 12883
This theorem is referenced by:  fdc1  34904
  Copyright terms: Public domain W3C validator