Metamath Proof Explorer


Theorem fdc

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)

Ref Expression
Hypotheses 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 fdc ( 𝜂 → ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝐶𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) )

Proof

Step Hyp Ref Expression
1 fdc.1 𝐴 ∈ V
2 fdc.2 𝑀 ∈ ℤ
3 fdc.3 𝑍 = ( ℤ𝑀 )
4 fdc.4 𝑁 = ( 𝑀 + 1 )
5 fdc.5 ( 𝑎 = ( 𝑓 ‘ ( 𝑘 − 1 ) ) → ( 𝜑𝜓 ) )
6 fdc.6 ( 𝑏 = ( 𝑓𝑘 ) → ( 𝜓𝜒 ) )
7 fdc.7 ( 𝑎 = ( 𝑓𝑛 ) → ( 𝜃𝜏 ) )
8 fdc.8 ( 𝜂𝐶𝐴 )
9 fdc.9 ( 𝜂𝑅 Fr 𝐴 )
10 fdc.10 ( ( 𝜂𝑎𝐴 ) → ( 𝜃 ∨ ∃ 𝑏𝐴 𝜑 ) )
11 fdc.11 ( ( ( 𝜂𝜑 ) ∧ ( 𝑎𝐴𝑏𝐴 ) ) → 𝑏 𝑅 𝑎 )
12 uzid ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ𝑀 ) )
13 2 12 ax-mp 𝑀 ∈ ( ℤ𝑀 )
14 13 3 eleqtrri 𝑀𝑍
15 eqid { ⟨ 𝑀 , 𝑎 ⟩ } = { ⟨ 𝑀 , 𝑎 ⟩ }
16 2 elexi 𝑀 ∈ V
17 vex 𝑎 ∈ V
18 16 17 fsn ( { ⟨ 𝑀 , 𝑎 ⟩ } : { 𝑀 } ⟶ { 𝑎 } ↔ { ⟨ 𝑀 , 𝑎 ⟩ } = { ⟨ 𝑀 , 𝑎 ⟩ } )
19 15 18 mpbir { ⟨ 𝑀 , 𝑎 ⟩ } : { 𝑀 } ⟶ { 𝑎 }
20 snssi ( 𝑎𝐴 → { 𝑎 } ⊆ 𝐴 )
21 fss ( ( { ⟨ 𝑀 , 𝑎 ⟩ } : { 𝑀 } ⟶ { 𝑎 } ∧ { 𝑎 } ⊆ 𝐴 ) → { ⟨ 𝑀 , 𝑎 ⟩ } : { 𝑀 } ⟶ 𝐴 )
22 19 20 21 sylancr ( 𝑎𝐴 → { ⟨ 𝑀 , 𝑎 ⟩ } : { 𝑀 } ⟶ 𝐴 )
23 fzsn ( 𝑀 ∈ ℤ → ( 𝑀 ... 𝑀 ) = { 𝑀 } )
24 2 23 ax-mp ( 𝑀 ... 𝑀 ) = { 𝑀 }
25 24 feq2i ( { ⟨ 𝑀 , 𝑎 ⟩ } : ( 𝑀 ... 𝑀 ) ⟶ 𝐴 ↔ { ⟨ 𝑀 , 𝑎 ⟩ } : { 𝑀 } ⟶ 𝐴 )
26 22 25 sylibr ( 𝑎𝐴 → { ⟨ 𝑀 , 𝑎 ⟩ } : ( 𝑀 ... 𝑀 ) ⟶ 𝐴 )
27 26 adantr ( ( 𝑎𝐴𝜃 ) → { ⟨ 𝑀 , 𝑎 ⟩ } : ( 𝑀 ... 𝑀 ) ⟶ 𝐴 )
28 16 17 fvsn ( { ⟨ 𝑀 , 𝑎 ⟩ } ‘ 𝑀 ) = 𝑎
29 28 a1i ( ( 𝑎𝐴𝜃 ) → ( { ⟨ 𝑀 , 𝑎 ⟩ } ‘ 𝑀 ) = 𝑎 )
30 simpr ( ( 𝑎𝐴𝜃 ) → 𝜃 )
31 snex { ⟨ 𝑀 , 𝑎 ⟩ } ∈ V
32 feq1 ( 𝑓 = { ⟨ 𝑀 , 𝑎 ⟩ } → ( 𝑓 : ( 𝑀 ... 𝑀 ) ⟶ 𝐴 ↔ { ⟨ 𝑀 , 𝑎 ⟩ } : ( 𝑀 ... 𝑀 ) ⟶ 𝐴 ) )
33 fveq1 ( 𝑓 = { ⟨ 𝑀 , 𝑎 ⟩ } → ( 𝑓𝑀 ) = ( { ⟨ 𝑀 , 𝑎 ⟩ } ‘ 𝑀 ) )
34 33 eqeq1d ( 𝑓 = { ⟨ 𝑀 , 𝑎 ⟩ } → ( ( 𝑓𝑀 ) = 𝑎 ↔ ( { ⟨ 𝑀 , 𝑎 ⟩ } ‘ 𝑀 ) = 𝑎 ) )
35 33 28 eqtrdi ( 𝑓 = { ⟨ 𝑀 , 𝑎 ⟩ } → ( 𝑓𝑀 ) = 𝑎 )
36 sbceq2a ( ( 𝑓𝑀 ) = 𝑎 → ( [ ( 𝑓𝑀 ) / 𝑎 ] 𝜃𝜃 ) )
37 35 36 syl ( 𝑓 = { ⟨ 𝑀 , 𝑎 ⟩ } → ( [ ( 𝑓𝑀 ) / 𝑎 ] 𝜃𝜃 ) )
38 34 37 anbi12d ( 𝑓 = { ⟨ 𝑀 , 𝑎 ⟩ } → ( ( ( 𝑓𝑀 ) = 𝑎[ ( 𝑓𝑀 ) / 𝑎 ] 𝜃 ) ↔ ( ( { ⟨ 𝑀 , 𝑎 ⟩ } ‘ 𝑀 ) = 𝑎𝜃 ) ) )
39 32 38 anbi12d ( 𝑓 = { ⟨ 𝑀 , 𝑎 ⟩ } → ( ( 𝑓 : ( 𝑀 ... 𝑀 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎[ ( 𝑓𝑀 ) / 𝑎 ] 𝜃 ) ) ↔ ( { ⟨ 𝑀 , 𝑎 ⟩ } : ( 𝑀 ... 𝑀 ) ⟶ 𝐴 ∧ ( ( { ⟨ 𝑀 , 𝑎 ⟩ } ‘ 𝑀 ) = 𝑎𝜃 ) ) ) )
40 31 39 spcev ( ( { ⟨ 𝑀 , 𝑎 ⟩ } : ( 𝑀 ... 𝑀 ) ⟶ 𝐴 ∧ ( ( { ⟨ 𝑀 , 𝑎 ⟩ } ‘ 𝑀 ) = 𝑎𝜃 ) ) → ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑀 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎[ ( 𝑓𝑀 ) / 𝑎 ] 𝜃 ) ) )
41 27 29 30 40 syl12anc ( ( 𝑎𝐴𝜃 ) → ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑀 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎[ ( 𝑓𝑀 ) / 𝑎 ] 𝜃 ) ) )
42 oveq2 ( 𝑛 = 𝑀 → ( 𝑀 ... 𝑛 ) = ( 𝑀 ... 𝑀 ) )
43 42 feq2d ( 𝑛 = 𝑀 → ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴𝑓 : ( 𝑀 ... 𝑀 ) ⟶ 𝐴 ) )
44 fvex ( 𝑓𝑛 ) ∈ V
45 44 7 sbcie ( [ ( 𝑓𝑛 ) / 𝑎 ] 𝜃𝜏 )
46 fveq2 ( 𝑛 = 𝑀 → ( 𝑓𝑛 ) = ( 𝑓𝑀 ) )
47 46 sbceq1d ( 𝑛 = 𝑀 → ( [ ( 𝑓𝑛 ) / 𝑎 ] 𝜃[ ( 𝑓𝑀 ) / 𝑎 ] 𝜃 ) )
48 45 47 bitr3id ( 𝑛 = 𝑀 → ( 𝜏[ ( 𝑓𝑀 ) / 𝑎 ] 𝜃 ) )
49 48 anbi2d ( 𝑛 = 𝑀 → ( ( ( 𝑓𝑀 ) = 𝑎𝜏 ) ↔ ( ( 𝑓𝑀 ) = 𝑎[ ( 𝑓𝑀 ) / 𝑎 ] 𝜃 ) ) )
50 oveq2 ( 𝑛 = 𝑀 → ( 𝑁 ... 𝑛 ) = ( 𝑁 ... 𝑀 ) )
51 4 oveq1i ( 𝑁 ... 𝑀 ) = ( ( 𝑀 + 1 ) ... 𝑀 )
52 2 zrei 𝑀 ∈ ℝ
53 52 ltp1i 𝑀 < ( 𝑀 + 1 )
54 peano2z ( 𝑀 ∈ ℤ → ( 𝑀 + 1 ) ∈ ℤ )
55 2 54 ax-mp ( 𝑀 + 1 ) ∈ ℤ
56 fzn ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑀 < ( 𝑀 + 1 ) ↔ ( ( 𝑀 + 1 ) ... 𝑀 ) = ∅ ) )
57 55 2 56 mp2an ( 𝑀 < ( 𝑀 + 1 ) ↔ ( ( 𝑀 + 1 ) ... 𝑀 ) = ∅ )
58 53 57 mpbi ( ( 𝑀 + 1 ) ... 𝑀 ) = ∅
59 51 58 eqtri ( 𝑁 ... 𝑀 ) = ∅
60 50 59 eqtrdi ( 𝑛 = 𝑀 → ( 𝑁 ... 𝑛 ) = ∅ )
61 60 raleqdv ( 𝑛 = 𝑀 → ( ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ↔ ∀ 𝑘 ∈ ∅ 𝜒 ) )
62 43 49 61 3anbi123d ( 𝑛 = 𝑀 → ( ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ↔ ( 𝑓 : ( 𝑀 ... 𝑀 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎[ ( 𝑓𝑀 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ∅ 𝜒 ) ) )
63 ral0 𝑘 ∈ ∅ 𝜒
64 df-3an ( ( 𝑓 : ( 𝑀 ... 𝑀 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎[ ( 𝑓𝑀 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ∅ 𝜒 ) ↔ ( ( 𝑓 : ( 𝑀 ... 𝑀 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎[ ( 𝑓𝑀 ) / 𝑎 ] 𝜃 ) ) ∧ ∀ 𝑘 ∈ ∅ 𝜒 ) )
65 63 64 mpbiran2 ( ( 𝑓 : ( 𝑀 ... 𝑀 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎[ ( 𝑓𝑀 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ∅ 𝜒 ) ↔ ( 𝑓 : ( 𝑀 ... 𝑀 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎[ ( 𝑓𝑀 ) / 𝑎 ] 𝜃 ) ) )
66 62 65 bitrdi ( 𝑛 = 𝑀 → ( ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ↔ ( 𝑓 : ( 𝑀 ... 𝑀 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎[ ( 𝑓𝑀 ) / 𝑎 ] 𝜃 ) ) ) )
67 66 exbidv ( 𝑛 = 𝑀 → ( ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ↔ ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑀 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎[ ( 𝑓𝑀 ) / 𝑎 ] 𝜃 ) ) ) )
68 67 rspcev ( ( 𝑀𝑍 ∧ ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑀 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎[ ( 𝑓𝑀 ) / 𝑎 ] 𝜃 ) ) ) → ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) )
69 14 41 68 sylancr ( ( 𝑎𝐴𝜃 ) → ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) )
70 69 adantll ( ( ( 𝜂𝑎𝐴 ) ∧ 𝜃 ) → ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) )
71 70 a1d ( ( ( 𝜂𝑎𝐴 ) ∧ 𝜃 ) → ( ∀ 𝑑 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ¬ 𝑑 𝑅 𝑎 → ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ) )
72 breq1 ( 𝑑 = 𝑏 → ( 𝑑 𝑅 𝑎𝑏 𝑅 𝑎 ) )
73 72 rspcev ( ( 𝑏 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ∧ 𝑏 𝑅 𝑎 ) → ∃ 𝑑 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) 𝑑 𝑅 𝑎 )
74 73 expcom ( 𝑏 𝑅 𝑎 → ( 𝑏 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) → ∃ 𝑑 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) 𝑑 𝑅 𝑎 ) )
75 11 74 syl ( ( ( 𝜂𝜑 ) ∧ ( 𝑎𝐴𝑏𝐴 ) ) → ( 𝑏 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) → ∃ 𝑑 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) 𝑑 𝑅 𝑎 ) )
76 dfrex2 ( ∃ 𝑑 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) 𝑑 𝑅 𝑎 ↔ ¬ ∀ 𝑑 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ¬ 𝑑 𝑅 𝑎 )
77 75 76 syl6ib ( ( ( 𝜂𝜑 ) ∧ ( 𝑎𝐴𝑏𝐴 ) ) → ( 𝑏 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) → ¬ ∀ 𝑑 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ¬ 𝑑 𝑅 𝑎 ) )
78 77 con2d ( ( ( 𝜂𝜑 ) ∧ ( 𝑎𝐴𝑏𝐴 ) ) → ( ∀ 𝑑 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ¬ 𝑑 𝑅 𝑎 → ¬ 𝑏 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ) )
79 eldif ( 𝑏 ∈ ( 𝐴 ∖ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ) ↔ ( 𝑏𝐴 ∧ ¬ 𝑏 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ) )
80 79 simplbi2 ( 𝑏𝐴 → ( ¬ 𝑏 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) → 𝑏 ∈ ( 𝐴 ∖ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ) ) )
81 ssrab2 { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ⊆ 𝐴
82 dfss4 ( { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ⊆ 𝐴 ↔ ( 𝐴 ∖ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ) = { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } )
83 81 82 mpbi ( 𝐴 ∖ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ) = { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) }
84 83 eleq2i ( 𝑏 ∈ ( 𝐴 ∖ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ) ↔ 𝑏 ∈ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } )
85 eqeq2 ( 𝑐 = 𝑏 → ( ( 𝑓𝑀 ) = 𝑐 ↔ ( 𝑓𝑀 ) = 𝑏 ) )
86 85 anbi1d ( 𝑐 = 𝑏 → ( ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ↔ ( ( 𝑓𝑀 ) = 𝑏𝜏 ) ) )
87 86 3anbi2d ( 𝑐 = 𝑏 → ( ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ↔ ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑏𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ) )
88 87 exbidv ( 𝑐 = 𝑏 → ( ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ↔ ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑏𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ) )
89 88 rexbidv ( 𝑐 = 𝑏 → ( ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ↔ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑏𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ) )
90 89 elrab3 ( 𝑏𝐴 → ( 𝑏 ∈ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ↔ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑏𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ) )
91 84 90 syl5bb ( 𝑏𝐴 → ( 𝑏 ∈ ( 𝐴 ∖ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ) ↔ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑏𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ) )
92 80 91 sylibd ( 𝑏𝐴 → ( ¬ 𝑏 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) → ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑏𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ) )
93 92 ad2antll ( ( ( 𝜂𝜑 ) ∧ ( 𝑎𝐴𝑏𝐴 ) ) → ( ¬ 𝑏 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) → ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑏𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ) )
94 oveq2 ( 𝑛 = 𝑚 → ( 𝑀 ... 𝑛 ) = ( 𝑀 ... 𝑚 ) )
95 94 feq2d ( 𝑛 = 𝑚 → ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴𝑓 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ) )
96 fveq2 ( 𝑛 = 𝑚 → ( 𝑓𝑛 ) = ( 𝑓𝑚 ) )
97 96 sbceq1d ( 𝑛 = 𝑚 → ( [ ( 𝑓𝑛 ) / 𝑎 ] 𝜃[ ( 𝑓𝑚 ) / 𝑎 ] 𝜃 ) )
98 45 97 bitr3id ( 𝑛 = 𝑚 → ( 𝜏[ ( 𝑓𝑚 ) / 𝑎 ] 𝜃 ) )
99 98 anbi2d ( 𝑛 = 𝑚 → ( ( ( 𝑓𝑀 ) = 𝑏𝜏 ) ↔ ( ( 𝑓𝑀 ) = 𝑏[ ( 𝑓𝑚 ) / 𝑎 ] 𝜃 ) ) )
100 oveq2 ( 𝑛 = 𝑚 → ( 𝑁 ... 𝑛 ) = ( 𝑁 ... 𝑚 ) )
101 100 raleqdv ( 𝑛 = 𝑚 → ( ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ↔ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) 𝜒 ) )
102 95 99 101 3anbi123d ( 𝑛 = 𝑚 → ( ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑏𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ↔ ( 𝑓 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑏[ ( 𝑓𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) 𝜒 ) ) )
103 102 exbidv ( 𝑛 = 𝑚 → ( ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑏𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ↔ ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑏[ ( 𝑓𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) 𝜒 ) ) )
104 103 cbvrexvw ( ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑏𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ↔ ∃ 𝑚𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑏[ ( 𝑓𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) 𝜒 ) )
105 feq1 ( 𝑓 = 𝑔 → ( 𝑓 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ) )
106 fveq1 ( 𝑓 = 𝑔 → ( 𝑓𝑀 ) = ( 𝑔𝑀 ) )
107 106 eqeq1d ( 𝑓 = 𝑔 → ( ( 𝑓𝑀 ) = 𝑏 ↔ ( 𝑔𝑀 ) = 𝑏 ) )
108 fveq1 ( 𝑓 = 𝑔 → ( 𝑓𝑚 ) = ( 𝑔𝑚 ) )
109 108 sbceq1d ( 𝑓 = 𝑔 → ( [ ( 𝑓𝑚 ) / 𝑎 ] 𝜃[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) )
110 107 109 anbi12d ( 𝑓 = 𝑔 → ( ( ( 𝑓𝑀 ) = 𝑏[ ( 𝑓𝑚 ) / 𝑎 ] 𝜃 ) ↔ ( ( 𝑔𝑀 ) = 𝑏[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ) )
111 fvex ( 𝑓 ‘ ( 𝑘 − 1 ) ) ∈ V
112 5 sbcbidv ( 𝑎 = ( 𝑓 ‘ ( 𝑘 − 1 ) ) → ( [ ( 𝑓𝑘 ) / 𝑏 ] 𝜑[ ( 𝑓𝑘 ) / 𝑏 ] 𝜓 ) )
113 111 112 sbcie ( [ ( 𝑓 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑓𝑘 ) / 𝑏 ] 𝜑[ ( 𝑓𝑘 ) / 𝑏 ] 𝜓 )
114 fvex ( 𝑓𝑘 ) ∈ V
115 114 6 sbcie ( [ ( 𝑓𝑘 ) / 𝑏 ] 𝜓𝜒 )
116 113 115 bitri ( [ ( 𝑓 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑓𝑘 ) / 𝑏 ] 𝜑𝜒 )
117 fveq1 ( 𝑓 = 𝑔 → ( 𝑓 ‘ ( 𝑘 − 1 ) ) = ( 𝑔 ‘ ( 𝑘 − 1 ) ) )
118 fveq1 ( 𝑓 = 𝑔 → ( 𝑓𝑘 ) = ( 𝑔𝑘 ) )
119 118 sbceq1d ( 𝑓 = 𝑔 → ( [ ( 𝑓𝑘 ) / 𝑏 ] 𝜑[ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) )
120 117 119 sbceqbid ( 𝑓 = 𝑔 → ( [ ( 𝑓 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑓𝑘 ) / 𝑏 ] 𝜑[ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) )
121 116 120 bitr3id ( 𝑓 = 𝑔 → ( 𝜒[ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) )
122 121 ralbidv ( 𝑓 = 𝑔 → ( ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) 𝜒 ↔ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) )
123 105 110 122 3anbi123d ( 𝑓 = 𝑔 → ( ( 𝑓 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑏[ ( 𝑓𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) 𝜒 ) ↔ ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑔𝑀 ) = 𝑏[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) ) )
124 123 cbvexvw ( ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑏[ ( 𝑓𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) 𝜒 ) ↔ ∃ 𝑔 ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑔𝑀 ) = 𝑏[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) )
125 124 rexbii ( ∃ 𝑚𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑏[ ( 𝑓𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) 𝜒 ) ↔ ∃ 𝑚𝑍𝑔 ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑔𝑀 ) = 𝑏[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) )
126 104 125 bitri ( ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑏𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ↔ ∃ 𝑚𝑍𝑔 ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑔𝑀 ) = 𝑏[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) )
127 3 peano2uzs ( 𝑚𝑍 → ( 𝑚 + 1 ) ∈ 𝑍 )
128 127 ad2antlr ( ( ( ( ( 𝜂𝜑 ) ∧ ( 𝑎𝐴𝑏𝐴 ) ) ∧ 𝑚𝑍 ) ∧ ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑔𝑀 ) = 𝑏[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) ) → ( 𝑚 + 1 ) ∈ 𝑍 )
129 sbceq2a ( 𝑑 = 𝑏 → ( [ 𝑑 / 𝑏 ] 𝜑𝜑 ) )
130 129 anbi1d ( 𝑑 = 𝑏 → ( ( [ 𝑑 / 𝑏 ] 𝜑𝑎𝐴 ) ↔ ( 𝜑𝑎𝐴 ) ) )
131 130 anbi1d ( 𝑑 = 𝑏 → ( ( ( [ 𝑑 / 𝑏 ] 𝜑𝑎𝐴 ) ∧ 𝑚𝑍 ) ↔ ( ( 𝜑𝑎𝐴 ) ∧ 𝑚𝑍 ) ) )
132 eqeq2 ( 𝑑 = 𝑏 → ( ( 𝑔𝑀 ) = 𝑑 ↔ ( 𝑔𝑀 ) = 𝑏 ) )
133 132 anbi1d ( 𝑑 = 𝑏 → ( ( ( 𝑔𝑀 ) = 𝑑[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ↔ ( ( 𝑔𝑀 ) = 𝑏[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ) )
134 133 3anbi2d ( 𝑑 = 𝑏 → ( ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑔𝑀 ) = 𝑑[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) ↔ ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑔𝑀 ) = 𝑏[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) ) )
135 134 imbi1d ( 𝑑 = 𝑏 → ( ( ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑔𝑀 ) = 𝑑[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) → ∃ 𝑓 ( 𝑓 : ( 𝑀 ... ( 𝑚 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎[ ( 𝑓 ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) 𝜒 ) ) ↔ ( ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑔𝑀 ) = 𝑏[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) → ∃ 𝑓 ( 𝑓 : ( 𝑀 ... ( 𝑚 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎[ ( 𝑓 ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) 𝜒 ) ) ) )
136 131 135 imbi12d ( 𝑑 = 𝑏 → ( ( ( ( [ 𝑑 / 𝑏 ] 𝜑𝑎𝐴 ) ∧ 𝑚𝑍 ) → ( ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑔𝑀 ) = 𝑑[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) → ∃ 𝑓 ( 𝑓 : ( 𝑀 ... ( 𝑚 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎[ ( 𝑓 ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) 𝜒 ) ) ) ↔ ( ( ( 𝜑𝑎𝐴 ) ∧ 𝑚𝑍 ) → ( ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑔𝑀 ) = 𝑏[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) → ∃ 𝑓 ( 𝑓 : ( 𝑀 ... ( 𝑚 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎[ ( 𝑓 ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) 𝜒 ) ) ) ) )
137 sbceq2a ( 𝑐 = 𝑎 → ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑[ 𝑑 / 𝑏 ] 𝜑 ) )
138 eleq1 ( 𝑐 = 𝑎 → ( 𝑐𝐴𝑎𝐴 ) )
139 137 138 anbi12d ( 𝑐 = 𝑎 → ( ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑𝑐𝐴 ) ↔ ( [ 𝑑 / 𝑏 ] 𝜑𝑎𝐴 ) ) )
140 139 anbi1d ( 𝑐 = 𝑎 → ( ( ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑𝑐𝐴 ) ∧ 𝑚𝑍 ) ↔ ( ( [ 𝑑 / 𝑏 ] 𝜑𝑎𝐴 ) ∧ 𝑚𝑍 ) ) )
141 eqeq2 ( 𝑐 = 𝑎 → ( ( 𝑓𝑀 ) = 𝑐 ↔ ( 𝑓𝑀 ) = 𝑎 ) )
142 141 anbi1d ( 𝑐 = 𝑎 → ( ( ( 𝑓𝑀 ) = 𝑐[ ( 𝑓 ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 ) ↔ ( ( 𝑓𝑀 ) = 𝑎[ ( 𝑓 ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 ) ) )
143 142 3anbi2d ( 𝑐 = 𝑎 → ( ( 𝑓 : ( 𝑀 ... ( 𝑚 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐[ ( 𝑓 ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) 𝜒 ) ↔ ( 𝑓 : ( 𝑀 ... ( 𝑚 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎[ ( 𝑓 ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) 𝜒 ) ) )
144 143 exbidv ( 𝑐 = 𝑎 → ( ∃ 𝑓 ( 𝑓 : ( 𝑀 ... ( 𝑚 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐[ ( 𝑓 ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) 𝜒 ) ↔ ∃ 𝑓 ( 𝑓 : ( 𝑀 ... ( 𝑚 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎[ ( 𝑓 ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) 𝜒 ) ) )
145 144 imbi2d ( 𝑐 = 𝑎 → ( ( ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑔𝑀 ) = 𝑑[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) → ∃ 𝑓 ( 𝑓 : ( 𝑀 ... ( 𝑚 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐[ ( 𝑓 ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) 𝜒 ) ) ↔ ( ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑔𝑀 ) = 𝑑[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) → ∃ 𝑓 ( 𝑓 : ( 𝑀 ... ( 𝑚 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎[ ( 𝑓 ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) 𝜒 ) ) ) )
146 140 145 imbi12d ( 𝑐 = 𝑎 → ( ( ( ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑𝑐𝐴 ) ∧ 𝑚𝑍 ) → ( ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑔𝑀 ) = 𝑑[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) → ∃ 𝑓 ( 𝑓 : ( 𝑀 ... ( 𝑚 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐[ ( 𝑓 ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) 𝜒 ) ) ) ↔ ( ( ( [ 𝑑 / 𝑏 ] 𝜑𝑎𝐴 ) ∧ 𝑚𝑍 ) → ( ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑔𝑀 ) = 𝑑[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) → ∃ 𝑓 ( 𝑓 : ( 𝑀 ... ( 𝑚 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎[ ( 𝑓 ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) 𝜒 ) ) ) ) )
147 peano2uz ( 𝑚 ∈ ( ℤ𝑀 ) → ( 𝑚 + 1 ) ∈ ( ℤ𝑀 ) )
148 147 3 eleq2s ( 𝑚𝑍 → ( 𝑚 + 1 ) ∈ ( ℤ𝑀 ) )
149 elfzp12 ( ( 𝑚 + 1 ) ∈ ( ℤ𝑀 ) → ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↔ ( 𝑥 = 𝑀𝑥 ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) ) ) )
150 148 149 syl ( 𝑚𝑍 → ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↔ ( 𝑥 = 𝑀𝑥 ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) ) ) )
151 150 ad2antlr ( ( ( 𝑐𝐴𝑚𝑍 ) ∧ 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ) → ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↔ ( 𝑥 = 𝑀𝑥 ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) ) ) )
152 iftrue ( 𝑥 = 𝑀 → if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) = 𝑐 )
153 152 eleq1d ( 𝑥 = 𝑀 → ( if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ∈ 𝐴𝑐𝐴 ) )
154 153 biimprcd ( 𝑐𝐴 → ( 𝑥 = 𝑀 → if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ∈ 𝐴 ) )
155 154 ad2antrr ( ( ( 𝑐𝐴𝑚𝑍 ) ∧ 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ) → ( 𝑥 = 𝑀 → if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ∈ 𝐴 ) )
156 1re 1 ∈ ℝ
157 52 156 readdcli ( 𝑀 + 1 ) ∈ ℝ
158 52 157 ltnlei ( 𝑀 < ( 𝑀 + 1 ) ↔ ¬ ( 𝑀 + 1 ) ≤ 𝑀 )
159 53 158 mpbi ¬ ( 𝑀 + 1 ) ≤ 𝑀
160 eleq1 ( 𝑥 = 𝑀 → ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) ↔ 𝑀 ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) ) )
161 elfzle1 ( 𝑀 ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) → ( 𝑀 + 1 ) ≤ 𝑀 )
162 160 161 syl6bi ( 𝑥 = 𝑀 → ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) → ( 𝑀 + 1 ) ≤ 𝑀 ) )
163 162 com12 ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) → ( 𝑥 = 𝑀 → ( 𝑀 + 1 ) ≤ 𝑀 ) )
164 159 163 mtoi ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) → ¬ 𝑥 = 𝑀 )
165 164 adantl ( ( ( 𝑚𝑍𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ) ∧ 𝑥 ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) ) → ¬ 𝑥 = 𝑀 )
166 165 iffalsed ( ( ( 𝑚𝑍𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ) ∧ 𝑥 ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) ) → if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) = ( 𝑔 ‘ ( 𝑥 − 1 ) ) )
167 elfzelz ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) → 𝑥 ∈ ℤ )
168 167 adantl ( ( 𝑚𝑍𝑥 ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) ) → 𝑥 ∈ ℤ )
169 eluzelz ( 𝑚 ∈ ( ℤ𝑀 ) → 𝑚 ∈ ℤ )
170 169 3 eleq2s ( 𝑚𝑍𝑚 ∈ ℤ )
171 170 peano2zd ( 𝑚𝑍 → ( 𝑚 + 1 ) ∈ ℤ )
172 1z 1 ∈ ℤ
173 fzsubel ( ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ ( 𝑚 + 1 ) ∈ ℤ ) ∧ ( 𝑥 ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) ↔ ( 𝑥 − 1 ) ∈ ( ( ( 𝑀 + 1 ) − 1 ) ... ( ( 𝑚 + 1 ) − 1 ) ) ) )
174 173 biimpd ( ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ ( 𝑚 + 1 ) ∈ ℤ ) ∧ ( 𝑥 ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) → ( 𝑥 − 1 ) ∈ ( ( ( 𝑀 + 1 ) − 1 ) ... ( ( 𝑚 + 1 ) − 1 ) ) ) )
175 172 174 mpanr2 ( ( ( ( 𝑀 + 1 ) ∈ ℤ ∧ ( 𝑚 + 1 ) ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) → ( 𝑥 − 1 ) ∈ ( ( ( 𝑀 + 1 ) − 1 ) ... ( ( 𝑚 + 1 ) − 1 ) ) ) )
176 55 175 mpanl1 ( ( ( 𝑚 + 1 ) ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) → ( 𝑥 − 1 ) ∈ ( ( ( 𝑀 + 1 ) − 1 ) ... ( ( 𝑚 + 1 ) − 1 ) ) ) )
177 176 ex ( ( 𝑚 + 1 ) ∈ ℤ → ( 𝑥 ∈ ℤ → ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) → ( 𝑥 − 1 ) ∈ ( ( ( 𝑀 + 1 ) − 1 ) ... ( ( 𝑚 + 1 ) − 1 ) ) ) ) )
178 171 177 syl ( 𝑚𝑍 → ( 𝑥 ∈ ℤ → ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) → ( 𝑥 − 1 ) ∈ ( ( ( 𝑀 + 1 ) − 1 ) ... ( ( 𝑚 + 1 ) − 1 ) ) ) ) )
179 178 com23 ( 𝑚𝑍 → ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) → ( 𝑥 ∈ ℤ → ( 𝑥 − 1 ) ∈ ( ( ( 𝑀 + 1 ) − 1 ) ... ( ( 𝑚 + 1 ) − 1 ) ) ) ) )
180 179 imp ( ( 𝑚𝑍𝑥 ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) ) → ( 𝑥 ∈ ℤ → ( 𝑥 − 1 ) ∈ ( ( ( 𝑀 + 1 ) − 1 ) ... ( ( 𝑚 + 1 ) − 1 ) ) ) )
181 168 180 mpd ( ( 𝑚𝑍𝑥 ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) ) → ( 𝑥 − 1 ) ∈ ( ( ( 𝑀 + 1 ) − 1 ) ... ( ( 𝑚 + 1 ) − 1 ) ) )
182 52 recni 𝑀 ∈ ℂ
183 ax-1cn 1 ∈ ℂ
184 182 183 pncan3oi ( ( 𝑀 + 1 ) − 1 ) = 𝑀
185 184 a1i ( 𝑚𝑍 → ( ( 𝑀 + 1 ) − 1 ) = 𝑀 )
186 170 zcnd ( 𝑚𝑍𝑚 ∈ ℂ )
187 pncan ( ( 𝑚 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑚 + 1 ) − 1 ) = 𝑚 )
188 186 183 187 sylancl ( 𝑚𝑍 → ( ( 𝑚 + 1 ) − 1 ) = 𝑚 )
189 185 188 oveq12d ( 𝑚𝑍 → ( ( ( 𝑀 + 1 ) − 1 ) ... ( ( 𝑚 + 1 ) − 1 ) ) = ( 𝑀 ... 𝑚 ) )
190 189 adantr ( ( 𝑚𝑍𝑥 ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) ) → ( ( ( 𝑀 + 1 ) − 1 ) ... ( ( 𝑚 + 1 ) − 1 ) ) = ( 𝑀 ... 𝑚 ) )
191 181 190 eleqtrd ( ( 𝑚𝑍𝑥 ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) ) → ( 𝑥 − 1 ) ∈ ( 𝑀 ... 𝑚 ) )
192 ffvelrn ( ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( 𝑥 − 1 ) ∈ ( 𝑀 ... 𝑚 ) ) → ( 𝑔 ‘ ( 𝑥 − 1 ) ) ∈ 𝐴 )
193 191 192 sylan2 ( ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( 𝑚𝑍𝑥 ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) ) ) → ( 𝑔 ‘ ( 𝑥 − 1 ) ) ∈ 𝐴 )
194 193 anassrs ( ( ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴𝑚𝑍 ) ∧ 𝑥 ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) ) → ( 𝑔 ‘ ( 𝑥 − 1 ) ) ∈ 𝐴 )
195 194 ancom1s ( ( ( 𝑚𝑍𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ) ∧ 𝑥 ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) ) → ( 𝑔 ‘ ( 𝑥 − 1 ) ) ∈ 𝐴 )
196 166 195 eqeltrd ( ( ( 𝑚𝑍𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ) ∧ 𝑥 ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) ) → if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ∈ 𝐴 )
197 196 ex ( ( 𝑚𝑍𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ) → ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) → if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ∈ 𝐴 ) )
198 197 adantll ( ( ( 𝑐𝐴𝑚𝑍 ) ∧ 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ) → ( 𝑥 ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) → if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ∈ 𝐴 ) )
199 155 198 jaod ( ( ( 𝑐𝐴𝑚𝑍 ) ∧ 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ) → ( ( 𝑥 = 𝑀𝑥 ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) ) → if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ∈ 𝐴 ) )
200 151 199 sylbid ( ( ( 𝑐𝐴𝑚𝑍 ) ∧ 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ) → ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) → if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ∈ 𝐴 ) )
201 200 ralrimiv ( ( ( 𝑐𝐴𝑚𝑍 ) ∧ 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ) → ∀ 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ∈ 𝐴 )
202 eqid ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) = ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) )
203 202 fmpt ( ∀ 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ∈ 𝐴 ↔ ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) : ( 𝑀 ... ( 𝑚 + 1 ) ) ⟶ 𝐴 )
204 201 203 sylib ( ( ( 𝑐𝐴𝑚𝑍 ) ∧ 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ) → ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) : ( 𝑀 ... ( 𝑚 + 1 ) ) ⟶ 𝐴 )
205 204 adantlll ( ( ( ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑𝑐𝐴 ) ∧ 𝑚𝑍 ) ∧ 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ) → ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) : ( 𝑀 ... ( 𝑚 + 1 ) ) ⟶ 𝐴 )
206 205 3ad2antr1 ( ( ( ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑𝑐𝐴 ) ∧ 𝑚𝑍 ) ∧ ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑔𝑀 ) = 𝑑[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) ) → ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) : ( 𝑀 ... ( 𝑚 + 1 ) ) ⟶ 𝐴 )
207 eluzfz1 ( ( 𝑚 + 1 ) ∈ ( ℤ𝑀 ) → 𝑀 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) )
208 147 207 syl ( 𝑚 ∈ ( ℤ𝑀 ) → 𝑀 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) )
209 208 3 eleq2s ( 𝑚𝑍𝑀 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) )
210 vex 𝑐 ∈ V
211 152 202 210 fvmpt ( 𝑀 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) → ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑀 ) = 𝑐 )
212 209 211 syl ( 𝑚𝑍 → ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑀 ) = 𝑐 )
213 212 ad2antlr ( ( ( ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑𝑐𝐴 ) ∧ 𝑚𝑍 ) ∧ ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑔𝑀 ) = 𝑑[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) ) → ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑀 ) = 𝑐 )
214 eluzfz2 ( ( 𝑚 + 1 ) ∈ ( ℤ𝑀 ) → ( 𝑚 + 1 ) ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) )
215 147 214 syl ( 𝑚 ∈ ( ℤ𝑀 ) → ( 𝑚 + 1 ) ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) )
216 215 3 eleq2s ( 𝑚𝑍 → ( 𝑚 + 1 ) ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) )
217 eqeq1 ( 𝑥 = ( 𝑚 + 1 ) → ( 𝑥 = 𝑀 ↔ ( 𝑚 + 1 ) = 𝑀 ) )
218 fvoveq1 ( 𝑥 = ( 𝑚 + 1 ) → ( 𝑔 ‘ ( 𝑥 − 1 ) ) = ( 𝑔 ‘ ( ( 𝑚 + 1 ) − 1 ) ) )
219 217 218 ifbieq2d ( 𝑥 = ( 𝑚 + 1 ) → if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) = if ( ( 𝑚 + 1 ) = 𝑀 , 𝑐 , ( 𝑔 ‘ ( ( 𝑚 + 1 ) − 1 ) ) ) )
220 fvex ( 𝑔 ‘ ( ( 𝑚 + 1 ) − 1 ) ) ∈ V
221 210 220 ifex if ( ( 𝑚 + 1 ) = 𝑀 , 𝑐 , ( 𝑔 ‘ ( ( 𝑚 + 1 ) − 1 ) ) ) ∈ V
222 219 202 221 fvmpt ( ( 𝑚 + 1 ) ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) → ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑚 + 1 ) ) = if ( ( 𝑚 + 1 ) = 𝑀 , 𝑐 , ( 𝑔 ‘ ( ( 𝑚 + 1 ) − 1 ) ) ) )
223 216 222 syl ( 𝑚𝑍 → ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑚 + 1 ) ) = if ( ( 𝑚 + 1 ) = 𝑀 , 𝑐 , ( 𝑔 ‘ ( ( 𝑚 + 1 ) − 1 ) ) ) )
224 eluzle ( 𝑚 ∈ ( ℤ𝑀 ) → 𝑀𝑚 )
225 224 3 eleq2s ( 𝑚𝑍𝑀𝑚 )
226 zleltp1 ( ( 𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ ) → ( 𝑀𝑚𝑀 < ( 𝑚 + 1 ) ) )
227 2 170 226 sylancr ( 𝑚𝑍 → ( 𝑀𝑚𝑀 < ( 𝑚 + 1 ) ) )
228 225 227 mpbid ( 𝑚𝑍𝑀 < ( 𝑚 + 1 ) )
229 ltne ( ( 𝑀 ∈ ℝ ∧ 𝑀 < ( 𝑚 + 1 ) ) → ( 𝑚 + 1 ) ≠ 𝑀 )
230 52 228 229 sylancr ( 𝑚𝑍 → ( 𝑚 + 1 ) ≠ 𝑀 )
231 230 neneqd ( 𝑚𝑍 → ¬ ( 𝑚 + 1 ) = 𝑀 )
232 231 iffalsed ( 𝑚𝑍 → if ( ( 𝑚 + 1 ) = 𝑀 , 𝑐 , ( 𝑔 ‘ ( ( 𝑚 + 1 ) − 1 ) ) ) = ( 𝑔 ‘ ( ( 𝑚 + 1 ) − 1 ) ) )
233 188 fveq2d ( 𝑚𝑍 → ( 𝑔 ‘ ( ( 𝑚 + 1 ) − 1 ) ) = ( 𝑔𝑚 ) )
234 223 232 233 3eqtrd ( 𝑚𝑍 → ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑚 + 1 ) ) = ( 𝑔𝑚 ) )
235 234 sbceq1d ( 𝑚𝑍 → ( [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) )
236 235 biimpar ( ( 𝑚𝑍[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) → [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 )
237 236 ad2ant2l ( ( ( ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑𝑐𝐴 ) ∧ 𝑚𝑍 ) ∧ ( ( 𝑔𝑀 ) = 𝑑[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ) → [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 )
238 237 3ad2antr2 ( ( ( ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑𝑐𝐴 ) ∧ 𝑚𝑍 ) ∧ ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑔𝑀 ) = 𝑑[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) ) → [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 )
239 eluzp1p1 ( 𝑚 ∈ ( ℤ𝑀 ) → ( 𝑚 + 1 ) ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) )
240 239 3 eleq2s ( 𝑚𝑍 → ( 𝑚 + 1 ) ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) )
241 4 fveq2i ( ℤ𝑁 ) = ( ℤ ‘ ( 𝑀 + 1 ) )
242 240 241 eleqtrrdi ( 𝑚𝑍 → ( 𝑚 + 1 ) ∈ ( ℤ𝑁 ) )
243 elfzp12 ( ( 𝑚 + 1 ) ∈ ( ℤ𝑁 ) → ( 𝑗 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) ↔ ( 𝑗 = 𝑁𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ) ) )
244 242 243 syl ( 𝑚𝑍 → ( 𝑗 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) ↔ ( 𝑗 = 𝑁𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ) ) )
245 244 biimpa ( ( 𝑚𝑍𝑗 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) ) → ( 𝑗 = 𝑁𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ) )
246 245 adantll ( ( ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑𝑚𝑍 ) ∧ 𝑗 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) ) → ( 𝑗 = 𝑁𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ) )
247 246 adantlr ( ( ( ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑𝑚𝑍 ) ∧ ( ( 𝑔𝑀 ) = 𝑑 ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) ) ∧ 𝑗 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) ) → ( 𝑗 = 𝑁𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ) )
248 oveq1 ( 𝑗 = 𝑁 → ( 𝑗 − 1 ) = ( 𝑁 − 1 ) )
249 4 oveq1i ( 𝑁 − 1 ) = ( ( 𝑀 + 1 ) − 1 )
250 249 184 eqtri ( 𝑁 − 1 ) = 𝑀
251 248 250 eqtrdi ( 𝑗 = 𝑁 → ( 𝑗 − 1 ) = 𝑀 )
252 251 fveq2d ( 𝑗 = 𝑁 → ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑗 − 1 ) ) = ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑀 ) )
253 252 ad2antll ( ( 𝑚𝑍 ∧ ( ( 𝑔𝑀 ) = 𝑑𝑗 = 𝑁 ) ) → ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑗 − 1 ) ) = ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑀 ) )
254 212 adantr ( ( 𝑚𝑍 ∧ ( ( 𝑔𝑀 ) = 𝑑𝑗 = 𝑁 ) ) → ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑀 ) = 𝑐 )
255 253 254 eqtrd ( ( 𝑚𝑍 ∧ ( ( 𝑔𝑀 ) = 𝑑𝑗 = 𝑁 ) ) → ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑗 − 1 ) ) = 𝑐 )
256 4 eqeq2i ( 𝑗 = 𝑁𝑗 = ( 𝑀 + 1 ) )
257 fveq2 ( 𝑗 = ( 𝑀 + 1 ) → ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑗 ) = ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑀 + 1 ) ) )
258 256 257 sylbi ( 𝑗 = 𝑁 → ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑗 ) = ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑀 + 1 ) ) )
259 258 ad2antll ( ( 𝑚𝑍 ∧ ( ( 𝑔𝑀 ) = 𝑑𝑗 = 𝑁 ) ) → ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑗 ) = ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑀 + 1 ) ) )
260 52 157 53 ltleii 𝑀 ≤ ( 𝑀 + 1 )
261 eluz2 ( ( 𝑀 + 1 ) ∈ ( ℤ𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ ( 𝑀 + 1 ) ∈ ℤ ∧ 𝑀 ≤ ( 𝑀 + 1 ) ) )
262 2 55 260 261 mpbir3an ( 𝑀 + 1 ) ∈ ( ℤ𝑀 )
263 fzss1 ( ( 𝑀 + 1 ) ∈ ( ℤ𝑀 ) → ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) ⊆ ( 𝑀 ... ( 𝑚 + 1 ) ) )
264 262 263 ax-mp ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) ⊆ ( 𝑀 ... ( 𝑚 + 1 ) )
265 eluzfz1 ( 𝑚 ∈ ( ℤ𝑀 ) → 𝑀 ∈ ( 𝑀 ... 𝑚 ) )
266 265 3 eleq2s ( 𝑚𝑍𝑀 ∈ ( 𝑀 ... 𝑚 ) )
267 fzaddel ( ( ( 𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ ) ∧ ( 𝑀 ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( 𝑀 ∈ ( 𝑀 ... 𝑚 ) ↔ ( 𝑀 + 1 ) ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) ) )
268 2 172 267 mpanr12 ( ( 𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ ) → ( 𝑀 ∈ ( 𝑀 ... 𝑚 ) ↔ ( 𝑀 + 1 ) ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) ) )
269 2 170 268 sylancr ( 𝑚𝑍 → ( 𝑀 ∈ ( 𝑀 ... 𝑚 ) ↔ ( 𝑀 + 1 ) ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) ) )
270 266 269 mpbid ( 𝑚𝑍 → ( 𝑀 + 1 ) ∈ ( ( 𝑀 + 1 ) ... ( 𝑚 + 1 ) ) )
271 264 270 sselid ( 𝑚𝑍 → ( 𝑀 + 1 ) ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) )
272 eqeq1 ( 𝑥 = ( 𝑀 + 1 ) → ( 𝑥 = 𝑀 ↔ ( 𝑀 + 1 ) = 𝑀 ) )
273 oveq1 ( 𝑥 = ( 𝑀 + 1 ) → ( 𝑥 − 1 ) = ( ( 𝑀 + 1 ) − 1 ) )
274 273 184 eqtrdi ( 𝑥 = ( 𝑀 + 1 ) → ( 𝑥 − 1 ) = 𝑀 )
275 274 fveq2d ( 𝑥 = ( 𝑀 + 1 ) → ( 𝑔 ‘ ( 𝑥 − 1 ) ) = ( 𝑔𝑀 ) )
276 272 275 ifbieq2d ( 𝑥 = ( 𝑀 + 1 ) → if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) = if ( ( 𝑀 + 1 ) = 𝑀 , 𝑐 , ( 𝑔𝑀 ) ) )
277 fvex ( 𝑔𝑀 ) ∈ V
278 210 277 ifex if ( ( 𝑀 + 1 ) = 𝑀 , 𝑐 , ( 𝑔𝑀 ) ) ∈ V
279 276 202 278 fvmpt ( ( 𝑀 + 1 ) ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) → ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑀 + 1 ) ) = if ( ( 𝑀 + 1 ) = 𝑀 , 𝑐 , ( 𝑔𝑀 ) ) )
280 271 279 syl ( 𝑚𝑍 → ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑀 + 1 ) ) = if ( ( 𝑀 + 1 ) = 𝑀 , 𝑐 , ( 𝑔𝑀 ) ) )
281 52 53 gtneii ( 𝑀 + 1 ) ≠ 𝑀
282 ifnefalse ( ( 𝑀 + 1 ) ≠ 𝑀 → if ( ( 𝑀 + 1 ) = 𝑀 , 𝑐 , ( 𝑔𝑀 ) ) = ( 𝑔𝑀 ) )
283 281 282 ax-mp if ( ( 𝑀 + 1 ) = 𝑀 , 𝑐 , ( 𝑔𝑀 ) ) = ( 𝑔𝑀 )
284 280 283 eqtrdi ( 𝑚𝑍 → ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑀 + 1 ) ) = ( 𝑔𝑀 ) )
285 284 adantr ( ( 𝑚𝑍 ∧ ( ( 𝑔𝑀 ) = 𝑑𝑗 = 𝑁 ) ) → ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑀 + 1 ) ) = ( 𝑔𝑀 ) )
286 simprl ( ( 𝑚𝑍 ∧ ( ( 𝑔𝑀 ) = 𝑑𝑗 = 𝑁 ) ) → ( 𝑔𝑀 ) = 𝑑 )
287 259 285 286 3eqtrd ( ( 𝑚𝑍 ∧ ( ( 𝑔𝑀 ) = 𝑑𝑗 = 𝑁 ) ) → ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑗 ) = 𝑑 )
288 287 sbceq1d ( ( 𝑚𝑍 ∧ ( ( 𝑔𝑀 ) = 𝑑𝑗 = 𝑁 ) ) → ( [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑗 ) / 𝑏 ] 𝜑[ 𝑑 / 𝑏 ] 𝜑 ) )
289 255 288 sbceqbid ( ( 𝑚𝑍 ∧ ( ( 𝑔𝑀 ) = 𝑑𝑗 = 𝑁 ) ) → ( [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑗 − 1 ) ) / 𝑎 ] [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑗 ) / 𝑏 ] 𝜑[ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ) )
290 289 biimparc ( ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑 ∧ ( 𝑚𝑍 ∧ ( ( 𝑔𝑀 ) = 𝑑𝑗 = 𝑁 ) ) ) → [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑗 − 1 ) ) / 𝑎 ] [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑗 ) / 𝑏 ] 𝜑 )
291 290 anassrs ( ( ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑𝑚𝑍 ) ∧ ( ( 𝑔𝑀 ) = 𝑑𝑗 = 𝑁 ) ) → [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑗 − 1 ) ) / 𝑎 ] [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑗 ) / 𝑏 ] 𝜑 )
292 291 anassrs ( ( ( ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑𝑚𝑍 ) ∧ ( 𝑔𝑀 ) = 𝑑 ) ∧ 𝑗 = 𝑁 ) → [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑗 − 1 ) ) / 𝑎 ] [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑗 ) / 𝑏 ] 𝜑 )
293 292 adantlrr ( ( ( ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑𝑚𝑍 ) ∧ ( ( 𝑔𝑀 ) = 𝑑 ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) ) ∧ 𝑗 = 𝑁 ) → [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑗 − 1 ) ) / 𝑎 ] [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑗 ) / 𝑏 ] 𝜑 )
294 elfzelz ( 𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) → 𝑗 ∈ ℤ )
295 294 adantl ( ( 𝑚𝑍𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ) → 𝑗 ∈ ℤ )
296 4 55 eqeltri 𝑁 ∈ ℤ
297 peano2z ( 𝑁 ∈ ℤ → ( 𝑁 + 1 ) ∈ ℤ )
298 296 297 ax-mp ( 𝑁 + 1 ) ∈ ℤ
299 fzsubel ( ( ( ( 𝑁 + 1 ) ∈ ℤ ∧ ( 𝑚 + 1 ) ∈ ℤ ) ∧ ( 𝑗 ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( 𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ↔ ( 𝑗 − 1 ) ∈ ( ( ( 𝑁 + 1 ) − 1 ) ... ( ( 𝑚 + 1 ) − 1 ) ) ) )
300 299 biimpd ( ( ( ( 𝑁 + 1 ) ∈ ℤ ∧ ( 𝑚 + 1 ) ∈ ℤ ) ∧ ( 𝑗 ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( 𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) → ( 𝑗 − 1 ) ∈ ( ( ( 𝑁 + 1 ) − 1 ) ... ( ( 𝑚 + 1 ) − 1 ) ) ) )
301 172 300 mpanr2 ( ( ( ( 𝑁 + 1 ) ∈ ℤ ∧ ( 𝑚 + 1 ) ∈ ℤ ) ∧ 𝑗 ∈ ℤ ) → ( 𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) → ( 𝑗 − 1 ) ∈ ( ( ( 𝑁 + 1 ) − 1 ) ... ( ( 𝑚 + 1 ) − 1 ) ) ) )
302 301 ex ( ( ( 𝑁 + 1 ) ∈ ℤ ∧ ( 𝑚 + 1 ) ∈ ℤ ) → ( 𝑗 ∈ ℤ → ( 𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) → ( 𝑗 − 1 ) ∈ ( ( ( 𝑁 + 1 ) − 1 ) ... ( ( 𝑚 + 1 ) − 1 ) ) ) ) )
303 298 171 302 sylancr ( 𝑚𝑍 → ( 𝑗 ∈ ℤ → ( 𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) → ( 𝑗 − 1 ) ∈ ( ( ( 𝑁 + 1 ) − 1 ) ... ( ( 𝑚 + 1 ) − 1 ) ) ) ) )
304 303 com23 ( 𝑚𝑍 → ( 𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) → ( 𝑗 ∈ ℤ → ( 𝑗 − 1 ) ∈ ( ( ( 𝑁 + 1 ) − 1 ) ... ( ( 𝑚 + 1 ) − 1 ) ) ) ) )
305 304 imp ( ( 𝑚𝑍𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ) → ( 𝑗 ∈ ℤ → ( 𝑗 − 1 ) ∈ ( ( ( 𝑁 + 1 ) − 1 ) ... ( ( 𝑚 + 1 ) − 1 ) ) ) )
306 295 305 mpd ( ( 𝑚𝑍𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ) → ( 𝑗 − 1 ) ∈ ( ( ( 𝑁 + 1 ) − 1 ) ... ( ( 𝑚 + 1 ) − 1 ) ) )
307 296 zrei 𝑁 ∈ ℝ
308 307 recni 𝑁 ∈ ℂ
309 308 183 pncan3oi ( ( 𝑁 + 1 ) − 1 ) = 𝑁
310 309 a1i ( 𝑚𝑍 → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
311 310 188 oveq12d ( 𝑚𝑍 → ( ( ( 𝑁 + 1 ) − 1 ) ... ( ( 𝑚 + 1 ) − 1 ) ) = ( 𝑁 ... 𝑚 ) )
312 311 adantr ( ( 𝑚𝑍𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ) → ( ( ( 𝑁 + 1 ) − 1 ) ... ( ( 𝑚 + 1 ) − 1 ) ) = ( 𝑁 ... 𝑚 ) )
313 306 312 eleqtrd ( ( 𝑚𝑍𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ) → ( 𝑗 − 1 ) ∈ ( 𝑁 ... 𝑚 ) )
314 fvoveq1 ( 𝑘 = ( 𝑗 − 1 ) → ( 𝑔 ‘ ( 𝑘 − 1 ) ) = ( 𝑔 ‘ ( ( 𝑗 − 1 ) − 1 ) ) )
315 fveq2 ( 𝑘 = ( 𝑗 − 1 ) → ( 𝑔𝑘 ) = ( 𝑔 ‘ ( 𝑗 − 1 ) ) )
316 315 sbceq1d ( 𝑘 = ( 𝑗 − 1 ) → ( [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑[ ( 𝑔 ‘ ( 𝑗 − 1 ) ) / 𝑏 ] 𝜑 ) )
317 314 316 sbceqbid ( 𝑘 = ( 𝑗 − 1 ) → ( [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑[ ( 𝑔 ‘ ( ( 𝑗 − 1 ) − 1 ) ) / 𝑎 ] [ ( 𝑔 ‘ ( 𝑗 − 1 ) ) / 𝑏 ] 𝜑 ) )
318 317 rspcva ( ( ( 𝑗 − 1 ) ∈ ( 𝑁 ... 𝑚 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) → [ ( 𝑔 ‘ ( ( 𝑗 − 1 ) − 1 ) ) / 𝑎 ] [ ( 𝑔 ‘ ( 𝑗 − 1 ) ) / 𝑏 ] 𝜑 )
319 313 318 sylan ( ( ( 𝑚𝑍𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) → [ ( 𝑔 ‘ ( ( 𝑗 − 1 ) − 1 ) ) / 𝑎 ] [ ( 𝑔 ‘ ( 𝑗 − 1 ) ) / 𝑏 ] 𝜑 )
320 4 262 eqeltri 𝑁 ∈ ( ℤ𝑀 )
321 fzss1 ( 𝑁 ∈ ( ℤ𝑀 ) → ( 𝑁 ... ( 𝑚 + 1 ) ) ⊆ ( 𝑀 ... ( 𝑚 + 1 ) ) )
322 320 321 ax-mp ( 𝑁 ... ( 𝑚 + 1 ) ) ⊆ ( 𝑀 ... ( 𝑚 + 1 ) )
323 fzssp1 ( 𝑁 ... 𝑚 ) ⊆ ( 𝑁 ... ( 𝑚 + 1 ) )
324 323 313 sselid ( ( 𝑚𝑍𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ) → ( 𝑗 − 1 ) ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) )
325 322 324 sselid ( ( 𝑚𝑍𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ) → ( 𝑗 − 1 ) ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) )
326 eqeq1 ( 𝑥 = ( 𝑗 − 1 ) → ( 𝑥 = 𝑀 ↔ ( 𝑗 − 1 ) = 𝑀 ) )
327 fvoveq1 ( 𝑥 = ( 𝑗 − 1 ) → ( 𝑔 ‘ ( 𝑥 − 1 ) ) = ( 𝑔 ‘ ( ( 𝑗 − 1 ) − 1 ) ) )
328 326 327 ifbieq2d ( 𝑥 = ( 𝑗 − 1 ) → if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) = if ( ( 𝑗 − 1 ) = 𝑀 , 𝑐 , ( 𝑔 ‘ ( ( 𝑗 − 1 ) − 1 ) ) ) )
329 fvex ( 𝑔 ‘ ( ( 𝑗 − 1 ) − 1 ) ) ∈ V
330 210 329 ifex if ( ( 𝑗 − 1 ) = 𝑀 , 𝑐 , ( 𝑔 ‘ ( ( 𝑗 − 1 ) − 1 ) ) ) ∈ V
331 328 202 330 fvmpt ( ( 𝑗 − 1 ) ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) → ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑗 − 1 ) ) = if ( ( 𝑗 − 1 ) = 𝑀 , 𝑐 , ( 𝑔 ‘ ( ( 𝑗 − 1 ) − 1 ) ) ) )
332 325 331 syl ( ( 𝑚𝑍𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ) → ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑗 − 1 ) ) = if ( ( 𝑗 − 1 ) = 𝑀 , 𝑐 , ( 𝑔 ‘ ( ( 𝑗 − 1 ) − 1 ) ) ) )
333 157 ltp1i ( 𝑀 + 1 ) < ( ( 𝑀 + 1 ) + 1 )
334 4 oveq1i ( 𝑁 + 1 ) = ( ( 𝑀 + 1 ) + 1 )
335 333 334 breqtrri ( 𝑀 + 1 ) < ( 𝑁 + 1 )
336 307 156 readdcli ( 𝑁 + 1 ) ∈ ℝ
337 157 336 ltnlei ( ( 𝑀 + 1 ) < ( 𝑁 + 1 ) ↔ ¬ ( 𝑁 + 1 ) ≤ ( 𝑀 + 1 ) )
338 335 337 mpbi ¬ ( 𝑁 + 1 ) ≤ ( 𝑀 + 1 )
339 294 zcnd ( 𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) → 𝑗 ∈ ℂ )
340 subadd ( ( 𝑗 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( ( 𝑗 − 1 ) = 𝑀 ↔ ( 1 + 𝑀 ) = 𝑗 ) )
341 183 182 340 mp3an23 ( 𝑗 ∈ ℂ → ( ( 𝑗 − 1 ) = 𝑀 ↔ ( 1 + 𝑀 ) = 𝑗 ) )
342 339 341 syl ( 𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) → ( ( 𝑗 − 1 ) = 𝑀 ↔ ( 1 + 𝑀 ) = 𝑗 ) )
343 eqcom ( ( 1 + 𝑀 ) = 𝑗𝑗 = ( 1 + 𝑀 ) )
344 183 182 addcomi ( 1 + 𝑀 ) = ( 𝑀 + 1 )
345 344 eqeq2i ( 𝑗 = ( 1 + 𝑀 ) ↔ 𝑗 = ( 𝑀 + 1 ) )
346 343 345 bitri ( ( 1 + 𝑀 ) = 𝑗𝑗 = ( 𝑀 + 1 ) )
347 eleq1 ( 𝑗 = ( 𝑀 + 1 ) → ( 𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ↔ ( 𝑀 + 1 ) ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ) )
348 elfzle1 ( ( 𝑀 + 1 ) ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) → ( 𝑁 + 1 ) ≤ ( 𝑀 + 1 ) )
349 347 348 syl6bi ( 𝑗 = ( 𝑀 + 1 ) → ( 𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) → ( 𝑁 + 1 ) ≤ ( 𝑀 + 1 ) ) )
350 349 com12 ( 𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) → ( 𝑗 = ( 𝑀 + 1 ) → ( 𝑁 + 1 ) ≤ ( 𝑀 + 1 ) ) )
351 346 350 syl5bi ( 𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) → ( ( 1 + 𝑀 ) = 𝑗 → ( 𝑁 + 1 ) ≤ ( 𝑀 + 1 ) ) )
352 342 351 sylbid ( 𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) → ( ( 𝑗 − 1 ) = 𝑀 → ( 𝑁 + 1 ) ≤ ( 𝑀 + 1 ) ) )
353 338 352 mtoi ( 𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) → ¬ ( 𝑗 − 1 ) = 𝑀 )
354 353 adantl ( ( 𝑚𝑍𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ) → ¬ ( 𝑗 − 1 ) = 𝑀 )
355 354 iffalsed ( ( 𝑚𝑍𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ) → if ( ( 𝑗 − 1 ) = 𝑀 , 𝑐 , ( 𝑔 ‘ ( ( 𝑗 − 1 ) − 1 ) ) ) = ( 𝑔 ‘ ( ( 𝑗 − 1 ) − 1 ) ) )
356 332 355 eqtrd ( ( 𝑚𝑍𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ) → ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑗 − 1 ) ) = ( 𝑔 ‘ ( ( 𝑗 − 1 ) − 1 ) ) )
357 peano2uz ( 𝑁 ∈ ( ℤ𝑀 ) → ( 𝑁 + 1 ) ∈ ( ℤ𝑀 ) )
358 fzss1 ( ( 𝑁 + 1 ) ∈ ( ℤ𝑀 ) → ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ⊆ ( 𝑀 ... ( 𝑚 + 1 ) ) )
359 320 357 358 mp2b ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ⊆ ( 𝑀 ... ( 𝑚 + 1 ) )
360 simpr ( ( 𝑚𝑍𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ) → 𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) )
361 359 360 sselid ( ( 𝑚𝑍𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ) → 𝑗 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) )
362 eqeq1 ( 𝑥 = 𝑗 → ( 𝑥 = 𝑀𝑗 = 𝑀 ) )
363 fvoveq1 ( 𝑥 = 𝑗 → ( 𝑔 ‘ ( 𝑥 − 1 ) ) = ( 𝑔 ‘ ( 𝑗 − 1 ) ) )
364 362 363 ifbieq2d ( 𝑥 = 𝑗 → if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) = if ( 𝑗 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑗 − 1 ) ) ) )
365 fvex ( 𝑔 ‘ ( 𝑗 − 1 ) ) ∈ V
366 210 365 ifex if ( 𝑗 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑗 − 1 ) ) ) ∈ V
367 364 202 366 fvmpt ( 𝑗 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) → ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑗 ) = if ( 𝑗 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑗 − 1 ) ) ) )
368 361 367 syl ( ( 𝑚𝑍𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ) → ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑗 ) = if ( 𝑗 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑗 − 1 ) ) ) )
369 53 4 breqtrri 𝑀 < 𝑁
370 307 ltp1i 𝑁 < ( 𝑁 + 1 )
371 52 307 336 lttri ( ( 𝑀 < 𝑁𝑁 < ( 𝑁 + 1 ) ) → 𝑀 < ( 𝑁 + 1 ) )
372 369 370 371 mp2an 𝑀 < ( 𝑁 + 1 )
373 52 336 ltnlei ( 𝑀 < ( 𝑁 + 1 ) ↔ ¬ ( 𝑁 + 1 ) ≤ 𝑀 )
374 372 373 mpbi ¬ ( 𝑁 + 1 ) ≤ 𝑀
375 eleq1 ( 𝑗 = 𝑀 → ( 𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ↔ 𝑀 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ) )
376 elfzle1 ( 𝑀 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) → ( 𝑁 + 1 ) ≤ 𝑀 )
377 375 376 syl6bi ( 𝑗 = 𝑀 → ( 𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) → ( 𝑁 + 1 ) ≤ 𝑀 ) )
378 377 com12 ( 𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) → ( 𝑗 = 𝑀 → ( 𝑁 + 1 ) ≤ 𝑀 ) )
379 374 378 mtoi ( 𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) → ¬ 𝑗 = 𝑀 )
380 379 adantl ( ( 𝑚𝑍𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ) → ¬ 𝑗 = 𝑀 )
381 380 iffalsed ( ( 𝑚𝑍𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ) → if ( 𝑗 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑗 − 1 ) ) ) = ( 𝑔 ‘ ( 𝑗 − 1 ) ) )
382 368 381 eqtrd ( ( 𝑚𝑍𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ) → ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑗 ) = ( 𝑔 ‘ ( 𝑗 − 1 ) ) )
383 382 sbceq1d ( ( 𝑚𝑍𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ) → ( [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑗 ) / 𝑏 ] 𝜑[ ( 𝑔 ‘ ( 𝑗 − 1 ) ) / 𝑏 ] 𝜑 ) )
384 356 383 sbceqbid ( ( 𝑚𝑍𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ) → ( [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑗 − 1 ) ) / 𝑎 ] [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑗 ) / 𝑏 ] 𝜑[ ( 𝑔 ‘ ( ( 𝑗 − 1 ) − 1 ) ) / 𝑎 ] [ ( 𝑔 ‘ ( 𝑗 − 1 ) ) / 𝑏 ] 𝜑 ) )
385 384 biimpar ( ( ( 𝑚𝑍𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ) ∧ [ ( 𝑔 ‘ ( ( 𝑗 − 1 ) − 1 ) ) / 𝑎 ] [ ( 𝑔 ‘ ( 𝑗 − 1 ) ) / 𝑏 ] 𝜑 ) → [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑗 − 1 ) ) / 𝑎 ] [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑗 ) / 𝑏 ] 𝜑 )
386 319 385 syldan ( ( ( 𝑚𝑍𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) → [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑗 − 1 ) ) / 𝑎 ] [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑗 ) / 𝑏 ] 𝜑 )
387 386 an32s ( ( ( 𝑚𝑍 ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) ∧ 𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ) → [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑗 − 1 ) ) / 𝑎 ] [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑗 ) / 𝑏 ] 𝜑 )
388 387 adantlrl ( ( ( 𝑚𝑍 ∧ ( ( 𝑔𝑀 ) = 𝑑 ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) ) ∧ 𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ) → [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑗 − 1 ) ) / 𝑎 ] [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑗 ) / 𝑏 ] 𝜑 )
389 388 adantlll ( ( ( ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑𝑚𝑍 ) ∧ ( ( 𝑔𝑀 ) = 𝑑 ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) ) ∧ 𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ) → [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑗 − 1 ) ) / 𝑎 ] [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑗 ) / 𝑏 ] 𝜑 )
390 293 389 jaodan ( ( ( ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑𝑚𝑍 ) ∧ ( ( 𝑔𝑀 ) = 𝑑 ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) ) ∧ ( 𝑗 = 𝑁𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) ) ) → [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑗 − 1 ) ) / 𝑎 ] [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑗 ) / 𝑏 ] 𝜑 )
391 247 390 syldan ( ( ( ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑𝑚𝑍 ) ∧ ( ( 𝑔𝑀 ) = 𝑑 ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) ) ∧ 𝑗 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) ) → [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑗 − 1 ) ) / 𝑎 ] [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑗 ) / 𝑏 ] 𝜑 )
392 391 ralrimiva ( ( ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑𝑚𝑍 ) ∧ ( ( 𝑔𝑀 ) = 𝑑 ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) ) → ∀ 𝑗 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑗 − 1 ) ) / 𝑎 ] [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑗 ) / 𝑏 ] 𝜑 )
393 fvoveq1 ( 𝑗 = 𝑘 → ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑗 − 1 ) ) = ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑘 − 1 ) ) )
394 fveq2 ( 𝑗 = 𝑘 → ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑗 ) = ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑘 ) )
395 394 sbceq1d ( 𝑗 = 𝑘 → ( [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑗 ) / 𝑏 ] 𝜑[ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑘 ) / 𝑏 ] 𝜑 ) )
396 393 395 sbceqbid ( 𝑗 = 𝑘 → ( [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑗 − 1 ) ) / 𝑎 ] [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑗 ) / 𝑏 ] 𝜑[ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑘 ) / 𝑏 ] 𝜑 ) )
397 396 cbvralvw ( ∀ 𝑗 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑗 − 1 ) ) / 𝑎 ] [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑗 ) / 𝑏 ] 𝜑 ↔ ∀ 𝑘 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑘 ) / 𝑏 ] 𝜑 )
398 392 397 sylib ( ( ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑𝑚𝑍 ) ∧ ( ( 𝑔𝑀 ) = 𝑑 ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) ) → ∀ 𝑘 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑘 ) / 𝑏 ] 𝜑 )
399 398 adantllr ( ( ( ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑𝑐𝐴 ) ∧ 𝑚𝑍 ) ∧ ( ( 𝑔𝑀 ) = 𝑑 ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) ) → ∀ 𝑘 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑘 ) / 𝑏 ] 𝜑 )
400 399 adantrlr ( ( ( ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑𝑐𝐴 ) ∧ 𝑚𝑍 ) ∧ ( ( ( 𝑔𝑀 ) = 𝑑[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) ) → ∀ 𝑘 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑘 ) / 𝑏 ] 𝜑 )
401 400 3adantr1 ( ( ( ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑𝑐𝐴 ) ∧ 𝑚𝑍 ) ∧ ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑔𝑀 ) = 𝑑[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) ) → ∀ 𝑘 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑘 ) / 𝑏 ] 𝜑 )
402 ovex ( 𝑀 ... ( 𝑚 + 1 ) ) ∈ V
403 402 mptex ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ∈ V
404 feq1 ( 𝑓 = ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) → ( 𝑓 : ( 𝑀 ... ( 𝑚 + 1 ) ) ⟶ 𝐴 ↔ ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) : ( 𝑀 ... ( 𝑚 + 1 ) ) ⟶ 𝐴 ) )
405 fveq1 ( 𝑓 = ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) → ( 𝑓𝑀 ) = ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑀 ) )
406 405 eqeq1d ( 𝑓 = ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) → ( ( 𝑓𝑀 ) = 𝑐 ↔ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑀 ) = 𝑐 ) )
407 fveq1 ( 𝑓 = ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) → ( 𝑓 ‘ ( 𝑚 + 1 ) ) = ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑚 + 1 ) ) )
408 407 sbceq1d ( 𝑓 = ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) → ( [ ( 𝑓 ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃[ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 ) )
409 406 408 anbi12d ( 𝑓 = ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) → ( ( ( 𝑓𝑀 ) = 𝑐[ ( 𝑓 ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 ) ↔ ( ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑀 ) = 𝑐[ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 ) ) )
410 fveq1 ( 𝑓 = ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) → ( 𝑓 ‘ ( 𝑘 − 1 ) ) = ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑘 − 1 ) ) )
411 fveq1 ( 𝑓 = ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) → ( 𝑓𝑘 ) = ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑘 ) )
412 411 sbceq1d ( 𝑓 = ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) → ( [ ( 𝑓𝑘 ) / 𝑏 ] 𝜑[ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑘 ) / 𝑏 ] 𝜑 ) )
413 410 412 sbceqbid ( 𝑓 = ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) → ( [ ( 𝑓 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑓𝑘 ) / 𝑏 ] 𝜑[ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑘 ) / 𝑏 ] 𝜑 ) )
414 116 413 bitr3id ( 𝑓 = ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) → ( 𝜒[ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑘 ) / 𝑏 ] 𝜑 ) )
415 414 ralbidv ( 𝑓 = ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) → ( ∀ 𝑘 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) 𝜒 ↔ ∀ 𝑘 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑘 ) / 𝑏 ] 𝜑 ) )
416 404 409 415 3anbi123d ( 𝑓 = ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 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 ) ) ) ) ‘ 𝑘 ) / 𝑏 ] 𝜑 ) ) )
417 403 416 spcev ( ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) : ( 𝑀 ... ( 𝑚 + 1 ) ) ⟶ 𝐴 ∧ ( ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑀 ) = 𝑐[ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( ( 𝑥 ∈ ( 𝑀 ... ( 𝑚 + 1 ) ) ↦ if ( 𝑥 = 𝑀 , 𝑐 , ( 𝑔 ‘ ( 𝑥 − 1 ) ) ) ) ‘ 𝑘 ) / 𝑏 ] 𝜑 ) → ∃ 𝑓 ( 𝑓 : ( 𝑀 ... ( 𝑚 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐[ ( 𝑓 ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) 𝜒 ) )
418 206 213 238 401 417 syl121anc ( ( ( ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑𝑐𝐴 ) ∧ 𝑚𝑍 ) ∧ ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑔𝑀 ) = 𝑑[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) ) → ∃ 𝑓 ( 𝑓 : ( 𝑀 ... ( 𝑚 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐[ ( 𝑓 ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) 𝜒 ) )
419 418 ex ( ( ( [ 𝑐 / 𝑎 ] [ 𝑑 / 𝑏 ] 𝜑𝑐𝐴 ) ∧ 𝑚𝑍 ) → ( ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑔𝑀 ) = 𝑑[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) → ∃ 𝑓 ( 𝑓 : ( 𝑀 ... ( 𝑚 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐[ ( 𝑓 ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) 𝜒 ) ) )
420 146 419 chvarvv ( ( ( [ 𝑑 / 𝑏 ] 𝜑𝑎𝐴 ) ∧ 𝑚𝑍 ) → ( ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑔𝑀 ) = 𝑑[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) → ∃ 𝑓 ( 𝑓 : ( 𝑀 ... ( 𝑚 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎[ ( 𝑓 ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) 𝜒 ) ) )
421 136 420 chvarvv ( ( ( 𝜑𝑎𝐴 ) ∧ 𝑚𝑍 ) → ( ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑔𝑀 ) = 𝑏[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) → ∃ 𝑓 ( 𝑓 : ( 𝑀 ... ( 𝑚 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎[ ( 𝑓 ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) 𝜒 ) ) )
422 421 adantlrr ( ( ( 𝜑 ∧ ( 𝑎𝐴𝑏𝐴 ) ) ∧ 𝑚𝑍 ) → ( ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑔𝑀 ) = 𝑏[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) → ∃ 𝑓 ( 𝑓 : ( 𝑀 ... ( 𝑚 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎[ ( 𝑓 ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) 𝜒 ) ) )
423 422 adantlll ( ( ( ( 𝜂𝜑 ) ∧ ( 𝑎𝐴𝑏𝐴 ) ) ∧ 𝑚𝑍 ) → ( ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑔𝑀 ) = 𝑏[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) → ∃ 𝑓 ( 𝑓 : ( 𝑀 ... ( 𝑚 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎[ ( 𝑓 ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) 𝜒 ) ) )
424 423 imp ( ( ( ( ( 𝜂𝜑 ) ∧ ( 𝑎𝐴𝑏𝐴 ) ) ∧ 𝑚𝑍 ) ∧ ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑔𝑀 ) = 𝑏[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) ) → ∃ 𝑓 ( 𝑓 : ( 𝑀 ... ( 𝑚 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎[ ( 𝑓 ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) 𝜒 ) )
425 oveq2 ( 𝑛 = ( 𝑚 + 1 ) → ( 𝑀 ... 𝑛 ) = ( 𝑀 ... ( 𝑚 + 1 ) ) )
426 425 feq2d ( 𝑛 = ( 𝑚 + 1 ) → ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴𝑓 : ( 𝑀 ... ( 𝑚 + 1 ) ) ⟶ 𝐴 ) )
427 fveq2 ( 𝑛 = ( 𝑚 + 1 ) → ( 𝑓𝑛 ) = ( 𝑓 ‘ ( 𝑚 + 1 ) ) )
428 427 sbceq1d ( 𝑛 = ( 𝑚 + 1 ) → ( [ ( 𝑓𝑛 ) / 𝑎 ] 𝜃[ ( 𝑓 ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 ) )
429 45 428 bitr3id ( 𝑛 = ( 𝑚 + 1 ) → ( 𝜏[ ( 𝑓 ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 ) )
430 429 anbi2d ( 𝑛 = ( 𝑚 + 1 ) → ( ( ( 𝑓𝑀 ) = 𝑎𝜏 ) ↔ ( ( 𝑓𝑀 ) = 𝑎[ ( 𝑓 ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 ) ) )
431 oveq2 ( 𝑛 = ( 𝑚 + 1 ) → ( 𝑁 ... 𝑛 ) = ( 𝑁 ... ( 𝑚 + 1 ) ) )
432 431 raleqdv ( 𝑛 = ( 𝑚 + 1 ) → ( ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ↔ ∀ 𝑘 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) 𝜒 ) )
433 426 430 432 3anbi123d ( 𝑛 = ( 𝑚 + 1 ) → ( ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ↔ ( 𝑓 : ( 𝑀 ... ( 𝑚 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎[ ( 𝑓 ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) 𝜒 ) ) )
434 433 exbidv ( 𝑛 = ( 𝑚 + 1 ) → ( ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ↔ ∃ 𝑓 ( 𝑓 : ( 𝑀 ... ( 𝑚 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎[ ( 𝑓 ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) 𝜒 ) ) )
435 434 rspcev ( ( ( 𝑚 + 1 ) ∈ 𝑍 ∧ ∃ 𝑓 ( 𝑓 : ( 𝑀 ... ( 𝑚 + 1 ) ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎[ ( 𝑓 ‘ ( 𝑚 + 1 ) ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... ( 𝑚 + 1 ) ) 𝜒 ) ) → ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) )
436 128 424 435 syl2anc ( ( ( ( ( 𝜂𝜑 ) ∧ ( 𝑎𝐴𝑏𝐴 ) ) ∧ 𝑚𝑍 ) ∧ ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑔𝑀 ) = 𝑏[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) ) → ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) )
437 436 ex ( ( ( ( 𝜂𝜑 ) ∧ ( 𝑎𝐴𝑏𝐴 ) ) ∧ 𝑚𝑍 ) → ( ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑔𝑀 ) = 𝑏[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) → ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ) )
438 437 exlimdv ( ( ( ( 𝜂𝜑 ) ∧ ( 𝑎𝐴𝑏𝐴 ) ) ∧ 𝑚𝑍 ) → ( ∃ 𝑔 ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑔𝑀 ) = 𝑏[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) → ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ) )
439 438 rexlimdva ( ( ( 𝜂𝜑 ) ∧ ( 𝑎𝐴𝑏𝐴 ) ) → ( ∃ 𝑚𝑍𝑔 ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( ( 𝑔𝑀 ) = 𝑏[ ( 𝑔𝑚 ) / 𝑎 ] 𝜃 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑚 ) [ ( 𝑔 ‘ ( 𝑘 − 1 ) ) / 𝑎 ] [ ( 𝑔𝑘 ) / 𝑏 ] 𝜑 ) → ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ) )
440 126 439 syl5bi ( ( ( 𝜂𝜑 ) ∧ ( 𝑎𝐴𝑏𝐴 ) ) → ( ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑏𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) → ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ) )
441 78 93 440 3syld ( ( ( 𝜂𝜑 ) ∧ ( 𝑎𝐴𝑏𝐴 ) ) → ( ∀ 𝑑 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ¬ 𝑑 𝑅 𝑎 → ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ) )
442 441 an42s ( ( ( 𝜂𝑎𝐴 ) ∧ ( 𝑏𝐴𝜑 ) ) → ( ∀ 𝑑 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ¬ 𝑑 𝑅 𝑎 → ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ) )
443 442 rexlimdvaa ( ( 𝜂𝑎𝐴 ) → ( ∃ 𝑏𝐴 𝜑 → ( ∀ 𝑑 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ¬ 𝑑 𝑅 𝑎 → ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ) ) )
444 443 imp ( ( ( 𝜂𝑎𝐴 ) ∧ ∃ 𝑏𝐴 𝜑 ) → ( ∀ 𝑑 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ¬ 𝑑 𝑅 𝑎 → ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ) )
445 71 444 10 mpjaodan ( ( 𝜂𝑎𝐴 ) → ( ∀ 𝑑 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ¬ 𝑑 𝑅 𝑎 → ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ) )
446 141 anbi1d ( 𝑐 = 𝑎 → ( ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ↔ ( ( 𝑓𝑀 ) = 𝑎𝜏 ) ) )
447 446 3anbi2d ( 𝑐 = 𝑎 → ( ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ↔ ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ) )
448 447 exbidv ( 𝑐 = 𝑎 → ( ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ↔ ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ) )
449 448 rexbidv ( 𝑐 = 𝑎 → ( ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ↔ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ) )
450 449 elrab3 ( 𝑎𝐴 → ( 𝑎 ∈ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ↔ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ) )
451 450 adantl ( ( 𝜂𝑎𝐴 ) → ( 𝑎 ∈ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ↔ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑎𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ) )
452 445 451 sylibrd ( ( 𝜂𝑎𝐴 ) → ( ∀ 𝑑 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ¬ 𝑑 𝑅 𝑎𝑎 ∈ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) )
453 452 ex ( 𝜂 → ( 𝑎𝐴 → ( ∀ 𝑑 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ¬ 𝑑 𝑅 𝑎𝑎 ∈ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ) )
454 453 com23 ( 𝜂 → ( ∀ 𝑑 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ¬ 𝑑 𝑅 𝑎 → ( 𝑎𝐴𝑎 ∈ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ) )
455 eldif ( 𝑎 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ↔ ( 𝑎𝐴 ∧ ¬ 𝑎 ∈ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) )
456 455 notbii ( ¬ 𝑎 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ↔ ¬ ( 𝑎𝐴 ∧ ¬ 𝑎 ∈ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) )
457 iman ( ( 𝑎𝐴𝑎 ∈ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ↔ ¬ ( 𝑎𝐴 ∧ ¬ 𝑎 ∈ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) )
458 456 457 bitr4i ( ¬ 𝑎 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ↔ ( 𝑎𝐴𝑎 ∈ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) )
459 454 458 syl6ibr ( 𝜂 → ( ∀ 𝑑 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ¬ 𝑑 𝑅 𝑎 → ¬ 𝑎 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ) )
460 459 con2d ( 𝜂 → ( 𝑎 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) → ¬ ∀ 𝑑 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ¬ 𝑑 𝑅 𝑎 ) )
461 460 imp ( ( 𝜂𝑎 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ) → ¬ ∀ 𝑑 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ¬ 𝑑 𝑅 𝑎 )
462 461 nrexdv ( 𝜂 → ¬ ∃ 𝑎 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ∀ 𝑑 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ¬ 𝑑 𝑅 𝑎 )
463 df-ne ( ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ≠ ∅ ↔ ¬ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) = ∅ )
464 difss ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ⊆ 𝐴
465 difexg ( 𝐴 ∈ V → ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ∈ V )
466 1 465 ax-mp ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ∈ V
467 fri ( ( ( ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ∈ V ∧ 𝑅 Fr 𝐴 ) ∧ ( ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ⊆ 𝐴 ∧ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ≠ ∅ ) ) → ∃ 𝑎 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ∀ 𝑑 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ¬ 𝑑 𝑅 𝑎 )
468 466 467 mpanl1 ( ( 𝑅 Fr 𝐴 ∧ ( ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ⊆ 𝐴 ∧ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ≠ ∅ ) ) → ∃ 𝑎 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ∀ 𝑑 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ¬ 𝑑 𝑅 𝑎 )
469 468 expr ( ( 𝑅 Fr 𝐴 ∧ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ⊆ 𝐴 ) → ( ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ≠ ∅ → ∃ 𝑎 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ∀ 𝑑 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ¬ 𝑑 𝑅 𝑎 ) )
470 9 464 469 sylancl ( 𝜂 → ( ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ≠ ∅ → ∃ 𝑎 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ∀ 𝑑 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ¬ 𝑑 𝑅 𝑎 ) )
471 463 470 syl5bir ( 𝜂 → ( ¬ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) = ∅ → ∃ 𝑎 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ∀ 𝑑 ∈ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ¬ 𝑑 𝑅 𝑎 ) )
472 462 471 mt3d ( 𝜂 → ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) = ∅ )
473 ssdif0 ( 𝐴 ⊆ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ↔ ( 𝐴 ∖ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) = ∅ )
474 472 473 sylibr ( 𝜂𝐴 ⊆ { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } )
475 81 a1i ( 𝜂 → { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ⊆ 𝐴 )
476 474 475 eqssd ( 𝜂𝐴 = { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } )
477 rabid2 ( 𝐴 = { 𝑐𝐴 ∣ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ↔ ∀ 𝑐𝐴𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) )
478 476 477 sylib ( 𝜂 → ∀ 𝑐𝐴𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) )
479 eqeq2 ( 𝑐 = 𝐶 → ( ( 𝑓𝑀 ) = 𝑐 ↔ ( 𝑓𝑀 ) = 𝐶 ) )
480 479 anbi1d ( 𝑐 = 𝐶 → ( ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ↔ ( ( 𝑓𝑀 ) = 𝐶𝜏 ) ) )
481 480 3anbi2d ( 𝑐 = 𝐶 → ( ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ↔ ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝐶𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ) )
482 481 exbidv ( 𝑐 = 𝐶 → ( ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ↔ ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝐶𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ) )
483 482 rexbidv ( 𝑐 = 𝐶 → ( ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ↔ ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝐶𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ) )
484 483 rspcva ( ( 𝐶𝐴 ∧ ∀ 𝑐𝐴𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝑐𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ) → ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝐶𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) )
485 8 478 484 syl2anc ( 𝜂 → ∃ 𝑛𝑍𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓𝑀 ) = 𝐶𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) )