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 38198
Description: Lemma for poimir 38229- 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 6830 . . . . . . . . . . . . . . . . 17 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (𝑈:(1...𝑁)–onto→(1...𝑁) ∧ Fun ◡𝑈))
32simprbi 502 . . . . . . . . . . . . . . . 16 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → Fun ◡𝑈)
41, 3syl 18 . . . . . . . . . . . . . . 15 (𝜑 → Fun ◡𝑈)
5 imadif 6623 . . . . . . . . . . . . . . 15 (Fun ◡𝑈 → (𝑈 “ ((1...𝑁) ∖ {(𝑉 + 1)})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})))
64, 5syl 18 . . . . . . . . . . . . . 14 (𝜑 → (𝑈 “ ((1...𝑁) ∖ {(𝑉 + 1)})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})))
7 poimirlem2.4 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 𝑉 ∈ (1...(𝑁 − 1)))
8 fzp1elp1 13607 . . . . . . . . . . . . . . . . . . . 20 (𝑉 ∈ (1...(𝑁 − 1)) → (𝑉 + 1) ∈ (1...((𝑁 − 1) + 1)))
97, 8syl 18 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑉 + 1) ∈ (1...((𝑁 − 1) + 1)))
10 poimir.0 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 𝑁 ∈ ℕ)
1110nncnd 12251 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 𝑁 ∈ ℂ)
12 npcan1 11641 . . . . . . . . . . . . . . . . . . . . 21 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
1311, 12syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
1413oveq2d 7429 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁))
159, 14eleqtrd 2871 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑉 + 1) ∈ (1...𝑁))
16 fzsplit 13580 . . . . . . . . . . . . . . . . . 18 ((𝑉 + 1) ∈ (1...𝑁) → (1...𝑁) = ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁)))
1715, 16syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → (1...𝑁) = ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁)))
1817difeq1d 4088 . . . . . . . . . . . . . . . 16 (𝜑 → ((1...𝑁) ∖ {(𝑉 + 1)}) = (((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁)) ∖ {(𝑉 + 1)}))
19 difundir 4252 . . . . . . . . . . . . . . . . 17 (((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁)) ∖ {(𝑉 + 1)}) = (((1...(𝑉 + 1)) ∖ {(𝑉 + 1)}) ∪ ((((𝑉 + 1) + 1)...𝑁) ∖ {(𝑉 + 1)}))
20 elfzuz 13550 . . . . . . . . . . . . . . . . . . . . . 22 (𝑉 ∈ (1...(𝑁 − 1)) → 𝑉 ∈ (ℤ≥‘1))
217, 20syl 18 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 𝑉 ∈ (ℤ≥‘1))
22 fzsuc 13601 . . . . . . . . . . . . . . . . . . . . 21 (𝑉 ∈ (ℤ≥‘1) → (1...(𝑉 + 1)) = ((1...𝑉) ∪ {(𝑉 + 1)}))
2321, 22syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1...(𝑉 + 1)) = ((1...𝑉) ∪ {(𝑉 + 1)}))
2423difeq1d 4088 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((1...(𝑉 + 1)) ∖ {(𝑉 + 1)}) = (((1...𝑉) ∪ {(𝑉 + 1)}) ∖ {(𝑉 + 1)}))
25 difun2 4447 . . . . . . . . . . . . . . . . . . . 20 (((1...𝑉) ∪ {(𝑉 + 1)}) ∖ {(𝑉 + 1)}) = ((1...𝑉) ∖ {(𝑉 + 1)})
267elfzelzd 13555 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → 𝑉 ∈ ℤ)
2726zred 12702 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 𝑉 ∈ ℝ)
2827ltp1d 12147 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 𝑉 < (𝑉 + 1))
2926peano2zd 12705 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑉 + 1) ∈ ℤ)
3029zred 12702 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑉 + 1) ∈ ℝ)
3127, 30ltnled 11359 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑉 < (𝑉 + 1) ↔ ¬ (𝑉 + 1) ≤ 𝑉))
3228, 31mpbid 235 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ¬ (𝑉 + 1) ≤ 𝑉)
33 elfzle2 13558 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑉 + 1) ∈ (1...𝑉) → (𝑉 + 1) ≤ 𝑉)
3432, 33nsyl 141 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ¬ (𝑉 + 1) ∈ (1...𝑉))
35 difsn 4770 . . . . . . . . . . . . . . . . . . . . 21 (¬ (𝑉 + 1) ∈ (1...𝑉) → ((1...𝑉) ∖ {(𝑉 + 1)}) = (1...𝑉))
3634, 35syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((1...𝑉) ∖ {(𝑉 + 1)}) = (1...𝑉))
3725, 36eqtrid 2816 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((1...𝑉) ∪ {(𝑉 + 1)}) ∖ {(𝑉 + 1)}) = (1...𝑉))
3824, 37eqtrd 2804 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((1...(𝑉 + 1)) ∖ {(𝑉 + 1)}) = (1...𝑉))
3930ltp1d 12147 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑉 + 1) < ((𝑉 + 1) + 1))
40 peano2re 11385 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑉 + 1) ∈ ℝ → ((𝑉 + 1) + 1) ∈ ℝ)
4130, 40syl 18 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝑉 + 1) + 1) ∈ ℝ)
4230, 41ltnled 11359 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑉 + 1) < ((𝑉 + 1) + 1) ↔ ¬ ((𝑉 + 1) + 1) ≤ (𝑉 + 1)))
4339, 42mpbid 235 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ¬ ((𝑉 + 1) + 1) ≤ (𝑉 + 1))
44 elfzle1 13557 . . . . . . . . . . . . . . . . . . . 20 ((𝑉 + 1) ∈ (((𝑉 + 1) + 1)...𝑁) → ((𝑉 + 1) + 1) ≤ (𝑉 + 1))
4543, 44nsyl 141 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ¬ (𝑉 + 1) ∈ (((𝑉 + 1) + 1)...𝑁))
46 difsn 4770 . . . . . . . . . . . . . . . . . . 19 (¬ (𝑉 + 1) ∈ (((𝑉 + 1) + 1)...𝑁) → ((((𝑉 + 1) + 1)...𝑁) ∖ {(𝑉 + 1)}) = (((𝑉 + 1) + 1)...𝑁))
4745, 46syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((((𝑉 + 1) + 1)...𝑁) ∖ {(𝑉 + 1)}) = (((𝑉 + 1) + 1)...𝑁))
4838, 47uneq12d 4131 . . . . . . . . . . . . . . . . 17 (𝜑 → (((1...(𝑉 + 1)) ∖ {(𝑉 + 1)}) ∪ ((((𝑉 + 1) + 1)...𝑁) ∖ {(𝑉 + 1)})) = ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁)))
4919, 48eqtrid 2816 . . . . . . . . . . . . . . . 16 (𝜑 → (((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁)) ∖ {(𝑉 + 1)}) = ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁)))
5018, 49eqtrd 2804 . . . . . . . . . . . . . . 15 (𝜑 → ((1...𝑁) ∖ {(𝑉 + 1)}) = ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁)))
5150imaeq2d 6065 . . . . . . . . . . . . . 14 (𝜑 → (𝑈 “ ((1...𝑁) ∖ {(𝑉 + 1)})) = (𝑈 “ ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁))))
526, 51eqtr3d 2806 . . . . . . . . . . . . 13 (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})) = (𝑈 “ ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁))))
53 imaundi 6150 . . . . . . . . . . . . 13 (𝑈 “ ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁))) = ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))
5452, 53eqtrdi 2820 . . . . . . . . . . . 12 (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})) = ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))))
5554eleq2d 2855 . . . . . . . . . . 11 (𝜑 → (𝑛 ∈ ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})) ↔ 𝑛 ∈ ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))))
56 eldif 3923 . . . . . . . . . . 11 (𝑛 ∈ ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})) ↔ (𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)})))
57 elun 4115 . . . . . . . . . . 11 (𝑛 ∈ ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ↔ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))))
5855, 56, 573bitr3g 316 . . . . . . . . . 10 (𝜑 → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)})) ↔ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))))
5958adantr 485 . . . . . . . . 9 ((𝜑 ∧ 𝑀 < 𝑉) → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)})) ↔ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))))
60 imassrn 6076 . . . . . . . . . . . . . . . 16 (𝑈 “ (1...𝑉)) ⊆ ran 𝑈
61 f1of 6823 . . . . . . . . . . . . . . . . . 18 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)⟶(1...𝑁))
621, 61syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → 𝑈:(1...𝑁)⟶(1...𝑁))
6362frnd 6717 . . . . . . . . . . . . . . . 16 (𝜑 → ran 𝑈 ⊆ (1...𝑁))
6460, 63sstrid 3956 . . . . . . . . . . . . . . 15 (𝜑 → (𝑈 “ (1...𝑉)) ⊆ (1...𝑁))
6564sselda 3945 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → 𝑛 ∈ (1...𝑁))
66 poimirlem2.2 . . . . . . . . . . . . . . . . . 18 (𝜑 → 𝑇:(1...𝑁)⟶ℤ)
6766ffnd 6709 . . . . . . . . . . . . . . . . 17 (𝜑 → 𝑇 Fn (1...𝑁))
6867adantr 485 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → 𝑇 Fn (1...𝑁))
69 1ex 11205 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ V
70 fnconstg 6769 . . . . . . . . . . . . . . . . . . . . 21 (1 ∈ V → ((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉)))
7169, 70ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉))
72 c0ex 11202 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ V
73 fnconstg 6769 . . . . . . . . . . . . . . . . . . . . 21 (0 ∈ V → ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁)))
7472, 73ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁))
7571, 74pm3.2i 475 . . . . . . . . . . . . . . . . . . 19 (((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉)) ∧ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁)))
76 imain 6624 . . . . . . . . . . . . . . . . . . . . 21 (Fun ◡𝑈 → (𝑈 “ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = ((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))))
774, 76syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = ((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))))
78 fzdisj 13581 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑉 < (𝑉 + 1) → ((1...𝑉) ∩ ((𝑉 + 1)...𝑁)) = ∅)
7928, 78syl 18 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1...𝑉) ∩ ((𝑉 + 1)...𝑁)) = ∅)
8079imaeq2d 6065 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = (𝑈 “ ∅))
81 ima0 6082 . . . . . . . . . . . . . . . . . . . . 21 (𝑈 “ ∅) = ∅
8280, 81eqtrdi 2820 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = ∅)
8377, 82eqtr3d 2806 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅)
84 fnun 6652 . . . . . . . . . . . . . . . . . . 19 (((((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉)) ∧ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ ((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))))
8575, 83, 84sylancr 598 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))))
86 imaundi 6150 . . . . . . . . . . . . . . . . . . . 20 (𝑈 “ ((1...𝑉) ∪ ((𝑉 + 1)...𝑁))) = ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁)))
8710nnzd 12619 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → 𝑁 ∈ ℤ)
88 peano2zm 12639 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
89 uzid 12879 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ≥‘(𝑁 − 1)))
90 peano2uz 12927 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑁 − 1) ∈ (ℤ≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ≥‘(𝑁 − 1)))
9187, 88, 89, 904syl 20 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ≥‘(𝑁 − 1)))
9213, 91eqeltrrd 2870 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑁 − 1)))
93 fzss2 13594 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ (ℤ≥‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
9492, 93syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
9594, 7sseldd 3946 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 𝑉 ∈ (1...𝑁))
96 fzsplit 13580 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑉 ∈ (1...𝑁) → (1...𝑁) = ((1...𝑉) ∪ ((𝑉 + 1)...𝑁)))
9795, 96syl 18 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (1...𝑁) = ((1...𝑉) ∪ ((𝑉 + 1)...𝑁)))
9897imaeq2d 6065 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...𝑉) ∪ ((𝑉 + 1)...𝑁))))
99 f1ofo 6831 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–onto→(1...𝑁))
1001, 99syl 18 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 𝑈:(1...𝑁)–onto→(1...𝑁))
101 foima 6800 . . . . . . . . . . . . . . . . . . . . . 22 (𝑈:(1...𝑁)–onto→(1...𝑁) → (𝑈 “ (1...𝑁)) = (1...𝑁))
102100, 101syl 18 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ (1...𝑁)) = (1...𝑁))
10398, 102eqtr3d 2806 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...𝑉) ∪ ((𝑉 + 1)...𝑁))) = (1...𝑁))
10486, 103eqtr3id 2818 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))) = (1...𝑁))
105104fneq2d 6632 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))) ↔ (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁)))
10685, 105mpbid 235 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁))
107106adantr 485 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁))
108 fzfid 14011 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → (1...𝑁) ∈ Fin)
109 inidm 4187 . . . . . . . . . . . . . . . 16 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
110 eqidd 2770 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) = (𝑇‘𝑛))
111 fvun1 6975 . . . . . . . . . . . . . . . . . . . 20 ((((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉)) ∧ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁)) ∧ (((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...𝑉)))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...𝑉)) × {1})‘𝑛))
11271, 74, 111mp3an12 1477 . . . . . . . . . . . . . . . . . . 19 ((((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...𝑉)) × {1})‘𝑛))
11383, 112sylan 591 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...𝑉)) × {1})‘𝑛))
11469fvconst2 7205 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (𝑈 “ (1...𝑉)) → (((𝑈 “ (1...𝑉)) × {1})‘𝑛) = 1)
115114adantl 486 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → (((𝑈 “ (1...𝑉)) × {1})‘𝑛) = 1)
116113, 115eqtrd 2804 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 1)
117116adantr 485 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 1)
11868, 107, 108, 108, 109, 110, 117ofval 7688 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1))
119 fnconstg 6769 . . . . . . . . . . . . . . . . . . . . 21 (1 ∈ V → ((𝑈 “ (1...(𝑉 + 1))) × {1}) Fn (𝑈 “ (1...(𝑉 + 1))))
12069, 119ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 “ (1...(𝑉 + 1))) × {1}) Fn (𝑈 “ (1...(𝑉 + 1)))
121 fnconstg 6769 . . . . . . . . . . . . . . . . . . . . 21 (0 ∈ V → ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))
12272, 121ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑉 + 1) + 1)...𝑁))
123120, 122pm3.2i 475 . . . . . . . . . . . . . . . . . . 19 (((𝑈 “ (1...(𝑉 + 1))) × {1}) Fn (𝑈 “ (1...(𝑉 + 1))) ∧ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))
124 imain 6624 . . . . . . . . . . . . . . . . . . . . 21 (Fun ◡𝑈 → (𝑈 “ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))))
1254, 124syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))))
126 fzdisj 13581 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑉 + 1) < ((𝑉 + 1) + 1) → ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁)) = ∅)
12739, 126syl 18 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁)) = ∅)
128127imaeq2d 6065 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = (𝑈 “ ∅))
129128, 81eqtrdi 2820 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = ∅)
130125, 129eqtr3d 2806 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = ∅)
131 fnun 6652 . . . . . . . . . . . . . . . . . . 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)...𝑁))))
132123, 130, 131sylancr 598 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 + 1))) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))))
133 imaundi 6150 . . . . . . . . . . . . . . . . . . . 20 (𝑈 “ ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑉 + 1))) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))
13417imaeq2d 6065 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁))))
135134, 102eqtr3d 2806 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁))) = (1...𝑁))
136133, 135eqtr3id 2818 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑈 “ (1...(𝑉 + 1))) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = (1...𝑁))
137136fneq2d 6632 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 + 1))) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ↔ (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁)))
138132, 137mpbid 235 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁))
139138adantr 485 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁))
140 uzid 12879 . . . . . . . . . . . . . . . . . . . . 21 (𝑉 ∈ ℤ → 𝑉 ∈ (ℤ≥‘𝑉))
14126, 140syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 𝑉 ∈ (ℤ≥‘𝑉))
142 peano2uz 12927 . . . . . . . . . . . . . . . . . . . 20 (𝑉 ∈ (ℤ≥‘𝑉) → (𝑉 + 1) ∈ (ℤ≥‘𝑉))
143 fzss2 13594 . . . . . . . . . . . . . . . . . . . 20 ((𝑉 + 1) ∈ (ℤ≥‘𝑉) → (1...𝑉) ⊆ (1...(𝑉 + 1)))
144 imass2 6107 . . . . . . . . . . . . . . . . . . . 20 ((1...𝑉) ⊆ (1...(𝑉 + 1)) → (𝑈 “ (1...𝑉)) ⊆ (𝑈 “ (1...(𝑉 + 1))))
145141, 142, 143, 1444syl 20 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑈 “ (1...𝑉)) ⊆ (𝑈 “ (1...(𝑉 + 1))))
146145sselda 3945 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1))))
147 fvun1 6975 . . . . . . . . . . . . . . . . . . . . 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})‘𝑛))
148120, 122, 147mp3an12 1477 . . . . . . . . . . . . . . . . . . . 20 ((((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1)))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 + 1))) × {1})‘𝑛))
149130, 148sylan 591 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1)))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 + 1))) × {1})‘𝑛))
15069fvconst2 7205 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (𝑈 “ (1...(𝑉 + 1))) → (((𝑈 “ (1...(𝑉 + 1))) × {1})‘𝑛) = 1)
151150adantl 486 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1)))) → (((𝑈 “ (1...(𝑉 + 1))) × {1})‘𝑛) = 1)
152149, 151eqtrd 2804 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1)))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 1)
153146, 152syldan 602 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 1)
154153adantr 485 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 1)
15568, 139, 108, 108, 109, 110, 154ofval 7688 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1))
156118, 155eqtr4d 2807 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
15765, 156mpdan 699 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
158 imassrn 6076 . . . . . . . . . . . . . . . 16 (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ⊆ ran 𝑈
159158, 63sstrid 3956 . . . . . . . . . . . . . . 15 (𝜑 → (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ⊆ (1...𝑁))
160159sselda 3945 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → 𝑛 ∈ (1...𝑁))
16167adantr 485 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → 𝑇 Fn (1...𝑁))
162106adantr 485 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁))
163 fzfid 14011 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → (1...𝑁) ∈ Fin)
164 eqidd 2770 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) = (𝑇‘𝑛))
165 uzid 12879 . . . . . . . . . . . . . . . . . . . . 21 ((𝑉 + 1) ∈ ℤ → (𝑉 + 1) ∈ (ℤ≥‘(𝑉 + 1)))
16629, 165syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑉 + 1) ∈ (ℤ≥‘(𝑉 + 1)))
167 peano2uz 12927 . . . . . . . . . . . . . . . . . . . 20 ((𝑉 + 1) ∈ (ℤ≥‘(𝑉 + 1)) → ((𝑉 + 1) + 1) ∈ (ℤ≥‘(𝑉 + 1)))
168 fzss1 13593 . . . . . . . . . . . . . . . . . . . 20 (((𝑉 + 1) + 1) ∈ (ℤ≥‘(𝑉 + 1)) → (((𝑉 + 1) + 1)...𝑁) ⊆ ((𝑉 + 1)...𝑁))
169 imass2 6107 . . . . . . . . . . . . . . . . . . . 20 ((((𝑉 + 1) + 1)...𝑁) ⊆ ((𝑉 + 1)...𝑁) → (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ⊆ (𝑈 “ ((𝑉 + 1)...𝑁)))
170166, 167, 168, 1694syl 20 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ⊆ (𝑈 “ ((𝑉 + 1)...𝑁)))
171170sselda 3945 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))
172 fvun2 6976 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉)) ∧ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁)) ∧ (((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛))
17371, 74, 172mp3an12 1477 . . . . . . . . . . . . . . . . . . . 20 ((((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛))
17483, 173sylan 591 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛))
17572fvconst2 7205 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)) → (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛) = 0)
176175adantl 486 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛) = 0)
177174, 176eqtrd 2804 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 0)
178171, 177syldan 602 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 0)
179178adantr 485 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 0)
180161, 162, 163, 163, 109, 164, 179ofval 7688 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0))
181138adantr 485 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁))
182 fvun2 6976 . . . . . . . . . . . . . . . . . . . 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})‘𝑛))
183120, 122, 182mp3an12 1477 . . . . . . . . . . . . . . . . . . 19 ((((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})‘𝑛))
184130, 183sylan 591 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})‘𝑛))
18572fvconst2 7205 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) → (((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})‘𝑛) = 0)
186185adantl 486 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → (((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})‘𝑛) = 0)
187184, 186eqtrd 2804 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 0)
188187adantr 485 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 0)
189161, 181, 163, 163, 109, 164, 188ofval 7688 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0))
190180, 189eqtr4d 2807 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
191160, 190mpdan 699 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
192157, 191jaodan 972 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
193192adantlr 727 . . . . . . . . . . 11 (((𝜑 ∧ 𝑀 < 𝑉) ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
194 poimirlem2.1 . . . . . . . . . . . . . . 15 (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))))
195194adantr 485 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑀 < 𝑉) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))))
196 vex 3467 . . . . . . . . . . . . . . . . 17 𝑦 ∈ V
197 ovex 7446 . . . . . . . . . . . . . . . . 17 (𝑦 + 1) ∈ V
198196, 197ifex 4543 . . . . . . . . . . . . . . . 16 if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V
199198a1i 11 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V)
200 breq1 5116 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (𝑉 − 1) → (𝑦 < 𝑀 ↔ (𝑉 − 1) < 𝑀))
201200adantl 486 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑦 = (𝑉 − 1)) → (𝑦 < 𝑀 ↔ (𝑉 − 1) < 𝑀))
202 simpr 489 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑦 = (𝑉 − 1)) → 𝑦 = (𝑉 − 1))
203 oveq1 7420 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = (𝑉 − 1) → (𝑦 + 1) = ((𝑉 − 1) + 1))
20426zcnd 12703 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 𝑉 ∈ ℂ)
205 npcan1 11641 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑉 ∈ ℂ → ((𝑉 − 1) + 1) = 𝑉)
206204, 205syl 18 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝑉 − 1) + 1) = 𝑉)
207203, 206sylan9eqr 2826 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑦 = (𝑉 − 1)) → (𝑦 + 1) = 𝑉)
208201, 202, 207ifbieq12d 4521 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉))
209208adantlr 727 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉))
210 poimirlem2.5 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → 𝑀 ∈ ((0...𝑁) ∖ {𝑉}))
211210eldifad 3925 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → 𝑀 ∈ (0...𝑁))
212211elfzelzd 13555 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 𝑀 ∈ ℤ)
213 zltlem1 12649 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑀 ∈ ℤ ∧ 𝑉 ∈ ℤ) → (𝑀 < 𝑉 ↔ 𝑀 ≤ (𝑉 − 1)))
214212, 26, 213syl2anc 595 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑀 < 𝑉 ↔ 𝑀 ≤ (𝑉 − 1)))
215212zred 12702 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 𝑀 ∈ ℝ)
216 peano2zm 12639 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑉 ∈ ℤ → (𝑉 − 1) ∈ ℤ)
21726, 216syl 18 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝑉 − 1) ∈ ℤ)
218217zred 12702 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑉 − 1) ∈ ℝ)
219215, 218lenltd 11358 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑀 ≤ (𝑉 − 1) ↔ ¬ (𝑉 − 1) < 𝑀))
220214, 219bitrd 282 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑀 < 𝑉 ↔ ¬ (𝑉 − 1) < 𝑀))
221220biimpa 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑀 < 𝑉) → ¬ (𝑉 − 1) < 𝑀)
222221iffalsed 4503 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑀 < 𝑉) → if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉) = 𝑉)
223222adantr 485 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉) = 𝑉)
224209, 223eqtrd 2804 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = 𝑉)
225224eqeq2d 2780 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → (𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ↔ 𝑗 = 𝑉))
226225biimpa 481 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → 𝑗 = 𝑉)
227 oveq2 7421 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑉 → (1...𝑗) = (1...𝑉))
228227imaeq2d 6065 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑉 → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...𝑉)))
229228xpeq1d 5693 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑉 → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...𝑉)) × {1}))
230 oveq1 7420 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑉 → (𝑗 + 1) = (𝑉 + 1))
231230oveq1d 7428 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑉 → ((𝑗 + 1)...𝑁) = ((𝑉 + 1)...𝑁))
232231imaeq2d 6065 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑉 → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ ((𝑉 + 1)...𝑁)))
233232xpeq1d 5693 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑉 → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))
234229, 233uneq12d 4131 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑉 → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))
235234oveq2d 7429 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑉 → (𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
236226, 235syl 18 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → (𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
237199, 236csbied 3897 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
238 elfzm1b 13632 . . . . . . . . . . . . . . . . 17 ((𝑉 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑉 ∈ (1...𝑁) ↔ (𝑉 − 1) ∈ (0...(𝑁 − 1))))
23926, 87, 238syl2anc 595 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑉 ∈ (1...𝑁) ↔ (𝑉 − 1) ∈ (0...(𝑁 − 1))))
24095, 239mpbid 235 . . . . . . . . . . . . . . 15 (𝜑 → (𝑉 − 1) ∈ (0...(𝑁 − 1)))
241240adantr 485 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑀 < 𝑉) → (𝑉 − 1) ∈ (0...(𝑁 − 1)))
242 ovexd 7448 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑀 < 𝑉) → (𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))) ∈ V)
243195, 237, 241, 242fvmptd 7000 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑀 < 𝑉) → (𝐹‘(𝑉 − 1)) = (𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
244243fveq1d 6886 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑀 < 𝑉) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
245244adantr 485 . . . . . . . . . . 11 (((𝜑 ∧ 𝑀 < 𝑉) ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
246198a1i 11 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V)
247 breq1 5116 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑉 → (𝑦 < 𝑀 ↔ 𝑉 < 𝑀))
248 id 23 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑉 → 𝑦 = 𝑉)
249 oveq1 7420 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑉 → (𝑦 + 1) = (𝑉 + 1))
250247, 248, 249ifbieq12d 4521 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑉 → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if(𝑉 < 𝑀, 𝑉, (𝑉 + 1)))
251 ltnsym 11310 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑀 ∈ ℝ ∧ 𝑉 ∈ ℝ) → (𝑀 < 𝑉 → ¬ 𝑉 < 𝑀))
252215, 27, 251syl2anc 595 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑀 < 𝑉 → ¬ 𝑉 < 𝑀))
253252imp 411 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑀 < 𝑉) → ¬ 𝑉 < 𝑀)
254253iffalsed 4503 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑀 < 𝑉) → if(𝑉 < 𝑀, 𝑉, (𝑉 + 1)) = (𝑉 + 1))
255250, 254sylan9eqr 2826 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = (𝑉 + 1))
256255eqeq2d 2780 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) → (𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ↔ 𝑗 = (𝑉 + 1)))
257256biimpa 481 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → 𝑗 = (𝑉 + 1))
258 oveq2 7421 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = (𝑉 + 1) → (1...𝑗) = (1...(𝑉 + 1)))
259258imaeq2d 6065 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑉 + 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑉 + 1))))
260259xpeq1d 5693 . . . . . . . . . . . . . . . . . 18 (𝑗 = (𝑉 + 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑉 + 1))) × {1}))
261 oveq1 7420 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = (𝑉 + 1) → (𝑗 + 1) = ((𝑉 + 1) + 1))
262261oveq1d 7428 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = (𝑉 + 1) → ((𝑗 + 1)...𝑁) = (((𝑉 + 1) + 1)...𝑁))
263262imaeq2d 6065 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑉 + 1) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))
264263xpeq1d 5693 . . . . . . . . . . . . . . . . . 18 (𝑗 = (𝑉 + 1) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))
265260, 264uneq12d 4131 . . . . . . . . . . . . . . . . 17 (𝑗 = (𝑉 + 1) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))
266265oveq2d 7429 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑉 + 1) → (𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))))
267257, 266syl 18 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → (𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))))
268246, 267csbied 3897 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))))
269 fz1ssfz0 13653 . . . . . . . . . . . . . . . 16 (1...(𝑁 − 1)) ⊆ (0...(𝑁 − 1))
270269, 7sselid 3943 . . . . . . . . . . . . . . 15 (𝜑 → 𝑉 ∈ (0...(𝑁 − 1)))
271270adantr 485 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑀 < 𝑉) → 𝑉 ∈ (0...(𝑁 − 1)))
272 ovexd 7448 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑀 < 𝑉) → (𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))) ∈ V)
273195, 268, 271, 272fvmptd 7000 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑀 < 𝑉) → (𝐹‘𝑉) = (𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))))
274273fveq1d 6886 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑀 < 𝑉) → ((𝐹‘𝑉)‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
275274adantr 485 . . . . . . . . . . 11 (((𝜑 ∧ 𝑀 < 𝑉) ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝐹‘𝑉)‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
276193, 245, 2753eqtr4d 2814 . . . . . . . . . 10 (((𝜑 ∧ 𝑀 < 𝑉) ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛))
277276ex 417 . . . . . . . . 9 ((𝜑 ∧ 𝑀 < 𝑉) → ((𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛)))
27859, 277sylbid 243 . . . . . . . 8 ((𝜑 ∧ 𝑀 < 𝑉) → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)})) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛)))
279278expdimp 457 . . . . . . 7 (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)}) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛)))
280279necon1ad 2981 . . . . . 6 (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 ∈ (𝑈 “ {(𝑉 + 1)})))
281 elimasni 6096 . . . . . . . 8 (𝑛 ∈ (𝑈 “ {(𝑉 + 1)}) → (𝑉 + 1)𝑈𝑛)
282 eqcom 2776 . . . . . . . . 9 (𝑛 = (𝑈‘(𝑉 + 1)) ↔ (𝑈‘(𝑉 + 1)) = 𝑛)
283 f1ofn 6824 . . . . . . . . . . 11 (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 Fn (1...𝑁))
2841, 283syl 18 . . . . . . . . . 10 (𝜑 → 𝑈 Fn (1...𝑁))
285 fnbrfvb 6934 . . . . . . . . . 10 ((𝑈 Fn (1...𝑁) ∧ (𝑉 + 1) ∈ (1...𝑁)) → ((𝑈‘(𝑉 + 1)) = 𝑛 ↔ (𝑉 + 1)𝑈𝑛))
286284, 15, 285syl2anc 595 . . . . . . . . 9 (𝜑 → ((𝑈‘(𝑉 + 1)) = 𝑛 ↔ (𝑉 + 1)𝑈𝑛))
287282, 286bitrid 286 . . . . . . . 8 (𝜑 → (𝑛 = (𝑈‘(𝑉 + 1)) ↔ (𝑉 + 1)𝑈𝑛))
288281, 287imbitrrid 249 . . . . . . 7 (𝜑 → (𝑛 ∈ (𝑈 “ {(𝑉 + 1)}) → 𝑛 = (𝑈‘(𝑉 + 1))))
289288ad2antrr 738 . . . . . 6 (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (𝑛 ∈ (𝑈 “ {(𝑉 + 1)}) → 𝑛 = (𝑈‘(𝑉 + 1))))
290280, 289syld 48 . . . . 5 (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1))))
291290ralrimiva 3163 . . . 4 ((𝜑 ∧ 𝑀 < 𝑉) → ∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1))))
292 fvex 6897 . . . . 5 (𝑈‘(𝑉 + 1)) ∈ V
293 eqeq2 2781 . . . . . . 7 (𝑚 = (𝑈‘(𝑉 + 1)) → (𝑛 = 𝑚 ↔ 𝑛 = (𝑈‘(𝑉 + 1))))
294293imbi2d 343 . . . . . 6 (𝑚 = (𝑈‘(𝑉 + 1)) → ((((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1)))))
295294ralbidv 3194 . . . . 5 (𝑚 = (𝑈‘(𝑉 + 1)) → (∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ ∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1)))))
296292, 295spcev 3574 . . . 4 (∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1))) → ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚))
297291, 296syl 18 . . 3 ((𝜑 ∧ 𝑀 < 𝑉) → ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚))
298 imadif 6623 . . . . . . . . . . . . . . 15 (Fun ◡𝑈 → (𝑈 “ ((1...𝑁) ∖ {𝑉})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})))
2994, 298syl 18 . . . . . . . . . . . . . 14 (𝜑 → (𝑈 “ ((1...𝑁) ∖ {𝑉})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})))
30097difeq1d 4088 . . . . . . . . . . . . . . . 16 (𝜑 → ((1...𝑁) ∖ {𝑉}) = (((1...𝑉) ∪ ((𝑉 + 1)...𝑁)) ∖ {𝑉}))
301 difundir 4252 . . . . . . . . . . . . . . . . 17 (((1...𝑉) ∪ ((𝑉 + 1)...𝑁)) ∖ {𝑉}) = (((1...𝑉) ∖ {𝑉}) ∪ (((𝑉 + 1)...𝑁) ∖ {𝑉}))
302206, 21eqeltrd 2869 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝑉 − 1) + 1) ∈ (ℤ≥‘1))
303 uzid 12879 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑉 − 1) ∈ ℤ → (𝑉 − 1) ∈ (ℤ≥‘(𝑉 − 1)))
304 peano2uz 12927 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑉 − 1) ∈ (ℤ≥‘(𝑉 − 1)) → ((𝑉 − 1) + 1) ∈ (ℤ≥‘(𝑉 − 1)))
30526, 216, 303, 3044syl 20 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑉 − 1) + 1) ∈ (ℤ≥‘(𝑉 − 1)))
306206, 305eqeltrrd 2870 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 𝑉 ∈ (ℤ≥‘(𝑉 − 1)))
307 fzsplit2 13579 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑉 − 1) + 1) ∈ (ℤ≥‘1) ∧ 𝑉 ∈ (ℤ≥‘(𝑉 − 1))) → (1...𝑉) = ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑉)))
308302, 306, 307syl2anc 595 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (1...𝑉) = ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑉)))
309206oveq1d 7428 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((𝑉 − 1) + 1)...𝑉) = (𝑉...𝑉))
310 fzsn 13596 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑉 ∈ ℤ → (𝑉...𝑉) = {𝑉})
31126, 310syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑉...𝑉) = {𝑉})
312309, 311eqtrd 2804 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝑉 − 1) + 1)...𝑉) = {𝑉})
313312uneq2d 4130 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑉)) = ((1...(𝑉 − 1)) ∪ {𝑉}))
314308, 313eqtrd 2804 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1...𝑉) = ((1...(𝑉 − 1)) ∪ {𝑉}))
315314difeq1d 4088 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((1...𝑉) ∖ {𝑉}) = (((1...(𝑉 − 1)) ∪ {𝑉}) ∖ {𝑉}))
316 difun2 4447 . . . . . . . . . . . . . . . . . . . 20 (((1...(𝑉 − 1)) ∪ {𝑉}) ∖ {𝑉}) = ((1...(𝑉 − 1)) ∖ {𝑉})
31727ltm1d 12149 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑉 − 1) < 𝑉)
318218, 27ltnled 11359 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑉 − 1) < 𝑉 ↔ ¬ 𝑉 ≤ (𝑉 − 1)))
319317, 318mpbid 235 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ¬ 𝑉 ≤ (𝑉 − 1))
320 elfzle2 13558 . . . . . . . . . . . . . . . . . . . . . 22 (𝑉 ∈ (1...(𝑉 − 1)) → 𝑉 ≤ (𝑉 − 1))
321319, 320nsyl 141 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ¬ 𝑉 ∈ (1...(𝑉 − 1)))
322 difsn 4770 . . . . . . . . . . . . . . . . . . . . 21 (¬ 𝑉 ∈ (1...(𝑉 − 1)) → ((1...(𝑉 − 1)) ∖ {𝑉}) = (1...(𝑉 − 1)))
323321, 322syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((1...(𝑉 − 1)) ∖ {𝑉}) = (1...(𝑉 − 1)))
324316, 323eqtrid 2816 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((1...(𝑉 − 1)) ∪ {𝑉}) ∖ {𝑉}) = (1...(𝑉 − 1)))
325315, 324eqtrd 2804 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((1...𝑉) ∖ {𝑉}) = (1...(𝑉 − 1)))
326 elfzle1 13557 . . . . . . . . . . . . . . . . . . . 20 (𝑉 ∈ ((𝑉 + 1)...𝑁) → (𝑉 + 1) ≤ 𝑉)
32732, 326nsyl 141 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ¬ 𝑉 ∈ ((𝑉 + 1)...𝑁))
328 difsn 4770 . . . . . . . . . . . . . . . . . . 19 (¬ 𝑉 ∈ ((𝑉 + 1)...𝑁) → (((𝑉 + 1)...𝑁) ∖ {𝑉}) = ((𝑉 + 1)...𝑁))
329327, 328syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝑉 + 1)...𝑁) ∖ {𝑉}) = ((𝑉 + 1)...𝑁))
330325, 329uneq12d 4131 . . . . . . . . . . . . . . . . 17 (𝜑 → (((1...𝑉) ∖ {𝑉}) ∪ (((𝑉 + 1)...𝑁) ∖ {𝑉})) = ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁)))
331301, 330eqtrid 2816 . . . . . . . . . . . . . . . 16 (𝜑 → (((1...𝑉) ∪ ((𝑉 + 1)...𝑁)) ∖ {𝑉}) = ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁)))
332300, 331eqtrd 2804 . . . . . . . . . . . . . . 15 (𝜑 → ((1...𝑁) ∖ {𝑉}) = ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁)))
333332imaeq2d 6065 . . . . . . . . . . . . . 14 (𝜑 → (𝑈 “ ((1...𝑁) ∖ {𝑉})) = (𝑈 “ ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁))))
334299, 333eqtr3d 2806 . . . . . . . . . . . . 13 (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})) = (𝑈 “ ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁))))
335 imaundi 6150 . . . . . . . . . . . . 13 (𝑈 “ ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁))) = ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ ((𝑉 + 1)...𝑁)))
336334, 335eqtrdi 2820 . . . . . . . . . . . 12 (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})) = ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))))
337336eleq2d 2855 . . . . . . . . . . 11 (𝜑 → (𝑛 ∈ ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})) ↔ 𝑛 ∈ ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ ((𝑉 + 1)...𝑁)))))
338 eldif 3923 . . . . . . . . . . 11 (𝑛 ∈ ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})) ↔ (𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {𝑉})))
339 elun 4115 . . . . . . . . . . 11 (𝑛 ∈ ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))) ↔ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))))
340337, 338, 3393bitr3g 316 . . . . . . . . . 10 (𝜑 → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {𝑉})) ↔ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))))
341340adantr 485 . . . . . . . . 9 ((𝜑 ∧ 𝑉 < 𝑀) → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {𝑉})) ↔ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))))
342 imassrn 6076 . . . . . . . . . . . . . . . 16 (𝑈 “ (1...(𝑉 − 1))) ⊆ ran 𝑈
343342, 63sstrid 3956 . . . . . . . . . . . . . . 15 (𝜑 → (𝑈 “ (1...(𝑉 − 1))) ⊆ (1...𝑁))
344343sselda 3945 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → 𝑛 ∈ (1...𝑁))
34567adantr 485 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → 𝑇 Fn (1...𝑁))
346 fnconstg 6769 . . . . . . . . . . . . . . . . . . . . 21 (1 ∈ V → ((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1))))
34769, 346ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1)))
348 fnconstg 6769 . . . . . . . . . . . . . . . . . . . . 21 (0 ∈ V → ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁)))
34972, 348ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁))
350347, 349pm3.2i 475 . . . . . . . . . . . . . . . . . . 19 (((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1))) ∧ ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁)))
351 imain 6624 . . . . . . . . . . . . . . . . . . . . 21 (Fun ◡𝑈 → (𝑈 “ ((1...(𝑉 − 1)) ∩ (𝑉...𝑁))) = ((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))))
3524, 351syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...(𝑉 − 1)) ∩ (𝑉...𝑁))) = ((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))))
353 fzdisj 13581 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑉 − 1) < 𝑉 → ((1...(𝑉 − 1)) ∩ (𝑉...𝑁)) = ∅)
354317, 353syl 18 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1...(𝑉 − 1)) ∩ (𝑉...𝑁)) = ∅)
355354imaeq2d 6065 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ ((1...(𝑉 − 1)) ∩ (𝑉...𝑁))) = (𝑈 “ ∅))
356355, 81eqtrdi 2820 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...(𝑉 − 1)) ∩ (𝑉...𝑁))) = ∅)
357352, 356eqtr3d 2806 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅)
358 fnun 6652 . . . . . . . . . . . . . . . . . . 19 (((((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1))) ∧ ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁))) ∧ ((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅) → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁))))
359350, 357, 358sylancr 598 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁))))
360 imaundi 6150 . . . . . . . . . . . . . . . . . . . 20 (𝑈 “ ((1...(𝑉 − 1)) ∪ (𝑉...𝑁))) = ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁)))
361 uzss 12887 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑉 ∈ (ℤ≥‘(𝑉 − 1)) → (ℤ≥‘𝑉) ⊆ (ℤ≥‘(𝑉 − 1)))
362306, 361syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (ℤ≥‘𝑉) ⊆ (ℤ≥‘(𝑉 − 1)))
363 elfzuz3 13551 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑉 ∈ (1...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ≥‘𝑉))
3647, 363syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑 → (𝑁 − 1) ∈ (ℤ≥‘𝑉))
365362, 364sseldd 3946 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑁 − 1) ∈ (ℤ≥‘(𝑉 − 1)))
366 peano2uz 12927 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑁 − 1) ∈ (ℤ≥‘(𝑉 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ≥‘(𝑉 − 1)))
367365, 366syl 18 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ≥‘(𝑉 − 1)))
36813, 367eqeltrrd 2870 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑉 − 1)))
369 fzsplit2 13579 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑉 − 1) + 1) ∈ (ℤ≥‘1) ∧ 𝑁 ∈ (ℤ≥‘(𝑉 − 1))) → (1...𝑁) = ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑁)))
370302, 368, 369syl2anc 595 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1...𝑁) = ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑁)))
371206oveq1d 7428 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((𝑉 − 1) + 1)...𝑁) = (𝑉...𝑁))
372371uneq2d 4130 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑁)) = ((1...(𝑉 − 1)) ∪ (𝑉...𝑁)))
373370, 372eqtrd 2804 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (1...𝑁) = ((1...(𝑉 − 1)) ∪ (𝑉...𝑁)))
374373imaeq2d 6065 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...(𝑉 − 1)) ∪ (𝑉...𝑁))))
375374, 102eqtr3d 2806 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑈 “ ((1...(𝑉 − 1)) ∪ (𝑉...𝑁))) = (1...𝑁))
376360, 375eqtr3id 2818 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁))) = (1...𝑁))
377376fneq2d 6632 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁))) ↔ (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn (1...𝑁)))
378359, 377mpbid 235 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn (1...𝑁))
379378adantr 485 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn (1...𝑁))
380 fzfid 14011 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → (1...𝑁) ∈ Fin)
381 eqidd 2770 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) = (𝑇‘𝑛))
382 fvun1 6975 . . . . . . . . . . . . . . . . . . . 20 ((((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1))) ∧ ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁)) ∧ (((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛))
383347, 349, 382mp3an12 1477 . . . . . . . . . . . . . . . . . . 19 ((((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛))
384357, 383sylan 591 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛))
38569fvconst2 7205 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) → (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛) = 1)
386385adantl 486 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛) = 1)
387384, 386eqtrd 2804 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 1)
388387adantr 485 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 1)
389345, 379, 380, 380, 109, 381, 388ofval 7688 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1))
390106adantr 485 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁))
391 fzss2 13594 . . . . . . . . . . . . . . . . . . . . 21 (𝑉 ∈ (ℤ≥‘(𝑉 − 1)) → (1...(𝑉 − 1)) ⊆ (1...𝑉))
392306, 391syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1...(𝑉 − 1)) ⊆ (1...𝑉))
393 imass2 6107 . . . . . . . . . . . . . . . . . . . 20 ((1...(𝑉 − 1)) ⊆ (1...𝑉) → (𝑈 “ (1...(𝑉 − 1))) ⊆ (𝑈 “ (1...𝑉)))
394392, 393syl 18 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑈 “ (1...(𝑉 − 1))) ⊆ (𝑈 “ (1...𝑉)))
395394sselda 3945 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → 𝑛 ∈ (𝑈 “ (1...𝑉)))
396395, 116syldan 602 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 1)
397396adantr 485 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 1)
398345, 390, 380, 380, 109, 381, 397ofval 7688 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1))
399389, 398eqtr4d 2807 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
400344, 399mpdan 699 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
401 imassrn 6076 . . . . . . . . . . . . . . . 16 (𝑈 “ ((𝑉 + 1)...𝑁)) ⊆ ran 𝑈
402401, 63sstrid 3956 . . . . . . . . . . . . . . 15 (𝜑 → (𝑈 “ ((𝑉 + 1)...𝑁)) ⊆ (1...𝑁))
403402sselda 3945 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → 𝑛 ∈ (1...𝑁))
40467adantr 485 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → 𝑇 Fn (1...𝑁))
405378adantr 485 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn (1...𝑁))
406 fzfid 14011 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → (1...𝑁) ∈ Fin)
407 eqidd 2770 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) = (𝑇‘𝑛))
408 fzss1 13593 . . . . . . . . . . . . . . . . . . . 20 ((𝑉 + 1) ∈ (ℤ≥‘𝑉) → ((𝑉 + 1)...𝑁) ⊆ (𝑉...𝑁))
409 imass2 6107 . . . . . . . . . . . . . . . . . . . 20 (((𝑉 + 1)...𝑁) ⊆ (𝑉...𝑁) → (𝑈 “ ((𝑉 + 1)...𝑁)) ⊆ (𝑈 “ (𝑉...𝑁)))
410141, 142, 408, 4094syl 20 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑈 “ ((𝑉 + 1)...𝑁)) ⊆ (𝑈 “ (𝑉...𝑁)))
411410sselda 3945 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → 𝑛 ∈ (𝑈 “ (𝑉...𝑁)))
412 fvun2 6976 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1))) ∧ ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁)) ∧ (((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (𝑉...𝑁)))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛))
413347, 349, 412mp3an12 1477 . . . . . . . . . . . . . . . . . . . 20 ((((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (𝑉...𝑁))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛))
414357, 413sylan 591 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑉...𝑁))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛))
41572fvconst2 7205 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (𝑈 “ (𝑉...𝑁)) → (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛) = 0)
416415adantl 486 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑉...𝑁))) → (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛) = 0)
417414, 416eqtrd 2804 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑉...𝑁))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 0)
418411, 417syldan 602 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 0)
419418adantr 485 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 0)
420404, 405, 406, 406, 109, 407, 419ofval 7688 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0))
421106adantr 485 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁))
422177adantr 485 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 0)
423404, 421, 406, 406, 109, 407, 422ofval 7688 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0))
424420, 423eqtr4d 2807 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
425403, 424mpdan 699 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
426400, 425jaodan 972 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
427426adantlr 727 . . . . . . . . . . 11 (((𝜑 ∧ 𝑉 < 𝑀) ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
428194adantr 485 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑉 < 𝑀) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))))
429198a1i 11 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V)
430208adantlr 727 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉))
431 lttr 11288 . . . . . . . . . . . . . . . . . . . . 21 (((𝑉 − 1) ∈ ℝ ∧ 𝑉 ∈ ℝ ∧ 𝑀 ∈ ℝ) → (((𝑉 − 1) < 𝑉 ∧ 𝑉 < 𝑀) → (𝑉 − 1) < 𝑀))
432218, 27, 215, 431syl3anc 1396 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝑉 − 1) < 𝑉 ∧ 𝑉 < 𝑀) → (𝑉 − 1) < 𝑀))
433317, 432mpand 707 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑉 < 𝑀 → (𝑉 − 1) < 𝑀))
434433imp 411 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑉 < 𝑀) → (𝑉 − 1) < 𝑀)
435434iftrued 4500 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑉 < 𝑀) → if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉) = (𝑉 − 1))
436435adantr 485 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉) = (𝑉 − 1))
437430, 436eqtrd 2804 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = (𝑉 − 1))
438 simpll 778 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → 𝜑)
439 oveq2 7421 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = (𝑉 − 1) → (1...𝑗) = (1...(𝑉 − 1)))
440439imaeq2d 6065 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = (𝑉 − 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑉 − 1))))
441440xpeq1d 5693 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑉 − 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑉 − 1))) × {1}))
442441adantl 486 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑉 − 1))) × {1}))
443 oveq1 7420 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = (𝑉 − 1) → (𝑗 + 1) = ((𝑉 − 1) + 1))
444443, 206sylan9eqr 2826 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → (𝑗 + 1) = 𝑉)
445444oveq1d 7428 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → ((𝑗 + 1)...𝑁) = (𝑉...𝑁))
446445imaeq2d 6065 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (𝑉...𝑁)))
447446xpeq1d 5693 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (𝑉...𝑁)) × {0}))
448442, 447uneq12d 4131 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))
449448oveq2d 7429 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → (𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))))
450438, 449sylan 591 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) ∧ 𝑗 = (𝑉 − 1)) → (𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))))
451429, 437, 450csbied2 3898 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))))
452240adantr 485 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑉 < 𝑀) → (𝑉 − 1) ∈ (0...(𝑁 − 1)))
453 ovexd 7448 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑉 < 𝑀) → (𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))) ∈ V)
454428, 451, 452, 453fvmptd 7000 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑉 < 𝑀) → (𝐹‘(𝑉 − 1)) = (𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))))
455454fveq1d 6886 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑉 < 𝑀) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛))
456455adantr 485 . . . . . . . . . . 11 (((𝜑 ∧ 𝑉 < 𝑀) ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛))
457198a1i 11 . . . . . . . . . . . . . . . 16 ((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V)
458 iftrue 4498 . . . . . . . . . . . . . . . . . . . 20 (𝑉 < 𝑀 → if(𝑉 < 𝑀, 𝑉, (𝑉 + 1)) = 𝑉)
459250, 458sylan9eqr 2826 . . . . . . . . . . . . . . . . . . 19 ((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = 𝑉)
460459eqeq2d 2780 . . . . . . . . . . . . . . . . . 18 ((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) → (𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ↔ 𝑗 = 𝑉))
461460biimpa 481 . . . . . . . . . . . . . . . . 17 (((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → 𝑗 = 𝑉)
462461, 235syl 18 . . . . . . . . . . . . . . . 16 (((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → (𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
463457, 462csbied 3897 . . . . . . . . . . . . . . 15 ((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
464463adantll 726 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = 𝑉) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
465270adantr 485 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑉 < 𝑀) → 𝑉 ∈ (0...(𝑁 − 1)))
466 ovexd 7448 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑉 < 𝑀) → (𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))) ∈ V)
467428, 464, 465, 466fvmptd 7000 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑉 < 𝑀) → (𝐹‘𝑉) = (𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
468467fveq1d 6886 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑉 < 𝑀) → ((𝐹‘𝑉)‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
469468adantr 485 . . . . . . . . . . 11 (((𝜑 ∧ 𝑉 < 𝑀) ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝐹‘𝑉)‘𝑛) = ((𝑇 ∘f + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
470427, 456, 4693eqtr4d 2814 . . . . . . . . . 10 (((𝜑 ∧ 𝑉 < 𝑀) ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛))
471470ex 417 . . . . . . . . 9 ((𝜑 ∧ 𝑉 < 𝑀) → ((𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛)))
472341, 471sylbid 243 . . . . . . . 8 ((𝜑 ∧ 𝑉 < 𝑀) → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {𝑉})) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛)))
473472expdimp 457 . . . . . . 7 (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (¬ 𝑛 ∈ (𝑈 “ {𝑉}) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛)))
474473necon1ad 2981 . . . . . 6 (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 ∈ (𝑈 “ {𝑉})))
475 elimasni 6096 . . . . . . . 8 (𝑛 ∈ (𝑈 “ {𝑉}) → 𝑉𝑈𝑛)
476 eqcom 2776 . . . . . . . . 9 (𝑛 = (𝑈‘𝑉) ↔ (𝑈‘𝑉) = 𝑛)
477 fnbrfvb 6934 . . . . . . . . . 10 ((𝑈 Fn (1...𝑁) ∧ 𝑉 ∈ (1...𝑁)) → ((𝑈‘𝑉) = 𝑛 ↔ 𝑉𝑈𝑛))
478284, 95, 477syl2anc 595 . . . . . . . . 9 (𝜑 → ((𝑈‘𝑉) = 𝑛 ↔ 𝑉𝑈𝑛))
479476, 478bitrid 286 . . . . . . . 8 (𝜑 → (𝑛 = (𝑈‘𝑉) ↔ 𝑉𝑈𝑛))
480475, 479imbitrrid 249 . . . . . . 7 (𝜑 → (𝑛 ∈ (𝑈 “ {𝑉}) → 𝑛 = (𝑈‘𝑉)))
481480ad2antrr 738 . . . . . 6 (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (𝑛 ∈ (𝑈 “ {𝑉}) → 𝑛 = (𝑈‘𝑉)))
482474, 481syld 48 . . . . 5 (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘𝑉)))
483482ralrimiva 3163 . . . 4 ((𝜑 ∧ 𝑉 < 𝑀) → ∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘𝑉)))
484 fvex 6897 . . . . 5 (𝑈‘𝑉) ∈ V
485 eqeq2 2781 . . . . . . 7 (𝑚 = (𝑈‘𝑉) → (𝑛 = 𝑚 ↔ 𝑛 = (𝑈‘𝑉)))
486485imbi2d 343 . . . . . 6 (𝑚 = (𝑈‘𝑉) → ((((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘𝑉))))
487486ralbidv 3194 . . . . 5 (𝑚 = (𝑈‘𝑉) → (∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ ∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘𝑉))))
488484, 487spcev 3574 . . . 4 (∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘𝑉)) → ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚))
489483, 488syl 18 . . 3 ((𝜑 ∧ 𝑉 < 𝑀) → ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚))
490 eldifsni 4762 . . . . 5 (𝑀 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑀 ≠ 𝑉)
491210, 490syl 18 . . . 4 (𝜑 → 𝑀 ≠ 𝑉)
492215, 27lttri2d 11351 . . . 4 (𝜑 → (𝑀 ≠ 𝑉 ↔ (𝑀 < 𝑉 ∨ 𝑉 < 𝑀)))
493491, 492mpbid 235 . . 3 (𝜑 → (𝑀 < 𝑉 ∨ 𝑉 < 𝑀))
494297, 489, 493mpjaodan 973 . 2 (𝜑 → ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚))
495 nfv 1941 . . . 4 Ⅎ𝑚((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛)
496495rmo2 3849 . . 3 (∃*𝑛 ∈ (𝑈 “ (1...𝑁))((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) ↔ ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚))
497 rmoeq1 3407 . . . 4 ((𝑈 “ (1...𝑁)) = (1...𝑁) → (∃*𝑛 ∈ (𝑈 “ (1...𝑁))((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) ↔ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛)))
4981, 99, 101, 4974syl 20 . . 3 (𝜑 → (∃*𝑛 ∈ (𝑈 “ (1...𝑁))((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) ↔ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛)))
499496, 498bitr3id 288 . 2 (𝜑 → (∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛)))
500494, 499mpbid 235 1 (𝜑 → ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   = wceq 1567  ∃wex 1806   ∈ wcel 2149   ≠ wne 2964  ∀wral 3085  ∃*wrmo 3375  Vcvv 3463  ⦋csb 3861   ∖ cdif 3910   ∪ cun 3911   ∩ cin 3912   ⊆ wss 3913  ∅c0 4294  ifcif 4492  {csn 4594   class class class wbr 5113   ↦ cmpt 5196   × cxp 5662  ◡ccnv 5663  ran crn 5665   “ cima 5667  Fun wfun 6533   Fn wfn 6534  ⟶wf 6535  –onto→wfo 6537  –1-1-onto→wf1o 6538  ‘cfv 6539  (class class class)co 7413   ∘f cof 7675  Fincfn 8945  ℂcc 11100  ℝcr 11101  0cc0 11102  1c1 11103   + caddc 11105   < clt 11245   ≤ cle 11246   − cmin 11443  ℕcn 12235  ℤcz 12593  ℤ≥cuz 12864  ...cfz 13537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5242  ax-sep 5261  ax-nul 5273  ax-pow 5339  ax-pr 5407  ax-un 7735  ax-cnex 11158  ax-resscn 11159  ax-1cn 11160  ax-icn 11161  ax-addcl 11162  ax-addrcl 11163  ax-mulcl 11164  ax-mulrcl 11165  ax-mulcom 11166  ax-addass 11167  ax-mulass 11168  ax-distr 11169  ax-i2m1 11170  ax-1ne0 11171  ax-1rid 11172  ax-rnegex 11173  ax-rrecex 11174  ax-cnre 11175  ax-pre-lttri 11176  ax-pre-lttrn 11177  ax-pre-ltadd 11178  ax-pre-mulgt0 11179
This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5559  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5617  df-we 5619  df-xp 5670  df-rel 5671  df-cnv 5672  df-co 5673  df-dm 5674  df-rn 5675  df-res 5676  df-ima 5677  df-pred 6305  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6495  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-of 7677  df-om 7865  df-1st 7988  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-1o 8455  df-er 8696  df-en 8946  df-dom 8947  df-sdom 8948  df-fin 8949  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11445  df-neg 11446  df-nn 12236  df-n0 12507  df-z 12594  df-uz 12865  df-fz 13538
This theorem is referenced by:  poimirlem8  38204  poimirlem18  38214  poimirlem21  38217  poimirlem22  38218
  Copyright terms: Public domain W3C validator