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 36479
Description: Lemma for poimir 36510- 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 6837 . . . . . . . . . . . . . . . . 17 (π‘ˆ:(1...𝑁)–1-1-ontoβ†’(1...𝑁) ↔ (π‘ˆ:(1...𝑁)–ontoβ†’(1...𝑁) ∧ Fun β—‘π‘ˆ))
32simprbi 498 . . . . . . . . . . . . . . . 16 (π‘ˆ:(1...𝑁)–1-1-ontoβ†’(1...𝑁) β†’ Fun β—‘π‘ˆ)
41, 3syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ Fun β—‘π‘ˆ)
5 imadif 6630 . . . . . . . . . . . . . . 15 (Fun β—‘π‘ˆ β†’ (π‘ˆ β€œ ((1...𝑁) βˆ– {(𝑉 + 1)})) = ((π‘ˆ β€œ (1...𝑁)) βˆ– (π‘ˆ β€œ {(𝑉 + 1)})))
64, 5syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘ˆ β€œ ((1...𝑁) βˆ– {(𝑉 + 1)})) = ((π‘ˆ β€œ (1...𝑁)) βˆ– (π‘ˆ β€œ {(𝑉 + 1)})))
7 poimirlem2.4 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝑉 ∈ (1...(𝑁 βˆ’ 1)))
8 fzp1elp1 13551 . . . . . . . . . . . . . . . . . . . 20 (𝑉 ∈ (1...(𝑁 βˆ’ 1)) β†’ (𝑉 + 1) ∈ (1...((𝑁 βˆ’ 1) + 1)))
97, 8syl 17 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (𝑉 + 1) ∈ (1...((𝑁 βˆ’ 1) + 1)))
10 poimir.0 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ 𝑁 ∈ β„•)
1110nncnd 12225 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ 𝑁 ∈ β„‚)
12 npcan1 11636 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ β„‚ β†’ ((𝑁 βˆ’ 1) + 1) = 𝑁)
1311, 12syl 17 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((𝑁 βˆ’ 1) + 1) = 𝑁)
1413oveq2d 7422 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (1...((𝑁 βˆ’ 1) + 1)) = (1...𝑁))
159, 14eleqtrd 2836 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝑉 + 1) ∈ (1...𝑁))
16 fzsplit 13524 . . . . . . . . . . . . . . . . . 18 ((𝑉 + 1) ∈ (1...𝑁) β†’ (1...𝑁) = ((1...(𝑉 + 1)) βˆͺ (((𝑉 + 1) + 1)...𝑁)))
1715, 16syl 17 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (1...𝑁) = ((1...(𝑉 + 1)) βˆͺ (((𝑉 + 1) + 1)...𝑁)))
1817difeq1d 4121 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((1...𝑁) βˆ– {(𝑉 + 1)}) = (((1...(𝑉 + 1)) βˆͺ (((𝑉 + 1) + 1)...𝑁)) βˆ– {(𝑉 + 1)}))
19 difundir 4280 . . . . . . . . . . . . . . . . 17 (((1...(𝑉 + 1)) βˆͺ (((𝑉 + 1) + 1)...𝑁)) βˆ– {(𝑉 + 1)}) = (((1...(𝑉 + 1)) βˆ– {(𝑉 + 1)}) βˆͺ ((((𝑉 + 1) + 1)...𝑁) βˆ– {(𝑉 + 1)}))
20 elfzuz 13494 . . . . . . . . . . . . . . . . . . . . . 22 (𝑉 ∈ (1...(𝑁 βˆ’ 1)) β†’ 𝑉 ∈ (β„€β‰₯β€˜1))
217, 20syl 17 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ 𝑉 ∈ (β„€β‰₯β€˜1))
22 fzsuc 13545 . . . . . . . . . . . . . . . . . . . . 21 (𝑉 ∈ (β„€β‰₯β€˜1) β†’ (1...(𝑉 + 1)) = ((1...𝑉) βˆͺ {(𝑉 + 1)}))
2321, 22syl 17 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (1...(𝑉 + 1)) = ((1...𝑉) βˆͺ {(𝑉 + 1)}))
2423difeq1d 4121 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ((1...(𝑉 + 1)) βˆ– {(𝑉 + 1)}) = (((1...𝑉) βˆͺ {(𝑉 + 1)}) βˆ– {(𝑉 + 1)}))
25 difun2 4480 . . . . . . . . . . . . . . . . . . . 20 (((1...𝑉) βˆͺ {(𝑉 + 1)}) βˆ– {(𝑉 + 1)}) = ((1...𝑉) βˆ– {(𝑉 + 1)})
267elfzelzd 13499 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ 𝑉 ∈ β„€)
2726zred 12663 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ 𝑉 ∈ ℝ)
2827ltp1d 12141 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ 𝑉 < (𝑉 + 1))
2926peano2zd 12666 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ (𝑉 + 1) ∈ β„€)
3029zred 12663 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (𝑉 + 1) ∈ ℝ)
3127, 30ltnled 11358 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ (𝑉 < (𝑉 + 1) ↔ Β¬ (𝑉 + 1) ≀ 𝑉))
3228, 31mpbid 231 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ Β¬ (𝑉 + 1) ≀ 𝑉)
33 elfzle2 13502 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑉 + 1) ∈ (1...𝑉) β†’ (𝑉 + 1) ≀ 𝑉)
3432, 33nsyl 140 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ Β¬ (𝑉 + 1) ∈ (1...𝑉))
35 difsn 4801 . . . . . . . . . . . . . . . . . . . . 21 (Β¬ (𝑉 + 1) ∈ (1...𝑉) β†’ ((1...𝑉) βˆ– {(𝑉 + 1)}) = (1...𝑉))
3634, 35syl 17 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((1...𝑉) βˆ– {(𝑉 + 1)}) = (1...𝑉))
3725, 36eqtrid 2785 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (((1...𝑉) βˆͺ {(𝑉 + 1)}) βˆ– {(𝑉 + 1)}) = (1...𝑉))
3824, 37eqtrd 2773 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ ((1...(𝑉 + 1)) βˆ– {(𝑉 + 1)}) = (1...𝑉))
3930ltp1d 12141 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (𝑉 + 1) < ((𝑉 + 1) + 1))
40 peano2re 11384 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑉 + 1) ∈ ℝ β†’ ((𝑉 + 1) + 1) ∈ ℝ)
4130, 40syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ ((𝑉 + 1) + 1) ∈ ℝ)
4230, 41ltnled 11358 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ ((𝑉 + 1) < ((𝑉 + 1) + 1) ↔ Β¬ ((𝑉 + 1) + 1) ≀ (𝑉 + 1)))
4339, 42mpbid 231 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ Β¬ ((𝑉 + 1) + 1) ≀ (𝑉 + 1))
44 elfzle1 13501 . . . . . . . . . . . . . . . . . . . 20 ((𝑉 + 1) ∈ (((𝑉 + 1) + 1)...𝑁) β†’ ((𝑉 + 1) + 1) ≀ (𝑉 + 1))
4543, 44nsyl 140 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ Β¬ (𝑉 + 1) ∈ (((𝑉 + 1) + 1)...𝑁))
46 difsn 4801 . . . . . . . . . . . . . . . . . . 19 (Β¬ (𝑉 + 1) ∈ (((𝑉 + 1) + 1)...𝑁) β†’ ((((𝑉 + 1) + 1)...𝑁) βˆ– {(𝑉 + 1)}) = (((𝑉 + 1) + 1)...𝑁))
4745, 46syl 17 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ ((((𝑉 + 1) + 1)...𝑁) βˆ– {(𝑉 + 1)}) = (((𝑉 + 1) + 1)...𝑁))
4838, 47uneq12d 4164 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (((1...(𝑉 + 1)) βˆ– {(𝑉 + 1)}) βˆͺ ((((𝑉 + 1) + 1)...𝑁) βˆ– {(𝑉 + 1)})) = ((1...𝑉) βˆͺ (((𝑉 + 1) + 1)...𝑁)))
4919, 48eqtrid 2785 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (((1...(𝑉 + 1)) βˆͺ (((𝑉 + 1) + 1)...𝑁)) βˆ– {(𝑉 + 1)}) = ((1...𝑉) βˆͺ (((𝑉 + 1) + 1)...𝑁)))
5018, 49eqtrd 2773 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((1...𝑁) βˆ– {(𝑉 + 1)}) = ((1...𝑉) βˆͺ (((𝑉 + 1) + 1)...𝑁)))
5150imaeq2d 6058 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘ˆ β€œ ((1...𝑁) βˆ– {(𝑉 + 1)})) = (π‘ˆ β€œ ((1...𝑉) βˆͺ (((𝑉 + 1) + 1)...𝑁))))
526, 51eqtr3d 2775 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π‘ˆ β€œ (1...𝑁)) βˆ– (π‘ˆ β€œ {(𝑉 + 1)})) = (π‘ˆ β€œ ((1...𝑉) βˆͺ (((𝑉 + 1) + 1)...𝑁))))
53 imaundi 6147 . . . . . . . . . . . . 13 (π‘ˆ β€œ ((1...𝑉) βˆͺ (((𝑉 + 1) + 1)...𝑁))) = ((π‘ˆ β€œ (1...𝑉)) βˆͺ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)))
5452, 53eqtrdi 2789 . . . . . . . . . . . 12 (πœ‘ β†’ ((π‘ˆ β€œ (1...𝑁)) βˆ– (π‘ˆ β€œ {(𝑉 + 1)})) = ((π‘ˆ β€œ (1...𝑉)) βˆͺ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))))
5554eleq2d 2820 . . . . . . . . . . 11 (πœ‘ β†’ (𝑛 ∈ ((π‘ˆ β€œ (1...𝑁)) βˆ– (π‘ˆ β€œ {(𝑉 + 1)})) ↔ 𝑛 ∈ ((π‘ˆ β€œ (1...𝑉)) βˆͺ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)))))
56 eldif 3958 . . . . . . . . . . 11 (𝑛 ∈ ((π‘ˆ β€œ (1...𝑁)) βˆ– (π‘ˆ β€œ {(𝑉 + 1)})) ↔ (𝑛 ∈ (π‘ˆ β€œ (1...𝑁)) ∧ Β¬ 𝑛 ∈ (π‘ˆ β€œ {(𝑉 + 1)})))
57 elun 4148 . . . . . . . . . . 11 (𝑛 ∈ ((π‘ˆ β€œ (1...𝑉)) βˆͺ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) ↔ (𝑛 ∈ (π‘ˆ β€œ (1...𝑉)) ∨ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))))
5855, 56, 573bitr3g 313 . . . . . . . . . 10 (πœ‘ β†’ ((𝑛 ∈ (π‘ˆ β€œ (1...𝑁)) ∧ Β¬ 𝑛 ∈ (π‘ˆ β€œ {(𝑉 + 1)})) ↔ (𝑛 ∈ (π‘ˆ β€œ (1...𝑉)) ∨ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)))))
5958adantr 482 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ ((𝑛 ∈ (π‘ˆ β€œ (1...𝑁)) ∧ Β¬ 𝑛 ∈ (π‘ˆ β€œ {(𝑉 + 1)})) ↔ (𝑛 ∈ (π‘ˆ β€œ (1...𝑉)) ∨ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)))))
60 imassrn 6069 . . . . . . . . . . . . . . . 16 (π‘ˆ β€œ (1...𝑉)) βŠ† ran π‘ˆ
61 f1of 6831 . . . . . . . . . . . . . . . . . 18 (π‘ˆ:(1...𝑁)–1-1-ontoβ†’(1...𝑁) β†’ π‘ˆ:(1...𝑁)⟢(1...𝑁))
621, 61syl 17 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ π‘ˆ:(1...𝑁)⟢(1...𝑁))
6362frnd 6723 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ran π‘ˆ βŠ† (1...𝑁))
6460, 63sstrid 3993 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (π‘ˆ β€œ (1...𝑉)) βŠ† (1...𝑁))
6564sselda 3982 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) β†’ 𝑛 ∈ (1...𝑁))
66 poimirlem2.2 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝑇:(1...𝑁)βŸΆβ„€)
6766ffnd 6716 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝑇 Fn (1...𝑁))
6867adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) β†’ 𝑇 Fn (1...𝑁))
69 1ex 11207 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ V
70 fnconstg 6777 . . . . . . . . . . . . . . . . . . . . 21 (1 ∈ V β†’ ((π‘ˆ β€œ (1...𝑉)) Γ— {1}) Fn (π‘ˆ β€œ (1...𝑉)))
7169, 70ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((π‘ˆ β€œ (1...𝑉)) Γ— {1}) Fn (π‘ˆ β€œ (1...𝑉))
72 c0ex 11205 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ V
73 fnconstg 6777 . . . . . . . . . . . . . . . . . . . . 21 (0 ∈ V β†’ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}) Fn (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))
7472, 73ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}) Fn (π‘ˆ β€œ ((𝑉 + 1)...𝑁))
7571, 74pm3.2i 472 . . . . . . . . . . . . . . . . . . 19 (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) Fn (π‘ˆ β€œ (1...𝑉)) ∧ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}) Fn (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))
76 imain 6631 . . . . . . . . . . . . . . . . . . . . 21 (Fun β—‘π‘ˆ β†’ (π‘ˆ β€œ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = ((π‘ˆ β€œ (1...𝑉)) ∩ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))))
774, 76syl 17 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (π‘ˆ β€œ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = ((π‘ˆ β€œ (1...𝑉)) ∩ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))))
78 fzdisj 13525 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑉 < (𝑉 + 1) β†’ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁)) = βˆ…)
7928, 78syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁)) = βˆ…)
8079imaeq2d 6058 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (π‘ˆ β€œ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = (π‘ˆ β€œ βˆ…))
81 ima0 6074 . . . . . . . . . . . . . . . . . . . . 21 (π‘ˆ β€œ βˆ…) = βˆ…
8280, 81eqtrdi 2789 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (π‘ˆ β€œ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = βˆ…)
8377, 82eqtr3d 2775 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ((π‘ˆ β€œ (1...𝑉)) ∩ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) = βˆ…)
84 fnun 6661 . . . . . . . . . . . . . . . . . . 19 (((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) Fn (π‘ˆ β€œ (1...𝑉)) ∧ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}) Fn (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) ∧ ((π‘ˆ β€œ (1...𝑉)) ∩ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) = βˆ…) β†’ (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})) Fn ((π‘ˆ β€œ (1...𝑉)) βˆͺ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))))
8575, 83, 84sylancr 588 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})) Fn ((π‘ˆ β€œ (1...𝑉)) βˆͺ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))))
86 imaundi 6147 . . . . . . . . . . . . . . . . . . . 20 (π‘ˆ β€œ ((1...𝑉) βˆͺ ((𝑉 + 1)...𝑁))) = ((π‘ˆ β€œ (1...𝑉)) βˆͺ (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))
8710nnzd 12582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (πœ‘ β†’ 𝑁 ∈ β„€)
88 peano2zm 12602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ β„€ β†’ (𝑁 βˆ’ 1) ∈ β„€)
8987, 88syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (πœ‘ β†’ (𝑁 βˆ’ 1) ∈ β„€)
90 uzid 12834 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑁 βˆ’ 1) ∈ β„€ β†’ (𝑁 βˆ’ 1) ∈ (β„€β‰₯β€˜(𝑁 βˆ’ 1)))
9189, 90syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ (𝑁 βˆ’ 1) ∈ (β„€β‰₯β€˜(𝑁 βˆ’ 1)))
92 peano2uz 12882 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑁 βˆ’ 1) ∈ (β„€β‰₯β€˜(𝑁 βˆ’ 1)) β†’ ((𝑁 βˆ’ 1) + 1) ∈ (β„€β‰₯β€˜(𝑁 βˆ’ 1)))
9391, 92syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ ((𝑁 βˆ’ 1) + 1) ∈ (β„€β‰₯β€˜(𝑁 βˆ’ 1)))
9413, 93eqeltrrd 2835 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ 𝑁 ∈ (β„€β‰₯β€˜(𝑁 βˆ’ 1)))
95 fzss2 13538 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ (β„€β‰₯β€˜(𝑁 βˆ’ 1)) β†’ (1...(𝑁 βˆ’ 1)) βŠ† (1...𝑁))
9694, 95syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (1...(𝑁 βˆ’ 1)) βŠ† (1...𝑁))
9796, 7sseldd 3983 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ 𝑉 ∈ (1...𝑁))
98 fzsplit 13524 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑉 ∈ (1...𝑁) β†’ (1...𝑁) = ((1...𝑉) βˆͺ ((𝑉 + 1)...𝑁)))
9997, 98syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (1...𝑁) = ((1...𝑉) βˆͺ ((𝑉 + 1)...𝑁)))
10099imaeq2d 6058 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (π‘ˆ β€œ (1...𝑁)) = (π‘ˆ β€œ ((1...𝑉) βˆͺ ((𝑉 + 1)...𝑁))))
101 f1ofo 6838 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘ˆ:(1...𝑁)–1-1-ontoβ†’(1...𝑁) β†’ π‘ˆ:(1...𝑁)–ontoβ†’(1...𝑁))
1021, 101syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ π‘ˆ:(1...𝑁)–ontoβ†’(1...𝑁))
103 foima 6808 . . . . . . . . . . . . . . . . . . . . . 22 (π‘ˆ:(1...𝑁)–ontoβ†’(1...𝑁) β†’ (π‘ˆ β€œ (1...𝑁)) = (1...𝑁))
104102, 103syl 17 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (π‘ˆ β€œ (1...𝑁)) = (1...𝑁))
105100, 104eqtr3d 2775 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (π‘ˆ β€œ ((1...𝑉) βˆͺ ((𝑉 + 1)...𝑁))) = (1...𝑁))
10686, 105eqtr3id 2787 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ((π‘ˆ β€œ (1...𝑉)) βˆͺ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) = (1...𝑁))
107106fneq2d 6641 . . . . . . . . . . . . . . . . . 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 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) β†’ (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})) Fn (1...𝑁))
110 fzfid 13935 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) β†’ (1...𝑁) ∈ Fin)
111 inidm 4218 . . . . . . . . . . . . . . . 16 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
112 eqidd 2734 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘‡β€˜π‘›) = (π‘‡β€˜π‘›))
113 fvun1 6980 . . . . . . . . . . . . . . . . . . . 20 ((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) Fn (π‘ˆ β€œ (1...𝑉)) ∧ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}) Fn (π‘ˆ β€œ ((𝑉 + 1)...𝑁)) ∧ (((π‘ˆ β€œ (1...𝑉)) ∩ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) = βˆ… ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉)))) β†’ ((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ (1...𝑉)) Γ— {1})β€˜π‘›))
11471, 74, 113mp3an12 1452 . . . . . . . . . . . . . . . . . . 19 ((((π‘ˆ β€œ (1...𝑉)) ∩ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) = βˆ… ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) β†’ ((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ (1...𝑉)) Γ— {1})β€˜π‘›))
11583, 114sylan 581 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) β†’ ((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ (1...𝑉)) Γ— {1})β€˜π‘›))
11669fvconst2 7202 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (π‘ˆ β€œ (1...𝑉)) β†’ (((π‘ˆ β€œ (1...𝑉)) Γ— {1})β€˜π‘›) = 1)
117116adantl 483 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) β†’ (((π‘ˆ β€œ (1...𝑉)) Γ— {1})β€˜π‘›) = 1)
118115, 117eqtrd 2773 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) β†’ ((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))β€˜π‘›) = 1)
119118adantr 482 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))β€˜π‘›) = 1)
12068, 109, 110, 110, 111, 112, 119ofval 7678 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›) = ((π‘‡β€˜π‘›) + 1))
121 fnconstg 6777 . . . . . . . . . . . . . . . . . . . . 21 (1 ∈ V β†’ ((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) Fn (π‘ˆ β€œ (1...(𝑉 + 1))))
12269, 121ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) Fn (π‘ˆ β€œ (1...(𝑉 + 1)))
123 fnconstg 6777 . . . . . . . . . . . . . . . . . . . . 21 (0 ∈ V β†’ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}) Fn (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)))
12472, 123ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}) Fn (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))
125122, 124pm3.2i 472 . . . . . . . . . . . . . . . . . . 19 (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) Fn (π‘ˆ β€œ (1...(𝑉 + 1))) ∧ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}) Fn (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)))
126 imain 6631 . . . . . . . . . . . . . . . . . . . . 21 (Fun β—‘π‘ˆ β†’ (π‘ˆ β€œ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = ((π‘ˆ β€œ (1...(𝑉 + 1))) ∩ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))))
1274, 126syl 17 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (π‘ˆ β€œ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = ((π‘ˆ β€œ (1...(𝑉 + 1))) ∩ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))))
128 fzdisj 13525 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑉 + 1) < ((𝑉 + 1) + 1) β†’ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁)) = βˆ…)
12939, 128syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁)) = βˆ…)
130129imaeq2d 6058 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (π‘ˆ β€œ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = (π‘ˆ β€œ βˆ…))
131130, 81eqtrdi 2789 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (π‘ˆ β€œ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = βˆ…)
132127, 131eqtr3d 2775 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ((π‘ˆ β€œ (1...(𝑉 + 1))) ∩ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) = βˆ…)
133 fnun 6661 . . . . . . . . . . . . . . . . . . 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 588 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})) Fn ((π‘ˆ β€œ (1...(𝑉 + 1))) βˆͺ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))))
135 imaundi 6147 . . . . . . . . . . . . . . . . . . . 20 (π‘ˆ β€œ ((1...(𝑉 + 1)) βˆͺ (((𝑉 + 1) + 1)...𝑁))) = ((π‘ˆ β€œ (1...(𝑉 + 1))) βˆͺ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)))
13617imaeq2d 6058 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (π‘ˆ β€œ (1...𝑁)) = (π‘ˆ β€œ ((1...(𝑉 + 1)) βˆͺ (((𝑉 + 1) + 1)...𝑁))))
137136, 104eqtr3d 2775 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (π‘ˆ β€œ ((1...(𝑉 + 1)) βˆͺ (((𝑉 + 1) + 1)...𝑁))) = (1...𝑁))
138135, 137eqtr3id 2787 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ((π‘ˆ β€œ (1...(𝑉 + 1))) βˆͺ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) = (1...𝑁))
139138fneq2d 6641 . . . . . . . . . . . . . . . . . 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 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) β†’ (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})) Fn (1...𝑁))
142 uzid 12834 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑉 ∈ β„€ β†’ 𝑉 ∈ (β„€β‰₯β€˜π‘‰))
14326, 142syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ 𝑉 ∈ (β„€β‰₯β€˜π‘‰))
144 peano2uz 12882 . . . . . . . . . . . . . . . . . . . . . 22 (𝑉 ∈ (β„€β‰₯β€˜π‘‰) β†’ (𝑉 + 1) ∈ (β„€β‰₯β€˜π‘‰))
145143, 144syl 17 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (𝑉 + 1) ∈ (β„€β‰₯β€˜π‘‰))
146 fzss2 13538 . . . . . . . . . . . . . . . . . . . . 21 ((𝑉 + 1) ∈ (β„€β‰₯β€˜π‘‰) β†’ (1...𝑉) βŠ† (1...(𝑉 + 1)))
147145, 146syl 17 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (1...𝑉) βŠ† (1...(𝑉 + 1)))
148 imass2 6099 . . . . . . . . . . . . . . . . . . . 20 ((1...𝑉) βŠ† (1...(𝑉 + 1)) β†’ (π‘ˆ β€œ (1...𝑉)) βŠ† (π‘ˆ β€œ (1...(𝑉 + 1))))
149147, 148syl 17 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (π‘ˆ β€œ (1...𝑉)) βŠ† (π‘ˆ β€œ (1...(𝑉 + 1))))
150149sselda 3982 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) β†’ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 + 1))))
151 fvun1 6980 . . . . . . . . . . . . . . . . . . . . 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 1452 . . . . . . . . . . . . . . . . . . . 20 ((((π‘ˆ β€œ (1...(𝑉 + 1))) ∩ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) = βˆ… ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 + 1)))) β†’ ((((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1})β€˜π‘›))
153132, 152sylan 581 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 + 1)))) β†’ ((((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1})β€˜π‘›))
15469fvconst2 7202 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 + 1))) β†’ (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1})β€˜π‘›) = 1)
155154adantl 483 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 + 1)))) β†’ (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1})β€˜π‘›) = 1)
156153, 155eqtrd 2773 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 + 1)))) β†’ ((((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}))β€˜π‘›) = 1)
157150, 156syldan 592 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) β†’ ((((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}))β€˜π‘›) = 1)
158157adantr 482 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}))β€˜π‘›) = 1)
15968, 141, 110, 110, 111, 112, 158ofval 7678 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})))β€˜π‘›) = ((π‘‡β€˜π‘›) + 1))
160120, 159eqtr4d 2776 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})))β€˜π‘›))
16165, 160mpdan 686 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉))) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})))β€˜π‘›))
162 imassrn 6069 . . . . . . . . . . . . . . . 16 (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) βŠ† ran π‘ˆ
163162, 63sstrid 3993 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) βŠ† (1...𝑁))
164163sselda 3982 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) β†’ 𝑛 ∈ (1...𝑁))
16567adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) β†’ 𝑇 Fn (1...𝑁))
166108adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) β†’ (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})) Fn (1...𝑁))
167 fzfid 13935 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) β†’ (1...𝑁) ∈ Fin)
168 eqidd 2734 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘‡β€˜π‘›) = (π‘‡β€˜π‘›))
169 uzid 12834 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑉 + 1) ∈ β„€ β†’ (𝑉 + 1) ∈ (β„€β‰₯β€˜(𝑉 + 1)))
17029, 169syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (𝑉 + 1) ∈ (β„€β‰₯β€˜(𝑉 + 1)))
171 peano2uz 12882 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑉 + 1) ∈ (β„€β‰₯β€˜(𝑉 + 1)) β†’ ((𝑉 + 1) + 1) ∈ (β„€β‰₯β€˜(𝑉 + 1)))
172170, 171syl 17 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ ((𝑉 + 1) + 1) ∈ (β„€β‰₯β€˜(𝑉 + 1)))
173 fzss1 13537 . . . . . . . . . . . . . . . . . . . . 21 (((𝑉 + 1) + 1) ∈ (β„€β‰₯β€˜(𝑉 + 1)) β†’ (((𝑉 + 1) + 1)...𝑁) βŠ† ((𝑉 + 1)...𝑁))
174172, 173syl 17 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (((𝑉 + 1) + 1)...𝑁) βŠ† ((𝑉 + 1)...𝑁))
175 imass2 6099 . . . . . . . . . . . . . . . . . . . 20 ((((𝑉 + 1) + 1)...𝑁) βŠ† ((𝑉 + 1)...𝑁) β†’ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) βŠ† (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))
176174, 175syl 17 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) βŠ† (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))
177176sselda 3982 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) β†’ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))
178 fvun2 6981 . . . . . . . . . . . . . . . . . . . . 21 ((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) Fn (π‘ˆ β€œ (1...𝑉)) ∧ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}) Fn (π‘ˆ β€œ ((𝑉 + 1)...𝑁)) ∧ (((π‘ˆ β€œ (1...𝑉)) ∩ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) = βˆ… ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))) β†’ ((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})β€˜π‘›))
17971, 74, 178mp3an12 1452 . . . . . . . . . . . . . . . . . . . 20 ((((π‘ˆ β€œ (1...𝑉)) ∩ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) = βˆ… ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) β†’ ((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})β€˜π‘›))
18083, 179sylan 581 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) β†’ ((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})β€˜π‘›))
18172fvconst2 7202 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁)) β†’ (((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})β€˜π‘›) = 0)
182181adantl 483 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) β†’ (((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})β€˜π‘›) = 0)
183180, 182eqtrd 2773 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) β†’ ((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))β€˜π‘›) = 0)
184177, 183syldan 592 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) β†’ ((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))β€˜π‘›) = 0)
185184adantr 482 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))β€˜π‘›) = 0)
186165, 166, 167, 167, 111, 168, 185ofval 7678 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›) = ((π‘‡β€˜π‘›) + 0))
187140adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) β†’ (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})) Fn (1...𝑁))
188 fvun2 6981 . . . . . . . . . . . . . . . . . . . 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 1452 . . . . . . . . . . . . . . . . . . 19 ((((π‘ˆ β€œ (1...(𝑉 + 1))) ∩ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) = βˆ… ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) β†’ ((((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})β€˜π‘›))
190132, 189sylan 581 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) β†’ ((((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})β€˜π‘›))
19172fvconst2 7202 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) β†’ (((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})β€˜π‘›) = 0)
192191adantl 483 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) β†’ (((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})β€˜π‘›) = 0)
193190, 192eqtrd 2773 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) β†’ ((((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}))β€˜π‘›) = 0)
194193adantr 482 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}))β€˜π‘›) = 0)
195165, 187, 167, 167, 111, 168, 194ofval 7678 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})))β€˜π‘›) = ((π‘‡β€˜π‘›) + 0))
196186, 195eqtr4d 2776 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})))β€˜π‘›))
197164, 196mpdan 686 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})))β€˜π‘›))
198161, 197jaodan 957 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑛 ∈ (π‘ˆ β€œ (1...𝑉)) ∨ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)))) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})))β€˜π‘›))
199198adantlr 714 . . . . . . . . . . 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 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ 𝐹 = (𝑦 ∈ (0...(𝑁 βˆ’ 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / π‘—β¦Œ(𝑇 ∘f + (((π‘ˆ β€œ (1...𝑗)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0})))))
202 vex 3479 . . . . . . . . . . . . . . . . 17 𝑦 ∈ V
203 ovex 7439 . . . . . . . . . . . . . . . . 17 (𝑦 + 1) ∈ V
204202, 203ifex 4578 . . . . . . . . . . . . . . . 16 if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V
205204a1i 11 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 βˆ’ 1)) β†’ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V)
206 breq1 5151 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (𝑉 βˆ’ 1) β†’ (𝑦 < 𝑀 ↔ (𝑉 βˆ’ 1) < 𝑀))
207206adantl 483 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑦 = (𝑉 βˆ’ 1)) β†’ (𝑦 < 𝑀 ↔ (𝑉 βˆ’ 1) < 𝑀))
208 simpr 486 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑦 = (𝑉 βˆ’ 1)) β†’ 𝑦 = (𝑉 βˆ’ 1))
209 oveq1 7413 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (𝑉 βˆ’ 1) β†’ (𝑦 + 1) = ((𝑉 βˆ’ 1) + 1))
21026zcnd 12664 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ 𝑉 ∈ β„‚)
211 npcan1 11636 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑉 ∈ β„‚ β†’ ((𝑉 βˆ’ 1) + 1) = 𝑉)
212210, 211syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ ((𝑉 βˆ’ 1) + 1) = 𝑉)
213209, 212sylan9eqr 2795 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑦 = (𝑉 βˆ’ 1)) β†’ (𝑦 + 1) = 𝑉)
214207, 208, 213ifbieq12d 4556 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑦 = (𝑉 βˆ’ 1)) β†’ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑉 βˆ’ 1) < 𝑀, (𝑉 βˆ’ 1), 𝑉))
215214adantlr 714 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 βˆ’ 1)) β†’ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑉 βˆ’ 1) < 𝑀, (𝑉 βˆ’ 1), 𝑉))
216 poimirlem2.5 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ 𝑀 ∈ ((0...𝑁) βˆ– {𝑉}))
217216eldifad 3960 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ 𝑀 ∈ (0...𝑁))
218217elfzelzd 13499 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ 𝑀 ∈ β„€)
219 zltlem1 12612 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑀 ∈ β„€ ∧ 𝑉 ∈ β„€) β†’ (𝑀 < 𝑉 ↔ 𝑀 ≀ (𝑉 βˆ’ 1)))
220218, 26, 219syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ (𝑀 < 𝑉 ↔ 𝑀 ≀ (𝑉 βˆ’ 1)))
221218zred 12663 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ 𝑀 ∈ ℝ)
222 peano2zm 12602 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑉 ∈ β„€ β†’ (𝑉 βˆ’ 1) ∈ β„€)
22326, 222syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ (𝑉 βˆ’ 1) ∈ β„€)
224223zred 12663 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (𝑉 βˆ’ 1) ∈ ℝ)
225221, 224lenltd 11357 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ (𝑀 ≀ (𝑉 βˆ’ 1) ↔ Β¬ (𝑉 βˆ’ 1) < 𝑀))
226220, 225bitrd 279 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (𝑀 < 𝑉 ↔ Β¬ (𝑉 βˆ’ 1) < 𝑀))
227226biimpa 478 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ Β¬ (𝑉 βˆ’ 1) < 𝑀)
228227iffalsed 4539 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ if((𝑉 βˆ’ 1) < 𝑀, (𝑉 βˆ’ 1), 𝑉) = 𝑉)
229228adantr 482 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 βˆ’ 1)) β†’ if((𝑉 βˆ’ 1) < 𝑀, (𝑉 βˆ’ 1), 𝑉) = 𝑉)
230215, 229eqtrd 2773 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 βˆ’ 1)) β†’ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = 𝑉)
231230eqeq2d 2744 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 βˆ’ 1)) β†’ (𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ↔ 𝑗 = 𝑉))
232231biimpa 478 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 βˆ’ 1)) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) β†’ 𝑗 = 𝑉)
233 oveq2 7414 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑉 β†’ (1...𝑗) = (1...𝑉))
234233imaeq2d 6058 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑉 β†’ (π‘ˆ β€œ (1...𝑗)) = (π‘ˆ β€œ (1...𝑉)))
235234xpeq1d 5705 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑉 β†’ ((π‘ˆ β€œ (1...𝑗)) Γ— {1}) = ((π‘ˆ β€œ (1...𝑉)) Γ— {1}))
236 oveq1 7413 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑉 β†’ (𝑗 + 1) = (𝑉 + 1))
237236oveq1d 7421 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑉 β†’ ((𝑗 + 1)...𝑁) = ((𝑉 + 1)...𝑁))
238237imaeq2d 6058 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑉 β†’ (π‘ˆ β€œ ((𝑗 + 1)...𝑁)) = (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))
239238xpeq1d 5705 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑉 β†’ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0}) = ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))
240235, 239uneq12d 4164 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑉 β†’ (((π‘ˆ β€œ (1...𝑗)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0})) = (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))
241240oveq2d 7422 . . . . . . . . . . . . . . . 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 3931 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 βˆ’ 1)) β†’ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / π‘—β¦Œ(𝑇 ∘f + (((π‘ˆ β€œ (1...𝑗)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0}))) = (𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))))
244 elfzm1b 13576 . . . . . . . . . . . . . . . . 17 ((𝑉 ∈ β„€ ∧ 𝑁 ∈ β„€) β†’ (𝑉 ∈ (1...𝑁) ↔ (𝑉 βˆ’ 1) ∈ (0...(𝑁 βˆ’ 1))))
24526, 87, 244syl2anc 585 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝑉 ∈ (1...𝑁) ↔ (𝑉 βˆ’ 1) ∈ (0...(𝑁 βˆ’ 1))))
24697, 245mpbid 231 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑉 βˆ’ 1) ∈ (0...(𝑁 βˆ’ 1)))
247246adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ (𝑉 βˆ’ 1) ∈ (0...(𝑁 βˆ’ 1)))
248 ovexd 7441 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ (𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))) ∈ V)
249201, 243, 247, 248fvmptd 7003 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ (πΉβ€˜(𝑉 βˆ’ 1)) = (𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))))
250249fveq1d 6891 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ ((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›))
251250adantr 482 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ (𝑛 ∈ (π‘ˆ β€œ (1...𝑉)) ∨ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)))) β†’ ((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›))
252204a1i 11 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) β†’ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V)
253 breq1 5151 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑉 β†’ (𝑦 < 𝑀 ↔ 𝑉 < 𝑀))
254 id 22 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑉 β†’ 𝑦 = 𝑉)
255 oveq1 7413 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑉 β†’ (𝑦 + 1) = (𝑉 + 1))
256253, 254, 255ifbieq12d 4556 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑉 β†’ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if(𝑉 < 𝑀, 𝑉, (𝑉 + 1)))
257 ltnsym 11309 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑀 ∈ ℝ ∧ 𝑉 ∈ ℝ) β†’ (𝑀 < 𝑉 β†’ Β¬ 𝑉 < 𝑀))
258221, 27, 257syl2anc 585 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (𝑀 < 𝑉 β†’ Β¬ 𝑉 < 𝑀))
259258imp 408 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ Β¬ 𝑉 < 𝑀)
260259iffalsed 4539 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ if(𝑉 < 𝑀, 𝑉, (𝑉 + 1)) = (𝑉 + 1))
261256, 260sylan9eqr 2795 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) β†’ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = (𝑉 + 1))
262261eqeq2d 2744 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) β†’ (𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ↔ 𝑗 = (𝑉 + 1)))
263262biimpa 478 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) β†’ 𝑗 = (𝑉 + 1))
264 oveq2 7414 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = (𝑉 + 1) β†’ (1...𝑗) = (1...(𝑉 + 1)))
265264imaeq2d 6058 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑉 + 1) β†’ (π‘ˆ β€œ (1...𝑗)) = (π‘ˆ β€œ (1...(𝑉 + 1))))
266265xpeq1d 5705 . . . . . . . . . . . . . . . . . 18 (𝑗 = (𝑉 + 1) β†’ ((π‘ˆ β€œ (1...𝑗)) Γ— {1}) = ((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}))
267 oveq1 7413 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = (𝑉 + 1) β†’ (𝑗 + 1) = ((𝑉 + 1) + 1))
268267oveq1d 7421 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = (𝑉 + 1) β†’ ((𝑗 + 1)...𝑁) = (((𝑉 + 1) + 1)...𝑁))
269268imaeq2d 6058 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑉 + 1) β†’ (π‘ˆ β€œ ((𝑗 + 1)...𝑁)) = (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)))
270269xpeq1d 5705 . . . . . . . . . . . . . . . . . 18 (𝑗 = (𝑉 + 1) β†’ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0}) = ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}))
271266, 270uneq12d 4164 . . . . . . . . . . . . . . . . 17 (𝑗 = (𝑉 + 1) β†’ (((π‘ˆ β€œ (1...𝑗)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0})) = (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})))
272271oveq2d 7422 . . . . . . . . . . . . . . . 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 3931 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) β†’ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / π‘—β¦Œ(𝑇 ∘f + (((π‘ˆ β€œ (1...𝑗)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0}))) = (𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}))))
275 fz1ssfz0 13594 . . . . . . . . . . . . . . . 16 (1...(𝑁 βˆ’ 1)) βŠ† (0...(𝑁 βˆ’ 1))
276275, 7sselid 3980 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑉 ∈ (0...(𝑁 βˆ’ 1)))
277276adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ 𝑉 ∈ (0...(𝑁 βˆ’ 1)))
278 ovexd 7441 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ (𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}))) ∈ V)
279201, 274, 277, 278fvmptd 7003 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ (πΉβ€˜π‘‰) = (𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0}))))
280279fveq1d 6891 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ ((πΉβ€˜π‘‰)β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})))β€˜π‘›))
281280adantr 482 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ (𝑛 ∈ (π‘ˆ β€œ (1...𝑉)) ∨ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)))) β†’ ((πΉβ€˜π‘‰)β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 + 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)) Γ— {0})))β€˜π‘›))
282199, 251, 2813eqtr4d 2783 . . . . . . . . . 10 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ (𝑛 ∈ (π‘ˆ β€œ (1...𝑉)) ∨ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁)))) β†’ ((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) = ((πΉβ€˜π‘‰)β€˜π‘›))
283282ex 414 . . . . . . . . 9 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ ((𝑛 ∈ (π‘ˆ β€œ (1...𝑉)) ∨ 𝑛 ∈ (π‘ˆ β€œ (((𝑉 + 1) + 1)...𝑁))) β†’ ((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) = ((πΉβ€˜π‘‰)β€˜π‘›)))
28459, 283sylbid 239 . . . . . . . 8 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ ((𝑛 ∈ (π‘ˆ β€œ (1...𝑁)) ∧ Β¬ 𝑛 ∈ (π‘ˆ β€œ {(𝑉 + 1)})) β†’ ((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) = ((πΉβ€˜π‘‰)β€˜π‘›)))
285284expdimp 454 . . . . . . 7 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑁))) β†’ (Β¬ 𝑛 ∈ (π‘ˆ β€œ {(𝑉 + 1)}) β†’ ((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) = ((πΉβ€˜π‘‰)β€˜π‘›)))
286285necon1ad 2958 . . . . . 6 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑁))) β†’ (((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 ∈ (π‘ˆ β€œ {(𝑉 + 1)})))
287 elimasni 6088 . . . . . . . 8 (𝑛 ∈ (π‘ˆ β€œ {(𝑉 + 1)}) β†’ (𝑉 + 1)π‘ˆπ‘›)
288 eqcom 2740 . . . . . . . . 9 (𝑛 = (π‘ˆβ€˜(𝑉 + 1)) ↔ (π‘ˆβ€˜(𝑉 + 1)) = 𝑛)
289 f1ofn 6832 . . . . . . . . . . 11 (π‘ˆ:(1...𝑁)–1-1-ontoβ†’(1...𝑁) β†’ π‘ˆ Fn (1...𝑁))
2901, 289syl 17 . . . . . . . . . 10 (πœ‘ β†’ π‘ˆ Fn (1...𝑁))
291 fnbrfvb 6942 . . . . . . . . . 10 ((π‘ˆ Fn (1...𝑁) ∧ (𝑉 + 1) ∈ (1...𝑁)) β†’ ((π‘ˆβ€˜(𝑉 + 1)) = 𝑛 ↔ (𝑉 + 1)π‘ˆπ‘›))
292290, 15, 291syl2anc 585 . . . . . . . . 9 (πœ‘ β†’ ((π‘ˆβ€˜(𝑉 + 1)) = 𝑛 ↔ (𝑉 + 1)π‘ˆπ‘›))
293288, 292bitrid 283 . . . . . . . 8 (πœ‘ β†’ (𝑛 = (π‘ˆβ€˜(𝑉 + 1)) ↔ (𝑉 + 1)π‘ˆπ‘›))
294287, 293imbitrrid 245 . . . . . . 7 (πœ‘ β†’ (𝑛 ∈ (π‘ˆ β€œ {(𝑉 + 1)}) β†’ 𝑛 = (π‘ˆβ€˜(𝑉 + 1))))
295294ad2antrr 725 . . . . . 6 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑁))) β†’ (𝑛 ∈ (π‘ˆ β€œ {(𝑉 + 1)}) β†’ 𝑛 = (π‘ˆβ€˜(𝑉 + 1))))
296286, 295syld 47 . . . . 5 (((πœ‘ ∧ 𝑀 < 𝑉) ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑁))) β†’ (((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = (π‘ˆβ€˜(𝑉 + 1))))
297296ralrimiva 3147 . . . 4 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ βˆ€π‘› ∈ (π‘ˆ β€œ (1...𝑁))(((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = (π‘ˆβ€˜(𝑉 + 1))))
298 fvex 6902 . . . . 5 (π‘ˆβ€˜(𝑉 + 1)) ∈ V
299 eqeq2 2745 . . . . . . 7 (π‘š = (π‘ˆβ€˜(𝑉 + 1)) β†’ (𝑛 = π‘š ↔ 𝑛 = (π‘ˆβ€˜(𝑉 + 1))))
300299imbi2d 341 . . . . . 6 (π‘š = (π‘ˆβ€˜(𝑉 + 1)) β†’ ((((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = π‘š) ↔ (((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = (π‘ˆβ€˜(𝑉 + 1)))))
301300ralbidv 3178 . . . . 5 (π‘š = (π‘ˆβ€˜(𝑉 + 1)) β†’ (βˆ€π‘› ∈ (π‘ˆ β€œ (1...𝑁))(((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = π‘š) ↔ βˆ€π‘› ∈ (π‘ˆ β€œ (1...𝑁))(((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = (π‘ˆβ€˜(𝑉 + 1)))))
302298, 301spcev 3597 . . . 4 (βˆ€π‘› ∈ (π‘ˆ β€œ (1...𝑁))(((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = (π‘ˆβ€˜(𝑉 + 1))) β†’ βˆƒπ‘šβˆ€π‘› ∈ (π‘ˆ β€œ (1...𝑁))(((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = π‘š))
303297, 302syl 17 . . 3 ((πœ‘ ∧ 𝑀 < 𝑉) β†’ βˆƒπ‘šβˆ€π‘› ∈ (π‘ˆ β€œ (1...𝑁))(((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = π‘š))
304 imadif 6630 . . . . . . . . . . . . . . 15 (Fun β—‘π‘ˆ β†’ (π‘ˆ β€œ ((1...𝑁) βˆ– {𝑉})) = ((π‘ˆ β€œ (1...𝑁)) βˆ– (π‘ˆ β€œ {𝑉})))
3054, 304syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘ˆ β€œ ((1...𝑁) βˆ– {𝑉})) = ((π‘ˆ β€œ (1...𝑁)) βˆ– (π‘ˆ β€œ {𝑉})))
30699difeq1d 4121 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((1...𝑁) βˆ– {𝑉}) = (((1...𝑉) βˆͺ ((𝑉 + 1)...𝑁)) βˆ– {𝑉}))
307 difundir 4280 . . . . . . . . . . . . . . . . 17 (((1...𝑉) βˆͺ ((𝑉 + 1)...𝑁)) βˆ– {𝑉}) = (((1...𝑉) βˆ– {𝑉}) βˆͺ (((𝑉 + 1)...𝑁) βˆ– {𝑉}))
308212, 21eqeltrd 2834 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ ((𝑉 βˆ’ 1) + 1) ∈ (β„€β‰₯β€˜1))
309 uzid 12834 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑉 βˆ’ 1) ∈ β„€ β†’ (𝑉 βˆ’ 1) ∈ (β„€β‰₯β€˜(𝑉 βˆ’ 1)))
310223, 309syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (𝑉 βˆ’ 1) ∈ (β„€β‰₯β€˜(𝑉 βˆ’ 1)))
311 peano2uz 12882 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑉 βˆ’ 1) ∈ (β„€β‰₯β€˜(𝑉 βˆ’ 1)) β†’ ((𝑉 βˆ’ 1) + 1) ∈ (β„€β‰₯β€˜(𝑉 βˆ’ 1)))
312310, 311syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ ((𝑉 βˆ’ 1) + 1) ∈ (β„€β‰₯β€˜(𝑉 βˆ’ 1)))
313212, 312eqeltrrd 2835 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ 𝑉 ∈ (β„€β‰₯β€˜(𝑉 βˆ’ 1)))
314 fzsplit2 13523 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑉 βˆ’ 1) + 1) ∈ (β„€β‰₯β€˜1) ∧ 𝑉 ∈ (β„€β‰₯β€˜(𝑉 βˆ’ 1))) β†’ (1...𝑉) = ((1...(𝑉 βˆ’ 1)) βˆͺ (((𝑉 βˆ’ 1) + 1)...𝑉)))
315308, 313, 314syl2anc 585 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (1...𝑉) = ((1...(𝑉 βˆ’ 1)) βˆͺ (((𝑉 βˆ’ 1) + 1)...𝑉)))
316212oveq1d 7421 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ (((𝑉 βˆ’ 1) + 1)...𝑉) = (𝑉...𝑉))
317 fzsn 13540 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑉 ∈ β„€ β†’ (𝑉...𝑉) = {𝑉})
31826, 317syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ (𝑉...𝑉) = {𝑉})
319316, 318eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (((𝑉 βˆ’ 1) + 1)...𝑉) = {𝑉})
320319uneq2d 4163 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ ((1...(𝑉 βˆ’ 1)) βˆͺ (((𝑉 βˆ’ 1) + 1)...𝑉)) = ((1...(𝑉 βˆ’ 1)) βˆͺ {𝑉}))
321315, 320eqtrd 2773 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (1...𝑉) = ((1...(𝑉 βˆ’ 1)) βˆͺ {𝑉}))
322321difeq1d 4121 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ((1...𝑉) βˆ– {𝑉}) = (((1...(𝑉 βˆ’ 1)) βˆͺ {𝑉}) βˆ– {𝑉}))
323 difun2 4480 . . . . . . . . . . . . . . . . . . . 20 (((1...(𝑉 βˆ’ 1)) βˆͺ {𝑉}) βˆ– {𝑉}) = ((1...(𝑉 βˆ’ 1)) βˆ– {𝑉})
32427ltm1d 12143 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ (𝑉 βˆ’ 1) < 𝑉)
325224, 27ltnled 11358 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ ((𝑉 βˆ’ 1) < 𝑉 ↔ Β¬ 𝑉 ≀ (𝑉 βˆ’ 1)))
326324, 325mpbid 231 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ Β¬ 𝑉 ≀ (𝑉 βˆ’ 1))
327 elfzle2 13502 . . . . . . . . . . . . . . . . . . . . . 22 (𝑉 ∈ (1...(𝑉 βˆ’ 1)) β†’ 𝑉 ≀ (𝑉 βˆ’ 1))
328326, 327nsyl 140 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ Β¬ 𝑉 ∈ (1...(𝑉 βˆ’ 1)))
329 difsn 4801 . . . . . . . . . . . . . . . . . . . . 21 (Β¬ 𝑉 ∈ (1...(𝑉 βˆ’ 1)) β†’ ((1...(𝑉 βˆ’ 1)) βˆ– {𝑉}) = (1...(𝑉 βˆ’ 1)))
330328, 329syl 17 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((1...(𝑉 βˆ’ 1)) βˆ– {𝑉}) = (1...(𝑉 βˆ’ 1)))
331323, 330eqtrid 2785 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (((1...(𝑉 βˆ’ 1)) βˆͺ {𝑉}) βˆ– {𝑉}) = (1...(𝑉 βˆ’ 1)))
332322, 331eqtrd 2773 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ ((1...𝑉) βˆ– {𝑉}) = (1...(𝑉 βˆ’ 1)))
333 elfzle1 13501 . . . . . . . . . . . . . . . . . . . 20 (𝑉 ∈ ((𝑉 + 1)...𝑁) β†’ (𝑉 + 1) ≀ 𝑉)
33432, 333nsyl 140 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ Β¬ 𝑉 ∈ ((𝑉 + 1)...𝑁))
335 difsn 4801 . . . . . . . . . . . . . . . . . . 19 (Β¬ 𝑉 ∈ ((𝑉 + 1)...𝑁) β†’ (((𝑉 + 1)...𝑁) βˆ– {𝑉}) = ((𝑉 + 1)...𝑁))
336334, 335syl 17 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (((𝑉 + 1)...𝑁) βˆ– {𝑉}) = ((𝑉 + 1)...𝑁))
337332, 336uneq12d 4164 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (((1...𝑉) βˆ– {𝑉}) βˆͺ (((𝑉 + 1)...𝑁) βˆ– {𝑉})) = ((1...(𝑉 βˆ’ 1)) βˆͺ ((𝑉 + 1)...𝑁)))
338307, 337eqtrid 2785 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (((1...𝑉) βˆͺ ((𝑉 + 1)...𝑁)) βˆ– {𝑉}) = ((1...(𝑉 βˆ’ 1)) βˆͺ ((𝑉 + 1)...𝑁)))
339306, 338eqtrd 2773 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((1...𝑁) βˆ– {𝑉}) = ((1...(𝑉 βˆ’ 1)) βˆͺ ((𝑉 + 1)...𝑁)))
340339imaeq2d 6058 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘ˆ β€œ ((1...𝑁) βˆ– {𝑉})) = (π‘ˆ β€œ ((1...(𝑉 βˆ’ 1)) βˆͺ ((𝑉 + 1)...𝑁))))
341305, 340eqtr3d 2775 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π‘ˆ β€œ (1...𝑁)) βˆ– (π‘ˆ β€œ {𝑉})) = (π‘ˆ β€œ ((1...(𝑉 βˆ’ 1)) βˆͺ ((𝑉 + 1)...𝑁))))
342 imaundi 6147 . . . . . . . . . . . . 13 (π‘ˆ β€œ ((1...(𝑉 βˆ’ 1)) βˆͺ ((𝑉 + 1)...𝑁))) = ((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) βˆͺ (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))
343341, 342eqtrdi 2789 . . . . . . . . . . . 12 (πœ‘ β†’ ((π‘ˆ β€œ (1...𝑁)) βˆ– (π‘ˆ β€œ {𝑉})) = ((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) βˆͺ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))))
344343eleq2d 2820 . . . . . . . . . . 11 (πœ‘ β†’ (𝑛 ∈ ((π‘ˆ β€œ (1...𝑁)) βˆ– (π‘ˆ β€œ {𝑉})) ↔ 𝑛 ∈ ((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) βˆͺ (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))))
345 eldif 3958 . . . . . . . . . . 11 (𝑛 ∈ ((π‘ˆ β€œ (1...𝑁)) βˆ– (π‘ˆ β€œ {𝑉})) ↔ (𝑛 ∈ (π‘ˆ β€œ (1...𝑁)) ∧ Β¬ 𝑛 ∈ (π‘ˆ β€œ {𝑉})))
346 elun 4148 . . . . . . . . . . 11 (𝑛 ∈ ((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) βˆͺ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) ↔ (𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∨ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))))
347344, 345, 3463bitr3g 313 . . . . . . . . . 10 (πœ‘ β†’ ((𝑛 ∈ (π‘ˆ β€œ (1...𝑁)) ∧ Β¬ 𝑛 ∈ (π‘ˆ β€œ {𝑉})) ↔ (𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∨ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))))
348347adantr 482 . . . . . . . . 9 ((πœ‘ ∧ 𝑉 < 𝑀) β†’ ((𝑛 ∈ (π‘ˆ β€œ (1...𝑁)) ∧ Β¬ 𝑛 ∈ (π‘ˆ β€œ {𝑉})) ↔ (𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∨ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))))
349 imassrn 6069 . . . . . . . . . . . . . . . 16 (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) βŠ† ran π‘ˆ
350349, 63sstrid 3993 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) βŠ† (1...𝑁))
351350sselda 3982 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) β†’ 𝑛 ∈ (1...𝑁))
35267adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) β†’ 𝑇 Fn (1...𝑁))
353 fnconstg 6777 . . . . . . . . . . . . . . . . . . . . 21 (1 ∈ V β†’ ((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) Fn (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))))
35469, 353ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) Fn (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))
355 fnconstg 6777 . . . . . . . . . . . . . . . . . . . . 21 (0 ∈ V β†’ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}) Fn (π‘ˆ β€œ (𝑉...𝑁)))
35672, 355ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}) Fn (π‘ˆ β€œ (𝑉...𝑁))
357354, 356pm3.2i 472 . . . . . . . . . . . . . . . . . . 19 (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) Fn (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∧ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}) Fn (π‘ˆ β€œ (𝑉...𝑁)))
358 imain 6631 . . . . . . . . . . . . . . . . . . . . 21 (Fun β—‘π‘ˆ β†’ (π‘ˆ β€œ ((1...(𝑉 βˆ’ 1)) ∩ (𝑉...𝑁))) = ((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∩ (π‘ˆ β€œ (𝑉...𝑁))))
3594, 358syl 17 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (π‘ˆ β€œ ((1...(𝑉 βˆ’ 1)) ∩ (𝑉...𝑁))) = ((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∩ (π‘ˆ β€œ (𝑉...𝑁))))
360 fzdisj 13525 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑉 βˆ’ 1) < 𝑉 β†’ ((1...(𝑉 βˆ’ 1)) ∩ (𝑉...𝑁)) = βˆ…)
361324, 360syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ ((1...(𝑉 βˆ’ 1)) ∩ (𝑉...𝑁)) = βˆ…)
362361imaeq2d 6058 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (π‘ˆ β€œ ((1...(𝑉 βˆ’ 1)) ∩ (𝑉...𝑁))) = (π‘ˆ β€œ βˆ…))
363362, 81eqtrdi 2789 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (π‘ˆ β€œ ((1...(𝑉 βˆ’ 1)) ∩ (𝑉...𝑁))) = βˆ…)
364359, 363eqtr3d 2775 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∩ (π‘ˆ β€œ (𝑉...𝑁))) = βˆ…)
365 fnun 6661 . . . . . . . . . . . . . . . . . . 19 (((((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) Fn (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∧ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}) Fn (π‘ˆ β€œ (𝑉...𝑁))) ∧ ((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∩ (π‘ˆ β€œ (𝑉...𝑁))) = βˆ…) β†’ (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})) Fn ((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) βˆͺ (π‘ˆ β€œ (𝑉...𝑁))))
366357, 364, 365sylancr 588 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})) Fn ((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) βˆͺ (π‘ˆ β€œ (𝑉...𝑁))))
367 imaundi 6147 . . . . . . . . . . . . . . . . . . . 20 (π‘ˆ β€œ ((1...(𝑉 βˆ’ 1)) βˆͺ (𝑉...𝑁))) = ((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) βˆͺ (π‘ˆ β€œ (𝑉...𝑁)))
368 uzss 12842 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑉 ∈ (β„€β‰₯β€˜(𝑉 βˆ’ 1)) β†’ (β„€β‰₯β€˜π‘‰) βŠ† (β„€β‰₯β€˜(𝑉 βˆ’ 1)))
369313, 368syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ (β„€β‰₯β€˜π‘‰) βŠ† (β„€β‰₯β€˜(𝑉 βˆ’ 1)))
370 elfzuz3 13495 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑉 ∈ (1...(𝑁 βˆ’ 1)) β†’ (𝑁 βˆ’ 1) ∈ (β„€β‰₯β€˜π‘‰))
3717, 370syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (πœ‘ β†’ (𝑁 βˆ’ 1) ∈ (β„€β‰₯β€˜π‘‰))
372369, 371sseldd 3983 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (πœ‘ β†’ (𝑁 βˆ’ 1) ∈ (β„€β‰₯β€˜(𝑉 βˆ’ 1)))
373 peano2uz 12882 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑁 βˆ’ 1) ∈ (β„€β‰₯β€˜(𝑉 βˆ’ 1)) β†’ ((𝑁 βˆ’ 1) + 1) ∈ (β„€β‰₯β€˜(𝑉 βˆ’ 1)))
374372, 373syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (πœ‘ β†’ ((𝑁 βˆ’ 1) + 1) ∈ (β„€β‰₯β€˜(𝑉 βˆ’ 1)))
37513, 374eqeltrrd 2835 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ 𝑁 ∈ (β„€β‰₯β€˜(𝑉 βˆ’ 1)))
376 fzsplit2 13523 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑉 βˆ’ 1) + 1) ∈ (β„€β‰₯β€˜1) ∧ 𝑁 ∈ (β„€β‰₯β€˜(𝑉 βˆ’ 1))) β†’ (1...𝑁) = ((1...(𝑉 βˆ’ 1)) βˆͺ (((𝑉 βˆ’ 1) + 1)...𝑁)))
377308, 375, 376syl2anc 585 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ (1...𝑁) = ((1...(𝑉 βˆ’ 1)) βˆͺ (((𝑉 βˆ’ 1) + 1)...𝑁)))
378212oveq1d 7421 . . . . . . . . . . . . . . . . . . . . . . . 24 (πœ‘ β†’ (((𝑉 βˆ’ 1) + 1)...𝑁) = (𝑉...𝑁))
379378uneq2d 4163 . . . . . . . . . . . . . . . . . . . . . . 23 (πœ‘ β†’ ((1...(𝑉 βˆ’ 1)) βˆͺ (((𝑉 βˆ’ 1) + 1)...𝑁)) = ((1...(𝑉 βˆ’ 1)) βˆͺ (𝑉...𝑁)))
380377, 379eqtrd 2773 . . . . . . . . . . . . . . . . . . . . . 22 (πœ‘ β†’ (1...𝑁) = ((1...(𝑉 βˆ’ 1)) βˆͺ (𝑉...𝑁)))
381380imaeq2d 6058 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (π‘ˆ β€œ (1...𝑁)) = (π‘ˆ β€œ ((1...(𝑉 βˆ’ 1)) βˆͺ (𝑉...𝑁))))
382381, 104eqtr3d 2775 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (π‘ˆ β€œ ((1...(𝑉 βˆ’ 1)) βˆͺ (𝑉...𝑁))) = (1...𝑁))
383367, 382eqtr3id 2787 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ ((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) βˆͺ (π‘ˆ β€œ (𝑉...𝑁))) = (1...𝑁))
384383fneq2d 6641 . . . . . . . . . . . . . . . . . 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 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) β†’ (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})) Fn (1...𝑁))
387 fzfid 13935 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) β†’ (1...𝑁) ∈ Fin)
388 eqidd 2734 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘‡β€˜π‘›) = (π‘‡β€˜π‘›))
389 fvun1 6980 . . . . . . . . . . . . . . . . . . . 20 ((((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) Fn (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∧ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}) Fn (π‘ˆ β€œ (𝑉...𝑁)) ∧ (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∩ (π‘ˆ β€œ (𝑉...𝑁))) = βˆ… ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))))) β†’ ((((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1})β€˜π‘›))
390354, 356, 389mp3an12 1452 . . . . . . . . . . . . . . . . . . 19 ((((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∩ (π‘ˆ β€œ (𝑉...𝑁))) = βˆ… ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) β†’ ((((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1})β€˜π‘›))
391364, 390sylan 581 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) β†’ ((((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1})β€˜π‘›))
39269fvconst2 7202 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) β†’ (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1})β€˜π‘›) = 1)
393392adantl 483 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) β†’ (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1})β€˜π‘›) = 1)
394391, 393eqtrd 2773 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) β†’ ((((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))β€˜π‘›) = 1)
395394adantr 482 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))β€˜π‘›) = 1)
396352, 386, 387, 387, 111, 388, 395ofval 7678 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})))β€˜π‘›) = ((π‘‡β€˜π‘›) + 1))
397108adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) β†’ (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})) Fn (1...𝑁))
398 fzss2 13538 . . . . . . . . . . . . . . . . . . . . 21 (𝑉 ∈ (β„€β‰₯β€˜(𝑉 βˆ’ 1)) β†’ (1...(𝑉 βˆ’ 1)) βŠ† (1...𝑉))
399313, 398syl 17 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (1...(𝑉 βˆ’ 1)) βŠ† (1...𝑉))
400 imass2 6099 . . . . . . . . . . . . . . . . . . . 20 ((1...(𝑉 βˆ’ 1)) βŠ† (1...𝑉) β†’ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) βŠ† (π‘ˆ β€œ (1...𝑉)))
401399, 400syl 17 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) βŠ† (π‘ˆ β€œ (1...𝑉)))
402401sselda 3982 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) β†’ 𝑛 ∈ (π‘ˆ β€œ (1...𝑉)))
403402, 118syldan 592 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) β†’ ((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))β€˜π‘›) = 1)
404403adantr 482 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))β€˜π‘›) = 1)
405352, 397, 387, 387, 111, 388, 404ofval 7678 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›) = ((π‘‡β€˜π‘›) + 1))
406396, 405eqtr4d 2776 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})))β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›))
407351, 406mpdan 686 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1)))) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})))β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›))
408 imassrn 6069 . . . . . . . . . . . . . . . 16 (π‘ˆ β€œ ((𝑉 + 1)...𝑁)) βŠ† ran π‘ˆ
409408, 63sstrid 3993 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (π‘ˆ β€œ ((𝑉 + 1)...𝑁)) βŠ† (1...𝑁))
410409sselda 3982 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) β†’ 𝑛 ∈ (1...𝑁))
41167adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) β†’ 𝑇 Fn (1...𝑁))
412385adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) β†’ (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})) Fn (1...𝑁))
413 fzfid 13935 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) β†’ (1...𝑁) ∈ Fin)
414 eqidd 2734 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) β†’ (π‘‡β€˜π‘›) = (π‘‡β€˜π‘›))
415 fzss1 13537 . . . . . . . . . . . . . . . . . . . . 21 ((𝑉 + 1) ∈ (β„€β‰₯β€˜π‘‰) β†’ ((𝑉 + 1)...𝑁) βŠ† (𝑉...𝑁))
416145, 415syl 17 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((𝑉 + 1)...𝑁) βŠ† (𝑉...𝑁))
417 imass2 6099 . . . . . . . . . . . . . . . . . . . 20 (((𝑉 + 1)...𝑁) βŠ† (𝑉...𝑁) β†’ (π‘ˆ β€œ ((𝑉 + 1)...𝑁)) βŠ† (π‘ˆ β€œ (𝑉...𝑁)))
418416, 417syl 17 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (π‘ˆ β€œ ((𝑉 + 1)...𝑁)) βŠ† (π‘ˆ β€œ (𝑉...𝑁)))
419418sselda 3982 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) β†’ 𝑛 ∈ (π‘ˆ β€œ (𝑉...𝑁)))
420 fvun2 6981 . . . . . . . . . . . . . . . . . . . . 21 ((((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) Fn (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∧ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}) Fn (π‘ˆ β€œ (𝑉...𝑁)) ∧ (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∩ (π‘ˆ β€œ (𝑉...𝑁))) = βˆ… ∧ 𝑛 ∈ (π‘ˆ β€œ (𝑉...𝑁)))) β†’ ((((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})β€˜π‘›))
421354, 356, 420mp3an12 1452 . . . . . . . . . . . . . . . . . . . 20 ((((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∩ (π‘ˆ β€œ (𝑉...𝑁))) = βˆ… ∧ 𝑛 ∈ (π‘ˆ β€œ (𝑉...𝑁))) β†’ ((((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})β€˜π‘›))
422364, 421sylan 581 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (𝑉...𝑁))) β†’ ((((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))β€˜π‘›) = (((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})β€˜π‘›))
42372fvconst2 7202 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (π‘ˆ β€œ (𝑉...𝑁)) β†’ (((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})β€˜π‘›) = 0)
424423adantl 483 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (𝑉...𝑁))) β†’ (((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})β€˜π‘›) = 0)
425422, 424eqtrd 2773 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ (𝑉...𝑁))) β†’ ((((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))β€˜π‘›) = 0)
426419, 425syldan 592 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) β†’ ((((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))β€˜π‘›) = 0)
427426adantr 482 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))β€˜π‘›) = 0)
428411, 412, 413, 413, 111, 414, 427ofval 7678 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})))β€˜π‘›) = ((π‘‡β€˜π‘›) + 0))
429108adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) β†’ (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})) Fn (1...𝑁))
430183adantr 482 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))β€˜π‘›) = 0)
431411, 429, 413, 413, 111, 414, 430ofval 7678 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›) = ((π‘‡β€˜π‘›) + 0))
432428, 431eqtr4d 2776 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})))β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›))
433410, 432mpdan 686 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})))β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›))
434407, 433jaodan 957 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∨ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})))β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›))
435434adantlr 714 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑉 < 𝑀) ∧ (𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∨ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))) β†’ ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})))β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›))
436200adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑉 < 𝑀) β†’ 𝐹 = (𝑦 ∈ (0...(𝑁 βˆ’ 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / π‘—β¦Œ(𝑇 ∘f + (((π‘ˆ β€œ (1...𝑗)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0})))))
437204a1i 11 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 βˆ’ 1)) β†’ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V)
438214adantlr 714 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 βˆ’ 1)) β†’ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑉 βˆ’ 1) < 𝑀, (𝑉 βˆ’ 1), 𝑉))
439 lttr 11287 . . . . . . . . . . . . . . . . . . . . 21 (((𝑉 βˆ’ 1) ∈ ℝ ∧ 𝑉 ∈ ℝ ∧ 𝑀 ∈ ℝ) β†’ (((𝑉 βˆ’ 1) < 𝑉 ∧ 𝑉 < 𝑀) β†’ (𝑉 βˆ’ 1) < 𝑀))
440224, 27, 221, 439syl3anc 1372 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (((𝑉 βˆ’ 1) < 𝑉 ∧ 𝑉 < 𝑀) β†’ (𝑉 βˆ’ 1) < 𝑀))
441324, 440mpand 694 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (𝑉 < 𝑀 β†’ (𝑉 βˆ’ 1) < 𝑀))
442441imp 408 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑉 < 𝑀) β†’ (𝑉 βˆ’ 1) < 𝑀)
443442iftrued 4536 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑉 < 𝑀) β†’ if((𝑉 βˆ’ 1) < 𝑀, (𝑉 βˆ’ 1), 𝑉) = (𝑉 βˆ’ 1))
444443adantr 482 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 βˆ’ 1)) β†’ if((𝑉 βˆ’ 1) < 𝑀, (𝑉 βˆ’ 1), 𝑉) = (𝑉 βˆ’ 1))
445438, 444eqtrd 2773 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 βˆ’ 1)) β†’ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = (𝑉 βˆ’ 1))
446 simpll 766 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 βˆ’ 1)) β†’ πœ‘)
447 oveq2 7414 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = (𝑉 βˆ’ 1) β†’ (1...𝑗) = (1...(𝑉 βˆ’ 1)))
448447imaeq2d 6058 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = (𝑉 βˆ’ 1) β†’ (π‘ˆ β€œ (1...𝑗)) = (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))))
449448xpeq1d 5705 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑉 βˆ’ 1) β†’ ((π‘ˆ β€œ (1...𝑗)) Γ— {1}) = ((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}))
450449adantl 483 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑗 = (𝑉 βˆ’ 1)) β†’ ((π‘ˆ β€œ (1...𝑗)) Γ— {1}) = ((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}))
451 oveq1 7413 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = (𝑉 βˆ’ 1) β†’ (𝑗 + 1) = ((𝑉 βˆ’ 1) + 1))
452451, 212sylan9eqr 2795 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑗 = (𝑉 βˆ’ 1)) β†’ (𝑗 + 1) = 𝑉)
453452oveq1d 7421 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑗 = (𝑉 βˆ’ 1)) β†’ ((𝑗 + 1)...𝑁) = (𝑉...𝑁))
454453imaeq2d 6058 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑗 = (𝑉 βˆ’ 1)) β†’ (π‘ˆ β€œ ((𝑗 + 1)...𝑁)) = (π‘ˆ β€œ (𝑉...𝑁)))
455454xpeq1d 5705 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑗 = (𝑉 βˆ’ 1)) β†’ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0}) = ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))
456450, 455uneq12d 4164 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑗 = (𝑉 βˆ’ 1)) β†’ (((π‘ˆ β€œ (1...𝑗)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0})) = (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})))
457456oveq2d 7422 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑗 = (𝑉 βˆ’ 1)) β†’ (𝑇 ∘f + (((π‘ˆ β€œ (1...𝑗)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0}))) = (𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))))
458446, 457sylan 581 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 βˆ’ 1)) ∧ 𝑗 = (𝑉 βˆ’ 1)) β†’ (𝑇 ∘f + (((π‘ˆ β€œ (1...𝑗)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0}))) = (𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))))
459437, 445, 458csbied2 3933 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 βˆ’ 1)) β†’ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / π‘—β¦Œ(𝑇 ∘f + (((π‘ˆ β€œ (1...𝑗)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0}))) = (𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))))
460246adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑉 < 𝑀) β†’ (𝑉 βˆ’ 1) ∈ (0...(𝑁 βˆ’ 1)))
461 ovexd 7441 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑉 < 𝑀) β†’ (𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))) ∈ V)
462436, 459, 460, 461fvmptd 7003 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑉 < 𝑀) β†’ (πΉβ€˜(𝑉 βˆ’ 1)) = (𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0}))))
463462fveq1d 6891 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑉 < 𝑀) β†’ ((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})))β€˜π‘›))
464463adantr 482 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑉 < 𝑀) ∧ (𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∨ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))) β†’ ((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) Γ— {1}) βˆͺ ((π‘ˆ β€œ (𝑉...𝑁)) Γ— {0})))β€˜π‘›))
465204a1i 11 . . . . . . . . . . . . . . . 16 ((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) β†’ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V)
466 iftrue 4534 . . . . . . . . . . . . . . . . . . . 20 (𝑉 < 𝑀 β†’ if(𝑉 < 𝑀, 𝑉, (𝑉 + 1)) = 𝑉)
467256, 466sylan9eqr 2795 . . . . . . . . . . . . . . . . . . 19 ((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) β†’ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = 𝑉)
468467eqeq2d 2744 . . . . . . . . . . . . . . . . . 18 ((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) β†’ (𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ↔ 𝑗 = 𝑉))
469468biimpa 478 . . . . . . . . . . . . . . . . 17 (((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) β†’ 𝑗 = 𝑉)
470469, 241syl 17 . . . . . . . . . . . . . . . 16 (((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) β†’ (𝑇 ∘f + (((π‘ˆ β€œ (1...𝑗)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0}))) = (𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))))
471465, 470csbied 3931 . . . . . . . . . . . . . . 15 ((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) β†’ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / π‘—β¦Œ(𝑇 ∘f + (((π‘ˆ β€œ (1...𝑗)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0}))) = (𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))))
472471adantll 713 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑉 < 𝑀) ∧ 𝑦 = 𝑉) β†’ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / π‘—β¦Œ(𝑇 ∘f + (((π‘ˆ β€œ (1...𝑗)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑗 + 1)...𝑁)) Γ— {0}))) = (𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))))
473276adantr 482 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑉 < 𝑀) β†’ 𝑉 ∈ (0...(𝑁 βˆ’ 1)))
474 ovexd 7441 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑉 < 𝑀) β†’ (𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))) ∈ V)
475436, 472, 473, 474fvmptd 7003 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑉 < 𝑀) β†’ (πΉβ€˜π‘‰) = (𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0}))))
476475fveq1d 6891 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑉 < 𝑀) β†’ ((πΉβ€˜π‘‰)β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›))
477476adantr 482 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑉 < 𝑀) ∧ (𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∨ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))) β†’ ((πΉβ€˜π‘‰)β€˜π‘›) = ((𝑇 ∘f + (((π‘ˆ β€œ (1...𝑉)) Γ— {1}) βˆͺ ((π‘ˆ β€œ ((𝑉 + 1)...𝑁)) Γ— {0})))β€˜π‘›))
478435, 464, 4773eqtr4d 2783 . . . . . . . . . 10 (((πœ‘ ∧ 𝑉 < 𝑀) ∧ (𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∨ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁)))) β†’ ((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) = ((πΉβ€˜π‘‰)β€˜π‘›))
479478ex 414 . . . . . . . . 9 ((πœ‘ ∧ 𝑉 < 𝑀) β†’ ((𝑛 ∈ (π‘ˆ β€œ (1...(𝑉 βˆ’ 1))) ∨ 𝑛 ∈ (π‘ˆ β€œ ((𝑉 + 1)...𝑁))) β†’ ((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) = ((πΉβ€˜π‘‰)β€˜π‘›)))
480348, 479sylbid 239 . . . . . . . 8 ((πœ‘ ∧ 𝑉 < 𝑀) β†’ ((𝑛 ∈ (π‘ˆ β€œ (1...𝑁)) ∧ Β¬ 𝑛 ∈ (π‘ˆ β€œ {𝑉})) β†’ ((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) = ((πΉβ€˜π‘‰)β€˜π‘›)))
481480expdimp 454 . . . . . . 7 (((πœ‘ ∧ 𝑉 < 𝑀) ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑁))) β†’ (Β¬ 𝑛 ∈ (π‘ˆ β€œ {𝑉}) β†’ ((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) = ((πΉβ€˜π‘‰)β€˜π‘›)))
482481necon1ad 2958 . . . . . 6 (((πœ‘ ∧ 𝑉 < 𝑀) ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑁))) β†’ (((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 ∈ (π‘ˆ β€œ {𝑉})))
483 elimasni 6088 . . . . . . . 8 (𝑛 ∈ (π‘ˆ β€œ {𝑉}) β†’ π‘‰π‘ˆπ‘›)
484 eqcom 2740 . . . . . . . . 9 (𝑛 = (π‘ˆβ€˜π‘‰) ↔ (π‘ˆβ€˜π‘‰) = 𝑛)
485 fnbrfvb 6942 . . . . . . . . . 10 ((π‘ˆ Fn (1...𝑁) ∧ 𝑉 ∈ (1...𝑁)) β†’ ((π‘ˆβ€˜π‘‰) = 𝑛 ↔ π‘‰π‘ˆπ‘›))
486290, 97, 485syl2anc 585 . . . . . . . . 9 (πœ‘ β†’ ((π‘ˆβ€˜π‘‰) = 𝑛 ↔ π‘‰π‘ˆπ‘›))
487484, 486bitrid 283 . . . . . . . 8 (πœ‘ β†’ (𝑛 = (π‘ˆβ€˜π‘‰) ↔ π‘‰π‘ˆπ‘›))
488483, 487imbitrrid 245 . . . . . . 7 (πœ‘ β†’ (𝑛 ∈ (π‘ˆ β€œ {𝑉}) β†’ 𝑛 = (π‘ˆβ€˜π‘‰)))
489488ad2antrr 725 . . . . . 6 (((πœ‘ ∧ 𝑉 < 𝑀) ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑁))) β†’ (𝑛 ∈ (π‘ˆ β€œ {𝑉}) β†’ 𝑛 = (π‘ˆβ€˜π‘‰)))
490482, 489syld 47 . . . . 5 (((πœ‘ ∧ 𝑉 < 𝑀) ∧ 𝑛 ∈ (π‘ˆ β€œ (1...𝑁))) β†’ (((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = (π‘ˆβ€˜π‘‰)))
491490ralrimiva 3147 . . . 4 ((πœ‘ ∧ 𝑉 < 𝑀) β†’ βˆ€π‘› ∈ (π‘ˆ β€œ (1...𝑁))(((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = (π‘ˆβ€˜π‘‰)))
492 fvex 6902 . . . . 5 (π‘ˆβ€˜π‘‰) ∈ V
493 eqeq2 2745 . . . . . . 7 (π‘š = (π‘ˆβ€˜π‘‰) β†’ (𝑛 = π‘š ↔ 𝑛 = (π‘ˆβ€˜π‘‰)))
494493imbi2d 341 . . . . . 6 (π‘š = (π‘ˆβ€˜π‘‰) β†’ ((((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = π‘š) ↔ (((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = (π‘ˆβ€˜π‘‰))))
495494ralbidv 3178 . . . . 5 (π‘š = (π‘ˆβ€˜π‘‰) β†’ (βˆ€π‘› ∈ (π‘ˆ β€œ (1...𝑁))(((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = π‘š) ↔ βˆ€π‘› ∈ (π‘ˆ β€œ (1...𝑁))(((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = (π‘ˆβ€˜π‘‰))))
496492, 495spcev 3597 . . . 4 (βˆ€π‘› ∈ (π‘ˆ β€œ (1...𝑁))(((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = (π‘ˆβ€˜π‘‰)) β†’ βˆƒπ‘šβˆ€π‘› ∈ (π‘ˆ β€œ (1...𝑁))(((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = π‘š))
497491, 496syl 17 . . 3 ((πœ‘ ∧ 𝑉 < 𝑀) β†’ βˆƒπ‘šβˆ€π‘› ∈ (π‘ˆ β€œ (1...𝑁))(((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = π‘š))
498 eldifsni 4793 . . . . 5 (𝑀 ∈ ((0...𝑁) βˆ– {𝑉}) β†’ 𝑀 β‰  𝑉)
499216, 498syl 17 . . . 4 (πœ‘ β†’ 𝑀 β‰  𝑉)
500221, 27lttri2d 11350 . . . 4 (πœ‘ β†’ (𝑀 β‰  𝑉 ↔ (𝑀 < 𝑉 ∨ 𝑉 < 𝑀)))
501499, 500mpbid 231 . . 3 (πœ‘ β†’ (𝑀 < 𝑉 ∨ 𝑉 < 𝑀))
502303, 497, 501mpjaodan 958 . 2 (πœ‘ β†’ βˆƒπ‘šβˆ€π‘› ∈ (π‘ˆ β€œ (1...𝑁))(((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = π‘š))
503 nfv 1918 . . . 4 β„²π‘š((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›)
504503rmo2 3881 . . 3 (βˆƒ*𝑛 ∈ (π‘ˆ β€œ (1...𝑁))((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) ↔ βˆƒπ‘šβˆ€π‘› ∈ (π‘ˆ β€œ (1...𝑁))(((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) β†’ 𝑛 = π‘š))
505 rmoeq1 3415 . . . 4 ((π‘ˆ β€œ (1...𝑁)) = (1...𝑁) β†’ (βˆƒ*𝑛 ∈ (π‘ˆ β€œ (1...𝑁))((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) ↔ βˆƒ*𝑛 ∈ (1...𝑁)((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›)))
506104, 505syl 17 . . 3 (πœ‘ β†’ (βˆƒ*𝑛 ∈ (π‘ˆ β€œ (1...𝑁))((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›) ↔ βˆƒ*𝑛 ∈ (1...𝑁)((πΉβ€˜(𝑉 βˆ’ 1))β€˜π‘›) β‰  ((πΉβ€˜π‘‰)β€˜π‘›)))
507504, 506bitr3id 285 . 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 397   ∨ wo 846   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107   β‰  wne 2941  βˆ€wral 3062  βˆƒ*wrmo 3376  Vcvv 3475  β¦‹csb 3893   βˆ– cdif 3945   βˆͺ cun 3946   ∩ cin 3947   βŠ† wss 3948  βˆ…c0 4322  ifcif 4528  {csn 4628   class class class wbr 5148   ↦ cmpt 5231   Γ— cxp 5674  β—‘ccnv 5675  ran crn 5677   β€œ cima 5679  Fun wfun 6535   Fn wfn 6536  βŸΆwf 6537  β€“ontoβ†’wfo 6539  β€“1-1-ontoβ†’wf1o 6540  β€˜cfv 6541  (class class class)co 7406   ∘f cof 7665  Fincfn 8936  β„‚cc 11105  β„cr 11106  0cc0 11107  1c1 11108   + caddc 11110   < clt 11245   ≀ cle 11246   βˆ’ cmin 11441  β„•cn 12209  β„€cz 12555  β„€β‰₯cuz 12819  ...cfz 13481
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-of 7667  df-om 7853  df-1st 7972  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-1o 8463  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-nn 12210  df-n0 12470  df-z 12556  df-uz 12820  df-fz 13482
This theorem is referenced by:  poimirlem8  36485  poimirlem18  36495  poimirlem21  36498  poimirlem22  36499
  Copyright terms: Public domain W3C validator