Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  poimirlem2 Structured version   Visualization version   GIF version

Theorem poimirlem2 36080
Description: Lemma for poimir 36111- consecutive vertices differ in at most one dimension. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0 (πœ‘ β†’ 𝑁 ∈ β„•)
poimirlem2.1 (πœ‘ β†’ 𝐹 = (𝑦 ∈ (0...(𝑁 βˆ’ 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / π‘—β¦Œ(𝑇 ∘f + (((π‘ˆ β€œ (1...𝑗)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0})))))
poimirlem2.2 (πœ‘ β†’ 𝑇:(1...𝑁)βŸΆβ„€)
poimirlem2.3 (πœ‘ β†’ π‘ˆ:(1...𝑁)–1-1-ontoβ†’(1...𝑁))
poimirlem2.4 (πœ‘ β†’ 𝑉 ∈ (1...(𝑁 βˆ’ 1)))
poimirlem2.5 (πœ‘ β†’ 𝑀 ∈ ((0...𝑁) βˆ– {𝑉}))
Assertion
Ref Expression
poimirlem2 (πœ‘ β†’ βˆƒ*𝑛 ∈ (1...𝑁)((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›))
Distinct variable groups:   𝑗,𝑛,𝑦,πœ‘   𝑗,𝐹,𝑛,𝑦   𝑗,𝑀,𝑛,𝑦   𝑗,𝑁,𝑛,𝑦   𝑇,𝑗,𝑛,𝑦   π‘ˆ,𝑗,𝑛,𝑦   𝑗,𝑉,𝑛,𝑦

Proof of Theorem poimirlem2
Dummy variable π‘š is distinct from all other variables.
StepHypRef Expression
1 poimirlem2.3 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ π‘ˆ:(1...𝑁)–1-1-ontoβ†’(1...𝑁))
2 dff1o3 6790 . . . . . . . . . . . . . . . . 17 (π‘ˆ:(1...𝑁)–1-1-ontoβ†’(1...𝑁) ↔ (π‘ˆ:(1...𝑁)–ontoβ†’(1...𝑁) ∧ Fun β—‘π‘ˆ))
32simprbi 497 . . . . . . . . . . . . . . . 16 (π‘ˆ:(1...𝑁)–1-1-ontoβ†’(1...𝑁) β†’ Fun β—‘π‘ˆ)
41, 3syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ Fun β—‘π‘ˆ)
5 imadif 6585 . . . . . . . . . . . . . . 15 (Fun β—‘π‘ˆ β†’ (π‘ˆ β€œ ((1...𝑁) βˆ– {(𝑉 + 1)})) = ((π‘ˆ β€œ (1...𝑁)) βˆ– (π‘ˆ β€œ {(𝑉 + 1)})))
64, 5syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘ˆ β€œ ((1...𝑁) βˆ– {(𝑉 + 1)})) = ((π‘ˆ β€œ (1...𝑁)) βˆ– (π‘ˆ β€œ {(𝑉 + 1)})))
7 poimirlem2.4 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝑉 ∈ (1...(𝑁 βˆ’ 1)))
8 fzp1elp1 13494 . . . . . . . . . . . . . . . . . . . 20 (𝑉 ∈ (1...(𝑁 βˆ’ 1)) β†’ (𝑉 + 1) ∈ (1...((𝑁 βˆ’ 1) + 1)))
97, 8syl 17 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (𝑉 + 1) ∈ (1...((𝑁 βˆ’ 1) + 1)))
10 poimir.0 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ 𝑁 ∈ β„•)
1110nncnd 12169 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ 𝑁 ∈ β„‚)
12 npcan1 11580 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ β„‚ β†’ ((𝑁 βˆ’ 1) + 1) = 𝑁)
1311, 12syl 17 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((𝑁 βˆ’ 1) + 1) = 𝑁)
1413oveq2d 7373 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (1...((𝑁 βˆ’ 1) + 1)) = (1...𝑁))
159, 14eleqtrd 2839 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝑉 + 1) ∈ (1...𝑁))
16 fzsplit 13467 . . . . . . . . . . . . . . . . . 18 ((𝑉 + 1) ∈ (1...𝑁) β†’ (1...𝑁) = ((1...(𝑉 + 1)) βˆͺ (((𝑉 + 1) + 1)...𝑁)))
1715, 16syl 17 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (1...𝑁) = ((1...(𝑉 + 1)) βˆͺ (((𝑉 + 1) + 1)...𝑁)))
1817difeq1d 4081 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((1...𝑁) βˆ– {(𝑉 + 1)}) = (((1...(𝑉 + 1)) βˆͺ (((𝑉 + 1) + 1)...𝑁)) βˆ– {(𝑉 + 1)}))
19 difundir 4240 . . . . . . . . . . . . . . . . 17 (((1...(𝑉 + 1)) βˆͺ (((𝑉 + 1) + 1)...𝑁)) βˆ– {(𝑉 + 1)}) = (((1...(𝑉 + 1)) βˆ– {(𝑉 + 1)}) βˆͺ ((((𝑉 + 1) + 1)...𝑁) βˆ– {(𝑉 + 1)}))
20 elfzuz 13437 . . . . . . . . . . . . . . . . . . . . . 22 (𝑉 ∈ (1...(𝑁 βˆ’ 1)) β†’ 𝑉 ∈ (β„€β‰₯β€˜1))
217, 20syl 17 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ 𝑉 ∈ (β„€β‰₯β€˜1))
22 fzsuc 13488 . . . . . . . . . . . . . . . . . . . . 21 (𝑉 ∈ (β„€β‰₯β€˜1) β†’ (1...(𝑉 + 1)) = ((1...𝑉) βˆͺ {(𝑉 + 1)}))
2321, 22syl 17 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (1...(𝑉 + 1)) = ((1...𝑉) βˆͺ {(𝑉 + 1)}))
2423difeq1d 4081 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ((1...(𝑉 + 1)) βˆ– {(𝑉 + 1)}) = (((1...𝑉) βˆͺ {(𝑉 + 1)}) βˆ– {(𝑉 + 1)}))
25 difun2 4440 . . . . . . . . . . . . . . . . . . . 20 (((1...𝑉) βˆͺ {(𝑉 + 1)}) βˆ– {(𝑉 + 1)}) = ((1...𝑉) βˆ– {(𝑉 + 1)})
267elfzelzd 13442 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ 𝑉 ∈ β„€)
2726zred 12607 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ 𝑉 ∈ ℝ)
2827ltp1d 12085 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ 𝑉 < (𝑉 + 1))
2926peano2zd 12610 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ (𝑉 + 1) ∈ β„€)
3029zred 12607 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (𝑉 + 1) ∈ ℝ)
3127, 30ltnled 11302 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ (𝑉 < (𝑉 + 1) ↔ Β¬ (𝑉 + 1) ≀ 𝑉))
3228, 31mpbid 231 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ Β¬ (𝑉 + 1) ≀ 𝑉)
33 elfzle2 13445 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑉 + 1) ∈ (1...𝑉) β†’ (𝑉 + 1) ≀ 𝑉)
3432, 33nsyl 140 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ Β¬ (𝑉 + 1) ∈ (1...𝑉))
35 difsn 4758 . . . . . . . . . . . . . . . . . . . . 21 (Β¬ (𝑉 + 1) ∈ (1...𝑉) β†’ ((1...𝑉) βˆ– {(𝑉 + 1)}) = (1...𝑉))
3634, 35syl 17 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((1...𝑉) βˆ– {(𝑉 + 1)}) = (1...𝑉))
3725, 36eqtrid 2788 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (((1...𝑉) βˆͺ {(𝑉 + 1)}) βˆ– {(𝑉 + 1)}) = (1...𝑉))
3824, 37eqtrd 2776 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ ((1...(𝑉 + 1)) βˆ– {(𝑉 + 1)}) = (1...𝑉))
3930ltp1d 12085 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (𝑉 + 1) < ((𝑉 + 1) + 1))
40 peano2re 11328 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑉 + 1) ∈ ℝ β†’ ((𝑉 + 1) + 1) ∈ ℝ)
4130, 40syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ ((𝑉 + 1) + 1) ∈ ℝ)
4230, 41ltnled 11302 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ ((𝑉 + 1) < ((𝑉 + 1) + 1) ↔ Β¬ ((𝑉 + 1) + 1) ≀ (𝑉 + 1)))
4339, 42mpbid 231 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ Β¬ ((𝑉 + 1) + 1) ≀ (𝑉 + 1))
44 elfzle1 13444 . . . . . . . . . . . . . . . . . . . 20 ((𝑉 + 1) ∈ (((𝑉 + 1) + 1)...𝑁) β†’ ((𝑉 + 1) + 1) ≀ (𝑉 + 1))
4543, 44nsyl 140 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ Β¬ (𝑉 + 1) ∈ (((𝑉 + 1) + 1)...𝑁))
46 difsn 4758 . . . . . . . . . . . . . . . . . . 19 (Β¬ (𝑉 + 1) ∈ (((𝑉 + 1) + 1)...𝑁) β†’ ((((𝑉 + 1) + 1)...𝑁) βˆ– {(𝑉 + 1)}) = (((𝑉 + 1) + 1)...𝑁))
4745, 46syl 17 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ ((((𝑉 + 1) + 1)...𝑁) βˆ– {(𝑉 + 1)}) = (((𝑉 + 1) + 1)...𝑁))
4838, 47uneq12d 4124 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (((1...(𝑉 + 1)) βˆ– {(𝑉 + 1)}) βˆͺ ((((𝑉 + 1) + 1)...𝑁) βˆ– {(𝑉 + 1)})) = ((1...𝑉) βˆͺ (((𝑉 + 1) + 1)...𝑁)))
4919, 48eqtrid 2788 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (((1...(𝑉 + 1)) βˆͺ (((𝑉 + 1) + 1)...𝑁)) βˆ– {(𝑉 + 1)}) = ((1...𝑉) βˆͺ (((𝑉 + 1) + 1)...𝑁)))
5018, 49eqtrd 2776 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((1...𝑁) βˆ– {(𝑉 + 1)}) = ((1...𝑉) βˆͺ (((𝑉 + 1) + 1)...𝑁)))
5150imaeq2d 6013 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘ˆ β€œ ((1...𝑁) βˆ– {(𝑉 + 1)})) = (π‘ˆ β€œ ((1...𝑉) βˆͺ (((𝑉 + 1) + 1)...𝑁))))
526, 51eqtr3d 2778 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π‘ˆ β€œ (1...𝑁)) βˆ– (π‘ˆ β€œ {(𝑉 + 1)})) = (π‘ˆ β€œ ((1...𝑉) βˆͺ (((𝑉 + 1) + 1)...𝑁))))
53 imaundi 6102 . . . . . . . . . . . . 13 (π‘ˆ β€œ ((1...𝑉) βˆͺ (((𝑉 + 1) + 1)...𝑁))) = ((π‘ˆ β€œ (1...𝑉)) βˆͺ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)))
5452, 53eqtrdi 2792 . . . . . . . . . . . 12 (πœ‘ β†’ ((π‘ˆ β€œ (1...𝑁)) βˆ– (π‘ˆ β€œ {(𝑉 + 1)})) = ((π‘ˆ β€œ (1...𝑉)) βˆͺ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))))
5554eleq2d 2823 . . . . . . . . . . 11 (πœ‘ β†’ (𝑛 ∈ ((π‘ˆ β€œ (1...𝑁)) βˆ– (π‘ˆ β€œ {(𝑉 + 1)})) ↔ 𝑛 ∈ ((π‘ˆ β€œ (1...𝑉)) βˆͺ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)))))
56 eldif 3920 . . . . . . . . . . 11 (𝑛 ∈ ((π‘ˆ β€œ (1...𝑁)) βˆ– (π‘ˆ β€œ {(𝑉 + 1)})) ↔ (𝑛 ∈ (π‘ˆ β€œ (1...𝑁)) ∧ Β¬ 𝑛 ∈ (π‘ˆ β€œ {(𝑉 + 1)})))
57 elun 4108 . . . . . . . . . . 11 (𝑛 ∈ ((π‘ˆ β€œ (1...𝑉)) βˆͺ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) ↔ (𝑛 ∈ (π‘ˆ β€œ (1...𝑉)) ∨ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))))
5855, 56, 573bitr3g 312 . . . . . . . . . 10 (πœ‘ β†’ ((𝑛 ∈ (π‘ˆ β€œ (1...𝑁)) ∧ Β¬ 𝑛 ∈ (π‘ˆ β€œ {(𝑉 + 1)})) ↔ (𝑛 ∈ (π‘ˆ β€œ (1...𝑉)) ∨ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)))))
5958adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ ((𝑛 ∈ (π‘ˆ β€œ (1...𝑁)) ∧ Β¬ 𝑛 ∈ (π‘ˆ β€œ {(𝑉 + 1)})) ↔ (𝑛 ∈ (π‘ˆ β€œ (1...𝑉)) ∨ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)))))
60 imassrn 6024 . . . . . . . . . . . . . . . 16 (π‘ˆ β€œ (1...𝑉)) βŠ† ran π‘ˆ
61 f1of 6784 . . . . . . . . . . . . . . . . . 18 (π‘ˆ:(1...𝑁)–1-1-ontoβ†’(1...𝑁) β†’ π‘ˆ:(1...𝑁)⟢(1...𝑁))
621, 61syl 17 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ π‘ˆ:(1...𝑁)⟢(1...𝑁))
6362frnd 6676 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ran π‘ˆ βŠ† (1...𝑁))
6460, 63sstrid 3955 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (π‘ˆ β€œ (1...𝑉)) βŠ† (1...𝑁))
6564sselda 3944 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) β†’ 𝑛 ∈ (1...𝑁))
66 poimirlem2.2 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝑇:(1...𝑁)βŸΆβ„€)
6766ffnd 6669 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝑇 Fn (1...𝑁))
6867adantr 481 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) β†’ 𝑇 Fn (1...𝑁))
69 1ex 11151 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ V
70 fnconstg 6730 . . . . . . . . . . . . . . . . . . . . 21 (1 ∈ V β†’ ((π‘ˆ β€œ (1...𝑉)) Γ— {1}) Fn (π‘ˆ β€œ (1...𝑉)))
7169, 70ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((π‘ˆ β€œ (1...𝑉)) Γ— {1}) Fn (π‘ˆ β€œ (1...𝑉))
72 c0ex 11149 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ V
73 fnconstg 6730 . . . . . . . . . . . . . . . . . . . . 21 (0 ∈ V β†’ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}) Fn (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))
7472, 73ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}) Fn (π‘ˆ β€œ ((𝑉 + 1)...𝑁))
7571, 74pm3.2i 471 . . . . . . . . . . . . . . . . . . 19 (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) Fn (π‘ˆ β€œ (1...𝑉)) ∧ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}) Fn (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))
76 imain 6586 . . . . . . . . . . . . . . . . . . . . 21 (Fun β—‘π‘ˆ β†’ (π‘ˆ β€œ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = ((π‘ˆ β€œ (1...𝑉)) ∩ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))))
774, 76syl 17 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (π‘ˆ β€œ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = ((π‘ˆ β€œ (1...𝑉)) ∩ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))))
78 fzdisj 13468 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑉 < (𝑉 + 1) β†’ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁)) = βˆ…)
7928, 78syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁)) = βˆ…)
8079imaeq2d 6013 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (π‘ˆ β€œ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = (π‘ˆ β€œ βˆ…))
81 ima0 6029 . . . . . . . . . . . . . . . . . . . . 21 (π‘ˆ β€œ βˆ…) = βˆ…
8280, 81eqtrdi 2792 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (π‘ˆ β€œ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = βˆ…)
8377, 82eqtr3d 2778 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ((π‘ˆ β€œ (1...𝑉)) ∩ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) = βˆ…)
84 fnun 6614 . . . . . . . . . . . . . . . . . . 19 (((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) Fn (π‘ˆ β€œ (1...𝑉)) ∧ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}) Fn (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) ∧ ((π‘ˆ β€œ (1...𝑉)) ∩ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) = βˆ…) β†’ (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})) Fn ((π‘ˆ β€œ (1...𝑉)) βˆͺ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))))
8575, 83, 84sylancr 587 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})) Fn ((π‘ˆ β€œ (1...𝑉)) βˆͺ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))))
86 imaundi 6102 . . . . . . . . . . . . . . . . . . . 20 (π‘ˆ β€œ ((1...𝑉) βˆͺ ((𝑉 + 1)...𝑁))) = ((π‘ˆ β€œ (1...𝑉)) βˆͺ (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))
8710nnzd 12526 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (πœ‘ β†’ 𝑁 ∈ β„€)
88 peano2zm 12546 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ β„€ β†’ (𝑁 βˆ’ 1) ∈ β„€)
8987, 88syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ (𝑁 βˆ’ 1) ∈ β„€)
90 uzid 12778 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑁 βˆ’ 1) ∈ β„€ β†’ (𝑁 βˆ’ 1) ∈ (β„€β‰₯β€˜(𝑁 βˆ’ 1)))
9189, 90syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ (𝑁 βˆ’ 1) ∈ (β„€β‰₯β€˜(𝑁 βˆ’ 1)))
92 peano2uz 12826 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑁 βˆ’ 1) ∈ (β„€β‰₯β€˜(𝑁 βˆ’ 1)) β†’ ((𝑁 βˆ’ 1) + 1) ∈ (β„€β‰₯β€˜(𝑁 βˆ’ 1)))
9391, 92syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ ((𝑁 βˆ’ 1) + 1) ∈ (β„€β‰₯β€˜(𝑁 βˆ’ 1)))
9413, 93eqeltrrd 2838 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ 𝑁 ∈ (β„€β‰₯β€˜(𝑁 βˆ’ 1)))
95 fzss2 13481 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ (β„€β‰₯β€˜(𝑁 βˆ’ 1)) β†’ (1...(𝑁 βˆ’ 1)) βŠ† (1...𝑁))
9694, 95syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (1...(𝑁 βˆ’ 1)) βŠ† (1...𝑁))
9796, 7sseldd 3945 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ 𝑉 ∈ (1...𝑁))
98 fzsplit 13467 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑉 ∈ (1...𝑁) β†’ (1...𝑁) = ((1...𝑉) βˆͺ ((𝑉 + 1)...𝑁)))
9997, 98syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (1...𝑁) = ((1...𝑉) βˆͺ ((𝑉 + 1)...𝑁)))
10099imaeq2d 6013 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (π‘ˆ β€œ (1...𝑁)) = (π‘ˆ β€œ ((1...𝑉) βˆͺ ((𝑉 + 1)...𝑁))))
101 f1ofo 6791 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘ˆ:(1...𝑁)–1-1-ontoβ†’(1...𝑁) β†’ π‘ˆ:(1...𝑁)–ontoβ†’(1...𝑁))
1021, 101syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ π‘ˆ:(1...𝑁)–ontoβ†’(1...𝑁))
103 foima 6761 . . . . . . . . . . . . . . . . . . . . . 22 (π‘ˆ:(1...𝑁)–ontoβ†’(1...𝑁) β†’ (π‘ˆ β€œ (1...𝑁)) = (1...𝑁))
104102, 103syl 17 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (π‘ˆ β€œ (1...𝑁)) = (1...𝑁))
105100, 104eqtr3d 2778 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (π‘ˆ β€œ ((1...𝑉) βˆͺ ((𝑉 + 1)...𝑁))) = (1...𝑁))
10686, 105eqtr3id 2790 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ((π‘ˆ β€œ (1...𝑉)) βˆͺ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) = (1...𝑁))
107106fneq2d 6596 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ ((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})) Fn ((π‘ˆ β€œ (1...𝑉)) βˆͺ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) ↔ (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})) Fn (1...𝑁)))
10885, 107mpbid 231 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})) Fn (1...𝑁))
109108adantr 481 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) β†’ (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})) Fn (1...𝑁))
110 fzfid 13878 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) β†’ (1...𝑁) ∈ Fin)
111 inidm 4178 . . . . . . . . . . . . . . . 16 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
112 eqidd 2737 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘‡β€˜π‘›) = (π‘‡β€˜π‘›))
113 fvun1 6932 . . . . . . . . . . . . . . . . . . . 20 ((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) Fn (π‘ˆ β€œ (1...𝑉)) ∧ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}) Fn (π‘ˆ β€œ ((𝑉 + 1)...𝑁)) ∧ (((π‘ˆ β€œ (1...𝑉)) ∩ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) = βˆ… ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉)))) β†’ ((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ (1...𝑉)) Γ— {1})β€˜π‘›))
11471, 74, 113mp3an12 1451 . . . . . . . . . . . . . . . . . . 19 ((((π‘ˆ β€œ (1...𝑉)) ∩ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) = βˆ… ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) β†’ ((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ (1...𝑉)) Γ— {1})β€˜π‘›))
11583, 114sylan 580 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) β†’ ((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ (1...𝑉)) Γ— {1})β€˜π‘›))
11669fvconst2 7153 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (π‘ˆ β€œ (1...𝑉)) β†’ (((π‘ˆ β€œ (1...𝑉)) Γ— {1})β€˜π‘›) = 1)
117116adantl 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) β†’ (((π‘ˆ β€œ (1...𝑉)) Γ— {1})β€˜π‘›) = 1)
118115, 117eqtrd 2776 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) β†’ ((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))β€˜π‘›) = 1)
119118adantr 481 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))β€˜π‘›) = 1)
12068, 109, 110, 110, 111, 112, 119ofval 7628 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›) = ((π‘‡β€˜π‘›) + 1))
121 fnconstg 6730 . . . . . . . . . . . . . . . . . . . . 21 (1 ∈ V β†’ ((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) Fn (π‘ˆ β€œ (1...(𝑉 + 1))))
12269, 121ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) Fn (π‘ˆ β€œ (1...(𝑉 + 1)))
123 fnconstg 6730 . . . . . . . . . . . . . . . . . . . . 21 (0 ∈ V β†’ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}) Fn (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)))
12472, 123ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}) Fn (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))
125122, 124pm3.2i 471 . . . . . . . . . . . . . . . . . . 19 (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) Fn (π‘ˆ β€œ (1...(𝑉 + 1))) ∧ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}) Fn (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)))
126 imain 6586 . . . . . . . . . . . . . . . . . . . . 21 (Fun β—‘π‘ˆ β†’ (π‘ˆ β€œ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = ((π‘ˆ β€œ (1...(𝑉 + 1))) ∩ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))))
1274, 126syl 17 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (π‘ˆ β€œ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = ((π‘ˆ β€œ (1...(𝑉 + 1))) ∩ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))))
128 fzdisj 13468 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑉 + 1) < ((𝑉 + 1) + 1) β†’ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁)) = βˆ…)
12939, 128syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁)) = βˆ…)
130129imaeq2d 6013 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (π‘ˆ β€œ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = (π‘ˆ β€œ βˆ…))
131130, 81eqtrdi 2792 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (π‘ˆ β€œ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = βˆ…)
132127, 131eqtr3d 2778 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ((π‘ˆ β€œ (1...(𝑉 + 1))) ∩ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) = βˆ…)
133 fnun 6614 . . . . . . . . . . . . . . . . . . 19 (((((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) Fn (π‘ˆ β€œ (1...(𝑉 + 1))) ∧ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}) Fn (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) ∧ ((π‘ˆ β€œ (1...(𝑉 + 1))) ∩ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) = βˆ…) β†’ (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})) Fn ((π‘ˆ β€œ (1...(𝑉 + 1))) βˆͺ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))))
134125, 132, 133sylancr 587 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})) Fn ((π‘ˆ β€œ (1...(𝑉 + 1))) βˆͺ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))))
135 imaundi 6102 . . . . . . . . . . . . . . . . . . . 20 (π‘ˆ β€œ ((1...(𝑉 + 1)) βˆͺ (((𝑉 + 1) + 1)...𝑁))) = ((π‘ˆ β€œ (1...(𝑉 + 1))) βˆͺ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)))
13617imaeq2d 6013 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (π‘ˆ β€œ (1...𝑁)) = (π‘ˆ β€œ ((1...(𝑉 + 1)) βˆͺ (((𝑉 + 1) + 1)...𝑁))))
137136, 104eqtr3d 2778 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (π‘ˆ β€œ ((1...(𝑉 + 1)) βˆͺ (((𝑉 + 1) + 1)...𝑁))) = (1...𝑁))
138135, 137eqtr3id 2790 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ((π‘ˆ β€œ (1...(𝑉 + 1))) βˆͺ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) = (1...𝑁))
139138fneq2d 6596 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ ((((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})) Fn ((π‘ˆ β€œ (1...(𝑉 + 1))) βˆͺ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) ↔ (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})) Fn (1...𝑁)))
140134, 139mpbid 231 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})) Fn (1...𝑁))
141140adantr 481 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) β†’ (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})) Fn (1...𝑁))
142 uzid 12778 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑉 ∈ β„€ β†’ 𝑉 ∈ (β„€β‰₯β€˜π‘‰))
14326, 142syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ 𝑉 ∈ (β„€β‰₯β€˜π‘‰))
144 peano2uz 12826 . . . . . . . . . . . . . . . . . . . . . 22 (𝑉 ∈ (β„€β‰₯β€˜π‘‰) β†’ (𝑉 + 1) ∈ (β„€β‰₯β€˜π‘‰))
145143, 144syl 17 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (𝑉 + 1) ∈ (β„€β‰₯β€˜π‘‰))
146 fzss2 13481 . . . . . . . . . . . . . . . . . . . . 21 ((𝑉 + 1) ∈ (β„€β‰₯β€˜π‘‰) β†’ (1...𝑉) βŠ† (1...(𝑉 + 1)))
147145, 146syl 17 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (1...𝑉) βŠ† (1...(𝑉 + 1)))
148 imass2 6054 . . . . . . . . . . . . . . . . . . . 20 ((1...𝑉) βŠ† (1...(𝑉 + 1)) β†’ (π‘ˆ β€œ (1...𝑉)) βŠ† (π‘ˆ β€œ (1...(𝑉 + 1))))
149147, 148syl 17 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (π‘ˆ β€œ (1...𝑉)) βŠ† (π‘ˆ β€œ (1...(𝑉 + 1))))
150149sselda 3944 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) β†’ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 + 1))))
151 fvun1 6932 . . . . . . . . . . . . . . . . . . . . 21 ((((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) Fn (π‘ˆ β€œ (1...(𝑉 + 1))) ∧ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}) Fn (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) ∧ (((π‘ˆ β€œ (1...(𝑉 + 1))) ∩ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) = βˆ… ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 + 1))))) β†’ ((((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1})β€˜π‘›))
152122, 124, 151mp3an12 1451 . . . . . . . . . . . . . . . . . . . 20 ((((π‘ˆ β€œ (1...(𝑉 + 1))) ∩ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) = βˆ… ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 + 1)))) β†’ ((((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1})β€˜π‘›))
153132, 152sylan 580 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 + 1)))) β†’ ((((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1})β€˜π‘›))
15469fvconst2 7153 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 + 1))) β†’ (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1})β€˜π‘›) = 1)
155154adantl 482 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 + 1)))) β†’ (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1})β€˜π‘›) = 1)
156153, 155eqtrd 2776 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 + 1)))) β†’ ((((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}))β€˜π‘›) = 1)
157150, 156syldan 591 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) β†’ ((((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}))β€˜π‘›) = 1)
158157adantr 481 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}))β€˜π‘›) = 1)
15968, 141, 110, 110, 111, 112, 158ofval 7628 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})))β€˜π‘›) = ((π‘‡β€˜π‘›) + 1))
160120, 159eqtr4d 2779 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})))β€˜π‘›))
16165, 160mpdan 685 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})))β€˜π‘›))
162 imassrn 6024 . . . . . . . . . . . . . . . 16 (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) βŠ† ran π‘ˆ
163162, 63sstrid 3955 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) βŠ† (1...𝑁))
164163sselda 3944 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) β†’ 𝑛 ∈ (1...𝑁))
16567adantr 481 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) β†’ 𝑇 Fn (1...𝑁))
166108adantr 481 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) β†’ (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})) Fn (1...𝑁))
167 fzfid 13878 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) β†’ (1...𝑁) ∈ Fin)
168 eqidd 2737 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘‡β€˜π‘›) = (π‘‡β€˜π‘›))
169 uzid 12778 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑉 + 1) ∈ β„€ β†’ (𝑉 + 1) ∈ (β„€β‰₯β€˜(𝑉 + 1)))
17029, 169syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (𝑉 + 1) ∈ (β„€β‰₯β€˜(𝑉 + 1)))
171 peano2uz 12826 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑉 + 1) ∈ (β„€β‰₯β€˜(𝑉 + 1)) β†’ ((𝑉 + 1) + 1) ∈ (β„€β‰₯β€˜(𝑉 + 1)))
172170, 171syl 17 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ ((𝑉 + 1) + 1) ∈ (β„€β‰₯β€˜(𝑉 + 1)))
173 fzss1 13480 . . . . . . . . . . . . . . . . . . . . 21 (((𝑉 + 1) + 1) ∈ (β„€β‰₯β€˜(𝑉 + 1)) β†’ (((𝑉 + 1) + 1)...𝑁) βŠ† ((𝑉 + 1)...𝑁))
174172, 173syl 17 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (((𝑉 + 1) + 1)...𝑁) βŠ† ((𝑉 + 1)...𝑁))
175 imass2 6054 . . . . . . . . . . . . . . . . . . . 20 ((((𝑉 + 1) + 1)...𝑁) βŠ† ((𝑉 + 1)...𝑁) β†’ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) βŠ† (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))
176174, 175syl 17 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) βŠ† (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))
177176sselda 3944 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) β†’ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))
178 fvun2 6933 . . . . . . . . . . . . . . . . . . . . 21 ((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) Fn (π‘ˆ β€œ (1...𝑉)) ∧ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}) Fn (π‘ˆ β€œ ((𝑉 + 1)...𝑁)) ∧ (((π‘ˆ β€œ (1...𝑉)) ∩ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) = βˆ… ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))) β†’ ((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})β€˜π‘›))
17971, 74, 178mp3an12 1451 . . . . . . . . . . . . . . . . . . . 20 ((((π‘ˆ β€œ (1...𝑉)) ∩ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) = βˆ… ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) β†’ ((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})β€˜π‘›))
18083, 179sylan 580 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) β†’ ((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})β€˜π‘›))
18172fvconst2 7153 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁)) β†’ (((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})β€˜π‘›) = 0)
182181adantl 482 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) β†’ (((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})β€˜π‘›) = 0)
183180, 182eqtrd 2776 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) β†’ ((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))β€˜π‘›) = 0)
184177, 183syldan 591 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) β†’ ((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))β€˜π‘›) = 0)
185184adantr 481 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))β€˜π‘›) = 0)
186165, 166, 167, 167, 111, 168, 185ofval 7628 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›) = ((π‘‡β€˜π‘›) + 0))
187140adantr 481 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) β†’ (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})) Fn (1...𝑁))
188 fvun2 6933 . . . . . . . . . . . . . . . . . . . 20 ((((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) Fn (π‘ˆ β€œ (1...(𝑉 + 1))) ∧ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}) Fn (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) ∧ (((π‘ˆ β€œ (1...(𝑉 + 1))) ∩ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) = βˆ… ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)))) β†’ ((((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})β€˜π‘›))
189122, 124, 188mp3an12 1451 . . . . . . . . . . . . . . . . . . 19 ((((π‘ˆ β€œ (1...(𝑉 + 1))) ∩ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) = βˆ… ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) β†’ ((((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})β€˜π‘›))
190132, 189sylan 580 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) β†’ ((((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})β€˜π‘›))
19172fvconst2 7153 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) β†’ (((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})β€˜π‘›) = 0)
192191adantl 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) β†’ (((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})β€˜π‘›) = 0)
193190, 192eqtrd 2776 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) β†’ ((((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}))β€˜π‘›) = 0)
194193adantr 481 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}))β€˜π‘›) = 0)
195165, 187, 167, 167, 111, 168, 194ofval 7628 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})))β€˜π‘›) = ((π‘‡β€˜π‘›) + 0))
196186, 195eqtr4d 2779 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})))β€˜π‘›))
197164, 196mpdan 685 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})))β€˜π‘›))
198161, 197jaodan 956 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑛 ∈ (π‘ˆ β€œ (1...𝑉)) ∨ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)))) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})))β€˜π‘›))
199198adantlr 713 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ (𝑛 ∈ (π‘ˆ β€œ (1...𝑉)) ∨ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)))) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})))β€˜π‘›))
200 poimirlem2.1 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐹 = (𝑦 ∈ (0...(𝑁 βˆ’ 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / π‘—β¦Œ(𝑇 ∘f + (((π‘ˆ β€œ (1...𝑗)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0})))))
201200adantr 481 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ 𝐹 = (𝑦 ∈ (0...(𝑁 βˆ’ 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / π‘—β¦Œ(𝑇 ∘f + (((π‘ˆ β€œ (1...𝑗)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0})))))
202 vex 3449 . . . . . . . . . . . . . . . . 17 𝑦 ∈ V
203 ovex 7390 . . . . . . . . . . . . . . . . 17 (𝑦 + 1) ∈ V
204202, 203ifex 4536 . . . . . . . . . . . . . . . 16 if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V
205204a1i 11 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 βˆ’ 1)) β†’ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V)
206 breq1 5108 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (𝑉 βˆ’ 1) β†’ (𝑦 < 𝑀 ↔ (𝑉 βˆ’ 1) < 𝑀))
207206adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑦 = (𝑉 βˆ’ 1)) β†’ (𝑦 < 𝑀 ↔ (𝑉 βˆ’ 1) < 𝑀))
208 simpr 485 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑦 = (𝑉 βˆ’ 1)) β†’ 𝑦 = (𝑉 βˆ’ 1))
209 oveq1 7364 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (𝑉 βˆ’ 1) β†’ (𝑦 + 1) = ((𝑉 βˆ’ 1) + 1))
21026zcnd 12608 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ 𝑉 ∈ β„‚)
211 npcan1 11580 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑉 ∈ β„‚ β†’ ((𝑉 βˆ’ 1) + 1) = 𝑉)
212210, 211syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ ((𝑉 βˆ’ 1) + 1) = 𝑉)
213209, 212sylan9eqr 2798 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑦 = (𝑉 βˆ’ 1)) β†’ (𝑦 + 1) = 𝑉)
214207, 208, 213ifbieq12d 4514 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑦 = (𝑉 βˆ’ 1)) β†’ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑉 βˆ’ 1) < 𝑀, (𝑉 βˆ’ 1), 𝑉))
215214adantlr 713 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 βˆ’ 1)) β†’ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑉 βˆ’ 1) < 𝑀, (𝑉 βˆ’ 1), 𝑉))
216 poimirlem2.5 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ 𝑀 ∈ ((0...𝑁) βˆ– {𝑉}))
217216eldifad 3922 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ 𝑀 ∈ (0...𝑁))
218217elfzelzd 13442 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ 𝑀 ∈ β„€)
219 zltlem1 12556 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑀 ∈ β„€ ∧ 𝑉 ∈ β„€) β†’ (𝑀 < 𝑉 ↔ 𝑀 ≀ (𝑉 βˆ’ 1)))
220218, 26, 219syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ (𝑀 < 𝑉 ↔ 𝑀 ≀ (𝑉 βˆ’ 1)))
221218zred 12607 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ 𝑀 ∈ ℝ)
222 peano2zm 12546 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑉 ∈ β„€ β†’ (𝑉 βˆ’ 1) ∈ β„€)
22326, 222syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ (𝑉 βˆ’ 1) ∈ β„€)
224223zred 12607 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (𝑉 βˆ’ 1) ∈ ℝ)
225221, 224lenltd 11301 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ (𝑀 ≀ (𝑉 βˆ’ 1) ↔ Β¬ (𝑉 βˆ’ 1) < 𝑀))
226220, 225bitrd 278 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (𝑀 < 𝑉 ↔ Β¬ (𝑉 βˆ’ 1) < 𝑀))
227226biimpa 477 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ Β¬ (𝑉 βˆ’ 1) < 𝑀)
228227iffalsed 4497 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ if((𝑉 βˆ’ 1) < 𝑀, (𝑉 βˆ’ 1), 𝑉) = 𝑉)
229228adantr 481 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 βˆ’ 1)) β†’ if((𝑉 βˆ’ 1) < 𝑀, (𝑉 βˆ’ 1), 𝑉) = 𝑉)
230215, 229eqtrd 2776 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 βˆ’ 1)) β†’ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = 𝑉)
231230eqeq2d 2747 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 βˆ’ 1)) β†’ (𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ↔ 𝑗 = 𝑉))
232231biimpa 477 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 βˆ’ 1)) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) β†’ 𝑗 = 𝑉)
233 oveq2 7365 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑉 β†’ (1...𝑗) = (1...𝑉))
234233imaeq2d 6013 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑉 β†’ (π‘ˆ β€œ (1...𝑗)) = (π‘ˆ β€œ (1...𝑉)))
235234xpeq1d 5662 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑉 β†’ ((π‘ˆ β€œ (1...𝑗)) Γ— {1}) = ((π‘ˆ β€œ (1...𝑉)) Γ— {1}))
236 oveq1 7364 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑉 β†’ (𝑗 + 1) = (𝑉 + 1))
237236oveq1d 7372 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑉 β†’ ((𝑗 + 1)...𝑁) = ((𝑉 + 1)...𝑁))
238237imaeq2d 6013 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑉 β†’ (π‘ˆ β€œ ((𝑗 + 1)...𝑁)) = (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))
239238xpeq1d 5662 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑉 β†’ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0}) = ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))
240235, 239uneq12d 4124 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑉 β†’ (((π‘ˆ β€œ (1...𝑗)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0})) = (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))
241240oveq2d 7373 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑉 β†’ (𝑇 ∘f + (((π‘ˆ β€œ (1...𝑗)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0}))) = (𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))))
242232, 241syl 17 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 βˆ’ 1)) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) β†’ (𝑇 ∘f + (((π‘ˆ β€œ (1...𝑗)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0}))) = (𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))))
243205, 242csbied 3893 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 βˆ’ 1)) β†’ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / π‘—β¦Œ(𝑇 ∘f + (((π‘ˆ β€œ (1...𝑗)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0}))) = (𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))))
244 elfzm1b 13519 . . . . . . . . . . . . . . . . 17 ((𝑉 ∈ β„€ ∧ 𝑁 ∈ β„€) β†’ (𝑉 ∈ (1...𝑁) ↔ (𝑉 βˆ’ 1) ∈ (0...(𝑁 βˆ’ 1))))
24526, 87, 244syl2anc 584 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝑉 ∈ (1...𝑁) ↔ (𝑉 βˆ’ 1) ∈ (0...(𝑁 βˆ’ 1))))
24697, 245mpbid 231 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑉 βˆ’ 1) ∈ (0...(𝑁 βˆ’ 1)))
247246adantr 481 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ (𝑉 βˆ’ 1) ∈ (0...(𝑁 βˆ’ 1)))
248 ovexd 7392 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ (𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))) ∈ V)
249201, 243, 247, 248fvmptd 6955 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ (πΉβ€˜(𝑉 βˆ’ 1)) = (𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))))
250249fveq1d 6844 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ ((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›))
251250adantr 481 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ (𝑛 ∈ (π‘ˆ β€œ (1...𝑉)) ∨ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)))) β†’ ((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›))
252204a1i 11 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) β†’ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V)
253 breq1 5108 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑉 β†’ (𝑦 < 𝑀 ↔ 𝑉 < 𝑀))
254 id 22 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑉 β†’ 𝑦 = 𝑉)
255 oveq1 7364 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑉 β†’ (𝑦 + 1) = (𝑉 + 1))
256253, 254, 255ifbieq12d 4514 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑉 β†’ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if(𝑉 < 𝑀, 𝑉, (𝑉 + 1)))
257 ltnsym 11253 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑀 ∈ ℝ ∧ 𝑉 ∈ ℝ) β†’ (𝑀 < 𝑉 β†’ Β¬ 𝑉 < 𝑀))
258221, 27, 257syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (𝑀 < 𝑉 β†’ Β¬ 𝑉 < 𝑀))
259258imp 407 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ Β¬ 𝑉 < 𝑀)
260259iffalsed 4497 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ if(𝑉 < 𝑀, 𝑉, (𝑉 + 1)) = (𝑉 + 1))
261256, 260sylan9eqr 2798 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) β†’ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = (𝑉 + 1))
262261eqeq2d 2747 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) β†’ (𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ↔ 𝑗 = (𝑉 + 1)))
263262biimpa 477 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) β†’ 𝑗 = (𝑉 + 1))
264 oveq2 7365 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = (𝑉 + 1) β†’ (1...𝑗) = (1...(𝑉 + 1)))
265264imaeq2d 6013 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑉 + 1) β†’ (π‘ˆ β€œ (1...𝑗)) = (π‘ˆ β€œ (1...(𝑉 + 1))))
266265xpeq1d 5662 . . . . . . . . . . . . . . . . . 18 (𝑗 = (𝑉 + 1) β†’ ((π‘ˆ β€œ (1...𝑗)) Γ— {1}) = ((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}))
267 oveq1 7364 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = (𝑉 + 1) β†’ (𝑗 + 1) = ((𝑉 + 1) + 1))
268267oveq1d 7372 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = (𝑉 + 1) β†’ ((𝑗 + 1)...𝑁) = (((𝑉 + 1) + 1)...𝑁))
269268imaeq2d 6013 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑉 + 1) β†’ (π‘ˆ β€œ ((𝑗 + 1)...𝑁)) = (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)))
270269xpeq1d 5662 . . . . . . . . . . . . . . . . . 18 (𝑗 = (𝑉 + 1) β†’ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0}) = ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}))
271266, 270uneq12d 4124 . . . . . . . . . . . . . . . . 17 (𝑗 = (𝑉 + 1) β†’ (((π‘ˆ β€œ (1...𝑗)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0})) = (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})))
272271oveq2d 7373 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑉 + 1) β†’ (𝑇 ∘f + (((π‘ˆ β€œ (1...𝑗)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0}))) = (𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}))))
273263, 272syl 17 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) β†’ (𝑇 ∘f + (((π‘ˆ β€œ (1...𝑗)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0}))) = (𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}))))
274252, 273csbied 3893 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) β†’ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / π‘—β¦Œ(𝑇 ∘f + (((π‘ˆ β€œ (1...𝑗)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0}))) = (𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}))))
275 fz1ssfz0 13537 . . . . . . . . . . . . . . . 16 (1...(𝑁 βˆ’ 1)) βŠ† (0...(𝑁 βˆ’ 1))
276275, 7sselid 3942 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑉 ∈ (0...(𝑁 βˆ’ 1)))
277276adantr 481 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ 𝑉 ∈ (0...(𝑁 βˆ’ 1)))
278 ovexd 7392 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ (𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}))) ∈ V)
279201, 274, 277, 278fvmptd 6955 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ (πΉβ€˜π‘‰) = (𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}))))
280279fveq1d 6844 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ ((πΉβ€˜π‘‰)β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})))β€˜π‘›))
281280adantr 481 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ (𝑛 ∈ (π‘ˆ β€œ (1...𝑉)) ∨ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)))) β†’ ((πΉβ€˜π‘‰)β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})))β€˜π‘›))
282199, 251, 2813eqtr4d 2786 . . . . . . . . . 10 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ (𝑛 ∈ (π‘ˆ β€œ (1...𝑉)) ∨ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)))) β†’ ((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) = ((πΉβ€˜π‘‰)β€˜π‘›))
283282ex 413 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ ((𝑛 ∈ (π‘ˆ β€œ (1...𝑉)) ∨ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) β†’ ((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) = ((πΉβ€˜π‘‰)β€˜π‘›)))
28459, 283sylbid 239 . . . . . . . 8 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ ((𝑛 ∈ (π‘ˆ β€œ (1...𝑁)) ∧ Β¬ 𝑛 ∈ (π‘ˆ β€œ {(𝑉 + 1)})) β†’ ((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) = ((πΉβ€˜π‘‰)β€˜π‘›)))
285284expdimp 453 . . . . . . 7 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑁))) β†’ (Β¬ 𝑛 ∈ (π‘ˆ β€œ {(𝑉 + 1)}) β†’ ((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) = ((πΉβ€˜π‘‰)β€˜π‘›)))
286285necon1ad 2960 . . . . . 6 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑁))) β†’ (((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 ∈ (π‘ˆ β€œ {(𝑉 + 1)})))
287 elimasni 6043 . . . . . . . 8 (𝑛 ∈ (π‘ˆ β€œ {(𝑉 + 1)}) β†’ (𝑉 + 1)π‘ˆπ‘›)
288 eqcom 2743 . . . . . . . . 9 (𝑛 = (π‘ˆβ€˜(𝑉 + 1)) ↔ (π‘ˆβ€˜(𝑉 + 1)) = 𝑛)
289 f1ofn 6785 . . . . . . . . . . 11 (π‘ˆ:(1...𝑁)–1-1-ontoβ†’(1...𝑁) β†’ π‘ˆ Fn (1...𝑁))
2901, 289syl 17 . . . . . . . . . 10 (πœ‘ β†’ π‘ˆ Fn (1...𝑁))
291 fnbrfvb 6895 . . . . . . . . . 10 ((π‘ˆ Fn (1...𝑁) ∧ (𝑉 + 1) ∈ (1...𝑁)) β†’ ((π‘ˆβ€˜(𝑉 + 1)) = 𝑛 ↔ (𝑉 + 1)π‘ˆπ‘›))
292290, 15, 291syl2anc 584 . . . . . . . . 9 (πœ‘ β†’ ((π‘ˆβ€˜(𝑉 + 1)) = 𝑛 ↔ (𝑉 + 1)π‘ˆπ‘›))
293288, 292bitrid 282 . . . . . . . 8 (πœ‘ β†’ (𝑛 = (π‘ˆβ€˜(𝑉 + 1)) ↔ (𝑉 + 1)π‘ˆπ‘›))
294287, 293syl5ibr 245 . . . . . . 7 (πœ‘ β†’ (𝑛 ∈ (π‘ˆ β€œ {(𝑉 + 1)}) β†’ 𝑛 = (π‘ˆβ€˜(𝑉 + 1))))
295294ad2antrr 724 . . . . . 6 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑁))) β†’ (𝑛 ∈ (π‘ˆ β€œ {(𝑉 + 1)}) β†’ 𝑛 = (π‘ˆβ€˜(𝑉 + 1))))
296286, 295syld 47 . . . . 5 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑁))) β†’ (((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = (π‘ˆβ€˜(𝑉 + 1))))
297296ralrimiva 3143 . . . 4 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ βˆ€π‘› ∈ (π‘ˆ β€œ (1...𝑁))(((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = (π‘ˆβ€˜(𝑉 + 1))))
298 fvex 6855 . . . . 5 (π‘ˆβ€˜(𝑉 + 1)) ∈ V
299 eqeq2 2748 . . . . . . 7 (π‘š = (π‘ˆβ€˜(𝑉 + 1)) β†’ (𝑛 = π‘š ↔ 𝑛 = (π‘ˆβ€˜(𝑉 + 1))))
300299imbi2d 340 . . . . . 6 (π‘š = (π‘ˆβ€˜(𝑉 + 1)) β†’ ((((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = π‘š) ↔ (((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = (π‘ˆβ€˜(𝑉 + 1)))))
301300ralbidv 3174 . . . . 5 (π‘š = (π‘ˆβ€˜(𝑉 + 1)) β†’ (βˆ€π‘› ∈ (π‘ˆ β€œ (1...𝑁))(((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = π‘š) ↔ βˆ€π‘› ∈ (π‘ˆ β€œ (1...𝑁))(((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = (π‘ˆβ€˜(𝑉 + 1)))))
302298, 301spcev 3565 . . . 4 (βˆ€π‘› ∈ (π‘ˆ β€œ (1...𝑁))(((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = (π‘ˆβ€˜(𝑉 + 1))) β†’ βˆƒπ‘šβˆ€π‘› ∈ (π‘ˆ β€œ (1...𝑁))(((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = π‘š))
303297, 302syl 17 . . 3 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ βˆƒπ‘šβˆ€π‘› ∈ (π‘ˆ β€œ (1...𝑁))(((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = π‘š))
304 imadif 6585 . . . . . . . . . . . . . . 15 (Fun β—‘π‘ˆ β†’ (π‘ˆ β€œ ((1...𝑁) βˆ– {𝑉})) = ((π‘ˆ β€œ (1...𝑁)) βˆ– (π‘ˆ β€œ {𝑉})))
3054, 304syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘ˆ β€œ ((1...𝑁) βˆ– {𝑉})) = ((π‘ˆ β€œ (1...𝑁)) βˆ– (π‘ˆ β€œ {𝑉})))
30699difeq1d 4081 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((1...𝑁) βˆ– {𝑉}) = (((1...𝑉) βˆͺ ((𝑉 + 1)...𝑁)) βˆ– {𝑉}))
307 difundir 4240 . . . . . . . . . . . . . . . . 17 (((1...𝑉) βˆͺ ((𝑉 + 1)...𝑁)) βˆ– {𝑉}) = (((1...𝑉) βˆ– {𝑉}) βˆͺ (((𝑉 + 1)...𝑁) βˆ– {𝑉}))
308212, 21eqeltrd 2837 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ ((𝑉 βˆ’ 1) + 1) ∈ (β„€β‰₯β€˜1))
309 uzid 12778 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑉 βˆ’ 1) ∈ β„€ β†’ (𝑉 βˆ’ 1) ∈ (β„€β‰₯β€˜(𝑉 βˆ’ 1)))
310223, 309syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (𝑉 βˆ’ 1) ∈ (β„€β‰₯β€˜(𝑉 βˆ’ 1)))
311 peano2uz 12826 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑉 βˆ’ 1) ∈ (β„€β‰₯β€˜(𝑉 βˆ’ 1)) β†’ ((𝑉 βˆ’ 1) + 1) ∈ (β„€β‰₯β€˜(𝑉 βˆ’ 1)))
312310, 311syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ ((𝑉 βˆ’ 1) + 1) ∈ (β„€β‰₯β€˜(𝑉 βˆ’ 1)))
313212, 312eqeltrrd 2838 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ 𝑉 ∈ (β„€β‰₯β€˜(𝑉 βˆ’ 1)))
314 fzsplit2 13466 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑉 βˆ’ 1) + 1) ∈ (β„€β‰₯β€˜1) ∧ 𝑉 ∈ (β„€β‰₯β€˜(𝑉 βˆ’ 1))) β†’ (1...𝑉) = ((1...(𝑉 βˆ’ 1)) βˆͺ (((𝑉 βˆ’ 1) + 1)...𝑉)))
315308, 313, 314syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (1...𝑉) = ((1...(𝑉 βˆ’ 1)) βˆͺ (((𝑉 βˆ’ 1) + 1)...𝑉)))
316212oveq1d 7372 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ (((𝑉 βˆ’ 1) + 1)...𝑉) = (𝑉...𝑉))
317 fzsn 13483 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑉 ∈ β„€ β†’ (𝑉...𝑉) = {𝑉})
31826, 317syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ (𝑉...𝑉) = {𝑉})
319316, 318eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (((𝑉 βˆ’ 1) + 1)...𝑉) = {𝑉})
320319uneq2d 4123 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ ((1...(𝑉 βˆ’ 1)) βˆͺ (((𝑉 βˆ’ 1) + 1)...𝑉)) = ((1...(𝑉 βˆ’ 1)) βˆͺ {𝑉}))
321315, 320eqtrd 2776 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (1...𝑉) = ((1...(𝑉 βˆ’ 1)) βˆͺ {𝑉}))
322321difeq1d 4081 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ((1...𝑉) βˆ– {𝑉}) = (((1...(𝑉 βˆ’ 1)) βˆͺ {𝑉}) βˆ– {𝑉}))
323 difun2 4440 . . . . . . . . . . . . . . . . . . . 20 (((1...(𝑉 βˆ’ 1)) βˆͺ {𝑉}) βˆ– {𝑉}) = ((1...(𝑉 βˆ’ 1)) βˆ– {𝑉})
32427ltm1d 12087 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ (𝑉 βˆ’ 1) < 𝑉)
325224, 27ltnled 11302 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ ((𝑉 βˆ’ 1) < 𝑉 ↔ Β¬ 𝑉 ≀ (𝑉 βˆ’ 1)))
326324, 325mpbid 231 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ Β¬ 𝑉 ≀ (𝑉 βˆ’ 1))
327 elfzle2 13445 . . . . . . . . . . . . . . . . . . . . . 22 (𝑉 ∈ (1...(𝑉 βˆ’ 1)) β†’ 𝑉 ≀ (𝑉 βˆ’ 1))
328326, 327nsyl 140 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ Β¬ 𝑉 ∈ (1...(𝑉 βˆ’ 1)))
329 difsn 4758 . . . . . . . . . . . . . . . . . . . . 21 (Β¬ 𝑉 ∈ (1...(𝑉 βˆ’ 1)) β†’ ((1...(𝑉 βˆ’ 1)) βˆ– {𝑉}) = (1...(𝑉 βˆ’ 1)))
330328, 329syl 17 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((1...(𝑉 βˆ’ 1)) βˆ– {𝑉}) = (1...(𝑉 βˆ’ 1)))
331323, 330eqtrid 2788 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (((1...(𝑉 βˆ’ 1)) βˆͺ {𝑉}) βˆ– {𝑉}) = (1...(𝑉 βˆ’ 1)))
332322, 331eqtrd 2776 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ ((1...𝑉) βˆ– {𝑉}) = (1...(𝑉 βˆ’ 1)))
333 elfzle1 13444 . . . . . . . . . . . . . . . . . . . 20 (𝑉 ∈ ((𝑉 + 1)...𝑁) β†’ (𝑉 + 1) ≀ 𝑉)
33432, 333nsyl 140 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ Β¬ 𝑉 ∈ ((𝑉 + 1)...𝑁))
335 difsn 4758 . . . . . . . . . . . . . . . . . . 19 (Β¬ 𝑉 ∈ ((𝑉 + 1)...𝑁) β†’ (((𝑉 + 1)...𝑁) βˆ– {𝑉}) = ((𝑉 + 1)...𝑁))
336334, 335syl 17 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (((𝑉 + 1)...𝑁) βˆ– {𝑉}) = ((𝑉 + 1)...𝑁))
337332, 336uneq12d 4124 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (((1...𝑉) βˆ– {𝑉}) βˆͺ (((𝑉 + 1)...𝑁) βˆ– {𝑉})) = ((1...(𝑉 βˆ’ 1)) βˆͺ ((𝑉 + 1)...𝑁)))
338307, 337eqtrid 2788 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (((1...𝑉) βˆͺ ((𝑉 + 1)...𝑁)) βˆ– {𝑉}) = ((1...(𝑉 βˆ’ 1)) βˆͺ ((𝑉 + 1)...𝑁)))
339306, 338eqtrd 2776 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((1...𝑁) βˆ– {𝑉}) = ((1...(𝑉 βˆ’ 1)) βˆͺ ((𝑉 + 1)...𝑁)))
340339imaeq2d 6013 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘ˆ β€œ ((1...𝑁) βˆ– {𝑉})) = (π‘ˆ β€œ ((1...(𝑉 βˆ’ 1)) βˆͺ ((𝑉 + 1)...𝑁))))
341305, 340eqtr3d 2778 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π‘ˆ β€œ (1...𝑁)) βˆ– (π‘ˆ β€œ {𝑉})) = (π‘ˆ β€œ ((1...(𝑉 βˆ’ 1)) βˆͺ ((𝑉 + 1)...𝑁))))
342 imaundi 6102 . . . . . . . . . . . . 13 (π‘ˆ β€œ ((1...(𝑉 βˆ’ 1)) βˆͺ ((𝑉 + 1)...𝑁))) = ((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) βˆͺ (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))
343341, 342eqtrdi 2792 . . . . . . . . . . . 12 (πœ‘ β†’ ((π‘ˆ β€œ (1...𝑁)) βˆ– (π‘ˆ β€œ {𝑉})) = ((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) βˆͺ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))))
344343eleq2d 2823 . . . . . . . . . . 11 (πœ‘ β†’ (𝑛 ∈ ((π‘ˆ β€œ (1...𝑁)) βˆ– (π‘ˆ β€œ {𝑉})) ↔ 𝑛 ∈ ((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) βˆͺ (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))))
345 eldif 3920 . . . . . . . . . . 11 (𝑛 ∈ ((π‘ˆ β€œ (1...𝑁)) βˆ– (π‘ˆ β€œ {𝑉})) ↔ (𝑛 ∈ (π‘ˆ β€œ (1...𝑁)) ∧ Β¬ 𝑛 ∈ (π‘ˆ β€œ {𝑉})))
346 elun 4108 . . . . . . . . . . 11 (𝑛 ∈ ((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) βˆͺ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) ↔ (𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∨ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))))
347344, 345, 3463bitr3g 312 . . . . . . . . . 10 (πœ‘ β†’ ((𝑛 ∈ (π‘ˆ β€œ (1...𝑁)) ∧ Β¬ 𝑛 ∈ (π‘ˆ β€œ {𝑉})) ↔ (𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∨ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))))
348347adantr 481 . . . . . . . . 9 ((πœ‘ ∧ 𝑉 < 𝑀) β†’ ((𝑛 ∈ (π‘ˆ β€œ (1...𝑁)) ∧ Β¬ 𝑛 ∈ (π‘ˆ β€œ {𝑉})) ↔ (𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∨ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))))
349 imassrn 6024 . . . . . . . . . . . . . . . 16 (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) βŠ† ran π‘ˆ
350349, 63sstrid 3955 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) βŠ† (1...𝑁))
351350sselda 3944 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) β†’ 𝑛 ∈ (1...𝑁))
35267adantr 481 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) β†’ 𝑇 Fn (1...𝑁))
353 fnconstg 6730 . . . . . . . . . . . . . . . . . . . . 21 (1 ∈ V β†’ ((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) Fn (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))))
35469, 353ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) Fn (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))
355 fnconstg 6730 . . . . . . . . . . . . . . . . . . . . 21 (0 ∈ V β†’ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}) Fn (π‘ˆ β€œ (𝑉...𝑁)))
35672, 355ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}) Fn (π‘ˆ β€œ (𝑉...𝑁))
357354, 356pm3.2i 471 . . . . . . . . . . . . . . . . . . 19 (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) Fn (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∧ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}) Fn (π‘ˆ β€œ (𝑉...𝑁)))
358 imain 6586 . . . . . . . . . . . . . . . . . . . . 21 (Fun β—‘π‘ˆ β†’ (π‘ˆ β€œ ((1...(𝑉 βˆ’ 1)) ∩ (𝑉...𝑁))) = ((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∩ (π‘ˆ β€œ (𝑉...𝑁))))
3594, 358syl 17 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (π‘ˆ β€œ ((1...(𝑉 βˆ’ 1)) ∩ (𝑉...𝑁))) = ((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∩ (π‘ˆ β€œ (𝑉...𝑁))))
360 fzdisj 13468 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑉 βˆ’ 1) < 𝑉 β†’ ((1...(𝑉 βˆ’ 1)) ∩ (𝑉...𝑁)) = βˆ…)
361324, 360syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ ((1...(𝑉 βˆ’ 1)) ∩ (𝑉...𝑁)) = βˆ…)
362361imaeq2d 6013 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (π‘ˆ β€œ ((1...(𝑉 βˆ’ 1)) ∩ (𝑉...𝑁))) = (π‘ˆ β€œ βˆ…))
363362, 81eqtrdi 2792 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (π‘ˆ β€œ ((1...(𝑉 βˆ’ 1)) ∩ (𝑉...𝑁))) = βˆ…)
364359, 363eqtr3d 2778 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∩ (π‘ˆ β€œ (𝑉...𝑁))) = βˆ…)
365 fnun 6614 . . . . . . . . . . . . . . . . . . 19 (((((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) Fn (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∧ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}) Fn (π‘ˆ β€œ (𝑉...𝑁))) ∧ ((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∩ (π‘ˆ β€œ (𝑉...𝑁))) = βˆ…) β†’ (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})) Fn ((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) βˆͺ (π‘ˆ β€œ (𝑉...𝑁))))
366357, 364, 365sylancr 587 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})) Fn ((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) βˆͺ (π‘ˆ β€œ (𝑉...𝑁))))
367 imaundi 6102 . . . . . . . . . . . . . . . . . . . 20 (π‘ˆ β€œ ((1...(𝑉 βˆ’ 1)) βˆͺ (𝑉...𝑁))) = ((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) βˆͺ (π‘ˆ β€œ (𝑉...𝑁)))
368 uzss 12786 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑉 ∈ (β„€β‰₯β€˜(𝑉 βˆ’ 1)) β†’ (β„€β‰₯β€˜π‘‰) βŠ† (β„€β‰₯β€˜(𝑉 βˆ’ 1)))
369313, 368syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ (β„€β‰₯β€˜π‘‰) βŠ† (β„€β‰₯β€˜(𝑉 βˆ’ 1)))
370 elfzuz3 13438 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑉 ∈ (1...(𝑁 βˆ’ 1)) β†’ (𝑁 βˆ’ 1) ∈ (β„€β‰₯β€˜π‘‰))
3717, 370syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ (𝑁 βˆ’ 1) ∈ (β„€β‰₯β€˜π‘‰))
372369, 371sseldd 3945 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ (𝑁 βˆ’ 1) ∈ (β„€β‰₯β€˜(𝑉 βˆ’ 1)))
373 peano2uz 12826 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑁 βˆ’ 1) ∈ (β„€β‰₯β€˜(𝑉 βˆ’ 1)) β†’ ((𝑁 βˆ’ 1) + 1) ∈ (β„€β‰₯β€˜(𝑉 βˆ’ 1)))
374372, 373syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ ((𝑁 βˆ’ 1) + 1) ∈ (β„€β‰₯β€˜(𝑉 βˆ’ 1)))
37513, 374eqeltrrd 2838 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ 𝑁 ∈ (β„€β‰₯β€˜(𝑉 βˆ’ 1)))
376 fzsplit2 13466 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑉 βˆ’ 1) + 1) ∈ (β„€β‰₯β€˜1) ∧ 𝑁 ∈ (β„€β‰₯β€˜(𝑉 βˆ’ 1))) β†’ (1...𝑁) = ((1...(𝑉 βˆ’ 1)) βˆͺ (((𝑉 βˆ’ 1) + 1)...𝑁)))
377308, 375, 376syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ (1...𝑁) = ((1...(𝑉 βˆ’ 1)) βˆͺ (((𝑉 βˆ’ 1) + 1)...𝑁)))
378212oveq1d 7372 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (((𝑉 βˆ’ 1) + 1)...𝑁) = (𝑉...𝑁))
379378uneq2d 4123 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ ((1...(𝑉 βˆ’ 1)) βˆͺ (((𝑉 βˆ’ 1) + 1)...𝑁)) = ((1...(𝑉 βˆ’ 1)) βˆͺ (𝑉...𝑁)))
380377, 379eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (1...𝑁) = ((1...(𝑉 βˆ’ 1)) βˆͺ (𝑉...𝑁)))
381380imaeq2d 6013 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (π‘ˆ β€œ (1...𝑁)) = (π‘ˆ β€œ ((1...(𝑉 βˆ’ 1)) βˆͺ (𝑉...𝑁))))
382381, 104eqtr3d 2778 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (π‘ˆ β€œ ((1...(𝑉 βˆ’ 1)) βˆͺ (𝑉...𝑁))) = (1...𝑁))
383367, 382eqtr3id 2790 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) βˆͺ (π‘ˆ β€œ (𝑉...𝑁))) = (1...𝑁))
384383fneq2d 6596 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ ((((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})) Fn ((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) βˆͺ (π‘ˆ β€œ (𝑉...𝑁))) ↔ (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})) Fn (1...𝑁)))
385366, 384mpbid 231 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})) Fn (1...𝑁))
386385adantr 481 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) β†’ (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})) Fn (1...𝑁))
387 fzfid 13878 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) β†’ (1...𝑁) ∈ Fin)
388 eqidd 2737 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘‡β€˜π‘›) = (π‘‡β€˜π‘›))
389 fvun1 6932 . . . . . . . . . . . . . . . . . . . 20 ((((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) Fn (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∧ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}) Fn (π‘ˆ β€œ (𝑉...𝑁)) ∧ (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∩ (π‘ˆ β€œ (𝑉...𝑁))) = βˆ… ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))))) β†’ ((((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1})β€˜π‘›))
390354, 356, 389mp3an12 1451 . . . . . . . . . . . . . . . . . . 19 ((((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∩ (π‘ˆ β€œ (𝑉...𝑁))) = βˆ… ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) β†’ ((((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1})β€˜π‘›))
391364, 390sylan 580 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) β†’ ((((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1})β€˜π‘›))
39269fvconst2 7153 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) β†’ (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1})β€˜π‘›) = 1)
393392adantl 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) β†’ (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1})β€˜π‘›) = 1)
394391, 393eqtrd 2776 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) β†’ ((((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))β€˜π‘›) = 1)
395394adantr 481 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))β€˜π‘›) = 1)
396352, 386, 387, 387, 111, 388, 395ofval 7628 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})))β€˜π‘›) = ((π‘‡β€˜π‘›) + 1))
397108adantr 481 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) β†’ (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})) Fn (1...𝑁))
398 fzss2 13481 . . . . . . . . . . . . . . . . . . . . 21 (𝑉 ∈ (β„€β‰₯β€˜(𝑉 βˆ’ 1)) β†’ (1...(𝑉 βˆ’ 1)) βŠ† (1...𝑉))
399313, 398syl 17 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (1...(𝑉 βˆ’ 1)) βŠ† (1...𝑉))
400 imass2 6054 . . . . . . . . . . . . . . . . . . . 20 ((1...(𝑉 βˆ’ 1)) βŠ† (1...𝑉) β†’ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) βŠ† (π‘ˆ β€œ (1...𝑉)))
401399, 400syl 17 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) βŠ† (π‘ˆ β€œ (1...𝑉)))
402401sselda 3944 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) β†’ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉)))
403402, 118syldan 591 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) β†’ ((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))β€˜π‘›) = 1)
404403adantr 481 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))β€˜π‘›) = 1)
405352, 397, 387, 387, 111, 388, 404ofval 7628 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›) = ((π‘‡β€˜π‘›) + 1))
406396, 405eqtr4d 2779 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})))β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›))
407351, 406mpdan 685 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})))β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›))
408 imassrn 6024 . . . . . . . . . . . . . . . 16 (π‘ˆ β€œ ((𝑉 + 1)...𝑁)) βŠ† ran π‘ˆ
409408, 63sstrid 3955 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (π‘ˆ β€œ ((𝑉 + 1)...𝑁)) βŠ† (1...𝑁))
410409sselda 3944 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) β†’ 𝑛 ∈ (1...𝑁))
41167adantr 481 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) β†’ 𝑇 Fn (1...𝑁))
412385adantr 481 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) β†’ (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})) Fn (1...𝑁))
413 fzfid 13878 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) β†’ (1...𝑁) ∈ Fin)
414 eqidd 2737 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘‡β€˜π‘›) = (π‘‡β€˜π‘›))
415 fzss1 13480 . . . . . . . . . . . . . . . . . . . . 21 ((𝑉 + 1) ∈ (β„€β‰₯β€˜π‘‰) β†’ ((𝑉 + 1)...𝑁) βŠ† (𝑉...𝑁))
416145, 415syl 17 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((𝑉 + 1)...𝑁) βŠ† (𝑉...𝑁))
417 imass2 6054 . . . . . . . . . . . . . . . . . . . 20 (((𝑉 + 1)...𝑁) βŠ† (𝑉...𝑁) β†’ (π‘ˆ β€œ ((𝑉 + 1)...𝑁)) βŠ† (π‘ˆ β€œ (𝑉...𝑁)))
418416, 417syl 17 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (π‘ˆ β€œ ((𝑉 + 1)...𝑁)) βŠ† (π‘ˆ β€œ (𝑉...𝑁)))
419418sselda 3944 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) β†’ 𝑛 ∈ (π‘ˆ β€œ (𝑉...𝑁)))
420 fvun2 6933 . . . . . . . . . . . . . . . . . . . . 21 ((((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) Fn (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∧ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}) Fn (π‘ˆ β€œ (𝑉...𝑁)) ∧ (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∩ (π‘ˆ β€œ (𝑉...𝑁))) = βˆ… ∧ 𝑛 ∈ (π‘ˆ β€œ (𝑉...𝑁)))) β†’ ((((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})β€˜π‘›))
421354, 356, 420mp3an12 1451 . . . . . . . . . . . . . . . . . . . 20 ((((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∩ (π‘ˆ β€œ (𝑉...𝑁))) = βˆ… ∧ 𝑛 ∈ (π‘ˆ β€œ (𝑉...𝑁))) β†’ ((((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})β€˜π‘›))
422364, 421sylan 580 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (𝑉...𝑁))) β†’ ((((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})β€˜π‘›))
42372fvconst2 7153 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (π‘ˆ β€œ (𝑉...𝑁)) β†’ (((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})β€˜π‘›) = 0)
424423adantl 482 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (𝑉...𝑁))) β†’ (((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})β€˜π‘›) = 0)
425422, 424eqtrd 2776 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (𝑉...𝑁))) β†’ ((((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))β€˜π‘›) = 0)
426419, 425syldan 591 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) β†’ ((((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))β€˜π‘›) = 0)
427426adantr 481 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))β€˜π‘›) = 0)
428411, 412, 413, 413, 111, 414, 427ofval 7628 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})))β€˜π‘›) = ((π‘‡β€˜π‘›) + 0))
429108adantr 481 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) β†’ (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})) Fn (1...𝑁))
430183adantr 481 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))β€˜π‘›) = 0)
431411, 429, 413, 413, 111, 414, 430ofval 7628 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›) = ((π‘‡β€˜π‘›) + 0))
432428, 431eqtr4d 2779 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})))β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›))
433410, 432mpdan 685 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})))β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›))
434407, 433jaodan 956 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∨ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})))β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›))
435434adantlr 713 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑉 < 𝑀) ∧ (𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∨ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})))β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›))
436200adantr 481 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑉 < 𝑀) β†’ 𝐹 = (𝑦 ∈ (0...(𝑁 βˆ’ 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / π‘—β¦Œ(𝑇 ∘f + (((π‘ˆ β€œ (1...𝑗)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0})))))
437204a1i 11 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 βˆ’ 1)) β†’ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V)
438214adantlr 713 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 βˆ’ 1)) β†’ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑉 βˆ’ 1) < 𝑀, (𝑉 βˆ’ 1), 𝑉))
439 lttr 11231 . . . . . . . . . . . . . . . . . . . . 21 (((𝑉 βˆ’ 1) ∈ ℝ ∧ 𝑉 ∈ ℝ ∧ 𝑀 ∈ ℝ) β†’ (((𝑉 βˆ’ 1) < 𝑉 ∧ 𝑉 < 𝑀) β†’ (𝑉 βˆ’ 1) < 𝑀))
440224, 27, 221, 439syl3anc 1371 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (((𝑉 βˆ’ 1) < 𝑉 ∧ 𝑉 < 𝑀) β†’ (𝑉 βˆ’ 1) < 𝑀))
441324, 440mpand 693 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (𝑉 < 𝑀 β†’ (𝑉 βˆ’ 1) < 𝑀))
442441imp 407 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑉 < 𝑀) β†’ (𝑉 βˆ’ 1) < 𝑀)
443442iftrued 4494 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑉 < 𝑀) β†’ if((𝑉 βˆ’ 1) < 𝑀, (𝑉 βˆ’ 1), 𝑉) = (𝑉 βˆ’ 1))
444443adantr 481 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 βˆ’ 1)) β†’ if((𝑉 βˆ’ 1) < 𝑀, (𝑉 βˆ’ 1), 𝑉) = (𝑉 βˆ’ 1))
445438, 444eqtrd 2776 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 βˆ’ 1)) β†’ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = (𝑉 βˆ’ 1))
446 simpll 765 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 βˆ’ 1)) β†’ πœ‘)
447 oveq2 7365 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = (𝑉 βˆ’ 1) β†’ (1...𝑗) = (1...(𝑉 βˆ’ 1)))
448447imaeq2d 6013 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = (𝑉 βˆ’ 1) β†’ (π‘ˆ β€œ (1...𝑗)) = (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))))
449448xpeq1d 5662 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑉 βˆ’ 1) β†’ ((π‘ˆ β€œ (1...𝑗)) Γ— {1}) = ((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}))
450449adantl 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑗 = (𝑉 βˆ’ 1)) β†’ ((π‘ˆ β€œ (1...𝑗)) Γ— {1}) = ((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}))
451 oveq1 7364 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = (𝑉 βˆ’ 1) β†’ (𝑗 + 1) = ((𝑉 βˆ’ 1) + 1))
452451, 212sylan9eqr 2798 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑗 = (𝑉 βˆ’ 1)) β†’ (𝑗 + 1) = 𝑉)
453452oveq1d 7372 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑗 = (𝑉 βˆ’ 1)) β†’ ((𝑗 + 1)...𝑁) = (𝑉...𝑁))
454453imaeq2d 6013 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑗 = (𝑉 βˆ’ 1)) β†’ (π‘ˆ β€œ ((𝑗 + 1)...𝑁)) = (π‘ˆ β€œ (𝑉...𝑁)))
455454xpeq1d 5662 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑗 = (𝑉 βˆ’ 1)) β†’ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0}) = ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))
456450, 455uneq12d 4124 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑗 = (𝑉 βˆ’ 1)) β†’ (((π‘ˆ β€œ (1...𝑗)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0})) = (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})))
457456oveq2d 7373 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑗 = (𝑉 βˆ’ 1)) β†’ (𝑇 ∘f + (((π‘ˆ β€œ (1...𝑗)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0}))) = (𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))))
458446, 457sylan 580 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 βˆ’ 1)) ∧ 𝑗 = (𝑉 βˆ’ 1)) β†’ (𝑇 ∘f + (((π‘ˆ β€œ (1...𝑗)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0}))) = (𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))))
459437, 445, 458csbied2 3895 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 βˆ’ 1)) β†’ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / π‘—β¦Œ(𝑇 ∘f + (((π‘ˆ β€œ (1...𝑗)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0}))) = (𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))))
460246adantr 481 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑉 < 𝑀) β†’ (𝑉 βˆ’ 1) ∈ (0...(𝑁 βˆ’ 1)))
461 ovexd 7392 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑉 < 𝑀) β†’ (𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))) ∈ V)
462436, 459, 460, 461fvmptd 6955 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑉 < 𝑀) β†’ (πΉβ€˜(𝑉 βˆ’ 1)) = (𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))))
463462fveq1d 6844 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑉 < 𝑀) β†’ ((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})))β€˜π‘›))
464463adantr 481 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑉 < 𝑀) ∧ (𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∨ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))) β†’ ((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})))β€˜π‘›))
465204a1i 11 . . . . . . . . . . . . . . . 16 ((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) β†’ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V)
466 iftrue 4492 . . . . . . . . . . . . . . . . . . . 20 (𝑉 < 𝑀 β†’ if(𝑉 < 𝑀, 𝑉, (𝑉 + 1)) = 𝑉)
467256, 466sylan9eqr 2798 . . . . . . . . . . . . . . . . . . 19 ((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) β†’ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = 𝑉)
468467eqeq2d 2747 . . . . . . . . . . . . . . . . . 18 ((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) β†’ (𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ↔ 𝑗 = 𝑉))
469468biimpa 477 . . . . . . . . . . . . . . . . 17 (((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) β†’ 𝑗 = 𝑉)
470469, 241syl 17 . . . . . . . . . . . . . . . 16 (((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) β†’ (𝑇 ∘f + (((π‘ˆ β€œ (1...𝑗)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0}))) = (𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))))
471465, 470csbied 3893 . . . . . . . . . . . . . . 15 ((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) β†’ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / π‘—β¦Œ(𝑇 ∘f + (((π‘ˆ β€œ (1...𝑗)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0}))) = (𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))))
472471adantll 712 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑉 < 𝑀) ∧ 𝑦 = 𝑉) β†’ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / π‘—β¦Œ(𝑇 ∘f + (((π‘ˆ β€œ (1...𝑗)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0}))) = (𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))))
473276adantr 481 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑉 < 𝑀) β†’ 𝑉 ∈ (0...(𝑁 βˆ’ 1)))
474 ovexd 7392 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑉 < 𝑀) β†’ (𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))) ∈ V)
475436, 472, 473, 474fvmptd 6955 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑉 < 𝑀) β†’ (πΉβ€˜π‘‰) = (𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))))
476475fveq1d 6844 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑉 < 𝑀) β†’ ((πΉβ€˜π‘‰)β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›))
477476adantr 481 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑉 < 𝑀) ∧ (𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∨ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))) β†’ ((πΉβ€˜π‘‰)β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›))
478435, 464, 4773eqtr4d 2786 . . . . . . . . . 10 (((πœ‘ ∧ 𝑉 < 𝑀) ∧ (𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∨ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))) β†’ ((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) = ((πΉβ€˜π‘‰)β€˜π‘›))
479478ex 413 . . . . . . . . 9 ((πœ‘ ∧ 𝑉 < 𝑀) β†’ ((𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∨ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) β†’ ((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) = ((πΉβ€˜π‘‰)β€˜π‘›)))
480348, 479sylbid 239 . . . . . . . 8 ((πœ‘ ∧ 𝑉 < 𝑀) β†’ ((𝑛 ∈ (π‘ˆ β€œ (1...𝑁)) ∧ Β¬ 𝑛 ∈ (π‘ˆ β€œ {𝑉})) β†’ ((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) = ((πΉβ€˜π‘‰)β€˜π‘›)))
481480expdimp 453 . . . . . . 7 (((πœ‘ ∧ 𝑉 < 𝑀) ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑁))) β†’ (Β¬ 𝑛 ∈ (π‘ˆ β€œ {𝑉}) β†’ ((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) = ((πΉβ€˜π‘‰)β€˜π‘›)))
482481necon1ad 2960 . . . . . 6 (((πœ‘ ∧ 𝑉 < 𝑀) ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑁))) β†’ (((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 ∈ (π‘ˆ β€œ {𝑉})))
483 elimasni 6043 . . . . . . . 8 (𝑛 ∈ (π‘ˆ β€œ {𝑉}) β†’ π‘‰π‘ˆπ‘›)
484 eqcom 2743 . . . . . . . . 9 (𝑛 = (π‘ˆβ€˜π‘‰) ↔ (π‘ˆβ€˜π‘‰) = 𝑛)
485 fnbrfvb 6895 . . . . . . . . . 10 ((π‘ˆ Fn (1...𝑁) ∧ 𝑉 ∈ (1...𝑁)) β†’ ((π‘ˆβ€˜π‘‰) = 𝑛 ↔ π‘‰π‘ˆπ‘›))
486290, 97, 485syl2anc 584 . . . . . . . . 9 (πœ‘ β†’ ((π‘ˆβ€˜π‘‰) = 𝑛 ↔ π‘‰π‘ˆπ‘›))
487484, 486bitrid 282 . . . . . . . 8 (πœ‘ β†’ (𝑛 = (π‘ˆβ€˜π‘‰) ↔ π‘‰π‘ˆπ‘›))
488483, 487syl5ibr 245 . . . . . . 7 (πœ‘ β†’ (𝑛 ∈ (π‘ˆ β€œ {𝑉}) β†’ 𝑛 = (π‘ˆβ€˜π‘‰)))
489488ad2antrr 724 . . . . . 6 (((πœ‘ ∧ 𝑉 < 𝑀) ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑁))) β†’ (𝑛 ∈ (π‘ˆ β€œ {𝑉}) β†’ 𝑛 = (π‘ˆβ€˜π‘‰)))
490482, 489syld 47 . . . . 5 (((πœ‘ ∧ 𝑉 < 𝑀) ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑁))) β†’ (((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = (π‘ˆβ€˜π‘‰)))
491490ralrimiva 3143 . . . 4 ((πœ‘ ∧ 𝑉 < 𝑀) β†’ βˆ€π‘› ∈ (π‘ˆ β€œ (1...𝑁))(((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = (π‘ˆβ€˜π‘‰)))
492 fvex 6855 . . . . 5 (π‘ˆβ€˜π‘‰) ∈ V
493 eqeq2 2748 . . . . . . 7 (π‘š = (π‘ˆβ€˜π‘‰) β†’ (𝑛 = π‘š ↔ 𝑛 = (π‘ˆβ€˜π‘‰)))
494493imbi2d 340 . . . . . 6 (π‘š = (π‘ˆβ€˜π‘‰) β†’ ((((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = π‘š) ↔ (((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = (π‘ˆβ€˜π‘‰))))
495494ralbidv 3174 . . . . 5 (π‘š = (π‘ˆβ€˜π‘‰) β†’ (βˆ€π‘› ∈ (π‘ˆ β€œ (1...𝑁))(((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = π‘š) ↔ βˆ€π‘› ∈ (π‘ˆ β€œ (1...𝑁))(((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = (π‘ˆβ€˜π‘‰))))
496492, 495spcev 3565 . . . 4 (βˆ€π‘› ∈ (π‘ˆ β€œ (1...𝑁))(((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = (π‘ˆβ€˜π‘‰)) β†’ βˆƒπ‘šβˆ€π‘› ∈ (π‘ˆ β€œ (1...𝑁))(((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = π‘š))
497491, 496syl 17 . . 3 ((πœ‘ ∧ 𝑉 < 𝑀) β†’ βˆƒπ‘šβˆ€π‘› ∈ (π‘ˆ β€œ (1...𝑁))(((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = π‘š))
498 eldifsni 4750 . . . . 5 (𝑀 ∈ ((0...𝑁) βˆ– {𝑉}) β†’ 𝑀 β‰  𝑉)
499216, 498syl 17 . . . 4 (πœ‘ β†’ 𝑀 β‰  𝑉)
500221, 27lttri2d 11294 . . . 4 (πœ‘ β†’ (𝑀 β‰  𝑉 ↔ (𝑀 < 𝑉 ∨ 𝑉 < 𝑀)))
501499, 500mpbid 231 . . 3 (πœ‘ β†’ (𝑀 < 𝑉 ∨ 𝑉 < 𝑀))
502303, 497, 501mpjaodan 957 . 2 (πœ‘ β†’ βˆƒπ‘šβˆ€π‘› ∈ (π‘ˆ β€œ (1...𝑁))(((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = π‘š))
503 nfv 1917 . . . 4 β„²π‘š((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›)
504503rmo2 3843 . . 3 (βˆƒ*𝑛 ∈ (π‘ˆ β€œ (1...𝑁))((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) ↔ βˆƒπ‘šβˆ€π‘› ∈ (π‘ˆ β€œ (1...𝑁))(((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = π‘š))
505 rmoeq1 3391 . . . 4 ((π‘ˆ β€œ (1...𝑁)) = (1...𝑁) β†’ (βˆƒ*𝑛 ∈ (π‘ˆ β€œ (1...𝑁))((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) ↔ βˆƒ*𝑛 ∈ (1...𝑁)((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›)))
506104, 505syl 17 . . 3 (πœ‘ β†’ (βˆƒ*𝑛 ∈ (π‘ˆ β€œ (1...𝑁))((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) ↔ βˆƒ*𝑛 ∈ (1...𝑁)((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›)))
507504, 506bitr3id 284 . 2 (πœ‘ β†’ (βˆƒπ‘šβˆ€π‘› ∈ (π‘ˆ β€œ (1...𝑁))(((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = π‘š) ↔ βˆƒ*𝑛 ∈ (1...𝑁)((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›)))
508502, 507mpbid 231 1 (πœ‘ β†’ βˆƒ*𝑛 ∈ (1...𝑁)((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   = wceq 1541  βˆƒwex 1781   ∈ wcel 2106   β‰  wne 2943  βˆ€wral 3064  βˆƒ*wrmo 3352  Vcvv 3445  β¦‹csb 3855   βˆ– cdif 3907   βˆͺ cun 3908   ∩ cin 3909   βŠ† wss 3910  βˆ…c0 4282  ifcif 4486  {csn 4586   class class class wbr 5105   ↦ cmpt 5188   Γ— cxp 5631  β—‘ccnv 5632  ran crn 5634   β€œ cima 5636  Fun wfun 6490   Fn wfn 6491  βŸΆwf 6492  β€“ontoβ†’wfo 6494  β€“1-1-ontoβ†’wf1o 6495  β€˜cfv 6496  (class class class)co 7357   ∘f cof 7615  Fincfn 8883  β„‚cc 11049  β„cr 11050  0cc0 11051  1c1 11052   + caddc 11054   < clt 11189   ≀ cle 11190   βˆ’ cmin 11385  β„•cn 12153  β„€cz 12499  β„€β‰₯cuz 12763  ...cfz 13424
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-nn 12154  df-n0 12414  df-z 12500  df-uz 12764  df-fz 13425
This theorem is referenced by:  poimirlem8  36086  poimirlem18  36096  poimirlem21  36099  poimirlem22  36100
  Copyright terms: Public domain W3C validator