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 35473
Description: Lemma for poimir 35504- 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 6656 . . . . . . . . . . . . . . . . 17 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (𝑈:(1...𝑁)–onto→(1...𝑁) ∧ Fun ◡𝑈))
32simprbi 500 . . . . . . . . . . . . . . . 16 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → Fun ◡𝑈)
41, 3syl 17 . . . . . . . . . . . . . . 15 (𝜑 → Fun ◡𝑈)
5 imadif 6453 . . . . . . . . . . . . . . 15 (Fun ◡𝑈 → (𝑈 “ ((1...𝑁) ∖ {(𝑉 + 1)})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})))
64, 5syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑈 “ ((1...𝑁) ∖ {(𝑉 + 1)})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})))
7 poimirlem2.4 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 𝑉 ∈ (1...(𝑁 − 1)))
8 fzp1elp1 13148 . . . . . . . . . . . . . . . . . . . 20 (𝑉 ∈ (1...(𝑁 − 1)) → (𝑉 + 1) ∈ (1...((𝑁 − 1) + 1)))
97, 8syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑉 + 1) ∈ (1...((𝑁 − 1) + 1)))
10 poimir.0 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 𝑁 ∈ ℕ)
1110nncnd 11829 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 𝑁 ∈ ℂ)
12 npcan1 11240 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
1311, 12syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
1413oveq2d 7218 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁))
159, 14eleqtrd 2836 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑉 + 1) ∈ (1...𝑁))
16 fzsplit 13121 . . . . . . . . . . . . . . . . . 18 ((𝑉 + 1) ∈ (1...𝑁) → (1...𝑁) = ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁)))
1715, 16syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (1...𝑁) = ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁)))
1817difeq1d 4026 . . . . . . . . . . . . . . . 16 (𝜑 → ((1...𝑁) ∖ {(𝑉 + 1)}) = (((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁)) ∖ {(𝑉 + 1)}))
19 difundir 4185 . . . . . . . . . . . . . . . . 17 (((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁)) ∖ {(𝑉 + 1)}) = (((1...(𝑉 + 1)) ∖ {(𝑉 + 1)}) ∪ ((((𝑉 + 1) + 1)...𝑁) ∖ {(𝑉 + 1)}))
20 elfzuz 13091 . . . . . . . . . . . . . . . . . . . . . 22 (𝑉 ∈ (1...(𝑁 − 1)) → 𝑉 ∈ (ℤ≥‘1))
217, 20syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 𝑉 ∈ (ℤ≥‘1))
22 fzsuc 13142 . . . . . . . . . . . . . . . . . . . . 21 (𝑉 ∈ (ℤ≥‘1) → (1...(𝑉 + 1)) = ((1...𝑉) ∪ {(𝑉 + 1)}))
2321, 22syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1...(𝑉 + 1)) = ((1...𝑉) ∪ {(𝑉 + 1)}))
2423difeq1d 4026 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((1...(𝑉 + 1)) ∖ {(𝑉 + 1)}) = (((1...𝑉) ∪ {(𝑉 + 1)}) ∖ {(𝑉 + 1)}))
25 difun2 4385 . . . . . . . . . . . . . . . . . . . 20 (((1...𝑉) ∪ {(𝑉 + 1)}) ∖ {(𝑉 + 1)}) = ((1...𝑉) ∖ {(𝑉 + 1)})
267elfzelzd 13096 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → 𝑉 ∈ ℤ)
2726zred 12265 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 𝑉 ∈ ℝ)
2827ltp1d 11745 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 𝑉 < (𝑉 + 1))
2926peano2zd 12268 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑉 + 1) ∈ ℤ)
3029zred 12265 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑉 + 1) ∈ ℝ)
3127, 30ltnled 10962 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑉 < (𝑉 + 1) ↔ ¬ (𝑉 + 1) ≤ 𝑉))
3228, 31mpbid 235 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ¬ (𝑉 + 1) ≤ 𝑉)
33 elfzle2 13099 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑉 + 1) ∈ (1...𝑉) → (𝑉 + 1) ≤ 𝑉)
3432, 33nsyl 142 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ¬ (𝑉 + 1) ∈ (1...𝑉))
35 difsn 4701 . . . . . . . . . . . . . . . . . . . . 21 (¬ (𝑉 + 1) ∈ (1...𝑉) → ((1...𝑉) ∖ {(𝑉 + 1)}) = (1...𝑉))
3634, 35syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((1...𝑉) ∖ {(𝑉 + 1)}) = (1...𝑉))
3725, 36syl5eq 2786 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((1...𝑉) ∪ {(𝑉 + 1)}) ∖ {(𝑉 + 1)}) = (1...𝑉))
3824, 37eqtrd 2774 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((1...(𝑉 + 1)) ∖ {(𝑉 + 1)}) = (1...𝑉))
3930ltp1d 11745 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑉 + 1) < ((𝑉 + 1) + 1))
40 peano2re 10988 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑉 + 1) ∈ ℝ → ((𝑉 + 1) + 1) ∈ ℝ)
4130, 40syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝑉 + 1) + 1) ∈ ℝ)
4230, 41ltnled 10962 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑉 + 1) < ((𝑉 + 1) + 1) ↔ ¬ ((𝑉 + 1) + 1) ≤ (𝑉 + 1)))
4339, 42mpbid 235 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ¬ ((𝑉 + 1) + 1) ≤ (𝑉 + 1))
44 elfzle1 13098 . . . . . . . . . . . . . . . . . . . 20 ((𝑉 + 1) ∈ (((𝑉 + 1) + 1)...𝑁) → ((𝑉 + 1) + 1) ≤ (𝑉 + 1))
4543, 44nsyl 142 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ¬ (𝑉 + 1) ∈ (((𝑉 + 1) + 1)...𝑁))
46 difsn 4701 . . . . . . . . . . . . . . . . . . 19 (¬ (𝑉 + 1) ∈ (((𝑉 + 1) + 1)...𝑁) → ((((𝑉 + 1) + 1)...𝑁) ∖ {(𝑉 + 1)}) = (((𝑉 + 1) + 1)...𝑁))
4745, 46syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((((𝑉 + 1) + 1)...𝑁) ∖ {(𝑉 + 1)}) = (((𝑉 + 1) + 1)...𝑁))
4838, 47uneq12d 4068 . . . . . . . . . . . . . . . . 17 (𝜑 → (((1...(𝑉 + 1)) ∖ {(𝑉 + 1)}) ∪ ((((𝑉 + 1) + 1)...𝑁) ∖ {(𝑉 + 1)})) = ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁)))
4919, 48syl5eq 2786 . . . . . . . . . . . . . . . 16 (𝜑 → (((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁)) ∖ {(𝑉 + 1)}) = ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁)))
5018, 49eqtrd 2774 . . . . . . . . . . . . . . 15 (𝜑 → ((1...𝑁) ∖ {(𝑉 + 1)}) = ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁)))
5150imaeq2d 5918 . . . . . . . . . . . . . 14 (𝜑 → (𝑈 “ ((1...𝑁) ∖ {(𝑉 + 1)})) = (𝑈 “ ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁))))
526, 51eqtr3d 2776 . . . . . . . . . . . . 13 (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})) = (𝑈 “ ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁))))
53 imaundi 6002 . . . . . . . . . . . . 13 (𝑈 “ ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁))) = ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))
5452, 53eqtrdi 2790 . . . . . . . . . . . 12 (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})) = ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))))
5554eleq2d 2819 . . . . . . . . . . 11 (𝜑 → (𝑛 ∈ ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})) ↔ 𝑛 ∈ ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))))
56 eldif 3867 . . . . . . . . . . 11 (𝑛 ∈ ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})) ↔ (𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)})))
57 elun 4053 . . . . . . . . . . 11 (𝑛 ∈ ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ↔ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))))
5855, 56, 573bitr3g 316 . . . . . . . . . 10 (𝜑 → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)})) ↔ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))))
5958adantr 484 . . . . . . . . 9 ((𝜑 ∧ 𝑀 < 𝑉) → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)})) ↔ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))))
60 imassrn 5929 . . . . . . . . . . . . . . . 16 (𝑈 “ (1...𝑉)) ⊆ ran 𝑈
61 f1of 6650 . . . . . . . . . . . . . . . . . 18 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)⟶(1...𝑁))
621, 61syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → 𝑈:(1...𝑁)⟶(1...𝑁))
6362frnd 6542 . . . . . . . . . . . . . . . 16 (𝜑 → ran 𝑈 ⊆ (1...𝑁))
6460, 63sstrid 3902 . . . . . . . . . . . . . . 15 (𝜑 → (𝑈 “ (1...𝑉)) ⊆ (1...𝑁))
6564sselda 3891 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → 𝑛 ∈ (1...𝑁))
66 poimirlem2.2 . . . . . . . . . . . . . . . . . 18 (𝜑 → 𝑇:(1...𝑁)⟶ℤ)
6766ffnd 6535 . . . . . . . . . . . . . . . . 17 (𝜑 → 𝑇 Fn (1...𝑁))
6867adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → 𝑇 Fn (1...𝑁))
69 1ex 10812 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ V
70 fnconstg 6596 . . . . . . . . . . . . . . . . . . . . 21 (1 ∈ V → ((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉)))
7169, 70ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉))
72 c0ex 10810 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ V
73 fnconstg 6596 . . . . . . . . . . . . . . . . . . . . 21 (0 ∈ V → ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁)))
7472, 73ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁))
7571, 74pm3.2i 474 . . . . . . . . . . . . . . . . . . 19 (((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉)) ∧ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁)))
76 imain 6454 . . . . . . . . . . . . . . . . . . . . 21 (Fun ◡𝑈 → (𝑈 “ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = ((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))))
774, 76syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = ((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))))
78 fzdisj 13122 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑉 < (𝑉 + 1) → ((1...𝑉) ∩ ((𝑉 + 1)...𝑁)) = ∅)
7928, 78syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1...𝑉) ∩ ((𝑉 + 1)...𝑁)) = ∅)
8079imaeq2d 5918 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = (𝑈 “ ∅))
81 ima0 5934 . . . . . . . . . . . . . . . . . . . . 21 (𝑈 “ ∅) = ∅
8280, 81eqtrdi 2790 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = ∅)
8377, 82eqtr3d 2776 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅)
84 fnun 6479 . . . . . . . . . . . . . . . . . . 19 (((((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉)) ∧ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ ((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))))
8575, 83, 84sylancr 590 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))))
86 imaundi 6002 . . . . . . . . . . . . . . . . . . . 20 (𝑈 “ ((1...𝑉) ∪ ((𝑉 + 1)...𝑁))) = ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁)))
8710nnzd 12264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → 𝑁 ∈ ℤ)
88 peano2zm 12203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
8987, 88syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑁 − 1) ∈ ℤ)
90 uzid 12436 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ≥‘(𝑁 − 1)))
9189, 90syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑁 − 1) ∈ (ℤ≥‘(𝑁 − 1)))
92 peano2uz 12480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑁 − 1) ∈ (ℤ≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ≥‘(𝑁 − 1)))
9391, 92syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ≥‘(𝑁 − 1)))
9413, 93eqeltrrd 2835 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑁 − 1)))
95 fzss2 13135 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ (ℤ≥‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
9694, 95syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
9796, 7sseldd 3892 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 𝑉 ∈ (1...𝑁))
98 fzsplit 13121 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑉 ∈ (1...𝑁) → (1...𝑁) = ((1...𝑉) ∪ ((𝑉 + 1)...𝑁)))
9997, 98syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (1...𝑁) = ((1...𝑉) ∪ ((𝑉 + 1)...𝑁)))
10099imaeq2d 5918 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...𝑉) ∪ ((𝑉 + 1)...𝑁))))
101 f1ofo 6657 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–onto→(1...𝑁))
1021, 101syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 𝑈:(1...𝑁)–onto→(1...𝑁))
103 foima 6627 . . . . . . . . . . . . . . . . . . . . . 22 (𝑈:(1...𝑁)–onto→(1...𝑁) → (𝑈 “ (1...𝑁)) = (1...𝑁))
104102, 103syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ (1...𝑁)) = (1...𝑁))
105100, 104eqtr3d 2776 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...𝑉) ∪ ((𝑉 + 1)...𝑁))) = (1...𝑁))
10686, 105eqtr3id 2788 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))) = (1...𝑁))
107106fneq2d 6462 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))) ↔ (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁)))
10885, 107mpbid 235 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁))
109108adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁))
110 fzfid 13529 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → (1...𝑁) ∈ Fin)
111 inidm 4123 . . . . . . . . . . . . . . . 16 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
112 eqidd 2735 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) = (𝑇‘𝑛))
113 fvun1 6791 . . . . . . . . . . . . . . . . . . . 20 ((((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉)) ∧ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁)) ∧ (((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...𝑉)))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...𝑉)) × {1})‘𝑛))
11471, 74, 113mp3an12 1453 . . . . . . . . . . . . . . . . . . 19 ((((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...𝑉)) × {1})‘𝑛))
11583, 114sylan 583 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...𝑉)) × {1})‘𝑛))
11669fvconst2 7008 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (𝑈 “ (1...𝑉)) → (((𝑈 “ (1...𝑉)) × {1})‘𝑛) = 1)
117116adantl 485 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → (((𝑈 “ (1...𝑉)) × {1})‘𝑛) = 1)
118115, 117eqtrd 2774 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 1)
119118adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 1)
12068, 109, 110, 110, 111, 112, 119ofval 7468 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1))
121 fnconstg 6596 . . . . . . . . . . . . . . . . . . . . 21 (1 ∈ V → ((𝑈 “ (1...(𝑉 + 1))) × {1}) Fn (𝑈 “ (1...(𝑉 + 1))))
12269, 121ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 “ (1...(𝑉 + 1))) × {1}) Fn (𝑈 “ (1...(𝑉 + 1)))
123 fnconstg 6596 . . . . . . . . . . . . . . . . . . . . 21 (0 ∈ V → ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))
12472, 123ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑉 + 1) + 1)...𝑁))
125122, 124pm3.2i 474 . . . . . . . . . . . . . . . . . . 19 (((𝑈 “ (1...(𝑉 + 1))) × {1}) Fn (𝑈 “ (1...(𝑉 + 1))) ∧ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))
126 imain 6454 . . . . . . . . . . . . . . . . . . . . 21 (Fun ◡𝑈 → (𝑈 “ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))))
1274, 126syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))))
128 fzdisj 13122 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑉 + 1) < ((𝑉 + 1) + 1) → ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁)) = ∅)
12939, 128syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁)) = ∅)
130129imaeq2d 5918 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = (𝑈 “ ∅))
131130, 81eqtrdi 2790 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = ∅)
132127, 131eqtr3d 2776 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = ∅)
133 fnun 6479 . . . . . . . . . . . . . . . . . . 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 590 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 + 1))) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))))
135 imaundi 6002 . . . . . . . . . . . . . . . . . . . 20 (𝑈 “ ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑉 + 1))) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))
13617imaeq2d 5918 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁))))
137136, 104eqtr3d 2776 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁))) = (1...𝑁))
138135, 137eqtr3id 2788 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑈 “ (1...(𝑉 + 1))) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = (1...𝑁))
139138fneq2d 6462 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 + 1))) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ↔ (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁)))
140134, 139mpbid 235 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁))
141140adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁))
142 uzid 12436 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑉 ∈ ℤ → 𝑉 ∈ (ℤ≥‘𝑉))
14326, 142syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 𝑉 ∈ (ℤ≥‘𝑉))
144 peano2uz 12480 . . . . . . . . . . . . . . . . . . . . . 22 (𝑉 ∈ (ℤ≥‘𝑉) → (𝑉 + 1) ∈ (ℤ≥‘𝑉))
145143, 144syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑉 + 1) ∈ (ℤ≥‘𝑉))
146 fzss2 13135 . . . . . . . . . . . . . . . . . . . . 21 ((𝑉 + 1) ∈ (ℤ≥‘𝑉) → (1...𝑉) ⊆ (1...(𝑉 + 1)))
147145, 146syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1...𝑉) ⊆ (1...(𝑉 + 1)))
148 imass2 5959 . . . . . . . . . . . . . . . . . . . 20 ((1...𝑉) ⊆ (1...(𝑉 + 1)) → (𝑈 “ (1...𝑉)) ⊆ (𝑈 “ (1...(𝑉 + 1))))
149147, 148syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑈 “ (1...𝑉)) ⊆ (𝑈 “ (1...(𝑉 + 1))))
150149sselda 3891 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1))))
151 fvun1 6791 . . . . . . . . . . . . . . . . . . . . 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 1453 . . . . . . . . . . . . . . . . . . . 20 ((((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1)))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 + 1))) × {1})‘𝑛))
153132, 152sylan 583 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1)))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 + 1))) × {1})‘𝑛))
15469fvconst2 7008 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (𝑈 “ (1...(𝑉 + 1))) → (((𝑈 “ (1...(𝑉 + 1))) × {1})‘𝑛) = 1)
155154adantl 485 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1)))) → (((𝑈 “ (1...(𝑉 + 1))) × {1})‘𝑛) = 1)
156153, 155eqtrd 2774 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1)))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 1)
157150, 156syldan 594 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 1)
158157adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 1)
15968, 141, 110, 110, 111, 112, 158ofval 7468 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1))
160120, 159eqtr4d 2777 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
16165, 160mpdan 687 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
162 imassrn 5929 . . . . . . . . . . . . . . . 16 (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ⊆ ran 𝑈
163162, 63sstrid 3902 . . . . . . . . . . . . . . 15 (𝜑 → (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ⊆ (1...𝑁))
164163sselda 3891 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → 𝑛 ∈ (1...𝑁))
16567adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → 𝑇 Fn (1...𝑁))
166108adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁))
167 fzfid 13529 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → (1...𝑁) ∈ Fin)
168 eqidd 2735 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) = (𝑇‘𝑛))
169 uzid 12436 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑉 + 1) ∈ ℤ → (𝑉 + 1) ∈ (ℤ≥‘(𝑉 + 1)))
17029, 169syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑉 + 1) ∈ (ℤ≥‘(𝑉 + 1)))
171 peano2uz 12480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑉 + 1) ∈ (ℤ≥‘(𝑉 + 1)) → ((𝑉 + 1) + 1) ∈ (ℤ≥‘(𝑉 + 1)))
172170, 171syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑉 + 1) + 1) ∈ (ℤ≥‘(𝑉 + 1)))
173 fzss1 13134 . . . . . . . . . . . . . . . . . . . . 21 (((𝑉 + 1) + 1) ∈ (ℤ≥‘(𝑉 + 1)) → (((𝑉 + 1) + 1)...𝑁) ⊆ ((𝑉 + 1)...𝑁))
174172, 173syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝑉 + 1) + 1)...𝑁) ⊆ ((𝑉 + 1)...𝑁))
175 imass2 5959 . . . . . . . . . . . . . . . . . . . 20 ((((𝑉 + 1) + 1)...𝑁) ⊆ ((𝑉 + 1)...𝑁) → (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ⊆ (𝑈 “ ((𝑉 + 1)...𝑁)))
176174, 175syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ⊆ (𝑈 “ ((𝑉 + 1)...𝑁)))
177176sselda 3891 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))
178 fvun2 6792 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉)) ∧ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁)) ∧ (((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛))
17971, 74, 178mp3an12 1453 . . . . . . . . . . . . . . . . . . . 20 ((((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛))
18083, 179sylan 583 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛))
18172fvconst2 7008 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)) → (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛) = 0)
182181adantl 485 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛) = 0)
183180, 182eqtrd 2774 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 0)
184177, 183syldan 594 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 0)
185184adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 0)
186165, 166, 167, 167, 111, 168, 185ofval 7468 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0))
187140adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁))
188 fvun2 6792 . . . . . . . . . . . . . . . . . . . 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 1453 . . . . . . . . . . . . . . . . . . 19 ((((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})‘𝑛))
190132, 189sylan 583 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})‘𝑛))
19172fvconst2 7008 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) → (((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})‘𝑛) = 0)
192191adantl 485 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → (((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})‘𝑛) = 0)
193190, 192eqtrd 2774 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 0)
194193adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 0)
195165, 187, 167, 167, 111, 168, 194ofval 7468 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0))
196186, 195eqtr4d 2777 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
197164, 196mpdan 687 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
198161, 197jaodan 958 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
199198adantlr 715 . . . . . . . . . . 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 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑀 < 𝑉) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))))
202 vex 3405 . . . . . . . . . . . . . . . . 17 𝑦 ∈ V
203 ovex 7235 . . . . . . . . . . . . . . . . 17 (𝑦 + 1) ∈ V
204202, 203ifex 4479 . . . . . . . . . . . . . . . 16 if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V
205204a1i 11 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V)
206 breq1 5046 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (𝑉 − 1) → (𝑦 < 𝑀 ↔ (𝑉 − 1) < 𝑀))
207206adantl 485 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑦 = (𝑉 − 1)) → (𝑦 < 𝑀 ↔ (𝑉 − 1) < 𝑀))
208 simpr 488 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑦 = (𝑉 − 1)) → 𝑦 = (𝑉 − 1))
209 oveq1 7209 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (𝑉 − 1) → (𝑦 + 1) = ((𝑉 − 1) + 1))
21026zcnd 12266 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 𝑉 ∈ ℂ)
211 npcan1 11240 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑉 ∈ ℂ → ((𝑉 − 1) + 1) = 𝑉)
212210, 211syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝑉 − 1) + 1) = 𝑉)
213209, 212sylan9eqr 2796 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑦 = (𝑉 − 1)) → (𝑦 + 1) = 𝑉)
214207, 208, 213ifbieq12d 4457 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉))
215214adantlr 715 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉))
216 poimirlem2.5 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → 𝑀 ∈ ((0...𝑁) ∖ {𝑉}))
217216eldifad 3869 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → 𝑀 ∈ (0...𝑁))
218217elfzelzd 13096 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 𝑀 ∈ ℤ)
219 zltlem1 12213 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑀 ∈ ℤ ∧ 𝑉 ∈ ℤ) → (𝑀 < 𝑉 ↔ 𝑀 ≤ (𝑉 − 1)))
220218, 26, 219syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑀 < 𝑉 ↔ 𝑀 ≤ (𝑉 − 1)))
221218zred 12265 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 𝑀 ∈ ℝ)
222 peano2zm 12203 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑉 ∈ ℤ → (𝑉 − 1) ∈ ℤ)
22326, 222syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑉 − 1) ∈ ℤ)
224223zred 12265 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑉 − 1) ∈ ℝ)
225221, 224lenltd 10961 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑀 ≤ (𝑉 − 1) ↔ ¬ (𝑉 − 1) < 𝑀))
226220, 225bitrd 282 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑀 < 𝑉 ↔ ¬ (𝑉 − 1) < 𝑀))
227226biimpa 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑀 < 𝑉) → ¬ (𝑉 − 1) < 𝑀)
228227iffalsed 4440 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑀 < 𝑉) → if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉) = 𝑉)
229228adantr 484 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉) = 𝑉)
230215, 229eqtrd 2774 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = 𝑉)
231230eqeq2d 2745 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → (𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ↔ 𝑗 = 𝑉))
232231biimpa 480 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → 𝑗 = 𝑉)
233 oveq2 7210 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑉 → (1...𝑗) = (1...𝑉))
234233imaeq2d 5918 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑉 → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...𝑉)))
235234xpeq1d 5569 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑉 → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...𝑉)) × {1}))
236 oveq1 7209 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑉 → (𝑗 + 1) = (𝑉 + 1))
237236oveq1d 7217 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑉 → ((𝑗 + 1)...𝑁) = ((𝑉 + 1)...𝑁))
238237imaeq2d 5918 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑉 → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ ((𝑉 + 1)...𝑁)))
239238xpeq1d 5569 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑉 → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))
240235, 239uneq12d 4068 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑉 → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))
241240oveq2d 7218 . . . . . . . . . . . . . . . 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 3840 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
244 elfzm1b 13173 . . . . . . . . . . . . . . . . 17 ((𝑉 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑉 ∈ (1...𝑁) ↔ (𝑉 − 1) ∈ (0...(𝑁 − 1))))
24526, 87, 244syl2anc 587 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑉 ∈ (1...𝑁) ↔ (𝑉 − 1) ∈ (0...(𝑁 − 1))))
24697, 245mpbid 235 . . . . . . . . . . . . . . 15 (𝜑 → (𝑉 − 1) ∈ (0...(𝑁 − 1)))
247246adantr 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑀 < 𝑉) → (𝑉 − 1) ∈ (0...(𝑁 − 1)))
248 ovexd 7237 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑀 < 𝑉) → (𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))) ∈ V)
249201, 243, 247, 248fvmptd 6814 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑀 < 𝑉) → (𝐹‘(𝑉 − 1)) = (𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
250249fveq1d 6708 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑀 < 𝑉) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
251250adantr 484 . . . . . . . . . . 11 (((𝜑 ∧ 𝑀 < 𝑉) ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
252204a1i 11 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V)
253 breq1 5046 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑉 → (𝑦 < 𝑀 ↔ 𝑉 < 𝑀))
254 id 22 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑉 → 𝑦 = 𝑉)
255 oveq1 7209 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑉 → (𝑦 + 1) = (𝑉 + 1))
256253, 254, 255ifbieq12d 4457 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑉 → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if(𝑉 < 𝑀, 𝑉, (𝑉 + 1)))
257 ltnsym 10913 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑀 ∈ ℝ ∧ 𝑉 ∈ ℝ) → (𝑀 < 𝑉 → ¬ 𝑉 < 𝑀))
258221, 27, 257syl2anc 587 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑀 < 𝑉 → ¬ 𝑉 < 𝑀))
259258imp 410 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑀 < 𝑉) → ¬ 𝑉 < 𝑀)
260259iffalsed 4440 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑀 < 𝑉) → if(𝑉 < 𝑀, 𝑉, (𝑉 + 1)) = (𝑉 + 1))
261256, 260sylan9eqr 2796 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = (𝑉 + 1))
262261eqeq2d 2745 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) → (𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ↔ 𝑗 = (𝑉 + 1)))
263262biimpa 480 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → 𝑗 = (𝑉 + 1))
264 oveq2 7210 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = (𝑉 + 1) → (1...𝑗) = (1...(𝑉 + 1)))
265264imaeq2d 5918 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑉 + 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑉 + 1))))
266265xpeq1d 5569 . . . . . . . . . . . . . . . . . 18 (𝑗 = (𝑉 + 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑉 + 1))) × {1}))
267 oveq1 7209 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = (𝑉 + 1) → (𝑗 + 1) = ((𝑉 + 1) + 1))
268267oveq1d 7217 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = (𝑉 + 1) → ((𝑗 + 1)...𝑁) = (((𝑉 + 1) + 1)...𝑁))
269268imaeq2d 5918 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑉 + 1) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))
270269xpeq1d 5569 . . . . . . . . . . . . . . . . . 18 (𝑗 = (𝑉 + 1) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))
271266, 270uneq12d 4068 . . . . . . . . . . . . . . . . 17 (𝑗 = (𝑉 + 1) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))
272271oveq2d 7218 . . . . . . . . . . . . . . . 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 3840 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))))
275 fz1ssfz0 13191 . . . . . . . . . . . . . . . 16 (1...(𝑁 − 1)) ⊆ (0...(𝑁 − 1))
276275, 7sseldi 3889 . . . . . . . . . . . . . . 15 (𝜑 → 𝑉 ∈ (0...(𝑁 − 1)))
277276adantr 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑀 < 𝑉) → 𝑉 ∈ (0...(𝑁 − 1)))
278 ovexd 7237 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑀 < 𝑉) → (𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))) ∈ V)
279201, 274, 277, 278fvmptd 6814 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑀 < 𝑉) → (𝐹‘𝑉) = (𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))))
280279fveq1d 6708 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑀 < 𝑉) → ((𝐹‘𝑉)‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
281280adantr 484 . . . . . . . . . . 11 (((𝜑 ∧ 𝑀 < 𝑉) ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝐹‘𝑉)‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
282199, 251, 2813eqtr4d 2784 . . . . . . . . . 10 (((𝜑 ∧ 𝑀 < 𝑉) ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛))
283282ex 416 . . . . . . . . 9 ((𝜑 ∧ 𝑀 < 𝑉) → ((𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛)))
28459, 283sylbid 243 . . . . . . . 8 ((𝜑 ∧ 𝑀 < 𝑉) → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)})) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛)))
285284expdimp 456 . . . . . . 7 (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)}) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛)))
286285necon1ad 2952 . . . . . 6 (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 ∈ (𝑈 “ {(𝑉 + 1)})))
287 elimasni 5948 . . . . . . . 8 (𝑛 ∈ (𝑈 “ {(𝑉 + 1)}) → (𝑉 + 1)𝑈𝑛)
288 eqcom 2741 . . . . . . . . 9 (𝑛 = (𝑈‘(𝑉 + 1)) ↔ (𝑈‘(𝑉 + 1)) = 𝑛)
289 f1ofn 6651 . . . . . . . . . . 11 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 Fn (1...𝑁))
2901, 289syl 17 . . . . . . . . . 10 (𝜑 → 𝑈 Fn (1...𝑁))
291 fnbrfvb 6754 . . . . . . . . . 10 ((𝑈 Fn (1...𝑁) ∧ (𝑉 + 1) ∈ (1...𝑁)) → ((𝑈‘(𝑉 + 1)) = 𝑛 ↔ (𝑉 + 1)𝑈𝑛))
292290, 15, 291syl2anc 587 . . . . . . . . 9 (𝜑 → ((𝑈‘(𝑉 + 1)) = 𝑛 ↔ (𝑉 + 1)𝑈𝑛))
293288, 292syl5bb 286 . . . . . . . 8 (𝜑 → (𝑛 = (𝑈‘(𝑉 + 1)) ↔ (𝑉 + 1)𝑈𝑛))
294287, 293syl5ibr 249 . . . . . . 7 (𝜑 → (𝑛 ∈ (𝑈 “ {(𝑉 + 1)}) → 𝑛 = (𝑈‘(𝑉 + 1))))
295294ad2antrr 726 . . . . . 6 (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (𝑛 ∈ (𝑈 “ {(𝑉 + 1)}) → 𝑛 = (𝑈‘(𝑉 + 1))))
296286, 295syld 47 . . . . 5 (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1))))
297296ralrimiva 3098 . . . 4 ((𝜑 ∧ 𝑀 < 𝑉) → ∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1))))
298 fvex 6719 . . . . 5 (𝑈‘(𝑉 + 1)) ∈ V
299 eqeq2 2746 . . . . . . 7 (𝑚 = (𝑈‘(𝑉 + 1)) → (𝑛 = 𝑚 ↔ 𝑛 = (𝑈‘(𝑉 + 1))))
300299imbi2d 344 . . . . . 6 (𝑚 = (𝑈‘(𝑉 + 1)) → ((((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1)))))
301300ralbidv 3111 . . . . 5 (𝑚 = (𝑈‘(𝑉 + 1)) → (∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ ∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1)))))
302298, 301spcev 3514 . . . 4 (∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1))) → ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚))
303297, 302syl 17 . . 3 ((𝜑 ∧ 𝑀 < 𝑉) → ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚))
304 imadif 6453 . . . . . . . . . . . . . . 15 (Fun ◡𝑈 → (𝑈 “ ((1...𝑁) ∖ {𝑉})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})))
3054, 304syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑈 “ ((1...𝑁) ∖ {𝑉})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})))
30699difeq1d 4026 . . . . . . . . . . . . . . . 16 (𝜑 → ((1...𝑁) ∖ {𝑉}) = (((1...𝑉) ∪ ((𝑉 + 1)...𝑁)) ∖ {𝑉}))
307 difundir 4185 . . . . . . . . . . . . . . . . 17 (((1...𝑉) ∪ ((𝑉 + 1)...𝑁)) ∖ {𝑉}) = (((1...𝑉) ∖ {𝑉}) ∪ (((𝑉 + 1)...𝑁) ∖ {𝑉}))
308212, 21eqeltrd 2834 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝑉 − 1) + 1) ∈ (ℤ≥‘1))
309 uzid 12436 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑉 − 1) ∈ ℤ → (𝑉 − 1) ∈ (ℤ≥‘(𝑉 − 1)))
310223, 309syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑉 − 1) ∈ (ℤ≥‘(𝑉 − 1)))
311 peano2uz 12480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑉 − 1) ∈ (ℤ≥‘(𝑉 − 1)) → ((𝑉 − 1) + 1) ∈ (ℤ≥‘(𝑉 − 1)))
312310, 311syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑉 − 1) + 1) ∈ (ℤ≥‘(𝑉 − 1)))
313212, 312eqeltrrd 2835 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 𝑉 ∈ (ℤ≥‘(𝑉 − 1)))
314 fzsplit2 13120 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑉 − 1) + 1) ∈ (ℤ≥‘1) ∧ 𝑉 ∈ (ℤ≥‘(𝑉 − 1))) → (1...𝑉) = ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑉)))
315308, 313, 314syl2anc 587 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (1...𝑉) = ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑉)))
316212oveq1d 7217 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((𝑉 − 1) + 1)...𝑉) = (𝑉...𝑉))
317 fzsn 13137 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑉 ∈ ℤ → (𝑉...𝑉) = {𝑉})
31826, 317syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑉...𝑉) = {𝑉})
319316, 318eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝑉 − 1) + 1)...𝑉) = {𝑉})
320319uneq2d 4067 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑉)) = ((1...(𝑉 − 1)) ∪ {𝑉}))
321315, 320eqtrd 2774 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1...𝑉) = ((1...(𝑉 − 1)) ∪ {𝑉}))
322321difeq1d 4026 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((1...𝑉) ∖ {𝑉}) = (((1...(𝑉 − 1)) ∪ {𝑉}) ∖ {𝑉}))
323 difun2 4385 . . . . . . . . . . . . . . . . . . . 20 (((1...(𝑉 − 1)) ∪ {𝑉}) ∖ {𝑉}) = ((1...(𝑉 − 1)) ∖ {𝑉})
32427ltm1d 11747 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑉 − 1) < 𝑉)
325224, 27ltnled 10962 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑉 − 1) < 𝑉 ↔ ¬ 𝑉 ≤ (𝑉 − 1)))
326324, 325mpbid 235 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ¬ 𝑉 ≤ (𝑉 − 1))
327 elfzle2 13099 . . . . . . . . . . . . . . . . . . . . . 22 (𝑉 ∈ (1...(𝑉 − 1)) → 𝑉 ≤ (𝑉 − 1))
328326, 327nsyl 142 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ¬ 𝑉 ∈ (1...(𝑉 − 1)))
329 difsn 4701 . . . . . . . . . . . . . . . . . . . . 21 (¬ 𝑉 ∈ (1...(𝑉 − 1)) → ((1...(𝑉 − 1)) ∖ {𝑉}) = (1...(𝑉 − 1)))
330328, 329syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((1...(𝑉 − 1)) ∖ {𝑉}) = (1...(𝑉 − 1)))
331323, 330syl5eq 2786 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((1...(𝑉 − 1)) ∪ {𝑉}) ∖ {𝑉}) = (1...(𝑉 − 1)))
332322, 331eqtrd 2774 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((1...𝑉) ∖ {𝑉}) = (1...(𝑉 − 1)))
333 elfzle1 13098 . . . . . . . . . . . . . . . . . . . 20 (𝑉 ∈ ((𝑉 + 1)...𝑁) → (𝑉 + 1) ≤ 𝑉)
33432, 333nsyl 142 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ¬ 𝑉 ∈ ((𝑉 + 1)...𝑁))
335 difsn 4701 . . . . . . . . . . . . . . . . . . 19 (¬ 𝑉 ∈ ((𝑉 + 1)...𝑁) → (((𝑉 + 1)...𝑁) ∖ {𝑉}) = ((𝑉 + 1)...𝑁))
336334, 335syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝑉 + 1)...𝑁) ∖ {𝑉}) = ((𝑉 + 1)...𝑁))
337332, 336uneq12d 4068 . . . . . . . . . . . . . . . . 17 (𝜑 → (((1...𝑉) ∖ {𝑉}) ∪ (((𝑉 + 1)...𝑁) ∖ {𝑉})) = ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁)))
338307, 337syl5eq 2786 . . . . . . . . . . . . . . . 16 (𝜑 → (((1...𝑉) ∪ ((𝑉 + 1)...𝑁)) ∖ {𝑉}) = ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁)))
339306, 338eqtrd 2774 . . . . . . . . . . . . . . 15 (𝜑 → ((1...𝑁) ∖ {𝑉}) = ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁)))
340339imaeq2d 5918 . . . . . . . . . . . . . 14 (𝜑 → (𝑈 “ ((1...𝑁) ∖ {𝑉})) = (𝑈 “ ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁))))
341305, 340eqtr3d 2776 . . . . . . . . . . . . 13 (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})) = (𝑈 “ ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁))))
342 imaundi 6002 . . . . . . . . . . . . 13 (𝑈 “ ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁))) = ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ ((𝑉 + 1)...𝑁)))
343341, 342eqtrdi 2790 . . . . . . . . . . . 12 (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})) = ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))))
344343eleq2d 2819 . . . . . . . . . . 11 (𝜑 → (𝑛 ∈ ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})) ↔ 𝑛 ∈ ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ ((𝑉 + 1)...𝑁)))))
345 eldif 3867 . . . . . . . . . . 11 (𝑛 ∈ ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})) ↔ (𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {𝑉})))
346 elun 4053 . . . . . . . . . . 11 (𝑛 ∈ ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))) ↔ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))))
347344, 345, 3463bitr3g 316 . . . . . . . . . 10 (𝜑 → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {𝑉})) ↔ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))))
348347adantr 484 . . . . . . . . 9 ((𝜑 ∧ 𝑉 < 𝑀) → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {𝑉})) ↔ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))))
349 imassrn 5929 . . . . . . . . . . . . . . . 16 (𝑈 “ (1...(𝑉 − 1))) ⊆ ran 𝑈
350349, 63sstrid 3902 . . . . . . . . . . . . . . 15 (𝜑 → (𝑈 “ (1...(𝑉 − 1))) ⊆ (1...𝑁))
351350sselda 3891 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → 𝑛 ∈ (1...𝑁))
35267adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → 𝑇 Fn (1...𝑁))
353 fnconstg 6596 . . . . . . . . . . . . . . . . . . . . 21 (1 ∈ V → ((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1))))
35469, 353ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1)))
355 fnconstg 6596 . . . . . . . . . . . . . . . . . . . . 21 (0 ∈ V → ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁)))
35672, 355ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁))
357354, 356pm3.2i 474 . . . . . . . . . . . . . . . . . . 19 (((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1))) ∧ ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁)))
358 imain 6454 . . . . . . . . . . . . . . . . . . . . 21 (Fun ◡𝑈 → (𝑈 “ ((1...(𝑉 − 1)) ∩ (𝑉...𝑁))) = ((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))))
3594, 358syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...(𝑉 − 1)) ∩ (𝑉...𝑁))) = ((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))))
360 fzdisj 13122 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑉 − 1) < 𝑉 → ((1...(𝑉 − 1)) ∩ (𝑉...𝑁)) = ∅)
361324, 360syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1...(𝑉 − 1)) ∩ (𝑉...𝑁)) = ∅)
362361imaeq2d 5918 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ ((1...(𝑉 − 1)) ∩ (𝑉...𝑁))) = (𝑈 “ ∅))
363362, 81eqtrdi 2790 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...(𝑉 − 1)) ∩ (𝑉...𝑁))) = ∅)
364359, 363eqtr3d 2776 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅)
365 fnun 6479 . . . . . . . . . . . . . . . . . . 19 (((((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1))) ∧ ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁))) ∧ ((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅) → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁))))
366357, 364, 365sylancr 590 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁))))
367 imaundi 6002 . . . . . . . . . . . . . . . . . . . 20 (𝑈 “ ((1...(𝑉 − 1)) ∪ (𝑉...𝑁))) = ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁)))
368 uzss 12444 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑉 ∈ (ℤ≥‘(𝑉 − 1)) → (ℤ≥‘𝑉) ⊆ (ℤ≥‘(𝑉 − 1)))
369313, 368syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (ℤ≥‘𝑉) ⊆ (ℤ≥‘(𝑉 − 1)))
370 elfzuz3 13092 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑉 ∈ (1...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ≥‘𝑉))
3717, 370syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑁 − 1) ∈ (ℤ≥‘𝑉))
372369, 371sseldd 3892 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑁 − 1) ∈ (ℤ≥‘(𝑉 − 1)))
373 peano2uz 12480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑁 − 1) ∈ (ℤ≥‘(𝑉 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ≥‘(𝑉 − 1)))
374372, 373syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ≥‘(𝑉 − 1)))
37513, 374eqeltrrd 2835 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑉 − 1)))
376 fzsplit2 13120 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑉 − 1) + 1) ∈ (ℤ≥‘1) ∧ 𝑁 ∈ (ℤ≥‘(𝑉 − 1))) → (1...𝑁) = ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑁)))
377308, 375, 376syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1...𝑁) = ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑁)))
378212oveq1d 7217 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((𝑉 − 1) + 1)...𝑁) = (𝑉...𝑁))
379378uneq2d 4067 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑁)) = ((1...(𝑉 − 1)) ∪ (𝑉...𝑁)))
380377, 379eqtrd 2774 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (1...𝑁) = ((1...(𝑉 − 1)) ∪ (𝑉...𝑁)))
381380imaeq2d 5918 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...(𝑉 − 1)) ∪ (𝑉...𝑁))))
382381, 104eqtr3d 2776 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...(𝑉 − 1)) ∪ (𝑉...𝑁))) = (1...𝑁))
383367, 382eqtr3id 2788 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁))) = (1...𝑁))
384383fneq2d 6462 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁))) ↔ (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn (1...𝑁)))
385366, 384mpbid 235 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn (1...𝑁))
386385adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn (1...𝑁))
387 fzfid 13529 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → (1...𝑁) ∈ Fin)
388 eqidd 2735 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) = (𝑇‘𝑛))
389 fvun1 6791 . . . . . . . . . . . . . . . . . . . 20 ((((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1))) ∧ ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁)) ∧ (((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛))
390354, 356, 389mp3an12 1453 . . . . . . . . . . . . . . . . . . 19 ((((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛))
391364, 390sylan 583 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛))
39269fvconst2 7008 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) → (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛) = 1)
393392adantl 485 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛) = 1)
394391, 393eqtrd 2774 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 1)
395394adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 1)
396352, 386, 387, 387, 111, 388, 395ofval 7468 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1))
397108adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁))
398 fzss2 13135 . . . . . . . . . . . . . . . . . . . . 21 (𝑉 ∈ (ℤ≥‘(𝑉 − 1)) → (1...(𝑉 − 1)) ⊆ (1...𝑉))
399313, 398syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1...(𝑉 − 1)) ⊆ (1...𝑉))
400 imass2 5959 . . . . . . . . . . . . . . . . . . . 20 ((1...(𝑉 − 1)) ⊆ (1...𝑉) → (𝑈 “ (1...(𝑉 − 1))) ⊆ (𝑈 “ (1...𝑉)))
401399, 400syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑈 “ (1...(𝑉 − 1))) ⊆ (𝑈 “ (1...𝑉)))
402401sselda 3891 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → 𝑛 ∈ (𝑈 “ (1...𝑉)))
403402, 118syldan 594 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 1)
404403adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 1)
405352, 397, 387, 387, 111, 388, 404ofval 7468 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1))
406396, 405eqtr4d 2777 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
407351, 406mpdan 687 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
408 imassrn 5929 . . . . . . . . . . . . . . . 16 (𝑈 “ ((𝑉 + 1)...𝑁)) ⊆ ran 𝑈
409408, 63sstrid 3902 . . . . . . . . . . . . . . 15 (𝜑 → (𝑈 “ ((𝑉 + 1)...𝑁)) ⊆ (1...𝑁))
410409sselda 3891 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → 𝑛 ∈ (1...𝑁))
41167adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → 𝑇 Fn (1...𝑁))
412385adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn (1...𝑁))
413 fzfid 13529 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → (1...𝑁) ∈ Fin)
414 eqidd 2735 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) = (𝑇‘𝑛))
415 fzss1 13134 . . . . . . . . . . . . . . . . . . . . 21 ((𝑉 + 1) ∈ (ℤ≥‘𝑉) → ((𝑉 + 1)...𝑁) ⊆ (𝑉...𝑁))
416145, 415syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑉 + 1)...𝑁) ⊆ (𝑉...𝑁))
417 imass2 5959 . . . . . . . . . . . . . . . . . . . 20 (((𝑉 + 1)...𝑁) ⊆ (𝑉...𝑁) → (𝑈 “ ((𝑉 + 1)...𝑁)) ⊆ (𝑈 “ (𝑉...𝑁)))
418416, 417syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑈 “ ((𝑉 + 1)...𝑁)) ⊆ (𝑈 “ (𝑉...𝑁)))
419418sselda 3891 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → 𝑛 ∈ (𝑈 “ (𝑉...𝑁)))
420 fvun2 6792 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1))) ∧ ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁)) ∧ (((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (𝑉...𝑁)))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛))
421354, 356, 420mp3an12 1453 . . . . . . . . . . . . . . . . . . . 20 ((((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (𝑉...𝑁))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛))
422364, 421sylan 583 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑉...𝑁))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛))
42372fvconst2 7008 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (𝑈 “ (𝑉...𝑁)) → (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛) = 0)
424423adantl 485 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑉...𝑁))) → (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛) = 0)
425422, 424eqtrd 2774 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑉...𝑁))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 0)
426419, 425syldan 594 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 0)
427426adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 0)
428411, 412, 413, 413, 111, 414, 427ofval 7468 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0))
429108adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁))
430183adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 0)
431411, 429, 413, 413, 111, 414, 430ofval 7468 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0))
432428, 431eqtr4d 2777 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
433410, 432mpdan 687 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
434407, 433jaodan 958 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
435434adantlr 715 . . . . . . . . . . 11 (((𝜑 ∧ 𝑉 < 𝑀) ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
436200adantr 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑉 < 𝑀) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))))
437204a1i 11 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V)
438214adantlr 715 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉))
439 lttr 10892 . . . . . . . . . . . . . . . . . . . . 21 (((𝑉 − 1) ∈ ℝ ∧ 𝑉 ∈ ℝ ∧ 𝑀 ∈ ℝ) → (((𝑉 − 1) < 𝑉 ∧ 𝑉 < 𝑀) → (𝑉 − 1) < 𝑀))
440224, 27, 221, 439syl3anc 1373 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝑉 − 1) < 𝑉 ∧ 𝑉 < 𝑀) → (𝑉 − 1) < 𝑀))
441324, 440mpand 695 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑉 < 𝑀 → (𝑉 − 1) < 𝑀))
442441imp 410 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑉 < 𝑀) → (𝑉 − 1) < 𝑀)
443442iftrued 4437 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑉 < 𝑀) → if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉) = (𝑉 − 1))
444443adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉) = (𝑉 − 1))
445438, 444eqtrd 2774 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = (𝑉 − 1))
446 simpll 767 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → 𝜑)
447 oveq2 7210 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = (𝑉 − 1) → (1...𝑗) = (1...(𝑉 − 1)))
448447imaeq2d 5918 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = (𝑉 − 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑉 − 1))))
449448xpeq1d 5569 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑉 − 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑉 − 1))) × {1}))
450449adantl 485 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑉 − 1))) × {1}))
451 oveq1 7209 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = (𝑉 − 1) → (𝑗 + 1) = ((𝑉 − 1) + 1))
452451, 212sylan9eqr 2796 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → (𝑗 + 1) = 𝑉)
453452oveq1d 7217 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → ((𝑗 + 1)...𝑁) = (𝑉...𝑁))
454453imaeq2d 5918 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (𝑉...𝑁)))
455454xpeq1d 5569 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (𝑉...𝑁)) × {0}))
456450, 455uneq12d 4068 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))
457456oveq2d 7218 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → (𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))))
458446, 457sylan 583 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) ∧ 𝑗 = (𝑉 − 1)) → (𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))))
459437, 445, 458csbied2 3842 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))))
460246adantr 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑉 < 𝑀) → (𝑉 − 1) ∈ (0...(𝑁 − 1)))
461 ovexd 7237 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑉 < 𝑀) → (𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))) ∈ V)
462436, 459, 460, 461fvmptd 6814 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑉 < 𝑀) → (𝐹‘(𝑉 − 1)) = (𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))))
463462fveq1d 6708 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑉 < 𝑀) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛))
464463adantr 484 . . . . . . . . . . 11 (((𝜑 ∧ 𝑉 < 𝑀) ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛))
465204a1i 11 . . . . . . . . . . . . . . . 16 ((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V)
466 iftrue 4435 . . . . . . . . . . . . . . . . . . . 20 (𝑉 < 𝑀 → if(𝑉 < 𝑀, 𝑉, (𝑉 + 1)) = 𝑉)
467256, 466sylan9eqr 2796 . . . . . . . . . . . . . . . . . . 19 ((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = 𝑉)
468467eqeq2d 2745 . . . . . . . . . . . . . . . . . 18 ((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) → (𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ↔ 𝑗 = 𝑉))
469468biimpa 480 . . . . . . . . . . . . . . . . 17 (((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → 𝑗 = 𝑉)
470469, 241syl 17 . . . . . . . . . . . . . . . 16 (((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → (𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
471465, 470csbied 3840 . . . . . . . . . . . . . . 15 ((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
472471adantll 714 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = 𝑉) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
473276adantr 484 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑉 < 𝑀) → 𝑉 ∈ (0...(𝑁 − 1)))
474 ovexd 7237 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑉 < 𝑀) → (𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))) ∈ V)
475436, 472, 473, 474fvmptd 6814 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑉 < 𝑀) → (𝐹‘𝑉) = (𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
476475fveq1d 6708 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑉 < 𝑀) → ((𝐹‘𝑉)‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
477476adantr 484 . . . . . . . . . . 11 (((𝜑 ∧ 𝑉 < 𝑀) ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝐹‘𝑉)‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
478435, 464, 4773eqtr4d 2784 . . . . . . . . . 10 (((𝜑 ∧ 𝑉 < 𝑀) ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛))
479478ex 416 . . . . . . . . 9 ((𝜑 ∧ 𝑉 < 𝑀) → ((𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛)))
480348, 479sylbid 243 . . . . . . . 8 ((𝜑 ∧ 𝑉 < 𝑀) → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {𝑉})) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛)))
481480expdimp 456 . . . . . . 7 (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (¬ 𝑛 ∈ (𝑈 “ {𝑉}) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛)))
482481necon1ad 2952 . . . . . 6 (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 ∈ (𝑈 “ {𝑉})))
483 elimasni 5948 . . . . . . . 8 (𝑛 ∈ (𝑈 “ {𝑉}) → 𝑉𝑈𝑛)
484 eqcom 2741 . . . . . . . . 9 (𝑛 = (𝑈‘𝑉) ↔ (𝑈‘𝑉) = 𝑛)
485 fnbrfvb 6754 . . . . . . . . . 10 ((𝑈 Fn (1...𝑁) ∧ 𝑉 ∈ (1...𝑁)) → ((𝑈‘𝑉) = 𝑛 ↔ 𝑉𝑈𝑛))
486290, 97, 485syl2anc 587 . . . . . . . . 9 (𝜑 → ((𝑈‘𝑉) = 𝑛 ↔ 𝑉𝑈𝑛))
487484, 486syl5bb 286 . . . . . . . 8 (𝜑 → (𝑛 = (𝑈‘𝑉) ↔ 𝑉𝑈𝑛))
488483, 487syl5ibr 249 . . . . . . 7 (𝜑 → (𝑛 ∈ (𝑈 “ {𝑉}) → 𝑛 = (𝑈‘𝑉)))
489488ad2antrr 726 . . . . . 6 (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (𝑛 ∈ (𝑈 “ {𝑉}) → 𝑛 = (𝑈‘𝑉)))
490482, 489syld 47 . . . . 5 (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘𝑉)))
491490ralrimiva 3098 . . . 4 ((𝜑 ∧ 𝑉 < 𝑀) → ∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘𝑉)))
492 fvex 6719 . . . . 5 (𝑈‘𝑉) ∈ V
493 eqeq2 2746 . . . . . . 7 (𝑚 = (𝑈‘𝑉) → (𝑛 = 𝑚 ↔ 𝑛 = (𝑈‘𝑉)))
494493imbi2d 344 . . . . . 6 (𝑚 = (𝑈‘𝑉) → ((((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘𝑉))))
495494ralbidv 3111 . . . . 5 (𝑚 = (𝑈‘𝑉) → (∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ ∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘𝑉))))
496492, 495spcev 3514 . . . 4 (∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘𝑉)) → ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚))
497491, 496syl 17 . . 3 ((𝜑 ∧ 𝑉 < 𝑀) → ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚))
498 eldifsni 4693 . . . . 5 (𝑀 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑀 ≠ 𝑉)
499216, 498syl 17 . . . 4 (𝜑 → 𝑀 ≠ 𝑉)
500221, 27lttri2d 10954 . . . 4 (𝜑 → (𝑀 ≠ 𝑉 ↔ (𝑀 < 𝑉 ∨ 𝑉 < 𝑀)))
501499, 500mpbid 235 . . 3 (𝜑 → (𝑀 < 𝑉 ∨ 𝑉 < 𝑀))
502303, 497, 501mpjaodan 959 . 2 (𝜑 → ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚))
503 nfv 1922 . . . 4 Ⅎ𝑚((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛)
504503rmo2 3790 . . 3 (∃*𝑛 ∈ (𝑈 “ (1...𝑁))((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) ↔ ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚))
505 rmoeq1 3315 . . . 4 ((𝑈 “ (1...𝑁)) = (1...𝑁) → (∃*𝑛 ∈ (𝑈 “ (1...𝑁))((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) ↔ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛)))
506104, 505syl 17 . . 3 (𝜑 → (∃*𝑛 ∈ (𝑈 “ (1...𝑁))((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) ↔ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛)))
507504, 506bitr3id 288 . 2 (𝜑 → (∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛)))
508502, 507mpbid 235 1 (𝜑 → ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 847   = wceq 1543  ∃wex 1787   ∈ wcel 2110   ≠ wne 2935  ∀wral 3054  ∃*wrmo 3057  Vcvv 3401  ⦋csb 3802   ∖ cdif 3854   ∪ cun 3855   ∩ cin 3856   ⊆ wss 3857  ∅c0 4227  ifcif 4429  {csn 4531   class class class wbr 5043   ↦ cmpt 5124   × cxp 5538  ◡ccnv 5539  ran crn 5541   “ cima 5543  Fun wfun 6363   Fn wfn 6364  ⟶wf 6365  –onto→wfo 6367  –1-1-onto→wf1o 6368  ‘cfv 6369  (class class class)co 7202   ∘f cof 7456  Fincfn 8615  ℂcc 10710  ℝcr 10711  0cc0 10712  1c1 10713   + caddc 10715   < clt 10850   ≤ cle 10851   − cmin 11045  ℕcn 11813  ℤcz 12159  ℤ≥cuz 12421  ...cfz 13078
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2706  ax-rep 5168  ax-sep 5181  ax-nul 5188  ax-pow 5247  ax-pr 5311  ax-un 7512  ax-cnex 10768  ax-resscn 10769  ax-1cn 10770  ax-icn 10771  ax-addcl 10772  ax-addrcl 10773  ax-mulcl 10774  ax-mulrcl 10775  ax-mulcom 10776  ax-addass 10777  ax-mulass 10778  ax-distr 10779  ax-i2m1 10780  ax-1ne0 10781  ax-1rid 10782  ax-rnegex 10783  ax-rrecex 10784  ax-cnre 10785  ax-pre-lttri 10786  ax-pre-lttrn 10787  ax-pre-ltadd 10788  ax-pre-mulgt0 10789
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2537  df-eu 2566  df-clab 2713  df-cleq 2726  df-clel 2812  df-nfc 2882  df-ne 2936  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3403  df-sbc 3688  df-csb 3803  df-dif 3860  df-un 3862  df-in 3864  df-ss 3874  df-pss 3876  df-nul 4228  df-if 4430  df-pw 4505  df-sn 4532  df-pr 4534  df-tp 4536  df-op 4538  df-uni 4810  df-iun 4896  df-br 5044  df-opab 5106  df-mpt 5125  df-tr 5151  df-id 5444  df-eprel 5449  df-po 5457  df-so 5458  df-fr 5498  df-we 5500  df-xp 5546  df-rel 5547  df-cnv 5548  df-co 5549  df-dm 5550  df-rn 5551  df-res 5552  df-ima 5553  df-pred 6149  df-ord 6205  df-on 6206  df-lim 6207  df-suc 6208  df-iota 6327  df-fun 6371  df-fn 6372  df-f 6373  df-f1 6374  df-fo 6375  df-f1o 6376  df-fv 6377  df-riota 7159  df-ov 7205  df-oprab 7206  df-mpo 7207  df-of 7458  df-om 7634  df-1st 7750  df-2nd 7751  df-wrecs 8036  df-recs 8097  df-rdg 8135  df-1o 8191  df-er 8380  df-en 8616  df-dom 8617  df-sdom 8618  df-fin 8619  df-pnf 10852  df-mnf 10853  df-xr 10854  df-ltxr 10855  df-le 10856  df-sub 11047  df-neg 11048  df-nn 11814  df-n0 12074  df-z 12160  df-uz 12422  df-fz 13079
This theorem is referenced by:  poimirlem8  35479  poimirlem18  35489  poimirlem21  35492  poimirlem22  35493
  Copyright terms: Public domain W3C validator