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

Theorem poimirlem7 37614
Description: Lemma for poimir 37640, similar to poimirlem6 37613, but for vertices after the opposite vertex. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0 (𝜑𝑁 ∈ ℕ)
poimirlem22.s 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
poimirlem9.1 (𝜑𝑇𝑆)
poimirlem9.2 (𝜑 → (2nd𝑇) ∈ (1...(𝑁 − 1)))
poimirlem7.3 (𝜑𝑀 ∈ ((((2nd𝑇) + 1) + 1)...𝑁))
Assertion
Ref Expression
poimirlem7 (𝜑 → (𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛)) = ((2nd ‘(1st𝑇))‘𝑀))
Distinct variable groups:   𝑓,𝑗,𝑛,𝑡,𝑦   𝜑,𝑗,𝑛,𝑦   𝑗,𝐹,𝑛,𝑦   𝑗,𝑀,𝑛,𝑦   𝑗,𝑁,𝑛,𝑦   𝑇,𝑗,𝑛,𝑦   𝜑,𝑡   𝑓,𝐾,𝑗,𝑛,𝑡   𝑓,𝑀,𝑡   𝑓,𝑁,𝑡   𝑇,𝑓   𝑓,𝐹,𝑡   𝑡,𝑇   𝑆,𝑗,𝑛,𝑡,𝑦
Allowed substitution hints:   𝜑(𝑓)   𝑆(𝑓)   𝐾(𝑦)

Proof of Theorem poimirlem7
StepHypRef Expression
1 poimirlem9.1 . . . . . . . 8 (𝜑𝑇𝑆)
2 elrabi 3690 . . . . . . . . 9 (𝑇 ∈ {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
3 poimirlem22.s . . . . . . . . 9 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
42, 3eleq2s 2857 . . . . . . . 8 (𝑇𝑆𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
51, 4syl 17 . . . . . . 7 (𝜑𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
6 xp1st 8045 . . . . . . 7 (𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
75, 6syl 17 . . . . . 6 (𝜑 → (1st𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
8 xp2nd 8046 . . . . . 6 ((1st𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
97, 8syl 17 . . . . 5 (𝜑 → (2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
10 fvex 6920 . . . . . 6 (2nd ‘(1st𝑇)) ∈ V
11 f1oeq1 6837 . . . . . 6 (𝑓 = (2nd ‘(1st𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
1210, 11elab 3681 . . . . 5 ((2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
139, 12sylib 218 . . . 4 (𝜑 → (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
14 f1of 6849 . . . 4 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)):(1...𝑁)⟶(1...𝑁))
1513, 14syl 17 . . 3 (𝜑 → (2nd ‘(1st𝑇)):(1...𝑁)⟶(1...𝑁))
16 poimirlem9.2 . . . . . . . . 9 (𝜑 → (2nd𝑇) ∈ (1...(𝑁 − 1)))
17 elfznn 13590 . . . . . . . . 9 ((2nd𝑇) ∈ (1...(𝑁 − 1)) → (2nd𝑇) ∈ ℕ)
1816, 17syl 17 . . . . . . . 8 (𝜑 → (2nd𝑇) ∈ ℕ)
1918peano2nnd 12281 . . . . . . 7 (𝜑 → ((2nd𝑇) + 1) ∈ ℕ)
2019peano2nnd 12281 . . . . . 6 (𝜑 → (((2nd𝑇) + 1) + 1) ∈ ℕ)
21 nnuz 12919 . . . . . 6 ℕ = (ℤ‘1)
2220, 21eleqtrdi 2849 . . . . 5 (𝜑 → (((2nd𝑇) + 1) + 1) ∈ (ℤ‘1))
23 fzss1 13600 . . . . 5 ((((2nd𝑇) + 1) + 1) ∈ (ℤ‘1) → ((((2nd𝑇) + 1) + 1)...𝑁) ⊆ (1...𝑁))
2422, 23syl 17 . . . 4 (𝜑 → ((((2nd𝑇) + 1) + 1)...𝑁) ⊆ (1...𝑁))
25 poimirlem7.3 . . . 4 (𝜑𝑀 ∈ ((((2nd𝑇) + 1) + 1)...𝑁))
2624, 25sseldd 3996 . . 3 (𝜑𝑀 ∈ (1...𝑁))
2715, 26ffvelcdmd 7105 . 2 (𝜑 → ((2nd ‘(1st𝑇))‘𝑀) ∈ (1...𝑁))
28 xp1st 8045 . . . . . . . . . . . . 13 ((1st𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)))
297, 28syl 17 . . . . . . . . . . . 12 (𝜑 → (1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)))
30 elmapfn 8904 . . . . . . . . . . . 12 ((1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st ‘(1st𝑇)) Fn (1...𝑁))
3129, 30syl 17 . . . . . . . . . . 11 (𝜑 → (1st ‘(1st𝑇)) Fn (1...𝑁))
3231adantr 480 . . . . . . . . . 10 ((𝜑𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀)) → (1st ‘(1st𝑇)) Fn (1...𝑁))
33 1ex 11255 . . . . . . . . . . . . . . 15 1 ∈ V
34 fnconstg 6797 . . . . . . . . . . . . . . 15 (1 ∈ V → (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))))
3533, 34ax-mp 5 . . . . . . . . . . . . . 14 (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1)))
36 c0ex 11253 . . . . . . . . . . . . . . 15 0 ∈ V
37 fnconstg 6797 . . . . . . . . . . . . . . 15 (0 ∈ V → (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ (𝑀...𝑁)))
3836, 37ax-mp 5 . . . . . . . . . . . . . 14 (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ (𝑀...𝑁))
3935, 38pm3.2i 470 . . . . . . . . . . . . 13 ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∧ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ (𝑀...𝑁)))
40 dff1o3 6855 . . . . . . . . . . . . . . . . 17 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd ‘(1st𝑇))))
4140simprbi 496 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun (2nd ‘(1st𝑇)))
4213, 41syl 17 . . . . . . . . . . . . . . 15 (𝜑 → Fun (2nd ‘(1st𝑇)))
43 imain 6653 . . . . . . . . . . . . . . 15 (Fun (2nd ‘(1st𝑇)) → ((2nd ‘(1st𝑇)) “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∩ ((2nd ‘(1st𝑇)) “ (𝑀...𝑁))))
4442, 43syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∩ ((2nd ‘(1st𝑇)) “ (𝑀...𝑁))))
4525elfzelzd 13562 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑀 ∈ ℤ)
4645zred 12720 . . . . . . . . . . . . . . . . . 18 (𝜑𝑀 ∈ ℝ)
4746ltm1d 12198 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑀 − 1) < 𝑀)
48 fzdisj 13588 . . . . . . . . . . . . . . . . 17 ((𝑀 − 1) < 𝑀 → ((1...(𝑀 − 1)) ∩ (𝑀...𝑁)) = ∅)
4947, 48syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ((1...(𝑀 − 1)) ∩ (𝑀...𝑁)) = ∅)
5049imaeq2d 6080 . . . . . . . . . . . . . . 15 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = ((2nd ‘(1st𝑇)) “ ∅))
51 ima0 6097 . . . . . . . . . . . . . . 15 ((2nd ‘(1st𝑇)) “ ∅) = ∅
5250, 51eqtrdi 2791 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = ∅)
5344, 52eqtr3d 2777 . . . . . . . . . . . . 13 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∩ ((2nd ‘(1st𝑇)) “ (𝑀...𝑁))) = ∅)
54 fnun 6683 . . . . . . . . . . . . 13 ((((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∧ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ (𝑀...𝑁))) ∧ (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∩ ((2nd ‘(1st𝑇)) “ (𝑀...𝑁))) = ∅) → ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})) Fn (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd ‘(1st𝑇)) “ (𝑀...𝑁))))
5539, 53, 54sylancr 587 . . . . . . . . . . . 12 (𝜑 → ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})) Fn (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd ‘(1st𝑇)) “ (𝑀...𝑁))))
5645zcnd 12721 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑀 ∈ ℂ)
57 npcan1 11686 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ ℂ → ((𝑀 − 1) + 1) = 𝑀)
5856, 57syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑀 − 1) + 1) = 𝑀)
59 1red 11260 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 1 ∈ ℝ)
6020nnred 12279 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((2nd𝑇) + 1) + 1) ∈ ℝ)
6119nnred 12279 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((2nd𝑇) + 1) ∈ ℝ)
6219nnge1d 12312 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 1 ≤ ((2nd𝑇) + 1))
6361ltp1d 12196 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((2nd𝑇) + 1) < (((2nd𝑇) + 1) + 1))
6459, 61, 60, 62, 63lelttrd 11417 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 1 < (((2nd𝑇) + 1) + 1))
65 elfzle1 13564 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑀 ∈ ((((2nd𝑇) + 1) + 1)...𝑁) → (((2nd𝑇) + 1) + 1) ≤ 𝑀)
6625, 65syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((2nd𝑇) + 1) + 1) ≤ 𝑀)
6759, 60, 46, 64, 66ltletrd 11419 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 1 < 𝑀)
6859, 46, 67ltled 11407 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 1 ≤ 𝑀)
69 elnnz1 12641 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 ∈ ℕ ↔ (𝑀 ∈ ℤ ∧ 1 ≤ 𝑀))
7045, 68, 69sylanbrc 583 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑀 ∈ ℕ)
7170, 21eleqtrdi 2849 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑀 ∈ (ℤ‘1))
7258, 71eqeltrd 2839 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑀 − 1) + 1) ∈ (ℤ‘1))
73 peano2zm 12658 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀 ∈ ℤ → (𝑀 − 1) ∈ ℤ)
7445, 73syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑀 − 1) ∈ ℤ)
75 uzid 12891 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑀 − 1) ∈ ℤ → (𝑀 − 1) ∈ (ℤ‘(𝑀 − 1)))
76 peano2uz 12941 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑀 − 1) ∈ (ℤ‘(𝑀 − 1)) → ((𝑀 − 1) + 1) ∈ (ℤ‘(𝑀 − 1)))
7774, 75, 763syl 18 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑀 − 1) + 1) ∈ (ℤ‘(𝑀 − 1)))
7858, 77eqeltrrd 2840 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑀 ∈ (ℤ‘(𝑀 − 1)))
79 uzss 12899 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ (ℤ‘(𝑀 − 1)) → (ℤ𝑀) ⊆ (ℤ‘(𝑀 − 1)))
8078, 79syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (ℤ𝑀) ⊆ (ℤ‘(𝑀 − 1)))
81 elfzuz3 13558 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ ((((2nd𝑇) + 1) + 1)...𝑁) → 𝑁 ∈ (ℤ𝑀))
8225, 81syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ (ℤ𝑀))
8380, 82sseldd 3996 . . . . . . . . . . . . . . . . . 18 (𝜑𝑁 ∈ (ℤ‘(𝑀 − 1)))
84 fzsplit2 13586 . . . . . . . . . . . . . . . . . 18 ((((𝑀 − 1) + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ‘(𝑀 − 1))) → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁)))
8572, 83, 84syl2anc 584 . . . . . . . . . . . . . . . . 17 (𝜑 → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁)))
8658oveq1d 7446 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝑀 − 1) + 1)...𝑁) = (𝑀...𝑁))
8786uneq2d 4178 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁)) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑁)))
8885, 87eqtrd 2775 . . . . . . . . . . . . . . . 16 (𝜑 → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑁)))
8988imaeq2d 6080 . . . . . . . . . . . . . . 15 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = ((2nd ‘(1st𝑇)) “ ((1...(𝑀 − 1)) ∪ (𝑀...𝑁))))
90 imaundi 6172 . . . . . . . . . . . . . . 15 ((2nd ‘(1st𝑇)) “ ((1...(𝑀 − 1)) ∪ (𝑀...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd ‘(1st𝑇)) “ (𝑀...𝑁)))
9189, 90eqtrdi 2791 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd ‘(1st𝑇)) “ (𝑀...𝑁))))
92 f1ofo 6856 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁))
9313, 92syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁))
94 foima 6826 . . . . . . . . . . . . . . 15 ((2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
9593, 94syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
9691, 95eqtr3d 2777 . . . . . . . . . . . . 13 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd ‘(1st𝑇)) “ (𝑀...𝑁))) = (1...𝑁))
9796fneq2d 6663 . . . . . . . . . . . 12 (𝜑 → (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})) Fn (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd ‘(1st𝑇)) “ (𝑀...𝑁))) ↔ ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})) Fn (1...𝑁)))
9855, 97mpbid 232 . . . . . . . . . . 11 (𝜑 → ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})) Fn (1...𝑁))
9998adantr 480 . . . . . . . . . 10 ((𝜑𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀)) → ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})) Fn (1...𝑁))
100 ovexd 7466 . . . . . . . . . 10 ((𝜑𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀)) → (1...𝑁) ∈ V)
101 inidm 4235 . . . . . . . . . 10 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
102 eqidd 2736 . . . . . . . . . 10 (((𝜑𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑛) = ((1st ‘(1st𝑇))‘𝑛))
103 imaundi 6172 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑇)) “ ({𝑀} ∪ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ {𝑀}) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)))
104 fzpred 13609 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ (ℤ𝑀) → (𝑀...𝑁) = ({𝑀} ∪ ((𝑀 + 1)...𝑁)))
10582, 104syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑀...𝑁) = ({𝑀} ∪ ((𝑀 + 1)...𝑁)))
106105imaeq2d 6080 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) = ((2nd ‘(1st𝑇)) “ ({𝑀} ∪ ((𝑀 + 1)...𝑁))))
107 f1ofn 6850 . . . . . . . . . . . . . . . . . . . . 21 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)) Fn (1...𝑁))
10813, 107syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (2nd ‘(1st𝑇)) Fn (1...𝑁))
109 fnsnfv 6988 . . . . . . . . . . . . . . . . . . . 20 (((2nd ‘(1st𝑇)) Fn (1...𝑁) ∧ 𝑀 ∈ (1...𝑁)) → {((2nd ‘(1st𝑇))‘𝑀)} = ((2nd ‘(1st𝑇)) “ {𝑀}))
110108, 26, 109syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (𝜑 → {((2nd ‘(1st𝑇))‘𝑀)} = ((2nd ‘(1st𝑇)) “ {𝑀}))
111110uneq1d 4177 . . . . . . . . . . . . . . . . . 18 (𝜑 → ({((2nd ‘(1st𝑇))‘𝑀)} ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ {𝑀}) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))))
112103, 106, 1113eqtr4a 2801 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) = ({((2nd ‘(1st𝑇))‘𝑀)} ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))))
113112xpeq1d 5718 . . . . . . . . . . . . . . . 16 (𝜑 → (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}) = (({((2nd ‘(1st𝑇))‘𝑀)} ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))) × {0}))
114 xpundir 5758 . . . . . . . . . . . . . . . 16 (({((2nd ‘(1st𝑇))‘𝑀)} ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))) × {0}) = (({((2nd ‘(1st𝑇))‘𝑀)} × {0}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))
115113, 114eqtrdi 2791 . . . . . . . . . . . . . . 15 (𝜑 → (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}) = (({((2nd ‘(1st𝑇))‘𝑀)} × {0}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))
116115uneq2d 4178 . . . . . . . . . . . . . 14 (𝜑 → ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (({((2nd ‘(1st𝑇))‘𝑀)} × {0}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
117 un12 4183 . . . . . . . . . . . . . 14 ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (({((2nd ‘(1st𝑇))‘𝑀)} × {0}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) = (({((2nd ‘(1st𝑇))‘𝑀)} × {0}) ∪ ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))
118116, 117eqtrdi 2791 . . . . . . . . . . . . 13 (𝜑 → ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})) = (({((2nd ‘(1st𝑇))‘𝑀)} × {0}) ∪ ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
119118fveq1d 6909 . . . . . . . . . . . 12 (𝜑 → (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}))‘𝑛) = ((({((2nd ‘(1st𝑇))‘𝑀)} × {0}) ∪ ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛))
120119ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}))‘𝑛) = ((({((2nd ‘(1st𝑇))‘𝑀)} × {0}) ∪ ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛))
121 fnconstg 6797 . . . . . . . . . . . . . . . . 17 (0 ∈ V → (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)))
12236, 121ax-mp 5 . . . . . . . . . . . . . . . 16 (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))
12335, 122pm3.2i 470 . . . . . . . . . . . . . . 15 ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∧ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)))
124 imain 6653 . . . . . . . . . . . . . . . . 17 (Fun (2nd ‘(1st𝑇)) → ((2nd ‘(1st𝑇)) “ ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∩ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))))
12542, 124syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∩ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))))
12674zred 12720 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑀 − 1) ∈ ℝ)
127 peano2re 11432 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 ∈ ℝ → (𝑀 + 1) ∈ ℝ)
12846, 127syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑀 + 1) ∈ ℝ)
12946ltp1d 12196 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑀 < (𝑀 + 1))
130126, 46, 128, 47, 129lttrd 11420 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑀 − 1) < (𝑀 + 1))
131 fzdisj 13588 . . . . . . . . . . . . . . . . . . 19 ((𝑀 − 1) < (𝑀 + 1) → ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁)) = ∅)
132130, 131syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁)) = ∅)
133132imaeq2d 6080 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁))) = ((2nd ‘(1st𝑇)) “ ∅))
134133, 51eqtrdi 2791 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁))) = ∅)
135125, 134eqtr3d 2777 . . . . . . . . . . . . . . 15 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∩ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅)
136 fnun 6683 . . . . . . . . . . . . . . 15 ((((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∧ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))) ∧ (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∩ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅) → ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))))
137123, 135, 136sylancr 587 . . . . . . . . . . . . . 14 (𝜑 → ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))))
138 imaundi 6172 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑇)) “ ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)))
139 imadif 6652 . . . . . . . . . . . . . . . . . 18 (Fun (2nd ‘(1st𝑇)) → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {𝑀})) = (((2nd ‘(1st𝑇)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑇)) “ {𝑀})))
14042, 139syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {𝑀})) = (((2nd ‘(1st𝑇)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑇)) “ {𝑀})))
141 fzsplit 13587 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 ∈ (1...𝑁) → (1...𝑁) = ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)))
14226, 141syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1...𝑁) = ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)))
143142difeq1d 4135 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((1...𝑁) ∖ {𝑀}) = (((1...𝑀) ∪ ((𝑀 + 1)...𝑁)) ∖ {𝑀}))
144 difundir 4297 . . . . . . . . . . . . . . . . . . . 20 (((1...𝑀) ∪ ((𝑀 + 1)...𝑁)) ∖ {𝑀}) = (((1...𝑀) ∖ {𝑀}) ∪ (((𝑀 + 1)...𝑁) ∖ {𝑀}))
145 fzsplit2 13586 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑀 − 1) + 1) ∈ (ℤ‘1) ∧ 𝑀 ∈ (ℤ‘(𝑀 − 1))) → (1...𝑀) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑀)))
14672, 78, 145syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (1...𝑀) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑀)))
14758oveq1d 7446 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (((𝑀 − 1) + 1)...𝑀) = (𝑀...𝑀))
148 fzsn 13603 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀})
14945, 148syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑀...𝑀) = {𝑀})
150147, 149eqtrd 2775 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (((𝑀 − 1) + 1)...𝑀) = {𝑀})
151150uneq2d 4178 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑀)) = ((1...(𝑀 − 1)) ∪ {𝑀}))
152146, 151eqtrd 2775 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1...𝑀) = ((1...(𝑀 − 1)) ∪ {𝑀}))
153152difeq1d 4135 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1...𝑀) ∖ {𝑀}) = (((1...(𝑀 − 1)) ∪ {𝑀}) ∖ {𝑀}))
154 difun2 4487 . . . . . . . . . . . . . . . . . . . . . . 23 (((1...(𝑀 − 1)) ∪ {𝑀}) ∖ {𝑀}) = ((1...(𝑀 − 1)) ∖ {𝑀})
155126, 46ltnled 11406 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((𝑀 − 1) < 𝑀 ↔ ¬ 𝑀 ≤ (𝑀 − 1)))
15647, 155mpbid 232 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ¬ 𝑀 ≤ (𝑀 − 1))
157 elfzle2 13565 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 ∈ (1...(𝑀 − 1)) → 𝑀 ≤ (𝑀 − 1))
158156, 157nsyl 140 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ¬ 𝑀 ∈ (1...(𝑀 − 1)))
159 difsn 4803 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑀 ∈ (1...(𝑀 − 1)) → ((1...(𝑀 − 1)) ∖ {𝑀}) = (1...(𝑀 − 1)))
160158, 159syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((1...(𝑀 − 1)) ∖ {𝑀}) = (1...(𝑀 − 1)))
161154, 160eqtrid 2787 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((1...(𝑀 − 1)) ∪ {𝑀}) ∖ {𝑀}) = (1...(𝑀 − 1)))
162153, 161eqtrd 2775 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((1...𝑀) ∖ {𝑀}) = (1...(𝑀 − 1)))
16346, 128ltnled 11406 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑀 < (𝑀 + 1) ↔ ¬ (𝑀 + 1) ≤ 𝑀))
164129, 163mpbid 232 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ¬ (𝑀 + 1) ≤ 𝑀)
165 elfzle1 13564 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀 ∈ ((𝑀 + 1)...𝑁) → (𝑀 + 1) ≤ 𝑀)
166164, 165nsyl 140 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ¬ 𝑀 ∈ ((𝑀 + 1)...𝑁))
167 difsn 4803 . . . . . . . . . . . . . . . . . . . . . 22 𝑀 ∈ ((𝑀 + 1)...𝑁) → (((𝑀 + 1)...𝑁) ∖ {𝑀}) = ((𝑀 + 1)...𝑁))
168166, 167syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((𝑀 + 1)...𝑁) ∖ {𝑀}) = ((𝑀 + 1)...𝑁))
169162, 168uneq12d 4179 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((1...𝑀) ∖ {𝑀}) ∪ (((𝑀 + 1)...𝑁) ∖ {𝑀})) = ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁)))
170144, 169eqtrid 2787 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((1...𝑀) ∪ ((𝑀 + 1)...𝑁)) ∖ {𝑀}) = ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁)))
171143, 170eqtrd 2775 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((1...𝑁) ∖ {𝑀}) = ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁)))
172171imaeq2d 6080 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {𝑀})) = ((2nd ‘(1st𝑇)) “ ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁))))
173110eqcomd 2741 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((2nd ‘(1st𝑇)) “ {𝑀}) = {((2nd ‘(1st𝑇))‘𝑀)})
17495, 173difeq12d 4137 . . . . . . . . . . . . . . . . 17 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑇)) “ {𝑀})) = ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑀)}))
175140, 172, 1743eqtr3d 2783 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁))) = ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑀)}))
176138, 175eqtr3id 2789 . . . . . . . . . . . . . . 15 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))) = ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑀)}))
177176fneq2d 6663 . . . . . . . . . . . . . 14 (𝜑 → (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))) ↔ ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑀)})))
178137, 177mpbid 232 . . . . . . . . . . . . 13 (𝜑 → ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑀)}))
179 eldifsn 4791 . . . . . . . . . . . . . . 15 (𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑀)}) ↔ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀)))
180179biimpri 228 . . . . . . . . . . . . . 14 ((𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀)) → 𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑀)}))
181180ancoms 458 . . . . . . . . . . . . 13 ((𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀) ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑀)}))
182 disjdif 4478 . . . . . . . . . . . . . 14 ({((2nd ‘(1st𝑇))‘𝑀)} ∩ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑀)})) = ∅
183 fnconstg 6797 . . . . . . . . . . . . . . . 16 (0 ∈ V → ({((2nd ‘(1st𝑇))‘𝑀)} × {0}) Fn {((2nd ‘(1st𝑇))‘𝑀)})
18436, 183ax-mp 5 . . . . . . . . . . . . . . 15 ({((2nd ‘(1st𝑇))‘𝑀)} × {0}) Fn {((2nd ‘(1st𝑇))‘𝑀)}
185 fvun2 7001 . . . . . . . . . . . . . . 15 ((({((2nd ‘(1st𝑇))‘𝑀)} × {0}) Fn {((2nd ‘(1st𝑇))‘𝑀)} ∧ ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑀)}) ∧ (({((2nd ‘(1st𝑇))‘𝑀)} ∩ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑀)})) = ∅ ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑀)}))) → ((({((2nd ‘(1st𝑇))‘𝑀)} × {0}) ∪ ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛))
186184, 185mp3an1 1447 . . . . . . . . . . . . . 14 ((((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑀)}) ∧ (({((2nd ‘(1st𝑇))‘𝑀)} ∩ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑀)})) = ∅ ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑀)}))) → ((({((2nd ‘(1st𝑇))‘𝑀)} × {0}) ∪ ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛))
187182, 186mpanr1 703 . . . . . . . . . . . . 13 ((((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑀)}) ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑀)})) → ((({((2nd ‘(1st𝑇))‘𝑀)} × {0}) ∪ ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛))
188178, 181, 187syl2an 596 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀) ∧ 𝑛 ∈ (1...𝑁))) → ((({((2nd ‘(1st𝑇))‘𝑀)} × {0}) ∪ ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛))
189188anassrs 467 . . . . . . . . . . 11 (((𝜑𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → ((({((2nd ‘(1st𝑇))‘𝑀)} × {0}) ∪ ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛))
190120, 189eqtrd 2775 . . . . . . . . . 10 (((𝜑𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}))‘𝑛) = (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛))
19132, 99, 100, 100, 101, 102, 190ofval 7708 . . . . . . . . 9 (((𝜑𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛) = (((1st ‘(1st𝑇))‘𝑛) + (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛)))
192 fnconstg 6797 . . . . . . . . . . . . . . 15 (1 ∈ V → (((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...𝑀)))
19333, 192ax-mp 5 . . . . . . . . . . . . . 14 (((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...𝑀))
194193, 122pm3.2i 470 . . . . . . . . . . . . 13 ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)))
195 imain 6653 . . . . . . . . . . . . . . 15 (Fun (2nd ‘(1st𝑇)) → ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))))
19642, 195syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))))
197 fzdisj 13588 . . . . . . . . . . . . . . . . 17 (𝑀 < (𝑀 + 1) → ((1...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅)
198129, 197syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ((1...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅)
199198imaeq2d 6080 . . . . . . . . . . . . . . 15 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ((2nd ‘(1st𝑇)) “ ∅))
200199, 51eqtrdi 2791 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ∅)
201196, 200eqtr3d 2777 . . . . . . . . . . . . 13 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅)
202 fnun 6683 . . . . . . . . . . . . 13 ((((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))) ∧ (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅) → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))))
203194, 201, 202sylancr 587 . . . . . . . . . . . 12 (𝜑 → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))))
204142imaeq2d 6080 . . . . . . . . . . . . . . 15 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))))
205 imaundi 6172 . . . . . . . . . . . . . . 15 ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)))
206204, 205eqtrdi 2791 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))))
207206, 95eqtr3d 2777 . . . . . . . . . . . . 13 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))) = (1...𝑁))
208207fneq2d 6663 . . . . . . . . . . . 12 (𝜑 → (((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))) ↔ ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁)))
209203, 208mpbid 232 . . . . . . . . . . 11 (𝜑 → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
210209adantr 480 . . . . . . . . . 10 ((𝜑𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀)) → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
211 imaundi 6172 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑇)) “ ((1...(𝑀 − 1)) ∪ {𝑀})) = (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd ‘(1st𝑇)) “ {𝑀}))
212152imaeq2d 6080 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑀)) = ((2nd ‘(1st𝑇)) “ ((1...(𝑀 − 1)) ∪ {𝑀})))
213110uneq2d 4178 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∪ {((2nd ‘(1st𝑇))‘𝑀)}) = (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd ‘(1st𝑇)) “ {𝑀})))
214211, 212, 2133eqtr4a 2801 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑀)) = (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∪ {((2nd ‘(1st𝑇))‘𝑀)}))
215214xpeq1d 5718 . . . . . . . . . . . . . . . 16 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) = ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∪ {((2nd ‘(1st𝑇))‘𝑀)}) × {1}))
216 xpundir 5758 . . . . . . . . . . . . . . . 16 ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∪ {((2nd ‘(1st𝑇))‘𝑀)}) × {1}) = ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ ({((2nd ‘(1st𝑇))‘𝑀)} × {1}))
217215, 216eqtrdi 2791 . . . . . . . . . . . . . . 15 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) = ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ ({((2nd ‘(1st𝑇))‘𝑀)} × {1})))
218217uneq1d 4177 . . . . . . . . . . . . . 14 (𝜑 → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) = (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ ({((2nd ‘(1st𝑇))‘𝑀)} × {1})) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))
219 un23 4184 . . . . . . . . . . . . . . 15 (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ ({((2nd ‘(1st𝑇))‘𝑀)} × {1})) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) = (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) ∪ ({((2nd ‘(1st𝑇))‘𝑀)} × {1}))
220219equncomi 4170 . . . . . . . . . . . . . 14 (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ ({((2nd ‘(1st𝑇))‘𝑀)} × {1})) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) = (({((2nd ‘(1st𝑇))‘𝑀)} × {1}) ∪ ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))
221218, 220eqtrdi 2791 . . . . . . . . . . . . 13 (𝜑 → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) = (({((2nd ‘(1st𝑇))‘𝑀)} × {1}) ∪ ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
222221fveq1d 6909 . . . . . . . . . . . 12 (𝜑 → (((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛) = ((({((2nd ‘(1st𝑇))‘𝑀)} × {1}) ∪ ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛))
223222ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛) = ((({((2nd ‘(1st𝑇))‘𝑀)} × {1}) ∪ ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛))
224 fnconstg 6797 . . . . . . . . . . . . . . . 16 (1 ∈ V → ({((2nd ‘(1st𝑇))‘𝑀)} × {1}) Fn {((2nd ‘(1st𝑇))‘𝑀)})
22533, 224ax-mp 5 . . . . . . . . . . . . . . 15 ({((2nd ‘(1st𝑇))‘𝑀)} × {1}) Fn {((2nd ‘(1st𝑇))‘𝑀)}
226 fvun2 7001 . . . . . . . . . . . . . . 15 ((({((2nd ‘(1st𝑇))‘𝑀)} × {1}) Fn {((2nd ‘(1st𝑇))‘𝑀)} ∧ ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑀)}) ∧ (({((2nd ‘(1st𝑇))‘𝑀)} ∩ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑀)})) = ∅ ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑀)}))) → ((({((2nd ‘(1st𝑇))‘𝑀)} × {1}) ∪ ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛))
227225, 226mp3an1 1447 . . . . . . . . . . . . . 14 ((((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑀)}) ∧ (({((2nd ‘(1st𝑇))‘𝑀)} ∩ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑀)})) = ∅ ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑀)}))) → ((({((2nd ‘(1st𝑇))‘𝑀)} × {1}) ∪ ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛))
228182, 227mpanr1 703 . . . . . . . . . . . . 13 ((((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑀)}) ∧ 𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑀)})) → ((({((2nd ‘(1st𝑇))‘𝑀)} × {1}) ∪ ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛))
229178, 181, 228syl2an 596 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀) ∧ 𝑛 ∈ (1...𝑁))) → ((({((2nd ‘(1st𝑇))‘𝑀)} × {1}) ∪ ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛))
230229anassrs 467 . . . . . . . . . . 11 (((𝜑𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → ((({((2nd ‘(1st𝑇))‘𝑀)} × {1}) ∪ ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛))
231223, 230eqtrd 2775 . . . . . . . . . 10 (((𝜑𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛) = (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛))
23232, 210, 100, 100, 101, 102, 231ofval 7708 . . . . . . . . 9 (((𝜑𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((1st ‘(1st𝑇))‘𝑛) + (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛)))
233191, 232eqtr4d 2778 . . . . . . . 8 (((𝜑𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛) = (((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛))
234233an32s 652 . . . . . . 7 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀)) → (((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛) = (((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛))
235234anasss 466 . . . . . 6 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀))) → (((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛) = (((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛))
236 fveq2 6907 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑇 → (2nd𝑡) = (2nd𝑇))
237236breq2d 5160 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑇 → (𝑦 < (2nd𝑡) ↔ 𝑦 < (2nd𝑇)))
238237ifbid 4554 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑇 → if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)))
239238csbeq1d 3912 . . . . . . . . . . . . . . 15 (𝑡 = 𝑇if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))
240 2fveq3 6912 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑇 → (1st ‘(1st𝑡)) = (1st ‘(1st𝑇)))
241 2fveq3 6912 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑇 → (2nd ‘(1st𝑡)) = (2nd ‘(1st𝑇)))
242241imaeq1d 6079 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...𝑗)))
243242xpeq1d 5718 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}))
244241imaeq1d 6079 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)))
245244xpeq1d 5718 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
246243, 245uneq12d 4179 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑇 → ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))
247240, 246oveq12d 7449 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑇 → ((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
248247csbeq2dv 3915 . . . . . . . . . . . . . . 15 (𝑡 = 𝑇if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
249239, 248eqtrd 2775 . . . . . . . . . . . . . 14 (𝑡 = 𝑇if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
250249mpteq2dv 5250 . . . . . . . . . . . . 13 (𝑡 = 𝑇 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
251250eqeq2d 2746 . . . . . . . . . . . 12 (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
252251, 3elrab2 3698 . . . . . . . . . . 11 (𝑇𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
253252simprbi 496 . . . . . . . . . 10 (𝑇𝑆𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
2541, 253syl 17 . . . . . . . . 9 (𝜑𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
255 breq1 5151 . . . . . . . . . . . . . 14 (𝑦 = (𝑀 − 2) → (𝑦 < (2nd𝑇) ↔ (𝑀 − 2) < (2nd𝑇)))
256255adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑦 = (𝑀 − 2)) → (𝑦 < (2nd𝑇) ↔ (𝑀 − 2) < (2nd𝑇)))
257 oveq1 7438 . . . . . . . . . . . . . 14 (𝑦 = (𝑀 − 2) → (𝑦 + 1) = ((𝑀 − 2) + 1))
258 sub1m1 12516 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ ℂ → ((𝑀 − 1) − 1) = (𝑀 − 2))
25956, 258syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑀 − 1) − 1) = (𝑀 − 2))
260259oveq1d 7446 . . . . . . . . . . . . . . 15 (𝜑 → (((𝑀 − 1) − 1) + 1) = ((𝑀 − 2) + 1))
26174zcnd 12721 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑀 − 1) ∈ ℂ)
262 npcan1 11686 . . . . . . . . . . . . . . . 16 ((𝑀 − 1) ∈ ℂ → (((𝑀 − 1) − 1) + 1) = (𝑀 − 1))
263261, 262syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (((𝑀 − 1) − 1) + 1) = (𝑀 − 1))
264260, 263eqtr3d 2777 . . . . . . . . . . . . . 14 (𝜑 → ((𝑀 − 2) + 1) = (𝑀 − 1))
265257, 264sylan9eqr 2797 . . . . . . . . . . . . 13 ((𝜑𝑦 = (𝑀 − 2)) → (𝑦 + 1) = (𝑀 − 1))
266256, 265ifbieq2d 4557 . . . . . . . . . . . 12 ((𝜑𝑦 = (𝑀 − 2)) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) = if((𝑀 − 2) < (2nd𝑇), 𝑦, (𝑀 − 1)))
26718nncnd 12280 . . . . . . . . . . . . . . . . 17 (𝜑 → (2nd𝑇) ∈ ℂ)
268 add1p1 12515 . . . . . . . . . . . . . . . . 17 ((2nd𝑇) ∈ ℂ → (((2nd𝑇) + 1) + 1) = ((2nd𝑇) + 2))
269267, 268syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (((2nd𝑇) + 1) + 1) = ((2nd𝑇) + 2))
270269, 66eqbrtrrd 5172 . . . . . . . . . . . . . . 15 (𝜑 → ((2nd𝑇) + 2) ≤ 𝑀)
27118nnred 12279 . . . . . . . . . . . . . . . . 17 (𝜑 → (2nd𝑇) ∈ ℝ)
272 2re 12338 . . . . . . . . . . . . . . . . . 18 2 ∈ ℝ
273 leaddsub 11737 . . . . . . . . . . . . . . . . . 18 (((2nd𝑇) ∈ ℝ ∧ 2 ∈ ℝ ∧ 𝑀 ∈ ℝ) → (((2nd𝑇) + 2) ≤ 𝑀 ↔ (2nd𝑇) ≤ (𝑀 − 2)))
274272, 273mp3an2 1448 . . . . . . . . . . . . . . . . 17 (((2nd𝑇) ∈ ℝ ∧ 𝑀 ∈ ℝ) → (((2nd𝑇) + 2) ≤ 𝑀 ↔ (2nd𝑇) ≤ (𝑀 − 2)))
275271, 46, 274syl2anc 584 . . . . . . . . . . . . . . . 16 (𝜑 → (((2nd𝑇) + 2) ≤ 𝑀 ↔ (2nd𝑇) ≤ (𝑀 − 2)))
27659, 46posdifd 11848 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (1 < 𝑀 ↔ 0 < (𝑀 − 1)))
27767, 276mpbid 232 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 0 < (𝑀 − 1))
278 elnnz 12621 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 − 1) ∈ ℕ ↔ ((𝑀 − 1) ∈ ℤ ∧ 0 < (𝑀 − 1)))
27974, 277, 278sylanbrc 583 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑀 − 1) ∈ ℕ)
280 nnm1nn0 12565 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 − 1) ∈ ℕ → ((𝑀 − 1) − 1) ∈ ℕ0)
281279, 280syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑀 − 1) − 1) ∈ ℕ0)
282259, 281eqeltrrd 2840 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑀 − 2) ∈ ℕ0)
283282nn0red 12586 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑀 − 2) ∈ ℝ)
284271, 283lenltd 11405 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd𝑇) ≤ (𝑀 − 2) ↔ ¬ (𝑀 − 2) < (2nd𝑇)))
285275, 284bitrd 279 . . . . . . . . . . . . . . 15 (𝜑 → (((2nd𝑇) + 2) ≤ 𝑀 ↔ ¬ (𝑀 − 2) < (2nd𝑇)))
286270, 285mpbid 232 . . . . . . . . . . . . . 14 (𝜑 → ¬ (𝑀 − 2) < (2nd𝑇))
287286iffalsed 4542 . . . . . . . . . . . . 13 (𝜑 → if((𝑀 − 2) < (2nd𝑇), 𝑦, (𝑀 − 1)) = (𝑀 − 1))
288287adantr 480 . . . . . . . . . . . 12 ((𝜑𝑦 = (𝑀 − 2)) → if((𝑀 − 2) < (2nd𝑇), 𝑦, (𝑀 − 1)) = (𝑀 − 1))
289266, 288eqtrd 2775 . . . . . . . . . . 11 ((𝜑𝑦 = (𝑀 − 2)) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) = (𝑀 − 1))
290289csbeq1d 3912 . . . . . . . . . 10 ((𝜑𝑦 = (𝑀 − 2)) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑀 − 1) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
291 oveq2 7439 . . . . . . . . . . . . . . . . 17 (𝑗 = (𝑀 − 1) → (1...𝑗) = (1...(𝑀 − 1)))
292291imaeq2d 6080 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑀 − 1) → ((2nd ‘(1st𝑇)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))))
293292xpeq1d 5718 . . . . . . . . . . . . . . 15 (𝑗 = (𝑀 − 1) → (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}))
294293adantl 481 . . . . . . . . . . . . . 14 ((𝜑𝑗 = (𝑀 − 1)) → (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}))
295 oveq1 7438 . . . . . . . . . . . . . . . . . 18 (𝑗 = (𝑀 − 1) → (𝑗 + 1) = ((𝑀 − 1) + 1))
296295, 58sylan9eqr 2797 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 = (𝑀 − 1)) → (𝑗 + 1) = 𝑀)
297296oveq1d 7446 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 = (𝑀 − 1)) → ((𝑗 + 1)...𝑁) = (𝑀...𝑁))
298297imaeq2d 6080 . . . . . . . . . . . . . . 15 ((𝜑𝑗 = (𝑀 − 1)) → ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ (𝑀...𝑁)))
299298xpeq1d 5718 . . . . . . . . . . . . . 14 ((𝜑𝑗 = (𝑀 − 1)) → (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}))
300294, 299uneq12d 4179 . . . . . . . . . . . . 13 ((𝜑𝑗 = (𝑀 − 1)) → ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})))
301300oveq2d 7447 . . . . . . . . . . . 12 ((𝜑𝑗 = (𝑀 − 1)) → ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}))))
30274, 301csbied 3946 . . . . . . . . . . 11 (𝜑(𝑀 − 1) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}))))
303302adantr 480 . . . . . . . . . 10 ((𝜑𝑦 = (𝑀 − 2)) → (𝑀 − 1) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}))))
304290, 303eqtrd 2775 . . . . . . . . 9 ((𝜑𝑦 = (𝑀 − 2)) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}))))
305 poimir.0 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℕ)
306 nnm1nn0 12565 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
307305, 306syl 17 . . . . . . . . . 10 (𝜑 → (𝑁 − 1) ∈ ℕ0)
308305nnred 12279 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℝ)
30946lem1d 12199 . . . . . . . . . . . . 13 (𝜑 → (𝑀 − 1) ≤ 𝑀)
310 elfzle2 13565 . . . . . . . . . . . . . 14 (𝑀 ∈ ((((2nd𝑇) + 1) + 1)...𝑁) → 𝑀𝑁)
31125, 310syl 17 . . . . . . . . . . . . 13 (𝜑𝑀𝑁)
312126, 46, 308, 309, 311letrd 11416 . . . . . . . . . . . 12 (𝜑 → (𝑀 − 1) ≤ 𝑁)
313126, 308, 59, 312lesub1dd 11877 . . . . . . . . . . 11 (𝜑 → ((𝑀 − 1) − 1) ≤ (𝑁 − 1))
314259, 313eqbrtrrd 5172 . . . . . . . . . 10 (𝜑 → (𝑀 − 2) ≤ (𝑁 − 1))
315 elfz2nn0 13655 . . . . . . . . . 10 ((𝑀 − 2) ∈ (0...(𝑁 − 1)) ↔ ((𝑀 − 2) ∈ ℕ0 ∧ (𝑁 − 1) ∈ ℕ0 ∧ (𝑀 − 2) ≤ (𝑁 − 1)))
316282, 307, 314, 315syl3anbrc 1342 . . . . . . . . 9 (𝜑 → (𝑀 − 2) ∈ (0...(𝑁 − 1)))
317 ovexd 7466 . . . . . . . . 9 (𝜑 → ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}))) ∈ V)
318254, 304, 316, 317fvmptd 7023 . . . . . . . 8 (𝜑 → (𝐹‘(𝑀 − 2)) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}))))
319318fveq1d 6909 . . . . . . 7 (𝜑 → ((𝐹‘(𝑀 − 2))‘𝑛) = (((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛))
320319adantr 480 . . . . . 6 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀))) → ((𝐹‘(𝑀 − 2))‘𝑛) = (((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛))
321 breq1 5151 . . . . . . . . . . . . . 14 (𝑦 = (𝑀 − 1) → (𝑦 < (2nd𝑇) ↔ (𝑀 − 1) < (2nd𝑇)))
322321adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑦 = (𝑀 − 1)) → (𝑦 < (2nd𝑇) ↔ (𝑀 − 1) < (2nd𝑇)))
323 oveq1 7438 . . . . . . . . . . . . . 14 (𝑦 = (𝑀 − 1) → (𝑦 + 1) = ((𝑀 − 1) + 1))
324323, 58sylan9eqr 2797 . . . . . . . . . . . . 13 ((𝜑𝑦 = (𝑀 − 1)) → (𝑦 + 1) = 𝑀)
325322, 324ifbieq2d 4557 . . . . . . . . . . . 12 ((𝜑𝑦 = (𝑀 − 1)) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) = if((𝑀 − 1) < (2nd𝑇), 𝑦, 𝑀))
32661lep1d 12197 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd𝑇) + 1) ≤ (((2nd𝑇) + 1) + 1))
32761, 60, 46, 326, 66letrd 11416 . . . . . . . . . . . . . . 15 (𝜑 → ((2nd𝑇) + 1) ≤ 𝑀)
328 1re 11259 . . . . . . . . . . . . . . . . . 18 1 ∈ ℝ
329 leaddsub 11737 . . . . . . . . . . . . . . . . . 18 (((2nd𝑇) ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑀 ∈ ℝ) → (((2nd𝑇) + 1) ≤ 𝑀 ↔ (2nd𝑇) ≤ (𝑀 − 1)))
330328, 329mp3an2 1448 . . . . . . . . . . . . . . . . 17 (((2nd𝑇) ∈ ℝ ∧ 𝑀 ∈ ℝ) → (((2nd𝑇) + 1) ≤ 𝑀 ↔ (2nd𝑇) ≤ (𝑀 − 1)))
331271, 46, 330syl2anc 584 . . . . . . . . . . . . . . . 16 (𝜑 → (((2nd𝑇) + 1) ≤ 𝑀 ↔ (2nd𝑇) ≤ (𝑀 − 1)))
332271, 126lenltd 11405 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd𝑇) ≤ (𝑀 − 1) ↔ ¬ (𝑀 − 1) < (2nd𝑇)))
333331, 332bitrd 279 . . . . . . . . . . . . . . 15 (𝜑 → (((2nd𝑇) + 1) ≤ 𝑀 ↔ ¬ (𝑀 − 1) < (2nd𝑇)))
334327, 333mpbid 232 . . . . . . . . . . . . . 14 (𝜑 → ¬ (𝑀 − 1) < (2nd𝑇))
335334iffalsed 4542 . . . . . . . . . . . . 13 (𝜑 → if((𝑀 − 1) < (2nd𝑇), 𝑦, 𝑀) = 𝑀)
336335adantr 480 . . . . . . . . . . . 12 ((𝜑𝑦 = (𝑀 − 1)) → if((𝑀 − 1) < (2nd𝑇), 𝑦, 𝑀) = 𝑀)
337325, 336eqtrd 2775 . . . . . . . . . . 11 ((𝜑𝑦 = (𝑀 − 1)) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) = 𝑀)
338337csbeq1d 3912 . . . . . . . . . 10 ((𝜑𝑦 = (𝑀 − 1)) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = 𝑀 / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
339 oveq2 7439 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑀 → (1...𝑗) = (1...𝑀))
340339imaeq2d 6080 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑀 → ((2nd ‘(1st𝑇)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...𝑀)))
341340xpeq1d 5718 . . . . . . . . . . . . . . 15 (𝑗 = 𝑀 → (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}))
342 oveq1 7438 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑀 → (𝑗 + 1) = (𝑀 + 1))
343342oveq1d 7446 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑀 → ((𝑗 + 1)...𝑁) = ((𝑀 + 1)...𝑁))
344343imaeq2d 6080 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑀 → ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)))
345344xpeq1d 5718 . . . . . . . . . . . . . . 15 (𝑗 = 𝑀 → (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))
346341, 345uneq12d 4179 . . . . . . . . . . . . . 14 (𝑗 = 𝑀 → ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))
347346oveq2d 7447 . . . . . . . . . . . . 13 (𝑗 = 𝑀 → ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
348347adantl 481 . . . . . . . . . . . 12 ((𝜑𝑗 = 𝑀) → ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
34925, 348csbied 3946 . . . . . . . . . . 11 (𝜑𝑀 / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
350349adantr 480 . . . . . . . . . 10 ((𝜑𝑦 = (𝑀 − 1)) → 𝑀 / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
351338, 350eqtrd 2775 . . . . . . . . 9 ((𝜑𝑦 = (𝑀 − 1)) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
352279nnnn0d 12585 . . . . . . . . . 10 (𝜑 → (𝑀 − 1) ∈ ℕ0)
35346, 308, 59, 311lesub1dd 11877 . . . . . . . . . 10 (𝜑 → (𝑀 − 1) ≤ (𝑁 − 1))
354 elfz2nn0 13655 . . . . . . . . . 10 ((𝑀 − 1) ∈ (0...(𝑁 − 1)) ↔ ((𝑀 − 1) ∈ ℕ0 ∧ (𝑁 − 1) ∈ ℕ0 ∧ (𝑀 − 1) ≤ (𝑁 − 1)))
355352, 307, 353, 354syl3anbrc 1342 . . . . . . . . 9 (𝜑 → (𝑀 − 1) ∈ (0...(𝑁 − 1)))
356 ovexd 7466 . . . . . . . . 9 (𝜑 → ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) ∈ V)
357254, 351, 355, 356fvmptd 7023 . . . . . . . 8 (𝜑 → (𝐹‘(𝑀 − 1)) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
358357fveq1d 6909 . . . . . . 7 (𝜑 → ((𝐹‘(𝑀 − 1))‘𝑛) = (((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛))
359358adantr 480 . . . . . 6 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀))) → ((𝐹‘(𝑀 − 1))‘𝑛) = (((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛))
360235, 320, 3593eqtr4d 2785 . . . . 5 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀))) → ((𝐹‘(𝑀 − 2))‘𝑛) = ((𝐹‘(𝑀 − 1))‘𝑛))
361360expr 456 . . . 4 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀) → ((𝐹‘(𝑀 − 2))‘𝑛) = ((𝐹‘(𝑀 − 1))‘𝑛)))
362361necon1d 2960 . . 3 ((𝜑𝑛 ∈ (1...𝑁)) → (((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛) → 𝑛 = ((2nd ‘(1st𝑇))‘𝑀)))
363 elmapi 8888 . . . . . . . . . . 11 ((1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾))
36429, 363syl 17 . . . . . . . . . 10 (𝜑 → (1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾))
365364, 27ffvelcdmd 7105 . . . . . . . . 9 (𝜑 → ((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) ∈ (0..^𝐾))
366 elfzonn0 13744 . . . . . . . . 9 (((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) ∈ (0..^𝐾) → ((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) ∈ ℕ0)
367365, 366syl 17 . . . . . . . 8 (𝜑 → ((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) ∈ ℕ0)
368367nn0red 12586 . . . . . . 7 (𝜑 → ((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) ∈ ℝ)
369368ltp1d 12196 . . . . . . 7 (𝜑 → ((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) < (((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) + 1))
370368, 369ltned 11395 . . . . . 6 (𝜑 → ((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) ≠ (((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) + 1))
371318fveq1d 6909 . . . . . . 7 (𝜑 → ((𝐹‘(𝑀 − 2))‘((2nd ‘(1st𝑇))‘𝑀)) = (((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})))‘((2nd ‘(1st𝑇))‘𝑀)))
372 ovexd 7466 . . . . . . . . 9 (𝜑 → (1...𝑁) ∈ V)
373 eqidd 2736 . . . . . . . . 9 ((𝜑 ∧ ((2nd ‘(1st𝑇))‘𝑀) ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) = ((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)))
374 fzss1 13600 . . . . . . . . . . . . . 14 (𝑀 ∈ (ℤ‘1) → (𝑀...𝑁) ⊆ (1...𝑁))
37571, 374syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑀...𝑁) ⊆ (1...𝑁))
376 eluzfz1 13568 . . . . . . . . . . . . . 14 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ (𝑀...𝑁))
37782, 376syl 17 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ (𝑀...𝑁))
378 fnfvima 7253 . . . . . . . . . . . . 13 (((2nd ‘(1st𝑇)) Fn (1...𝑁) ∧ (𝑀...𝑁) ⊆ (1...𝑁) ∧ 𝑀 ∈ (𝑀...𝑁)) → ((2nd ‘(1st𝑇))‘𝑀) ∈ ((2nd ‘(1st𝑇)) “ (𝑀...𝑁)))
379108, 375, 377, 378syl3anc 1370 . . . . . . . . . . . 12 (𝜑 → ((2nd ‘(1st𝑇))‘𝑀) ∈ ((2nd ‘(1st𝑇)) “ (𝑀...𝑁)))
380 fvun2 7001 . . . . . . . . . . . . 13 (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∧ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) ∧ ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∩ ((2nd ‘(1st𝑇)) “ (𝑀...𝑁))) = ∅ ∧ ((2nd ‘(1st𝑇))‘𝑀) ∈ ((2nd ‘(1st𝑇)) “ (𝑀...𝑁)))) → (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘𝑀)) = ((((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})‘((2nd ‘(1st𝑇))‘𝑀)))
38135, 38, 380mp3an12 1450 . . . . . . . . . . . 12 (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∩ ((2nd ‘(1st𝑇)) “ (𝑀...𝑁))) = ∅ ∧ ((2nd ‘(1st𝑇))‘𝑀) ∈ ((2nd ‘(1st𝑇)) “ (𝑀...𝑁))) → (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘𝑀)) = ((((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})‘((2nd ‘(1st𝑇))‘𝑀)))
38253, 379, 381syl2anc 584 . . . . . . . . . . 11 (𝜑 → (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘𝑀)) = ((((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})‘((2nd ‘(1st𝑇))‘𝑀)))
38336fvconst2 7224 . . . . . . . . . . . 12 (((2nd ‘(1st𝑇))‘𝑀) ∈ ((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) → ((((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})‘((2nd ‘(1st𝑇))‘𝑀)) = 0)
384379, 383syl 17 . . . . . . . . . . 11 (𝜑 → ((((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})‘((2nd ‘(1st𝑇))‘𝑀)) = 0)
385382, 384eqtrd 2775 . . . . . . . . . 10 (𝜑 → (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘𝑀)) = 0)
386385adantr 480 . . . . . . . . 9 ((𝜑 ∧ ((2nd ‘(1st𝑇))‘𝑀) ∈ (1...𝑁)) → (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘𝑀)) = 0)
38731, 98, 372, 372, 101, 373, 386ofval 7708 . . . . . . . 8 ((𝜑 ∧ ((2nd ‘(1st𝑇))‘𝑀) ∈ (1...𝑁)) → (((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})))‘((2nd ‘(1st𝑇))‘𝑀)) = (((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) + 0))
38827, 387mpdan 687 . . . . . . 7 (𝜑 → (((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})))‘((2nd ‘(1st𝑇))‘𝑀)) = (((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) + 0))
389367nn0cnd 12587 . . . . . . . 8 (𝜑 → ((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) ∈ ℂ)
390389addridd 11459 . . . . . . 7 (𝜑 → (((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) + 0) = ((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)))
391371, 388, 3903eqtrd 2779 . . . . . 6 (𝜑 → ((𝐹‘(𝑀 − 2))‘((2nd ‘(1st𝑇))‘𝑀)) = ((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)))
392357fveq1d 6909 . . . . . . 7 (𝜑 → ((𝐹‘(𝑀 − 1))‘((2nd ‘(1st𝑇))‘𝑀)) = (((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘((2nd ‘(1st𝑇))‘𝑀)))
393 fzss2 13601 . . . . . . . . . . . . . 14 (𝑁 ∈ (ℤ𝑀) → (1...𝑀) ⊆ (1...𝑁))
39482, 393syl 17 . . . . . . . . . . . . 13 (𝜑 → (1...𝑀) ⊆ (1...𝑁))
395 elfz1end 13591 . . . . . . . . . . . . . 14 (𝑀 ∈ ℕ ↔ 𝑀 ∈ (1...𝑀))
39670, 395sylib 218 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ (1...𝑀))
397 fnfvima 7253 . . . . . . . . . . . . 13 (((2nd ‘(1st𝑇)) Fn (1...𝑁) ∧ (1...𝑀) ⊆ (1...𝑁) ∧ 𝑀 ∈ (1...𝑀)) → ((2nd ‘(1st𝑇))‘𝑀) ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)))
398108, 394, 396, 397syl3anc 1370 . . . . . . . . . . . 12 (𝜑 → ((2nd ‘(1st𝑇))‘𝑀) ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)))
399 fvun1 7000 . . . . . . . . . . . . 13 (((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) ∧ ((((2nd ‘(1st𝑇)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅ ∧ ((2nd ‘(1st𝑇))‘𝑀) ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)))) → (((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘𝑀)) = ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1})‘((2nd ‘(1st𝑇))‘𝑀)))
400193, 122, 399mp3an12 1450 . . . . . . . . . . . 12 (((((2nd ‘(1st𝑇)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅ ∧ ((2nd ‘(1st𝑇))‘𝑀) ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → (((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘𝑀)) = ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1})‘((2nd ‘(1st𝑇))‘𝑀)))
401201, 398, 400syl2anc 584 . . . . . . . . . . 11 (𝜑 → (((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘𝑀)) = ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1})‘((2nd ‘(1st𝑇))‘𝑀)))
40233fvconst2 7224 . . . . . . . . . . . 12 (((2nd ‘(1st𝑇))‘𝑀) ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1})‘((2nd ‘(1st𝑇))‘𝑀)) = 1)
403398, 402syl 17 . . . . . . . . . . 11 (𝜑 → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1})‘((2nd ‘(1st𝑇))‘𝑀)) = 1)
404401, 403eqtrd 2775 . . . . . . . . . 10 (𝜑 → (((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘𝑀)) = 1)
405404adantr 480 . . . . . . . . 9 ((𝜑 ∧ ((2nd ‘(1st𝑇))‘𝑀) ∈ (1...𝑁)) → (((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘𝑀)) = 1)
40631, 209, 372, 372, 101, 373, 405ofval 7708 . . . . . . . 8 ((𝜑 ∧ ((2nd ‘(1st𝑇))‘𝑀) ∈ (1...𝑁)) → (((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘((2nd ‘(1st𝑇))‘𝑀)) = (((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) + 1))
40727, 406mpdan 687 . . . . . . 7 (𝜑 → (((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘((2nd ‘(1st𝑇))‘𝑀)) = (((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) + 1))
408392, 407eqtrd 2775 . . . . . 6 (𝜑 → ((𝐹‘(𝑀 − 1))‘((2nd ‘(1st𝑇))‘𝑀)) = (((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) + 1))
409370, 391, 4083netr4d 3016 . . . . 5 (𝜑 → ((𝐹‘(𝑀 − 2))‘((2nd ‘(1st𝑇))‘𝑀)) ≠ ((𝐹‘(𝑀 − 1))‘((2nd ‘(1st𝑇))‘𝑀)))
410 fveq2 6907 . . . . . 6 (𝑛 = ((2nd ‘(1st𝑇))‘𝑀) → ((𝐹‘(𝑀 − 2))‘𝑛) = ((𝐹‘(𝑀 − 2))‘((2nd ‘(1st𝑇))‘𝑀)))
411 fveq2 6907 . . . . . 6 (𝑛 = ((2nd ‘(1st𝑇))‘𝑀) → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝐹‘(𝑀 − 1))‘((2nd ‘(1st𝑇))‘𝑀)))
412410, 411neeq12d 3000 . . . . 5 (𝑛 = ((2nd ‘(1st𝑇))‘𝑀) → (((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛) ↔ ((𝐹‘(𝑀 − 2))‘((2nd ‘(1st𝑇))‘𝑀)) ≠ ((𝐹‘(𝑀 − 1))‘((2nd ‘(1st𝑇))‘𝑀))))
413409, 412syl5ibrcom 247 . . . 4 (𝜑 → (𝑛 = ((2nd ‘(1st𝑇))‘𝑀) → ((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛)))
414413adantr 480 . . 3 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑛 = ((2nd ‘(1st𝑇))‘𝑀) → ((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛)))
415362, 414impbid 212 . 2 ((𝜑𝑛 ∈ (1...𝑁)) → (((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛) ↔ 𝑛 = ((2nd ‘(1st𝑇))‘𝑀)))
41627, 415riota5 7417 1 (𝜑 → (𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛)) = ((2nd ‘(1st𝑇))‘𝑀))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395   = wceq 1537  wcel 2106  {cab 2712  wne 2938  {crab 3433  Vcvv 3478  csb 3908  cdif 3960  cun 3961  cin 3962  wss 3963  c0 4339  ifcif 4531  {csn 4631   class class class wbr 5148  cmpt 5231   × cxp 5687  ccnv 5688  cima 5692  Fun wfun 6557   Fn wfn 6558  wf 6559  ontowfo 6561  1-1-ontowf1o 6562  cfv 6563  crio 7387  (class class class)co 7431  f cof 7695  1st c1st 8011  2nd c2nd 8012  m cmap 8865  cc 11151  cr 11152  0cc0 11153  1c1 11154   + caddc 11156   < clt 11293  cle 11294  cmin 11490  cn 12264  2c2 12319  0cn0 12524  cz 12611  cuz 12876  ...cfz 13544  ..^cfzo 13691
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8013  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-er 8744  df-map 8867  df-en 8985  df-dom 8986  df-sdom 8987  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-nn 12265  df-2 12327  df-n0 12525  df-z 12612  df-uz 12877  df-fz 13545  df-fzo 13692
This theorem is referenced by:  poimirlem8  37615
  Copyright terms: Public domain W3C validator