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