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 imbitrdi ⊢ ( ( ( 𝜂 ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( 𝑏 ∈ ( 𝐴 ∖ { 𝑐 ∈ 𝐴 ∣ ∃ 𝑛 ∈ 𝑍 ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓 ‘ 𝑀 ) = 𝑐 ∧ 𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) → ¬ ∀ 𝑑 ∈ ( 𝐴 ∖ { 𝑐 ∈ 𝐴 ∣ ∃ 𝑛 ∈ 𝑍 ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓 ‘ 𝑀 ) = 𝑐 ∧ 𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ¬ 𝑑 𝑅 𝑎 ) )
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 bitrid ⊢ ( 𝑏 ∈ 𝐴 → ( 𝑏 ∈ ( 𝐴 ∖ ( 𝐴 ∖ { 𝑐 ∈ 𝐴 ∣ ∃ 𝑛 ∈ 𝑍 ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓 ‘ 𝑀 ) = 𝑐 ∧ 𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ) ↔ ∃ 𝑛 ∈ 𝑍 ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓 ‘ 𝑀 ) = 𝑏 ∧ 𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ) )
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 biimtrdi ⊢ ( 𝑥 = 𝑀 → ( 𝑥 ∈ ( ( 𝑀 + 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 ffvelcdm ⊢ ( ( 𝑔 : ( 𝑀 ... 𝑚 ) ⟶ 𝐴 ∧ ( 𝑥 − 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 biimtrdi ⊢ ( 𝑗 = ( 𝑀 + 1 ) → ( 𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) → ( 𝑁 + 1 ) ≤ ( 𝑀 + 1 ) ) )
350 349 com12 ⊢ ( 𝑗 ∈ ( ( 𝑁 + 1 ) ... ( 𝑚 + 1 ) ) → ( 𝑗 = ( 𝑀 + 1 ) → ( 𝑁 + 1 ) ≤ ( 𝑀 + 1 ) ) )
351 346 350 biimtrid ⊢ ( 𝑗 ∈ ( ( 𝑁 + 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 biimtrdi ⊢ ( 𝑗 = 𝑀 → ( 𝑗 ∈ ( ( 𝑁 + 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 biimtrid ⊢ ( ( ( 𝜂 ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( ∃ 𝑛 ∈ 𝑍 ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓 ‘ 𝑀 ) = 𝑏 ∧ 𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) → ∃ 𝑛 ∈ 𝑍 ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓 ‘ 𝑀 ) = 𝑎 ∧ 𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ) )
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 imbitrrdi ⊢ ( 𝜂 → ( ∀ 𝑑 ∈ ( 𝐴 ∖ { 𝑐 ∈ 𝐴 ∣ ∃ 𝑛 ∈ 𝑍 ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓 ‘ 𝑀 ) = 𝑐 ∧ 𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ¬ 𝑑 𝑅 𝑎 → ¬ 𝑎 ∈ ( 𝐴 ∖ { 𝑐 ∈ 𝐴 ∣ ∃ 𝑛 ∈ 𝑍 ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓 ‘ 𝑀 ) = 𝑐 ∧ 𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ) )
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 biimtrrid ⊢ ( 𝜂 → ( ¬ ( 𝐴 ∖ { 𝑐 ∈ 𝐴 ∣ ∃ 𝑛 ∈ 𝑍 ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓 ‘ 𝑀 ) = 𝑐 ∧ 𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) = ∅ → ∃ 𝑎 ∈ ( 𝐴 ∖ { 𝑐 ∈ 𝐴 ∣ ∃ 𝑛 ∈ 𝑍 ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓 ‘ 𝑀 ) = 𝑐 ∧ 𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ∀ 𝑑 ∈ ( 𝐴 ∖ { 𝑐 ∈ 𝐴 ∣ ∃ 𝑛 ∈ 𝑍 ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓 ‘ 𝑀 ) = 𝑐 ∧ 𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) } ) ¬ 𝑑 𝑅 𝑎 ) )
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 ⊢ ( 𝜂 → ∃ 𝑛 ∈ 𝑍 ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓 ‘ 𝑀 ) = 𝐶 ∧ 𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) )