Step | Hyp | Ref
| Expression |
1 | | fdc.8 |
. 2
⊢ (𝜂 → 𝐶 ∈ 𝐴) |
2 | | fdc.2 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑀 ∈ ℤ |
3 | | uzid 11702 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
4 | 2, 3 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑀 ∈
(ℤ≥‘𝑀) |
5 | | fdc.3 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑍 =
(ℤ≥‘𝑀) |
6 | 4, 5 | eleqtrri 2700 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑀 ∈ 𝑍 |
7 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
{〈𝑀, 𝑎〉} = {〈𝑀, 𝑎〉} |
8 | 2 | elexi 3213 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑀 ∈ V |
9 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑎 ∈ V |
10 | 8, 9 | fsn 6402 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
({〈𝑀, 𝑎〉}:{𝑀}⟶{𝑎} ↔ {〈𝑀, 𝑎〉} = {〈𝑀, 𝑎〉}) |
11 | 7, 10 | mpbir 221 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
{〈𝑀, 𝑎〉}:{𝑀}⟶{𝑎} |
12 | | snssi 4339 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 ∈ 𝐴 → {𝑎} ⊆ 𝐴) |
13 | | fss 6056 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(({〈𝑀, 𝑎〉}:{𝑀}⟶{𝑎} ∧ {𝑎} ⊆ 𝐴) → {〈𝑀, 𝑎〉}:{𝑀}⟶𝐴) |
14 | 11, 12, 13 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ∈ 𝐴 → {〈𝑀, 𝑎〉}:{𝑀}⟶𝐴) |
15 | | fzsn 12383 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀}) |
16 | 2, 15 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀...𝑀) = {𝑀} |
17 | 16 | feq2i 6037 |
. . . . . . . . . . . . . . . . . . . 20
⊢
({〈𝑀, 𝑎〉}:(𝑀...𝑀)⟶𝐴 ↔ {〈𝑀, 𝑎〉}:{𝑀}⟶𝐴) |
18 | 14, 17 | sylibr 224 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 ∈ 𝐴 → {〈𝑀, 𝑎〉}:(𝑀...𝑀)⟶𝐴) |
19 | 18 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ 𝐴 ∧ 𝜃) → {〈𝑀, 𝑎〉}:(𝑀...𝑀)⟶𝐴) |
20 | 8, 9 | fvsn 6446 |
. . . . . . . . . . . . . . . . . . 19
⊢
({〈𝑀, 𝑎〉}‘𝑀) = 𝑎 |
21 | 20 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ 𝐴 ∧ 𝜃) → ({〈𝑀, 𝑎〉}‘𝑀) = 𝑎) |
22 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ 𝐴 ∧ 𝜃) → 𝜃) |
23 | | snex 4908 |
. . . . . . . . . . . . . . . . . . 19
⊢
{〈𝑀, 𝑎〉} ∈
V |
24 | | feq1 6026 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = {〈𝑀, 𝑎〉} → (𝑓:(𝑀...𝑀)⟶𝐴 ↔ {〈𝑀, 𝑎〉}:(𝑀...𝑀)⟶𝐴)) |
25 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 = {〈𝑀, 𝑎〉} → (𝑓‘𝑀) = ({〈𝑀, 𝑎〉}‘𝑀)) |
26 | 25 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = {〈𝑀, 𝑎〉} → ((𝑓‘𝑀) = 𝑎 ↔ ({〈𝑀, 𝑎〉}‘𝑀) = 𝑎)) |
27 | 25, 20 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 = {〈𝑀, 𝑎〉} → (𝑓‘𝑀) = 𝑎) |
28 | | sbceq2a 3447 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑓‘𝑀) = 𝑎 → ([(𝑓‘𝑀) / 𝑎]𝜃 ↔ 𝜃)) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = {〈𝑀, 𝑎〉} → ([(𝑓‘𝑀) / 𝑎]𝜃 ↔ 𝜃)) |
30 | 26, 29 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = {〈𝑀, 𝑎〉} → (((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃) ↔ (({〈𝑀, 𝑎〉}‘𝑀) = 𝑎 ∧ 𝜃))) |
31 | 24, 30 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = {〈𝑀, 𝑎〉} → ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃)) ↔ ({〈𝑀, 𝑎〉}:(𝑀...𝑀)⟶𝐴 ∧ (({〈𝑀, 𝑎〉}‘𝑀) = 𝑎 ∧ 𝜃)))) |
32 | 23, 31 | spcev 3300 |
. . . . . . . . . . . . . . . . . 18
⊢
(({〈𝑀, 𝑎〉}:(𝑀...𝑀)⟶𝐴 ∧ (({〈𝑀, 𝑎〉}‘𝑀) = 𝑎 ∧ 𝜃)) → ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃))) |
33 | 19, 21, 22, 32 | syl12anc 1324 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ 𝐴 ∧ 𝜃) → ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃))) |
34 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = 𝑀 → (𝑀...𝑛) = (𝑀...𝑀)) |
35 | 34 | feq2d 6031 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑀 → (𝑓:(𝑀...𝑛)⟶𝐴 ↔ 𝑓:(𝑀...𝑀)⟶𝐴)) |
36 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓‘𝑛) ∈ V |
37 | | fdc.7 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑎 = (𝑓‘𝑛) → (𝜃 ↔ 𝜏)) |
38 | 36, 37 | sbcie 3470 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
([(𝑓‘𝑛) / 𝑎]𝜃 ↔ 𝜏) |
39 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 = 𝑀 → (𝑓‘𝑛) = (𝑓‘𝑀)) |
40 | 39 | sbceq1d 3440 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = 𝑀 → ([(𝑓‘𝑛) / 𝑎]𝜃 ↔ [(𝑓‘𝑀) / 𝑎]𝜃)) |
41 | 38, 40 | syl5bbr 274 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = 𝑀 → (𝜏 ↔ [(𝑓‘𝑀) / 𝑎]𝜃)) |
42 | 41 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑀 → (((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ↔ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃))) |
43 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = 𝑀 → (𝑁...𝑛) = (𝑁...𝑀)) |
44 | | fdc.4 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑁 = (𝑀 + 1) |
45 | 44 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁...𝑀) = ((𝑀 + 1)...𝑀) |
46 | 2 | zrei 11383 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝑀 ∈ ℝ |
47 | 46 | ltp1i 10927 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑀 < (𝑀 + 1) |
48 | | peano2z 11418 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑀 ∈ ℤ → (𝑀 + 1) ∈
ℤ) |
49 | 2, 48 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑀 + 1) ∈
ℤ |
50 | | fzn 12357 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑀 + 1) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 < (𝑀 + 1) ↔ ((𝑀 + 1)...𝑀) = ∅)) |
51 | 49, 2, 50 | mp2an 708 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑀 < (𝑀 + 1) ↔ ((𝑀 + 1)...𝑀) = ∅) |
52 | 47, 51 | mpbi 220 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑀 + 1)...𝑀) = ∅ |
53 | 45, 52 | eqtri 2644 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁...𝑀) = ∅ |
54 | 43, 53 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = 𝑀 → (𝑁...𝑛) = ∅) |
55 | 54 | raleqdv 3144 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑀 → (∀𝑘 ∈ (𝑁...𝑛)𝜒 ↔ ∀𝑘 ∈ ∅ 𝜒)) |
56 | 35, 42, 55 | 3anbi123d 1399 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑀 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃) ∧ ∀𝑘 ∈ ∅ 𝜒))) |
57 | | ral0 4076 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
∀𝑘 ∈
∅ 𝜒 |
58 | | df-3an 1039 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃) ∧ ∀𝑘 ∈ ∅ 𝜒) ↔ ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃)) ∧ ∀𝑘 ∈ ∅ 𝜒)) |
59 | 57, 58 | mpbiran2 954 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃) ∧ ∀𝑘 ∈ ∅ 𝜒) ↔ (𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃))) |
60 | 56, 59 | syl6bb 276 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑀 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃)))) |
61 | 60 | exbidv 1850 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑀 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃)))) |
62 | 61 | rspcev 3309 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ 𝑍 ∧ ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃))) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)) |
63 | 6, 33, 62 | sylancr 695 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ 𝐴 ∧ 𝜃) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)) |
64 | 63 | adantll 750 |
. . . . . . . . . . . . . . 15
⊢ (((𝜂 ∧ 𝑎 ∈ 𝐴) ∧ 𝜃) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)) |
65 | 64 | a1d 25 |
. . . . . . . . . . . . . 14
⊢ (((𝜂 ∧ 𝑎 ∈ 𝐴) ∧ 𝜃) → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))) |
66 | | fdc.11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑏𝑅𝑎) |
67 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑑 = 𝑏 → (𝑑𝑅𝑎 ↔ 𝑏𝑅𝑎)) |
68 | 67 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∧ 𝑏𝑅𝑎) → ∃𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎) |
69 | 68 | expcom 451 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏𝑅𝑎 → (𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎)) |
70 | 66, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎)) |
71 | | dfrex2 2996 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∃𝑑 ∈
(𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎 ↔ ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎) |
72 | 70, 71 | syl6ib 241 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)) |
73 | 72 | con2d 129 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ¬ 𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))) |
74 | | eldif 3584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) ↔ (𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))) |
75 | 74 | simplbi2 655 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 ∈ 𝐴 → (¬ 𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → 𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))) |
76 | | ssrab2 3687 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ⊆ 𝐴 |
77 | | dfss4 3858 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ({𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ⊆ 𝐴 ↔ (𝐴 ∖ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) = {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) |
78 | 76, 77 | mpbi 220 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐴 ∖ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) = {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} |
79 | 78 | eleq2i 2693 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) ↔ 𝑏 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) |
80 | | eqeq2 2633 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑐 = 𝑏 → ((𝑓‘𝑀) = 𝑐 ↔ (𝑓‘𝑀) = 𝑏)) |
81 | 80 | anbi1d 741 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑐 = 𝑏 → (((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ↔ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏))) |
82 | 81 | 3anbi2d 1404 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑐 = 𝑏 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))) |
83 | 82 | exbidv 1850 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑐 = 𝑏 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))) |
84 | 83 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑐 = 𝑏 → (∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))) |
85 | 84 | elrab3 3364 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 ∈ 𝐴 → (𝑏 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))) |
86 | 79, 85 | syl5bb 272 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 ∈ 𝐴 → (𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) ↔ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))) |
87 | 75, 86 | sylibd 229 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 ∈ 𝐴 → (¬ 𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))) |
88 | 87 | ad2antll 765 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (¬ 𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))) |
89 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 = 𝑚 → (𝑀...𝑛) = (𝑀...𝑚)) |
90 | 89 | feq2d 6031 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = 𝑚 → (𝑓:(𝑀...𝑛)⟶𝐴 ↔ 𝑓:(𝑀...𝑚)⟶𝐴)) |
91 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 = 𝑚 → (𝑓‘𝑛) = (𝑓‘𝑚)) |
92 | 91 | sbceq1d 3440 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 = 𝑚 → ([(𝑓‘𝑛) / 𝑎]𝜃 ↔ [(𝑓‘𝑚) / 𝑎]𝜃)) |
93 | 38, 92 | syl5bbr 274 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 = 𝑚 → (𝜏 ↔ [(𝑓‘𝑚) / 𝑎]𝜃)) |
94 | 93 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = 𝑚 → (((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ↔ ((𝑓‘𝑀) = 𝑏 ∧ [(𝑓‘𝑚) / 𝑎]𝜃))) |
95 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 = 𝑚 → (𝑁...𝑛) = (𝑁...𝑚)) |
96 | 95 | raleqdv 3144 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = 𝑚 → (∀𝑘 ∈ (𝑁...𝑛)𝜒 ↔ ∀𝑘 ∈ (𝑁...𝑚)𝜒)) |
97 | 90, 94, 96 | 3anbi123d 1399 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = 𝑚 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ [(𝑓‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒))) |
98 | 97 | exbidv 1850 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑚 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ [(𝑓‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒))) |
99 | 98 | cbvrexv 3172 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∃𝑛 ∈
𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑚 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ [(𝑓‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒)) |
100 | | feq1 6026 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 = 𝑔 → (𝑓:(𝑀...𝑚)⟶𝐴 ↔ 𝑔:(𝑀...𝑚)⟶𝐴)) |
101 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓 = 𝑔 → (𝑓‘𝑀) = (𝑔‘𝑀)) |
102 | 101 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓 = 𝑔 → ((𝑓‘𝑀) = 𝑏 ↔ (𝑔‘𝑀) = 𝑏)) |
103 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓 = 𝑔 → (𝑓‘𝑚) = (𝑔‘𝑚)) |
104 | 103 | sbceq1d 3440 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓 = 𝑔 → ([(𝑓‘𝑚) / 𝑎]𝜃 ↔ [(𝑔‘𝑚) / 𝑎]𝜃)) |
105 | 102, 104 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 = 𝑔 → (((𝑓‘𝑀) = 𝑏 ∧ [(𝑓‘𝑚) / 𝑎]𝜃) ↔ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃))) |
106 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓‘(𝑘 − 1)) ∈ V |
107 | | fdc.5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑎 = (𝑓‘(𝑘 − 1)) → (𝜑 ↔ 𝜓)) |
108 | 107 | sbcbidv 3490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑎 = (𝑓‘(𝑘 − 1)) → ([(𝑓‘𝑘) / 𝑏]𝜑 ↔ [(𝑓‘𝑘) / 𝑏]𝜓)) |
109 | 106, 108 | sbcie 3470 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓‘𝑘) / 𝑏]𝜑 ↔ [(𝑓‘𝑘) / 𝑏]𝜓) |
110 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓‘𝑘) ∈ V |
111 | | fdc.6 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑏 = (𝑓‘𝑘) → (𝜓 ↔ 𝜒)) |
112 | 110, 111 | sbcie 3470 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
([(𝑓‘𝑘) / 𝑏]𝜓 ↔ 𝜒) |
113 | 109, 112 | bitri 264 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓‘𝑘) / 𝑏]𝜑 ↔ 𝜒) |
114 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓 = 𝑔 → (𝑓‘(𝑘 − 1)) = (𝑔‘(𝑘 − 1))) |
115 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓 = 𝑔 → (𝑓‘𝑘) = (𝑔‘𝑘)) |
116 | 115 | sbceq1d 3440 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓 = 𝑔 → ([(𝑓‘𝑘) / 𝑏]𝜑 ↔ [(𝑔‘𝑘) / 𝑏]𝜑)) |
117 | 114, 116 | sbceqbid 3442 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓 = 𝑔 → ([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓‘𝑘) / 𝑏]𝜑 ↔ [(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) |
118 | 113, 117 | syl5bbr 274 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓 = 𝑔 → (𝜒 ↔ [(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) |
119 | 118 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 = 𝑔 → (∀𝑘 ∈ (𝑁...𝑚)𝜒 ↔ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) |
120 | 100, 105,
119 | 3anbi123d 1399 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 = 𝑔 → ((𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ [(𝑓‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒) ↔ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑))) |
121 | 120 | cbvexv 2275 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∃𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ [(𝑓‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒) ↔ ∃𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) |
122 | 121 | rexbii 3041 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∃𝑚 ∈
𝑍 ∃𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ [(𝑓‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒) ↔ ∃𝑚 ∈ 𝑍 ∃𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) |
123 | 99, 122 | bitri 264 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑛 ∈
𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑚 ∈ 𝑍 ∃𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) |
124 | 5 | peano2uzs 11742 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑚 ∈ 𝑍 → (𝑚 + 1) ∈ 𝑍) |
125 | 124 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑚 ∈ 𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → (𝑚 + 1) ∈ 𝑍) |
126 | | sbceq2a 3447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑑 = 𝑏 → ([𝑑 / 𝑏]𝜑 ↔ 𝜑)) |
127 | 126 | anbi1d 741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑑 = 𝑏 → (([𝑑 / 𝑏]𝜑 ∧ 𝑎 ∈ 𝐴) ↔ (𝜑 ∧ 𝑎 ∈ 𝐴))) |
128 | 127 | anbi1d 741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑑 = 𝑏 → ((([𝑑 / 𝑏]𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ↔ ((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍))) |
129 | | eqeq2 2633 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑑 = 𝑏 → ((𝑔‘𝑀) = 𝑑 ↔ (𝑔‘𝑀) = 𝑏)) |
130 | 129 | anbi1d 741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑑 = 𝑏 → (((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ↔ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃))) |
131 | 130 | 3anbi2d 1404 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑑 = 𝑏 → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) ↔ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑))) |
132 | 131 | imbi1d 331 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑑 = 𝑏 → (((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)) ↔ ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))) |
133 | 128, 132 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑑 = 𝑏 → (((([𝑑 / 𝑏]𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))) ↔ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))))) |
134 | | sbceq2a 3447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑐 = 𝑎 → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑏]𝜑)) |
135 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑐 = 𝑎 → (𝑐 ∈ 𝐴 ↔ 𝑎 ∈ 𝐴)) |
136 | 134, 135 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑐 = 𝑎 → (([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ↔ ([𝑑 / 𝑏]𝜑 ∧ 𝑎 ∈ 𝐴))) |
137 | 136 | anbi1d 741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑐 = 𝑎 → ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ↔ (([𝑑 / 𝑏]𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍))) |
138 | | eqeq2 2633 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑐 = 𝑎 → ((𝑓‘𝑀) = 𝑐 ↔ (𝑓‘𝑀) = 𝑎)) |
139 | 138 | anbi1d 741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑐 = 𝑎 → (((𝑓‘𝑀) = 𝑐 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ↔ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃))) |
140 | 139 | 3anbi2d 1404 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑐 = 𝑎 → ((𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒) ↔ (𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))) |
141 | 140 | exbidv 1850 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑐 = 𝑎 → (∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒) ↔ ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))) |
142 | 141 | imbi2d 330 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑐 = 𝑎 → (((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)) ↔ ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))) |
143 | 137, 142 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑐 = 𝑎 → (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))) ↔ ((([𝑑 / 𝑏]𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))))) |
144 | | peano2uz 11741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑚 ∈
(ℤ≥‘𝑀) → (𝑚 + 1) ∈
(ℤ≥‘𝑀)) |
145 | 144, 5 | eleq2s 2719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑚 ∈ 𝑍 → (𝑚 + 1) ∈
(ℤ≥‘𝑀)) |
146 | | elfzp12 12419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑚 + 1) ∈
(ℤ≥‘𝑀) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↔ (𝑥 = 𝑀 ∨ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))))) |
147 | 145, 146 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑚 ∈ 𝑍 → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↔ (𝑥 = 𝑀 ∨ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))))) |
148 | 147 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝑐 ∈ 𝐴 ∧ 𝑚 ∈ 𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↔ (𝑥 = 𝑀 ∨ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))))) |
149 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑥 = 𝑀 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = 𝑐) |
150 | 149 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑥 = 𝑀 → (if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴 ↔ 𝑐 ∈ 𝐴)) |
151 | 150 | biimprcd 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑐 ∈ 𝐴 → (𝑥 = 𝑀 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴)) |
152 | 151 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝑐 ∈ 𝐴 ∧ 𝑚 ∈ 𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 = 𝑀 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴)) |
153 | | 1re 10039 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ 1 ∈
ℝ |
154 | 46, 153 | readdcli 10053 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝑀 + 1) ∈
ℝ |
155 | 46, 154 | ltnlei 10158 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝑀 < (𝑀 + 1) ↔ ¬ (𝑀 + 1) ≤ 𝑀) |
156 | 47, 155 | mpbi 220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ¬
(𝑀 + 1) ≤ 𝑀 |
157 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝑥 = 𝑀 → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) ↔ 𝑀 ∈ ((𝑀 + 1)...(𝑚 + 1)))) |
158 | | elfzle1 12344 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝑀 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑀 + 1) ≤ 𝑀) |
159 | 157, 158 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝑥 = 𝑀 → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑀 + 1) ≤ 𝑀)) |
160 | 159 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 = 𝑀 → (𝑀 + 1) ≤ 𝑀)) |
161 | 156, 160 | mtoi 190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → ¬ 𝑥 = 𝑀) |
162 | 161 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑚 ∈ 𝑍 ∧ 𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → ¬ 𝑥 = 𝑀) |
163 | 162 | iffalsed 4097 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝑚 ∈ 𝑍 ∧ 𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = (𝑔‘(𝑥 − 1))) |
164 | | elfzelz 12342 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → 𝑥 ∈ ℤ) |
165 | 164 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → 𝑥 ∈ ℤ) |
166 | | eluzelz 11697 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ (𝑚 ∈
(ℤ≥‘𝑀) → 𝑚 ∈ ℤ) |
167 | 166, 5 | eleq2s 2719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ (𝑚 ∈ 𝑍 → 𝑚 ∈ ℤ) |
168 | 167 | peano2zd 11485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ (𝑚 ∈ 𝑍 → (𝑚 + 1) ∈ ℤ) |
169 | | 1z 11407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ 1 ∈
ℤ |
170 | | fzsubel 12377 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢ ((((𝑀 + 1) ∈ ℤ ∧
(𝑚 + 1) ∈ ℤ)
∧ (𝑥 ∈ ℤ
∧ 1 ∈ ℤ)) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) ↔ (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)))) |
171 | 170 | biimpd 219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ ((((𝑀 + 1) ∈ ℤ ∧
(𝑚 + 1) ∈ ℤ)
∧ (𝑥 ∈ ℤ
∧ 1 ∈ ℤ)) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)))) |
172 | 169, 171 | mpanr2 720 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ ((((𝑀 + 1) ∈ ℤ ∧
(𝑚 + 1) ∈ ℤ)
∧ 𝑥 ∈ ℤ)
→ (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)))) |
173 | 49, 172 | mpanl1 716 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ (((𝑚 + 1) ∈ ℤ ∧ 𝑥 ∈ ℤ) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)))) |
174 | 173 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((𝑚 + 1) ∈ ℤ →
(𝑥 ∈ ℤ →
(𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))))) |
175 | 168, 174 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (𝑚 ∈ 𝑍 → (𝑥 ∈ ℤ → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))))) |
176 | 175 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (𝑚 ∈ 𝑍 → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 ∈ ℤ → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))))) |
177 | 176 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑥 ∈ ℤ → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)))) |
178 | 165, 177 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))) |
179 | 46 | recni 10052 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ 𝑀 ∈ ℂ |
180 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ 1 ∈
ℂ |
181 | 179, 180 | pncan3oi 10297 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((𝑀 + 1) − 1) = 𝑀 |
182 | 181 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (𝑚 ∈ 𝑍 → ((𝑀 + 1) − 1) = 𝑀) |
183 | 167 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (𝑚 ∈ 𝑍 → 𝑚 ∈ ℂ) |
184 | | pncan 10287 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((𝑚 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑚 + 1)
− 1) = 𝑚) |
185 | 183, 180,
184 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (𝑚 ∈ 𝑍 → ((𝑚 + 1) − 1) = 𝑚) |
186 | 182, 185 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝑚 ∈ 𝑍 → (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑀...𝑚)) |
187 | 186 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑀...𝑚)) |
188 | 178, 187 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑥 − 1) ∈ (𝑀...𝑚)) |
189 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ (𝑥 − 1) ∈ (𝑀...𝑚)) → (𝑔‘(𝑥 − 1)) ∈ 𝐴) |
190 | 188, 189 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ (𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)))) → (𝑔‘(𝑥 − 1)) ∈ 𝐴) |
191 | 190 | anassrs 680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑔:(𝑀...𝑚)⟶𝐴 ∧ 𝑚 ∈ 𝑍) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑔‘(𝑥 − 1)) ∈ 𝐴) |
192 | 191 | ancom1s 847 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝑚 ∈ 𝑍 ∧ 𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑔‘(𝑥 − 1)) ∈ 𝐴) |
193 | 163, 192 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑚 ∈ 𝑍 ∧ 𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴) |
194 | 193 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴)) |
195 | 194 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝑐 ∈ 𝐴 ∧ 𝑚 ∈ 𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴)) |
196 | 152, 195 | jaod 395 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝑐 ∈ 𝐴 ∧ 𝑚 ∈ 𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → ((𝑥 = 𝑀 ∨ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴)) |
197 | 148, 196 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝑐 ∈ 𝐴 ∧ 𝑚 ∈ 𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴)) |
198 | 197 | ralrimiv 2965 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝑐 ∈ 𝐴 ∧ 𝑚 ∈ 𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → ∀𝑥 ∈ (𝑀...(𝑚 + 1))if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴) |
199 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) |
200 | 199 | fmpt 6381 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(∀𝑥 ∈
(𝑀...(𝑚 + 1))if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴 ↔ (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴) |
201 | 198, 200 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑐 ∈ 𝐴 ∧ 𝑚 ∈ 𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴) |
202 | 201 | adantlll 754 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((([𝑐 /
𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴) |
203 | 202 | 3ad2antr1 1226 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((([𝑐 /
𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴) |
204 | | eluzfz1 12348 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑚 + 1) ∈
(ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...(𝑚 + 1))) |
205 | 144, 204 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑚 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...(𝑚 + 1))) |
206 | 205, 5 | eleq2s 2719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑚 ∈ 𝑍 → 𝑀 ∈ (𝑀...(𝑚 + 1))) |
207 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ 𝑐 ∈ V |
208 | 149, 199,
207 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑀 ∈ (𝑀...(𝑚 + 1)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐) |
209 | 206, 208 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑚 ∈ 𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐) |
210 | 209 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((([𝑐 /
𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐) |
211 | | eluzfz2 12349 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑚 + 1) ∈
(ℤ≥‘𝑀) → (𝑚 + 1) ∈ (𝑀...(𝑚 + 1))) |
212 | 144, 211 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑚 ∈
(ℤ≥‘𝑀) → (𝑚 + 1) ∈ (𝑀...(𝑚 + 1))) |
213 | 212, 5 | eleq2s 2719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑚 ∈ 𝑍 → (𝑚 + 1) ∈ (𝑀...(𝑚 + 1))) |
214 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑥 = (𝑚 + 1) → (𝑥 = 𝑀 ↔ (𝑚 + 1) = 𝑀)) |
215 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑥 = (𝑚 + 1) → (𝑥 − 1) = ((𝑚 + 1) − 1)) |
216 | 215 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑥 = (𝑚 + 1) → (𝑔‘(𝑥 − 1)) = (𝑔‘((𝑚 + 1) − 1))) |
217 | 214, 216 | ifbieq2d 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑥 = (𝑚 + 1) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1)))) |
218 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑔‘((𝑚 + 1) − 1)) ∈ V |
219 | 207, 218 | ifex 4156 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1))) ∈ V |
220 | 217, 199,
219 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑚 + 1) ∈ (𝑀...(𝑚 + 1)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) = if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1)))) |
221 | 213, 220 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑚 ∈ 𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) = if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1)))) |
222 | | eluzle 11700 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑚 ∈
(ℤ≥‘𝑀) → 𝑀 ≤ 𝑚) |
223 | 222, 5 | eleq2s 2719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑚 ∈ 𝑍 → 𝑀 ≤ 𝑚) |
224 | | zleltp1 11428 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑀 ≤ 𝑚 ↔ 𝑀 < (𝑚 + 1))) |
225 | 2, 167, 224 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑚 ∈ 𝑍 → (𝑀 ≤ 𝑚 ↔ 𝑀 < (𝑚 + 1))) |
226 | 223, 225 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑚 ∈ 𝑍 → 𝑀 < (𝑚 + 1)) |
227 | | ltne 10134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑀 ∈ ℝ ∧ 𝑀 < (𝑚 + 1)) → (𝑚 + 1) ≠ 𝑀) |
228 | 46, 226, 227 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑚 ∈ 𝑍 → (𝑚 + 1) ≠ 𝑀) |
229 | 228 | neneqd 2799 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑚 ∈ 𝑍 → ¬ (𝑚 + 1) = 𝑀) |
230 | 229 | iffalsed 4097 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑚 ∈ 𝑍 → if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1))) = (𝑔‘((𝑚 + 1) − 1))) |
231 | 185 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑚 ∈ 𝑍 → (𝑔‘((𝑚 + 1) − 1)) = (𝑔‘𝑚)) |
232 | 221, 230,
231 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑚 ∈ 𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) = (𝑔‘𝑚)) |
233 | 232 | sbceq1d 3440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑚 ∈ 𝑍 → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃 ↔ [(𝑔‘𝑚) / 𝑎]𝜃)) |
234 | 233 | biimpar 502 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑚 ∈ 𝑍 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃) |
235 | 234 | ad2ant2l 782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((([𝑐 /
𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃)) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃) |
236 | 235 | 3ad2antr2 1227 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((([𝑐 /
𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃) |
237 | | eluzp1p1 11713 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑚 ∈
(ℤ≥‘𝑀) → (𝑚 + 1) ∈
(ℤ≥‘(𝑀 + 1))) |
238 | 237, 5 | eleq2s 2719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑚 ∈ 𝑍 → (𝑚 + 1) ∈
(ℤ≥‘(𝑀 + 1))) |
239 | 44 | fveq2i 6194 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢
(ℤ≥‘𝑁) = (ℤ≥‘(𝑀 + 1)) |
240 | 238, 239 | syl6eleqr 2712 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑚 ∈ 𝑍 → (𝑚 + 1) ∈
(ℤ≥‘𝑁)) |
241 | | elfzp12 12419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑚 + 1) ∈
(ℤ≥‘𝑁) → (𝑗 ∈ (𝑁...(𝑚 + 1)) ↔ (𝑗 = 𝑁 ∨ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))))) |
242 | 240, 241 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑚 ∈ 𝑍 → (𝑗 ∈ (𝑁...(𝑚 + 1)) ↔ (𝑗 = 𝑁 ∨ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))))) |
243 | 242 | biimpa 501 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ (𝑁...(𝑚 + 1))) → (𝑗 = 𝑁 ∨ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)))) |
244 | 243 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ 𝑗 ∈ (𝑁...(𝑚 + 1))) → (𝑗 = 𝑁 ∨ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)))) |
245 | 244 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((([𝑐 /
𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) ∧ 𝑗 ∈ (𝑁...(𝑚 + 1))) → (𝑗 = 𝑁 ∨ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)))) |
246 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (𝑗 = 𝑁 → (𝑗 − 1) = (𝑁 − 1)) |
247 | 44 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ (𝑁 − 1) = ((𝑀 + 1) −
1) |
248 | 247, 181 | eqtri 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (𝑁 − 1) = 𝑀 |
249 | 246, 248 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (𝑗 = 𝑁 → (𝑗 − 1) = 𝑀) |
250 | 249 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝑗 = 𝑁 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀)) |
251 | 250 | ad2antll 765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀)) |
252 | 209 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐) |
253 | 251, 252 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = 𝑐) |
254 | 44 | eqeq2i 2634 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (𝑗 = 𝑁 ↔ 𝑗 = (𝑀 + 1)) |
255 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (𝑗 = (𝑀 + 1) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1))) |
256 | 254, 255 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (𝑗 = 𝑁 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1))) |
257 | 256 | ad2antll 765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1))) |
258 | 46, 154, 47 | ltleii 10160 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ 𝑀 ≤ (𝑀 + 1) |
259 | | eluz2 11693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ ((𝑀 + 1) ∈
(ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑀 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑀 + 1))) |
260 | 2, 49, 258, 259 | mpbir3an 1244 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ (𝑀 + 1) ∈
(ℤ≥‘𝑀) |
261 | | fzss1 12380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ ((𝑀 + 1) ∈
(ℤ≥‘𝑀) → ((𝑀 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1))) |
262 | 260, 261 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ ((𝑀 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1)) |
263 | | eluzfz1 12348 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ (𝑚 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑚)) |
264 | 263, 5 | eleq2s 2719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ (𝑚 ∈ 𝑍 → 𝑀 ∈ (𝑀...𝑚)) |
265 | | fzaddel 12375 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢ (((𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 1 ∈
ℤ)) → (𝑀 ∈
(𝑀...𝑚) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1)))) |
266 | 2, 169, 265 | mpanr12 721 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ ((𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑀 ∈ (𝑀...𝑚) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1)))) |
267 | 2, 167, 266 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ (𝑚 ∈ 𝑍 → (𝑀 ∈ (𝑀...𝑚) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1)))) |
268 | 264, 267 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ (𝑚 ∈ 𝑍 → (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1))) |
269 | 262, 268 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ (𝑚 ∈ 𝑍 → (𝑀 + 1) ∈ (𝑀...(𝑚 + 1))) |
270 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ (𝑥 = (𝑀 + 1) → (𝑥 = 𝑀 ↔ (𝑀 + 1) = 𝑀)) |
271 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢ (𝑥 = (𝑀 + 1) → (𝑥 − 1) = ((𝑀 + 1) − 1)) |
272 | 271, 181 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ (𝑥 = (𝑀 + 1) → (𝑥 − 1) = 𝑀) |
273 | 272 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ (𝑥 = (𝑀 + 1) → (𝑔‘(𝑥 − 1)) = (𝑔‘𝑀)) |
274 | 270, 273 | ifbieq2d 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ (𝑥 = (𝑀 + 1) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if((𝑀 + 1) = 𝑀, 𝑐, (𝑔‘𝑀))) |
275 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ (𝑔‘𝑀) ∈ V |
276 | 207, 275 | ifex 4156 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ if((𝑀 + 1) = 𝑀, 𝑐, (𝑔‘𝑀)) ∈ V |
277 | 274, 199,
276 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((𝑀 + 1) ∈ (𝑀...(𝑚 + 1)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)) = if((𝑀 + 1) = 𝑀, 𝑐, (𝑔‘𝑀))) |
278 | 269, 277 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (𝑚 ∈ 𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)) = if((𝑀 + 1) = 𝑀, 𝑐, (𝑔‘𝑀))) |
279 | 46, 47 | gtneii 10149 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ (𝑀 + 1) ≠ 𝑀 |
280 | | ifnefalse 4098 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((𝑀 + 1) ≠ 𝑀 → if((𝑀 + 1) = 𝑀, 𝑐, (𝑔‘𝑀)) = (𝑔‘𝑀)) |
281 | 279, 280 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ if((𝑀 + 1) = 𝑀, 𝑐, (𝑔‘𝑀)) = (𝑔‘𝑀) |
282 | 278, 281 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (𝑚 ∈ 𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)) = (𝑔‘𝑀)) |
283 | 282 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)) = (𝑔‘𝑀)) |
284 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → (𝑔‘𝑀) = 𝑑) |
285 | 257, 283,
284 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = 𝑑) |
286 | 285 | sbceq1d 3440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑 ↔ [𝑑 / 𝑏]𝜑)) |
287 | 253, 286 | sbceqbid 3442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑 ↔ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑)) |
288 | 287 | biimparc 504 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢
(([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ (𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑) |
289 | 288 | anassrs 680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑) |
290 | 289 | anassrs 680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
(((([𝑐 /
𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ (𝑔‘𝑀) = 𝑑) ∧ 𝑗 = 𝑁) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑) |
291 | 290 | adantlrr 757 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(((([𝑐 /
𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) ∧ 𝑗 = 𝑁) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑) |
292 | | elfzelz 12342 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → 𝑗 ∈ ℤ) |
293 | 292 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → 𝑗 ∈ ℤ) |
294 | 44, 49 | eqeltri 2697 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ 𝑁 ∈ ℤ |
295 | | peano2z 11418 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ (𝑁 ∈ ℤ → (𝑁 + 1) ∈
ℤ) |
296 | 294, 295 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ (𝑁 + 1) ∈
ℤ |
297 | | fzsubel 12377 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ ((((𝑁 + 1) ∈ ℤ ∧
(𝑚 + 1) ∈ ℤ)
∧ (𝑗 ∈ ℤ
∧ 1 ∈ ℤ)) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) ↔ (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)))) |
298 | 297 | biimpd 219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ ((((𝑁 + 1) ∈ ℤ ∧
(𝑚 + 1) ∈ ℤ)
∧ (𝑗 ∈ ℤ
∧ 1 ∈ ℤ)) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)))) |
299 | 169, 298 | mpanr2 720 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ ((((𝑁 + 1) ∈ ℤ ∧
(𝑚 + 1) ∈ ℤ)
∧ 𝑗 ∈ ℤ)
→ (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)))) |
300 | 299 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ (((𝑁 + 1) ∈ ℤ ∧
(𝑚 + 1) ∈ ℤ)
→ (𝑗 ∈ ℤ
→ (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1))))) |
301 | 296, 168,
300 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (𝑚 ∈ 𝑍 → (𝑗 ∈ ℤ → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1))))) |
302 | 301 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (𝑚 ∈ 𝑍 → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 ∈ ℤ → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1))))) |
303 | 302 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 ∈ ℤ → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)))) |
304 | 293, 303 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1))) |
305 | 294 | zrei 11383 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ 𝑁 ∈ ℝ |
306 | 305 | recni 10052 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ 𝑁 ∈ ℂ |
307 | 306, 180 | pncan3oi 10297 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((𝑁 + 1) − 1) = 𝑁 |
308 | 307 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (𝑚 ∈ 𝑍 → ((𝑁 + 1) − 1) = 𝑁) |
309 | 308, 185 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝑚 ∈ 𝑍 → (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑁...𝑚)) |
310 | 309 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑁...𝑚)) |
311 | 304, 310 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 − 1) ∈ (𝑁...𝑚)) |
312 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (𝑘 = (𝑗 − 1) → (𝑘 − 1) = ((𝑗 − 1) − 1)) |
313 | 312 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝑘 = (𝑗 − 1) → (𝑔‘(𝑘 − 1)) = (𝑔‘((𝑗 − 1) − 1))) |
314 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (𝑘 = (𝑗 − 1) → (𝑔‘𝑘) = (𝑔‘(𝑗 − 1))) |
315 | 314 | sbceq1d 3440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝑘 = (𝑗 − 1) → ([(𝑔‘𝑘) / 𝑏]𝜑 ↔ [(𝑔‘(𝑗 − 1)) / 𝑏]𝜑)) |
316 | 313, 315 | sbceqbid 3442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝑘 = (𝑗 − 1) → ([(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑 ↔ [(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑)) |
317 | 316 | rspcva 3307 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝑗 − 1) ∈ (𝑁...𝑚) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → [(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑) |
318 | 311, 317 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → [(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑) |
319 | 44, 260 | eqeltri 2697 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ 𝑁 ∈
(ℤ≥‘𝑀) |
320 | | fzss1 12380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑁...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1))) |
321 | 319, 320 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (𝑁...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1)) |
322 | | fzssp1 12384 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ (𝑁...𝑚) ⊆ (𝑁...(𝑚 + 1)) |
323 | 322, 311 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 − 1) ∈ (𝑁...(𝑚 + 1))) |
324 | 321, 323 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 − 1) ∈ (𝑀...(𝑚 + 1))) |
325 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ (𝑥 = (𝑗 − 1) → (𝑥 = 𝑀 ↔ (𝑗 − 1) = 𝑀)) |
326 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ (𝑥 = (𝑗 − 1) → (𝑥 − 1) = ((𝑗 − 1) − 1)) |
327 | 326 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ (𝑥 = (𝑗 − 1) → (𝑔‘(𝑥 − 1)) = (𝑔‘((𝑗 − 1) − 1))) |
328 | 325, 327 | ifbieq2d 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (𝑥 = (𝑗 − 1) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1)))) |
329 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ (𝑔‘((𝑗 − 1) − 1)) ∈
V |
330 | 207, 329 | ifex 4156 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1))) ∈
V |
331 | 328, 199,
330 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((𝑗 − 1) ∈ (𝑀...(𝑚 + 1)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1)))) |
332 | 324, 331 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1)))) |
333 | 154 | ltp1i 10927 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ (𝑀 + 1) < ((𝑀 + 1) + 1) |
334 | 44 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ (𝑁 + 1) = ((𝑀 + 1) + 1) |
335 | 333, 334 | breqtrri 4680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ (𝑀 + 1) < (𝑁 + 1) |
336 | 305, 153 | readdcli 10053 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ (𝑁 + 1) ∈
ℝ |
337 | 154, 336 | ltnlei 10158 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ ((𝑀 + 1) < (𝑁 + 1) ↔ ¬ (𝑁 + 1) ≤ (𝑀 + 1)) |
338 | 335, 337 | mpbi 220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ¬
(𝑁 + 1) ≤ (𝑀 + 1) |
339 | 292 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → 𝑗 ∈ ℂ) |
340 | | subadd 10284 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ ((𝑗 ∈ ℂ ∧ 1 ∈
ℂ ∧ 𝑀 ∈
ℂ) → ((𝑗 −
1) = 𝑀 ↔ (1 + 𝑀) = 𝑗)) |
341 | 180, 179,
340 | mp3an23 1416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ (𝑗 ∈ ℂ → ((𝑗 − 1) = 𝑀 ↔ (1 + 𝑀) = 𝑗)) |
342 | 339, 341 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ((𝑗 − 1) = 𝑀 ↔ (1 + 𝑀) = 𝑗)) |
343 | | eqcom 2629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ ((1 +
𝑀) = 𝑗 ↔ 𝑗 = (1 + 𝑀)) |
344 | 180, 179 | addcomi 10227 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢ (1 +
𝑀) = (𝑀 + 1) |
345 | 344 | eqeq2i 2634 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ (𝑗 = (1 + 𝑀) ↔ 𝑗 = (𝑀 + 1)) |
346 | 343, 345 | bitri 264 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ ((1 +
𝑀) = 𝑗 ↔ 𝑗 = (𝑀 + 1)) |
347 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢ (𝑗 = (𝑀 + 1) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) ↔ (𝑀 + 1) ∈ ((𝑁 + 1)...(𝑚 + 1)))) |
348 | | elfzle1 12344 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢ ((𝑀 + 1) ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑁 + 1) ≤ (𝑀 + 1)) |
349 | 347, 348 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ (𝑗 = (𝑀 + 1) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑁 + 1) ≤ (𝑀 + 1))) |
350 | 349 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 = (𝑀 + 1) → (𝑁 + 1) ≤ (𝑀 + 1))) |
351 | 346, 350 | syl5bi 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ((1 + 𝑀) = 𝑗 → (𝑁 + 1) ≤ (𝑀 + 1))) |
352 | 342, 351 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ((𝑗 − 1) = 𝑀 → (𝑁 + 1) ≤ (𝑀 + 1))) |
353 | 338, 352 | mtoi 190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ¬ (𝑗 − 1) = 𝑀) |
354 | 353 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ¬ (𝑗 − 1) = 𝑀) |
355 | 354 | iffalsed 4097 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1))) = (𝑔‘((𝑗 − 1) − 1))) |
356 | 332, 355 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = (𝑔‘((𝑗 − 1) − 1))) |
357 | | peano2uz 11741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑁 + 1) ∈
(ℤ≥‘𝑀)) |
358 | | fzss1 12380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ ((𝑁 + 1) ∈
(ℤ≥‘𝑀) → ((𝑁 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1))) |
359 | 319, 357,
358 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((𝑁 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1)) |
360 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) |
361 | 359, 360 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → 𝑗 ∈ (𝑀...(𝑚 + 1))) |
362 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ (𝑥 = 𝑗 → (𝑥 = 𝑀 ↔ 𝑗 = 𝑀)) |
363 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ (𝑥 = 𝑗 → (𝑥 − 1) = (𝑗 − 1)) |
364 | 363 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ (𝑥 = 𝑗 → (𝑔‘(𝑥 − 1)) = (𝑔‘(𝑗 − 1))) |
365 | 362, 364 | ifbieq2d 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ (𝑥 = 𝑗 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1)))) |
366 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ (𝑔‘(𝑗 − 1)) ∈ V |
367 | 207, 366 | ifex 4156 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))) ∈ V |
368 | 365, 199,
367 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (𝑗 ∈ (𝑀...(𝑚 + 1)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1)))) |
369 | 361, 368 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1)))) |
370 | 47, 44 | breqtrri 4680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ 𝑀 < 𝑁 |
371 | 305 | ltp1i 10927 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ 𝑁 < (𝑁 + 1) |
372 | 46, 305, 336 | lttri 10163 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ ((𝑀 < 𝑁 ∧ 𝑁 < (𝑁 + 1)) → 𝑀 < (𝑁 + 1)) |
373 | 370, 371,
372 | mp2an 708 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ 𝑀 < (𝑁 + 1) |
374 | 46, 336 | ltnlei 10158 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ (𝑀 < (𝑁 + 1) ↔ ¬ (𝑁 + 1) ≤ 𝑀) |
375 | 373, 374 | mpbi 220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ ¬
(𝑁 + 1) ≤ 𝑀 |
376 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ (𝑗 = 𝑀 → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) ↔ 𝑀 ∈ ((𝑁 + 1)...(𝑚 + 1)))) |
377 | | elfzle1 12344 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ (𝑀 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑁 + 1) ≤ 𝑀) |
378 | 376, 377 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ (𝑗 = 𝑀 → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑁 + 1) ≤ 𝑀)) |
379 | 378 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢ (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 = 𝑀 → (𝑁 + 1) ≤ 𝑀)) |
380 | 375, 379 | mtoi 190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ¬ 𝑗 = 𝑀) |
381 | 380 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ¬ 𝑗 = 𝑀) |
382 | 381 | iffalsed 4097 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))) = (𝑔‘(𝑗 − 1))) |
383 | 369, 382 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = (𝑔‘(𝑗 − 1))) |
384 | 383 | sbceq1d 3440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑 ↔ [(𝑔‘(𝑗 − 1)) / 𝑏]𝜑)) |
385 | 356, 384 | sbceqbid 3442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑 ↔ [(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑)) |
386 | 385 | biimpar 502 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) ∧ [(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑) |
387 | 318, 386 | syldan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑) |
388 | 387 | an32s 846 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (((𝑚 ∈ 𝑍 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑) |
389 | 388 | adantlrl 756 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑) |
390 | 389 | adantlll 754 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(((([𝑐 /
𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑) |
391 | 291, 390 | jaodan 826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((([𝑐 /
𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) ∧ (𝑗 = 𝑁 ∨ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑) |
392 | 245, 391 | syldan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(((([𝑐 /
𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) ∧ 𝑗 ∈ (𝑁...(𝑚 + 1))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑) |
393 | 392 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ∀𝑗 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑) |
394 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑗 = 𝑘 → (𝑗 − 1) = (𝑘 − 1)) |
395 | 394 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑗 = 𝑘 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1))) |
396 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑗 = 𝑘 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘)) |
397 | 396 | sbceq1d 3440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑗 = 𝑘 → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑 ↔ [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)) |
398 | 395, 397 | sbceqbid 3442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑗 = 𝑘 → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑 ↔ [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)) |
399 | 398 | cbvralv 3171 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(∀𝑗 ∈
(𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑 ↔ ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑) |
400 | 393, 399 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑) |
401 | 400 | adantllr 755 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((([𝑐 /
𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑) |
402 | 401 | adantrlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((([𝑐 /
𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ (((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑) |
403 | 402 | 3adantr1 1220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((([𝑐 /
𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑) |
404 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑀...(𝑚 + 1)) ∈ V |
405 | 404 | mptex 6486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) ∈ V |
406 | | feq1 6026 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ↔ (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴)) |
407 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓‘𝑀) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀)) |
408 | 407 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ((𝑓‘𝑀) = 𝑐 ↔ ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐)) |
409 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓‘(𝑚 + 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1))) |
410 | 409 | sbceq1d 3440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ([(𝑓‘(𝑚 + 1)) / 𝑎]𝜃 ↔ [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃)) |
411 | 408, 410 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (((𝑓‘𝑀) = 𝑐 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ↔ (((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐 ∧ [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃))) |
412 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓‘(𝑘 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1))) |
413 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓‘𝑘) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘)) |
414 | 413 | sbceq1d 3440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ([(𝑓‘𝑘) / 𝑏]𝜑 ↔ [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)) |
415 | 412, 414 | sbceqbid 3442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓‘𝑘) / 𝑏]𝜑 ↔ [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)) |
416 | 113, 415 | syl5bbr 274 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝜒 ↔ [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)) |
417 | 416 | ralbidv 2986 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒 ↔ ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)) |
418 | 406, 411,
417 | 3anbi123d 1399 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ((𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒) ↔ ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴 ∧ (((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐 ∧ [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))) |
419 | 405, 418 | spcev 3300 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴 ∧ (((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐 ∧ [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)) |
420 | 203, 210,
236, 403, 419 | syl121anc 1331 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((([𝑐 /
𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)) |
421 | 420 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))) |
422 | 143, 421 | chvarv 2263 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((([𝑑 / 𝑏]𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))) |
423 | 133, 422 | chvarv 2263 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))) |
424 | 423 | adantlrr 757 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑚 ∈ 𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))) |
425 | 424 | adantlll 754 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑚 ∈ 𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))) |
426 | 425 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑚 ∈ 𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)) |
427 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑛 = (𝑚 + 1) → (𝑀...𝑛) = (𝑀...(𝑚 + 1))) |
428 | 427 | feq2d 6031 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 = (𝑚 + 1) → (𝑓:(𝑀...𝑛)⟶𝐴 ↔ 𝑓:(𝑀...(𝑚 + 1))⟶𝐴)) |
429 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑛 = (𝑚 + 1) → (𝑓‘𝑛) = (𝑓‘(𝑚 + 1))) |
430 | 429 | sbceq1d 3440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑛 = (𝑚 + 1) → ([(𝑓‘𝑛) / 𝑎]𝜃 ↔ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃)) |
431 | 38, 430 | syl5bbr 274 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑛 = (𝑚 + 1) → (𝜏 ↔ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃)) |
432 | 431 | anbi2d 740 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 = (𝑚 + 1) → (((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ↔ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃))) |
433 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑛 = (𝑚 + 1) → (𝑁...𝑛) = (𝑁...(𝑚 + 1))) |
434 | 433 | raleqdv 3144 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 = (𝑚 + 1) → (∀𝑘 ∈ (𝑁...𝑛)𝜒 ↔ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)) |
435 | 428, 432,
434 | 3anbi123d 1399 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 = (𝑚 + 1) → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))) |
436 | 435 | exbidv 1850 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 = (𝑚 + 1) → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))) |
437 | 436 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑚 + 1) ∈ 𝑍 ∧ ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)) |
438 | 125, 426,
437 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑚 ∈ 𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)) |
439 | 438 | ex 450 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑚 ∈ 𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))) |
440 | 439 | exlimdv 1861 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑚 ∈ 𝑍) → (∃𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))) |
441 | 440 | rexlimdva 3031 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (∃𝑚 ∈ 𝑍 ∃𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))) |
442 | 123, 441 | syl5bi 232 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))) |
443 | 73, 88, 442 | 3syld 60 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))) |
444 | 443 | an42s 870 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜂 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐴 ∧ 𝜑)) → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))) |
445 | 444 | rexlimdvaa 3032 |
. . . . . . . . . . . . . . 15
⊢ ((𝜂 ∧ 𝑎 ∈ 𝐴) → (∃𝑏 ∈ 𝐴 𝜑 → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))) |
446 | 445 | imp 445 |
. . . . . . . . . . . . . 14
⊢ (((𝜂 ∧ 𝑎 ∈ 𝐴) ∧ ∃𝑏 ∈ 𝐴 𝜑) → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))) |
447 | | fdc.10 |
. . . . . . . . . . . . . 14
⊢ ((𝜂 ∧ 𝑎 ∈ 𝐴) → (𝜃 ∨ ∃𝑏 ∈ 𝐴 𝜑)) |
448 | 65, 446, 447 | mpjaodan 827 |
. . . . . . . . . . . . 13
⊢ ((𝜂 ∧ 𝑎 ∈ 𝐴) → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))) |
449 | 138 | anbi1d 741 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 = 𝑎 → (((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ↔ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏))) |
450 | 449 | 3anbi2d 1404 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 = 𝑎 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))) |
451 | 450 | exbidv 1850 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = 𝑎 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))) |
452 | 451 | rexbidv 3052 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = 𝑎 → (∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))) |
453 | 452 | elrab3 3364 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ 𝐴 → (𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))) |
454 | 453 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝜂 ∧ 𝑎 ∈ 𝐴) → (𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))) |
455 | 448, 454 | sylibrd 249 |
. . . . . . . . . . . 12
⊢ ((𝜂 ∧ 𝑎 ∈ 𝐴) → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → 𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) |
456 | 455 | ex 450 |
. . . . . . . . . . 11
⊢ (𝜂 → (𝑎 ∈ 𝐴 → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → 𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))) |
457 | 456 | com23 86 |
. . . . . . . . . 10
⊢ (𝜂 → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → (𝑎 ∈ 𝐴 → 𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))) |
458 | | eldif 3584 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ↔ (𝑎 ∈ 𝐴 ∧ ¬ 𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) |
459 | 458 | notbii 310 |
. . . . . . . . . . 11
⊢ (¬
𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ↔ ¬ (𝑎 ∈ 𝐴 ∧ ¬ 𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) |
460 | | iman 440 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ 𝐴 → 𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ↔ ¬ (𝑎 ∈ 𝐴 ∧ ¬ 𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) |
461 | 459, 460 | bitr4i 267 |
. . . . . . . . . 10
⊢ (¬
𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ↔ (𝑎 ∈ 𝐴 → 𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) |
462 | 457, 461 | syl6ibr 242 |
. . . . . . . . 9
⊢ (𝜂 → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ¬ 𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))) |
463 | 462 | con2d 129 |
. . . . . . . 8
⊢ (𝜂 → (𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)) |
464 | 463 | imp 445 |
. . . . . . 7
⊢ ((𝜂 ∧ 𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) → ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎) |
465 | 464 | nrexdv 3001 |
. . . . . 6
⊢ (𝜂 → ¬ ∃𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎) |
466 | | df-ne 2795 |
. . . . . . 7
⊢ ((𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅ ↔ ¬ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅) |
467 | | fdc.9 |
. . . . . . . 8
⊢ (𝜂 → 𝑅 Fr 𝐴) |
468 | | difss 3737 |
. . . . . . . 8
⊢ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴 |
469 | | fdc.1 |
. . . . . . . . . . 11
⊢ 𝐴 ∈ V |
470 | | difexg 4808 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ V → (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∈ V) |
471 | 469, 470 | ax-mp 5 |
. . . . . . . . . 10
⊢ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∈ V |
472 | | fri 5076 |
. . . . . . . . . 10
⊢ ((((𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∈ V ∧ 𝑅 Fr 𝐴) ∧ ((𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴 ∧ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅)) → ∃𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎) |
473 | 471, 472 | mpanl1 716 |
. . . . . . . . 9
⊢ ((𝑅 Fr 𝐴 ∧ ((𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴 ∧ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅)) → ∃𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎) |
474 | 473 | expr 643 |
. . . . . . . 8
⊢ ((𝑅 Fr 𝐴 ∧ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴) → ((𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅ → ∃𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)) |
475 | 467, 468,
474 | sylancl 694 |
. . . . . . 7
⊢ (𝜂 → ((𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅ → ∃𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)) |
476 | 466, 475 | syl5bir 233 |
. . . . . 6
⊢ (𝜂 → (¬ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅ → ∃𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)) |
477 | 465, 476 | mt3d 140 |
. . . . 5
⊢ (𝜂 → (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅) |
478 | | ssdif0 3942 |
. . . . 5
⊢ (𝐴 ⊆ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅) |
479 | 477, 478 | sylibr 224 |
. . . 4
⊢ (𝜂 → 𝐴 ⊆ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) |
480 | 76 | a1i 11 |
. . . 4
⊢ (𝜂 → {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ⊆ 𝐴) |
481 | 479, 480 | eqssd 3620 |
. . 3
⊢ (𝜂 → 𝐴 = {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) |
482 | | rabid2 3118 |
. . 3
⊢ (𝐴 = {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∀𝑐 ∈ 𝐴 ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)) |
483 | 481, 482 | sylib 208 |
. 2
⊢ (𝜂 → ∀𝑐 ∈ 𝐴 ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)) |
484 | | eqeq2 2633 |
. . . . . . 7
⊢ (𝑐 = 𝐶 → ((𝑓‘𝑀) = 𝑐 ↔ (𝑓‘𝑀) = 𝐶)) |
485 | 484 | anbi1d 741 |
. . . . . 6
⊢ (𝑐 = 𝐶 → (((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ↔ ((𝑓‘𝑀) = 𝐶 ∧ 𝜏))) |
486 | 485 | 3anbi2d 1404 |
. . . . 5
⊢ (𝑐 = 𝐶 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝐶 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))) |
487 | 486 | exbidv 1850 |
. . . 4
⊢ (𝑐 = 𝐶 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝐶 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))) |
488 | 487 | rexbidv 3052 |
. . 3
⊢ (𝑐 = 𝐶 → (∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝐶 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))) |
489 | 488 | rspcva 3307 |
. 2
⊢ ((𝐶 ∈ 𝐴 ∧ ∀𝑐 ∈ 𝐴 ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝐶 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)) |
490 | 1, 483, 489 | syl2anc 693 |
1
⊢ (𝜂 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝐶 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)) |