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 32586
Description: Lemma for poimir 32612, similar to poimirlem6 32585, but for vertices after the opposite vertex. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0 (𝜑𝑁 ∈ ℕ)
poimirlem22.s 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((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 3328 . . . . . . . . 9 (𝑇 ∈ {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
3 poimirlem22.s . . . . . . . . 9 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
42, 3eleq2s 2706 . . . . . . . 8 (𝑇𝑆𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
51, 4syl 17 . . . . . . 7 (𝜑𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
6 xp1st 7089 . . . . . . 7 (𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
75, 6syl 17 . . . . . 6 (𝜑 → (1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
8 xp2nd 7090 . . . . . 6 ((1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (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 6113 . . . . . 6 (2nd ‘(1st𝑇)) ∈ V
11 f1oeq1 6040 . . . . . 6 (𝑓 = (2nd ‘(1st𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
1210, 11elab 3319 . . . . 5 ((2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
139, 12sylib 207 . . . 4 (𝜑 → (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
14 f1of 6050 . . . 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 12241 . . . . . . . . 9 ((2nd𝑇) ∈ (1...(𝑁 − 1)) → (2nd𝑇) ∈ ℕ)
1816, 17syl 17 . . . . . . . 8 (𝜑 → (2nd𝑇) ∈ ℕ)
1918peano2nnd 10914 . . . . . . 7 (𝜑 → ((2nd𝑇) + 1) ∈ ℕ)
2019peano2nnd 10914 . . . . . 6 (𝜑 → (((2nd𝑇) + 1) + 1) ∈ ℕ)
21 nnuz 11599 . . . . . 6 ℕ = (ℤ‘1)
2220, 21syl6eleq 2698 . . . . 5 (𝜑 → (((2nd𝑇) + 1) + 1) ∈ (ℤ‘1))
23 fzss1 12251 . . . . 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 3569 . . 3 (𝜑𝑀 ∈ (1...𝑁))
2715, 26ffvelrnd 6268 . 2 (𝜑 → ((2nd ‘(1st𝑇))‘𝑀) ∈ (1...𝑁))
28 xp1st 7089 . . . . . . . . . . . . 13 ((1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
297, 28syl 17 . . . . . . . . . . . 12 (𝜑 → (1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
30 elmapfn 7766 . . . . . . . . . . . 12 ((1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) → (1st ‘(1st𝑇)) Fn (1...𝑁))
3129, 30syl 17 . . . . . . . . . . 11 (𝜑 → (1st ‘(1st𝑇)) Fn (1...𝑁))
3231adantr 480 . . . . . . . . . 10 ((𝜑𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀)) → (1st ‘(1st𝑇)) Fn (1...𝑁))
33 1ex 9914 . . . . . . . . . . . . . . 15 1 ∈ V
34 fnconstg 6006 . . . . . . . . . . . . . . 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 9913 . . . . . . . . . . . . . . 15 0 ∈ V
37 fnconstg 6006 . . . . . . . . . . . . . . 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 6056 . . . . . . . . . . . . . . . . 17 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd ‘(1st𝑇))))
4140simprbi 479 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun (2nd ‘(1st𝑇)))
4213, 41syl 17 . . . . . . . . . . . . . . 15 (𝜑 → Fun (2nd ‘(1st𝑇)))
43 imain 5888 . . . . . . . . . . . . . . 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𝑇)) “ (𝑀...𝑁))))
45 elfzelz 12213 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ ((((2nd𝑇) + 1) + 1)...𝑁) → 𝑀 ∈ ℤ)
4625, 45syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑀 ∈ ℤ)
4746zred 11358 . . . . . . . . . . . . . . . . . 18 (𝜑𝑀 ∈ ℝ)
4847ltm1d 10835 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑀 − 1) < 𝑀)
49 fzdisj 12239 . . . . . . . . . . . . . . . . 17 ((𝑀 − 1) < 𝑀 → ((1...(𝑀 − 1)) ∩ (𝑀...𝑁)) = ∅)
5048, 49syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ((1...(𝑀 − 1)) ∩ (𝑀...𝑁)) = ∅)
5150imaeq2d 5385 . . . . . . . . . . . . . . 15 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = ((2nd ‘(1st𝑇)) “ ∅))
52 ima0 5400 . . . . . . . . . . . . . . 15 ((2nd ‘(1st𝑇)) “ ∅) = ∅
5351, 52syl6eq 2660 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = ∅)
5444, 53eqtr3d 2646 . . . . . . . . . . . . 13 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∩ ((2nd ‘(1st𝑇)) “ (𝑀...𝑁))) = ∅)
55 fnun 5911 . . . . . . . . . . . . 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𝑇)) “ (𝑀...𝑁))))
5639, 54, 55sylancr 694 . . . . . . . . . . . 12 (𝜑 → ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})) Fn (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd ‘(1st𝑇)) “ (𝑀...𝑁))))
5746zcnd 11359 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑀 ∈ ℂ)
58 npcan1 10334 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ ℂ → ((𝑀 − 1) + 1) = 𝑀)
5957, 58syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑀 − 1) + 1) = 𝑀)
60 1red 9934 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 1 ∈ ℝ)
6120nnred 10912 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((2nd𝑇) + 1) + 1) ∈ ℝ)
6219nnred 10912 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((2nd𝑇) + 1) ∈ ℝ)
6319nnge1d 10940 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → 1 ≤ ((2nd𝑇) + 1))
6462ltp1d 10833 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((2nd𝑇) + 1) < (((2nd𝑇) + 1) + 1))
6560, 62, 61, 63, 64lelttrd 10074 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 1 < (((2nd𝑇) + 1) + 1))
66 elfzle1 12215 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑀 ∈ ((((2nd𝑇) + 1) + 1)...𝑁) → (((2nd𝑇) + 1) + 1) ≤ 𝑀)
6725, 66syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (((2nd𝑇) + 1) + 1) ≤ 𝑀)
6860, 61, 47, 65, 67ltletrd 10076 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 1 < 𝑀)
6960, 47, 68ltled 10064 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 1 ≤ 𝑀)
70 elnnz1 11280 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 ∈ ℕ ↔ (𝑀 ∈ ℤ ∧ 1 ≤ 𝑀))
7146, 69, 70sylanbrc 695 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑀 ∈ ℕ)
7271, 21syl6eleq 2698 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑀 ∈ (ℤ‘1))
7359, 72eqeltrd 2688 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑀 − 1) + 1) ∈ (ℤ‘1))
74 peano2zm 11297 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀 ∈ ℤ → (𝑀 − 1) ∈ ℤ)
7546, 74syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑀 − 1) ∈ ℤ)
76 uzid 11578 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑀 − 1) ∈ ℤ → (𝑀 − 1) ∈ (ℤ‘(𝑀 − 1)))
77 peano2uz 11617 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑀 − 1) ∈ (ℤ‘(𝑀 − 1)) → ((𝑀 − 1) + 1) ∈ (ℤ‘(𝑀 − 1)))
7875, 76, 773syl 18 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑀 − 1) + 1) ∈ (ℤ‘(𝑀 − 1)))
7959, 78eqeltrrd 2689 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑀 ∈ (ℤ‘(𝑀 − 1)))
80 uzss 11584 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ (ℤ‘(𝑀 − 1)) → (ℤ𝑀) ⊆ (ℤ‘(𝑀 − 1)))
8179, 80syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (ℤ𝑀) ⊆ (ℤ‘(𝑀 − 1)))
82 elfzuz3 12210 . . . . . . . . . . . . . . . . . . . 20 (𝑀 ∈ ((((2nd𝑇) + 1) + 1)...𝑁) → 𝑁 ∈ (ℤ𝑀))
8325, 82syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ (ℤ𝑀))
8481, 83sseldd 3569 . . . . . . . . . . . . . . . . . 18 (𝜑𝑁 ∈ (ℤ‘(𝑀 − 1)))
85 fzsplit2 12237 . . . . . . . . . . . . . . . . . 18 ((((𝑀 − 1) + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ‘(𝑀 − 1))) → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁)))
8673, 84, 85syl2anc 691 . . . . . . . . . . . . . . . . 17 (𝜑 → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁)))
8759oveq1d 6564 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝑀 − 1) + 1)...𝑁) = (𝑀...𝑁))
8887uneq2d 3729 . . . . . . . . . . . . . . . . 17 (𝜑 → ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁)) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑁)))
8986, 88eqtrd 2644 . . . . . . . . . . . . . . . 16 (𝜑 → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑁)))
9089imaeq2d 5385 . . . . . . . . . . . . . . 15 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = ((2nd ‘(1st𝑇)) “ ((1...(𝑀 − 1)) ∪ (𝑀...𝑁))))
91 imaundi 5464 . . . . . . . . . . . . . . 15 ((2nd ‘(1st𝑇)) “ ((1...(𝑀 − 1)) ∪ (𝑀...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd ‘(1st𝑇)) “ (𝑀...𝑁)))
9290, 91syl6eq 2660 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd ‘(1st𝑇)) “ (𝑀...𝑁))))
93 f1ofo 6057 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁))
9413, 93syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁))
95 foima 6033 . . . . . . . . . . . . . . 15 ((2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
9694, 95syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
9792, 96eqtr3d 2646 . . . . . . . . . . . . 13 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd ‘(1st𝑇)) “ (𝑀...𝑁))) = (1...𝑁))
9897fneq2d 5896 . . . . . . . . . . . 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...𝑁)))
9956, 98mpbid 221 . . . . . . . . . . 11 (𝜑 → ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})) Fn (1...𝑁))
10099adantr 480 . . . . . . . . . 10 ((𝜑𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀)) → ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})) Fn (1...𝑁))
101 ovex 6577 . . . . . . . . . . 11 (1...𝑁) ∈ V
102101a1i 11 . . . . . . . . . 10 ((𝜑𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀)) → (1...𝑁) ∈ V)
103 inidm 3784 . . . . . . . . . 10 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
104 eqidd 2611 . . . . . . . . . 10 (((𝜑𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑛) = ((1st ‘(1st𝑇))‘𝑛))
105 imaundi 5464 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑇)) “ ({𝑀} ∪ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ {𝑀}) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)))
106 fzpred 12259 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ (ℤ𝑀) → (𝑀...𝑁) = ({𝑀} ∪ ((𝑀 + 1)...𝑁)))
10783, 106syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑀...𝑁) = ({𝑀} ∪ ((𝑀 + 1)...𝑁)))
108107imaeq2d 5385 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) = ((2nd ‘(1st𝑇)) “ ({𝑀} ∪ ((𝑀 + 1)...𝑁))))
109 f1ofn 6051 . . . . . . . . . . . . . . . . . . . . 21 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)) Fn (1...𝑁))
11013, 109syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (2nd ‘(1st𝑇)) Fn (1...𝑁))
111 fnsnfv 6168 . . . . . . . . . . . . . . . . . . . 20 (((2nd ‘(1st𝑇)) Fn (1...𝑁) ∧ 𝑀 ∈ (1...𝑁)) → {((2nd ‘(1st𝑇))‘𝑀)} = ((2nd ‘(1st𝑇)) “ {𝑀}))
112110, 26, 111syl2anc 691 . . . . . . . . . . . . . . . . . . 19 (𝜑 → {((2nd ‘(1st𝑇))‘𝑀)} = ((2nd ‘(1st𝑇)) “ {𝑀}))
113112uneq1d 3728 . . . . . . . . . . . . . . . . . 18 (𝜑 → ({((2nd ‘(1st𝑇))‘𝑀)} ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ {𝑀}) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))))
114105, 108, 1133eqtr4a 2670 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) = ({((2nd ‘(1st𝑇))‘𝑀)} ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))))
115114xpeq1d 5062 . . . . . . . . . . . . . . . 16 (𝜑 → (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}) = (({((2nd ‘(1st𝑇))‘𝑀)} ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))) × {0}))
116 xpundir 5095 . . . . . . . . . . . . . . . 16 (({((2nd ‘(1st𝑇))‘𝑀)} ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))) × {0}) = (({((2nd ‘(1st𝑇))‘𝑀)} × {0}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))
117115, 116syl6eq 2660 . . . . . . . . . . . . . . 15 (𝜑 → (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}) = (({((2nd ‘(1st𝑇))‘𝑀)} × {0}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))
118117uneq2d 3729 . . . . . . . . . . . . . 14 (𝜑 → ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (({((2nd ‘(1st𝑇))‘𝑀)} × {0}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
119 un12 3733 . . . . . . . . . . . . . 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})))
120118, 119syl6eq 2660 . . . . . . . . . . . . 13 (𝜑 → ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})) = (({((2nd ‘(1st𝑇))‘𝑀)} × {0}) ∪ ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
121120fveq1d 6105 . . . . . . . . . . . 12 (𝜑 → (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}))‘𝑛) = ((({((2nd ‘(1st𝑇))‘𝑀)} × {0}) ∪ ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛))
122121ad2antrr 758 . . . . . . . . . . 11 (((𝜑𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}))‘𝑛) = ((({((2nd ‘(1st𝑇))‘𝑀)} × {0}) ∪ ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛))
123 fnconstg 6006 . . . . . . . . . . . . . . . . 17 (0 ∈ V → (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)))
12436, 123ax-mp 5 . . . . . . . . . . . . . . . 16 (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))
12535, 124pm3.2i 470 . . . . . . . . . . . . . . 15 ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∧ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)))
126 imain 5888 . . . . . . . . . . . . . . . . 17 (Fun (2nd ‘(1st𝑇)) → ((2nd ‘(1st𝑇)) “ ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∩ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))))
12742, 126syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∩ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))))
12875zred 11358 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑀 − 1) ∈ ℝ)
129 peano2re 10088 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 ∈ ℝ → (𝑀 + 1) ∈ ℝ)
13047, 129syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑀 + 1) ∈ ℝ)
13147ltp1d 10833 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑀 < (𝑀 + 1))
132128, 47, 130, 48, 131lttrd 10077 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑀 − 1) < (𝑀 + 1))
133 fzdisj 12239 . . . . . . . . . . . . . . . . . . 19 ((𝑀 − 1) < (𝑀 + 1) → ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁)) = ∅)
134132, 133syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁)) = ∅)
135134imaeq2d 5385 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁))) = ((2nd ‘(1st𝑇)) “ ∅))
136135, 52syl6eq 2660 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...(𝑀 − 1)) ∩ ((𝑀 + 1)...𝑁))) = ∅)
137127, 136eqtr3d 2646 . . . . . . . . . . . . . . 15 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∩ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅)
138 fnun 5911 . . . . . . . . . . . . . . 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)...𝑁))))
139125, 137, 138sylancr 694 . . . . . . . . . . . . . 14 (𝜑 → ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))))
140 imaundi 5464 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑇)) “ ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)))
141 imadif 5887 . . . . . . . . . . . . . . . . . 18 (Fun (2nd ‘(1st𝑇)) → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {𝑀})) = (((2nd ‘(1st𝑇)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑇)) “ {𝑀})))
14242, 141syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {𝑀})) = (((2nd ‘(1st𝑇)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑇)) “ {𝑀})))
143 fzsplit 12238 . . . . . . . . . . . . . . . . . . . . 21 (𝑀 ∈ (1...𝑁) → (1...𝑁) = ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)))
14426, 143syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (1...𝑁) = ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)))
145144difeq1d 3689 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((1...𝑁) ∖ {𝑀}) = (((1...𝑀) ∪ ((𝑀 + 1)...𝑁)) ∖ {𝑀}))
146 difundir 3839 . . . . . . . . . . . . . . . . . . . 20 (((1...𝑀) ∪ ((𝑀 + 1)...𝑁)) ∖ {𝑀}) = (((1...𝑀) ∖ {𝑀}) ∪ (((𝑀 + 1)...𝑁) ∖ {𝑀}))
147 fzsplit2 12237 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑀 − 1) + 1) ∈ (ℤ‘1) ∧ 𝑀 ∈ (ℤ‘(𝑀 − 1))) → (1...𝑀) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑀)))
14873, 79, 147syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (1...𝑀) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑀)))
14959oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (((𝑀 − 1) + 1)...𝑀) = (𝑀...𝑀))
150 fzsn 12254 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀})
15146, 150syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝑀...𝑀) = {𝑀})
152149, 151eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (((𝑀 − 1) + 1)...𝑀) = {𝑀})
153152uneq2d 3729 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑀)) = ((1...(𝑀 − 1)) ∪ {𝑀}))
154148, 153eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1...𝑀) = ((1...(𝑀 − 1)) ∪ {𝑀}))
155154difeq1d 3689 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((1...𝑀) ∖ {𝑀}) = (((1...(𝑀 − 1)) ∪ {𝑀}) ∖ {𝑀}))
156 difun2 4000 . . . . . . . . . . . . . . . . . . . . . . 23 (((1...(𝑀 − 1)) ∪ {𝑀}) ∖ {𝑀}) = ((1...(𝑀 − 1)) ∖ {𝑀})
157128, 47ltnled 10063 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ((𝑀 − 1) < 𝑀 ↔ ¬ 𝑀 ≤ (𝑀 − 1)))
15848, 157mpbid 221 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ¬ 𝑀 ≤ (𝑀 − 1))
159 elfzle2 12216 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑀 ∈ (1...(𝑀 − 1)) → 𝑀 ≤ (𝑀 − 1))
160158, 159nsyl 134 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ¬ 𝑀 ∈ (1...(𝑀 − 1)))
161 difsn 4269 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑀 ∈ (1...(𝑀 − 1)) → ((1...(𝑀 − 1)) ∖ {𝑀}) = (1...(𝑀 − 1)))
162160, 161syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((1...(𝑀 − 1)) ∖ {𝑀}) = (1...(𝑀 − 1)))
163156, 162syl5eq 2656 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((1...(𝑀 − 1)) ∪ {𝑀}) ∖ {𝑀}) = (1...(𝑀 − 1)))
164155, 163eqtrd 2644 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((1...𝑀) ∖ {𝑀}) = (1...(𝑀 − 1)))
16547, 130ltnled 10063 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑀 < (𝑀 + 1) ↔ ¬ (𝑀 + 1) ≤ 𝑀))
166131, 165mpbid 221 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ¬ (𝑀 + 1) ≤ 𝑀)
167 elfzle1 12215 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀 ∈ ((𝑀 + 1)...𝑁) → (𝑀 + 1) ≤ 𝑀)
168166, 167nsyl 134 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ¬ 𝑀 ∈ ((𝑀 + 1)...𝑁))
169 difsn 4269 . . . . . . . . . . . . . . . . . . . . . 22 𝑀 ∈ ((𝑀 + 1)...𝑁) → (((𝑀 + 1)...𝑁) ∖ {𝑀}) = ((𝑀 + 1)...𝑁))
170168, 169syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (((𝑀 + 1)...𝑁) ∖ {𝑀}) = ((𝑀 + 1)...𝑁))
171164, 170uneq12d 3730 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((1...𝑀) ∖ {𝑀}) ∪ (((𝑀 + 1)...𝑁) ∖ {𝑀})) = ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁)))
172146, 171syl5eq 2656 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (((1...𝑀) ∪ ((𝑀 + 1)...𝑁)) ∖ {𝑀}) = ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁)))
173145, 172eqtrd 2644 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((1...𝑁) ∖ {𝑀}) = ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁)))
174173imaeq2d 5385 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑁) ∖ {𝑀})) = ((2nd ‘(1st𝑇)) “ ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁))))
175112eqcomd 2616 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((2nd ‘(1st𝑇)) “ {𝑀}) = {((2nd ‘(1st𝑇))‘𝑀)})
17696, 175difeq12d 3691 . . . . . . . . . . . . . . . . 17 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑇)) “ {𝑀})) = ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑀)}))
177142, 174, 1763eqtr3d 2652 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...(𝑀 − 1)) ∪ ((𝑀 + 1)...𝑁))) = ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑀)}))
178140, 177syl5eqr 2658 . . . . . . . . . . . . . . 15 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))) = ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑀)}))
179178fneq2d 5896 . . . . . . . . . . . . . 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𝑇))‘𝑀)})))
180139, 179mpbid 221 . . . . . . . . . . . . 13 (𝜑 → ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑀)}))
181 eldifsn 4260 . . . . . . . . . . . . . . 15 (𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑀)}) ↔ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀)))
182181biimpri 217 . . . . . . . . . . . . . 14 ((𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀)) → 𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑀)}))
183182ancoms 468 . . . . . . . . . . . . 13 ((𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀) ∧ 𝑛 ∈ (1...𝑁)) → 𝑛 ∈ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑀)}))
184 disjdif 3992 . . . . . . . . . . . . . 14 ({((2nd ‘(1st𝑇))‘𝑀)} ∩ ((1...𝑁) ∖ {((2nd ‘(1st𝑇))‘𝑀)})) = ∅
185 fnconstg 6006 . . . . . . . . . . . . . . . 16 (0 ∈ V → ({((2nd ‘(1st𝑇))‘𝑀)} × {0}) Fn {((2nd ‘(1st𝑇))‘𝑀)})
18636, 185ax-mp 5 . . . . . . . . . . . . . . 15 ({((2nd ‘(1st𝑇))‘𝑀)} × {0}) Fn {((2nd ‘(1st𝑇))‘𝑀)}
187 fvun2 6180 . . . . . . . . . . . . . . 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}))‘𝑛))
188186, 187mp3an1 1403 . . . . . . . . . . . . . 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}))‘𝑛))
189184, 188mpanr1 715 . . . . . . . . . . . . 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}))‘𝑛))
190180, 183, 189syl2an 493 . . . . . . . . . . . 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}))‘𝑛))
191190anassrs 678 . . . . . . . . . . 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}))‘𝑛))
192122, 191eqtrd 2644 . . . . . . . . . 10 (((𝜑𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}))‘𝑛) = (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛))
19332, 100, 102, 102, 103, 104, 192ofval 6804 . . . . . . . . 9 (((𝜑𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛) = (((1st ‘(1st𝑇))‘𝑛) + (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛)))
194 fnconstg 6006 . . . . . . . . . . . . . . 15 (1 ∈ V → (((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...𝑀)))
19533, 194ax-mp 5 . . . . . . . . . . . . . 14 (((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...𝑀))
196195, 124pm3.2i 470 . . . . . . . . . . . . 13 ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)))
197 imain 5888 . . . . . . . . . . . . . . 15 (Fun (2nd ‘(1st𝑇)) → ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))))
19842, 197syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))))
199 fzdisj 12239 . . . . . . . . . . . . . . . . 17 (𝑀 < (𝑀 + 1) → ((1...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅)
200131, 199syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ((1...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅)
201200imaeq2d 5385 . . . . . . . . . . . . . . 15 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ((2nd ‘(1st𝑇)) “ ∅))
202201, 52syl6eq 2660 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ∅)
203198, 202eqtr3d 2646 . . . . . . . . . . . . 13 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅)
204 fnun 5911 . . . . . . . . . . . . 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)...𝑁))))
205196, 203, 204sylancr 694 . . . . . . . . . . . 12 (𝜑 → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))))
206144imaeq2d 5385 . . . . . . . . . . . . . . 15 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))))
207 imaundi 5464 . . . . . . . . . . . . . . 15 ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)))
208206, 207syl6eq 2660 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))))
209208, 96eqtr3d 2646 . . . . . . . . . . . . 13 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))) = (1...𝑁))
210209fneq2d 5896 . . . . . . . . . . . 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...𝑁)))
211205, 210mpbid 221 . . . . . . . . . . 11 (𝜑 → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
212211adantr 480 . . . . . . . . . 10 ((𝜑𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀)) → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
213 imaundi 5464 . . . . . . . . . . . . . . . . . 18 ((2nd ‘(1st𝑇)) “ ((1...(𝑀 − 1)) ∪ {𝑀})) = (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd ‘(1st𝑇)) “ {𝑀}))
214154imaeq2d 5385 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑀)) = ((2nd ‘(1st𝑇)) “ ((1...(𝑀 − 1)) ∪ {𝑀})))
215112uneq2d 3729 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∪ {((2nd ‘(1st𝑇))‘𝑀)}) = (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∪ ((2nd ‘(1st𝑇)) “ {𝑀})))
216213, 214, 2153eqtr4a 2670 . . . . . . . . . . . . . . . . 17 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑀)) = (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∪ {((2nd ‘(1st𝑇))‘𝑀)}))
217216xpeq1d 5062 . . . . . . . . . . . . . . . 16 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) = ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∪ {((2nd ‘(1st𝑇))‘𝑀)}) × {1}))
218 xpundir 5095 . . . . . . . . . . . . . . . 16 ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) ∪ {((2nd ‘(1st𝑇))‘𝑀)}) × {1}) = ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ ({((2nd ‘(1st𝑇))‘𝑀)} × {1}))
219217, 218syl6eq 2660 . . . . . . . . . . . . . . 15 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) = ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ ({((2nd ‘(1st𝑇))‘𝑀)} × {1})))
220219uneq1d 3728 . . . . . . . . . . . . . 14 (𝜑 → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) = (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ ({((2nd ‘(1st𝑇))‘𝑀)} × {1})) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))
221 un23 3734 . . . . . . . . . . . . . . 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}))
222221equncomi 3721 . . . . . . . . . . . . . 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})))
223220, 222syl6eq 2660 . . . . . . . . . . . . 13 (𝜑 → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) = (({((2nd ‘(1st𝑇))‘𝑀)} × {1}) ∪ ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
224223fveq1d 6105 . . . . . . . . . . . 12 (𝜑 → (((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛) = ((({((2nd ‘(1st𝑇))‘𝑀)} × {1}) ∪ ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛))
225224ad2antrr 758 . . . . . . . . . . 11 (((𝜑𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛) = ((({((2nd ‘(1st𝑇))‘𝑀)} × {1}) ∪ ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛))
226 fnconstg 6006 . . . . . . . . . . . . . . . 16 (1 ∈ V → ({((2nd ‘(1st𝑇))‘𝑀)} × {1}) Fn {((2nd ‘(1st𝑇))‘𝑀)})
22733, 226ax-mp 5 . . . . . . . . . . . . . . 15 ({((2nd ‘(1st𝑇))‘𝑀)} × {1}) Fn {((2nd ‘(1st𝑇))‘𝑀)}
228 fvun2 6180 . . . . . . . . . . . . . . 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}))‘𝑛))
229227, 228mp3an1 1403 . . . . . . . . . . . . . 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}))‘𝑛))
230184, 229mpanr1 715 . . . . . . . . . . . . 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}))‘𝑛))
231180, 183, 230syl2an 493 . . . . . . . . . . . 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}))‘𝑛))
232231anassrs 678 . . . . . . . . . . 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}))‘𝑛))
233225, 232eqtrd 2644 . . . . . . . . . 10 (((𝜑𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛) = (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛))
23432, 212, 102, 102, 103, 104, 233ofval 6804 . . . . . . . . 9 (((𝜑𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛) = (((1st ‘(1st𝑇))‘𝑛) + (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑛)))
235193, 234eqtr4d 2647 . . . . . . . 8 (((𝜑𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀)) ∧ 𝑛 ∈ (1...𝑁)) → (((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛) = (((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛))
236235an32s 842 . . . . . . 7 (((𝜑𝑛 ∈ (1...𝑁)) ∧ 𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀)) → (((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛) = (((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛))
237236anasss 677 . . . . . 6 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀))) → (((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛) = (((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛))
238 fveq2 6103 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑇 → (2nd𝑡) = (2nd𝑇))
239238breq2d 4595 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑇 → (𝑦 < (2nd𝑡) ↔ 𝑦 < (2nd𝑇)))
240239ifbid 4058 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑇 → if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)))
241240csbeq1d 3506 . . . . . . . . . . . . . . 15 (𝑡 = 𝑇if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))
242 fveq2 6103 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑇 → (1st𝑡) = (1st𝑇))
243242fveq2d 6107 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑇 → (1st ‘(1st𝑡)) = (1st ‘(1st𝑇)))
244242fveq2d 6107 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑇 → (2nd ‘(1st𝑡)) = (2nd ‘(1st𝑇)))
245244imaeq1d 5384 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...𝑗)))
246245xpeq1d 5062 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}))
247244imaeq1d 5384 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)))
248247xpeq1d 5062 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
249246, 248uneq12d 3730 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑇 → ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))
250243, 249oveq12d 6567 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑇 → ((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
251250csbeq2dv 3944 . . . . . . . . . . . . . . 15 (𝑡 = 𝑇if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
252241, 251eqtrd 2644 . . . . . . . . . . . . . 14 (𝑡 = 𝑇if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
253252mpteq2dv 4673 . . . . . . . . . . . . 13 (𝑡 = 𝑇 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
254253eqeq2d 2620 . . . . . . . . . . . 12 (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
255254, 3elrab2 3333 . . . . . . . . . . 11 (𝑇𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
256255simprbi 479 . . . . . . . . . 10 (𝑇𝑆𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
2571, 256syl 17 . . . . . . . . 9 (𝜑𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
258 breq1 4586 . . . . . . . . . . . . . 14 (𝑦 = (𝑀 − 2) → (𝑦 < (2nd𝑇) ↔ (𝑀 − 2) < (2nd𝑇)))
259258adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑦 = (𝑀 − 2)) → (𝑦 < (2nd𝑇) ↔ (𝑀 − 2) < (2nd𝑇)))
260 oveq1 6556 . . . . . . . . . . . . . 14 (𝑦 = (𝑀 − 2) → (𝑦 + 1) = ((𝑀 − 2) + 1))
261 sub1m1 11161 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ ℂ → ((𝑀 − 1) − 1) = (𝑀 − 2))
26257, 261syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑀 − 1) − 1) = (𝑀 − 2))
263262oveq1d 6564 . . . . . . . . . . . . . . 15 (𝜑 → (((𝑀 − 1) − 1) + 1) = ((𝑀 − 2) + 1))
26475zcnd 11359 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑀 − 1) ∈ ℂ)
265 npcan1 10334 . . . . . . . . . . . . . . . 16 ((𝑀 − 1) ∈ ℂ → (((𝑀 − 1) − 1) + 1) = (𝑀 − 1))
266264, 265syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (((𝑀 − 1) − 1) + 1) = (𝑀 − 1))
267263, 266eqtr3d 2646 . . . . . . . . . . . . . 14 (𝜑 → ((𝑀 − 2) + 1) = (𝑀 − 1))
268260, 267sylan9eqr 2666 . . . . . . . . . . . . 13 ((𝜑𝑦 = (𝑀 − 2)) → (𝑦 + 1) = (𝑀 − 1))
269259, 268ifbieq2d 4061 . . . . . . . . . . . 12 ((𝜑𝑦 = (𝑀 − 2)) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) = if((𝑀 − 2) < (2nd𝑇), 𝑦, (𝑀 − 1)))
27018nncnd 10913 . . . . . . . . . . . . . . . . 17 (𝜑 → (2nd𝑇) ∈ ℂ)
271 add1p1 11160 . . . . . . . . . . . . . . . . 17 ((2nd𝑇) ∈ ℂ → (((2nd𝑇) + 1) + 1) = ((2nd𝑇) + 2))
272270, 271syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (((2nd𝑇) + 1) + 1) = ((2nd𝑇) + 2))
273272, 67eqbrtrrd 4607 . . . . . . . . . . . . . . 15 (𝜑 → ((2nd𝑇) + 2) ≤ 𝑀)
27418nnred 10912 . . . . . . . . . . . . . . . . 17 (𝜑 → (2nd𝑇) ∈ ℝ)
275 2re 10967 . . . . . . . . . . . . . . . . . 18 2 ∈ ℝ
276 leaddsub 10383 . . . . . . . . . . . . . . . . . 18 (((2nd𝑇) ∈ ℝ ∧ 2 ∈ ℝ ∧ 𝑀 ∈ ℝ) → (((2nd𝑇) + 2) ≤ 𝑀 ↔ (2nd𝑇) ≤ (𝑀 − 2)))
277275, 276mp3an2 1404 . . . . . . . . . . . . . . . . 17 (((2nd𝑇) ∈ ℝ ∧ 𝑀 ∈ ℝ) → (((2nd𝑇) + 2) ≤ 𝑀 ↔ (2nd𝑇) ≤ (𝑀 − 2)))
278274, 47, 277syl2anc 691 . . . . . . . . . . . . . . . 16 (𝜑 → (((2nd𝑇) + 2) ≤ 𝑀 ↔ (2nd𝑇) ≤ (𝑀 − 2)))
27960, 47posdifd 10493 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (1 < 𝑀 ↔ 0 < (𝑀 − 1)))
28068, 279mpbid 221 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 0 < (𝑀 − 1))
281 elnnz 11264 . . . . . . . . . . . . . . . . . . . . 21 ((𝑀 − 1) ∈ ℕ ↔ ((𝑀 − 1) ∈ ℤ ∧ 0 < (𝑀 − 1)))
28275, 280, 281sylanbrc 695 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑀 − 1) ∈ ℕ)
283 nnm1nn0 11211 . . . . . . . . . . . . . . . . . . . 20 ((𝑀 − 1) ∈ ℕ → ((𝑀 − 1) − 1) ∈ ℕ0)
284282, 283syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑀 − 1) − 1) ∈ ℕ0)
285262, 284eqeltrrd 2689 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑀 − 2) ∈ ℕ0)
286285nn0red 11229 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑀 − 2) ∈ ℝ)
287274, 286lenltd 10062 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd𝑇) ≤ (𝑀 − 2) ↔ ¬ (𝑀 − 2) < (2nd𝑇)))
288278, 287bitrd 267 . . . . . . . . . . . . . . 15 (𝜑 → (((2nd𝑇) + 2) ≤ 𝑀 ↔ ¬ (𝑀 − 2) < (2nd𝑇)))
289273, 288mpbid 221 . . . . . . . . . . . . . 14 (𝜑 → ¬ (𝑀 − 2) < (2nd𝑇))
290289iffalsed 4047 . . . . . . . . . . . . 13 (𝜑 → if((𝑀 − 2) < (2nd𝑇), 𝑦, (𝑀 − 1)) = (𝑀 − 1))
291290adantr 480 . . . . . . . . . . . 12 ((𝜑𝑦 = (𝑀 − 2)) → if((𝑀 − 2) < (2nd𝑇), 𝑦, (𝑀 − 1)) = (𝑀 − 1))
292269, 291eqtrd 2644 . . . . . . . . . . 11 ((𝜑𝑦 = (𝑀 − 2)) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) = (𝑀 − 1))
293292csbeq1d 3506 . . . . . . . . . 10 ((𝜑𝑦 = (𝑀 − 2)) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑀 − 1) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
294 oveq2 6557 . . . . . . . . . . . . . . . . 17 (𝑗 = (𝑀 − 1) → (1...𝑗) = (1...(𝑀 − 1)))
295294imaeq2d 5385 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑀 − 1) → ((2nd ‘(1st𝑇)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))))
296295xpeq1d 5062 . . . . . . . . . . . . . . 15 (𝑗 = (𝑀 − 1) → (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}))
297296adantl 481 . . . . . . . . . . . . . 14 ((𝜑𝑗 = (𝑀 − 1)) → (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}))
298 oveq1 6556 . . . . . . . . . . . . . . . . . 18 (𝑗 = (𝑀 − 1) → (𝑗 + 1) = ((𝑀 − 1) + 1))
299298, 59sylan9eqr 2666 . . . . . . . . . . . . . . . . 17 ((𝜑𝑗 = (𝑀 − 1)) → (𝑗 + 1) = 𝑀)
300299oveq1d 6564 . . . . . . . . . . . . . . . 16 ((𝜑𝑗 = (𝑀 − 1)) → ((𝑗 + 1)...𝑁) = (𝑀...𝑁))
301300imaeq2d 5385 . . . . . . . . . . . . . . 15 ((𝜑𝑗 = (𝑀 − 1)) → ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ (𝑀...𝑁)))
302301xpeq1d 5062 . . . . . . . . . . . . . 14 ((𝜑𝑗 = (𝑀 − 1)) → (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}))
303297, 302uneq12d 3730 . . . . . . . . . . . . 13 ((𝜑𝑗 = (𝑀 − 1)) → ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})))
304303oveq2d 6565 . . . . . . . . . . . 12 ((𝜑𝑗 = (𝑀 − 1)) → ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}))))
30575, 304csbied 3526 . . . . . . . . . . 11 (𝜑(𝑀 − 1) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}))))
306305adantr 480 . . . . . . . . . 10 ((𝜑𝑦 = (𝑀 − 2)) → (𝑀 − 1) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}))))
307293, 306eqtrd 2644 . . . . . . . . 9 ((𝜑𝑦 = (𝑀 − 2)) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}))))
308 poimir.0 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℕ)
309 nnm1nn0 11211 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
310308, 309syl 17 . . . . . . . . . 10 (𝜑 → (𝑁 − 1) ∈ ℕ0)
311308nnred 10912 . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℝ)
31247lem1d 10836 . . . . . . . . . . . . 13 (𝜑 → (𝑀 − 1) ≤ 𝑀)
313 elfzle2 12216 . . . . . . . . . . . . . 14 (𝑀 ∈ ((((2nd𝑇) + 1) + 1)...𝑁) → 𝑀𝑁)
31425, 313syl 17 . . . . . . . . . . . . 13 (𝜑𝑀𝑁)
315128, 47, 311, 312, 314letrd 10073 . . . . . . . . . . . 12 (𝜑 → (𝑀 − 1) ≤ 𝑁)
316128, 311, 60, 315lesub1dd 10522 . . . . . . . . . . 11 (𝜑 → ((𝑀 − 1) − 1) ≤ (𝑁 − 1))
317262, 316eqbrtrrd 4607 . . . . . . . . . 10 (𝜑 → (𝑀 − 2) ≤ (𝑁 − 1))
318 elfz2nn0 12300 . . . . . . . . . 10 ((𝑀 − 2) ∈ (0...(𝑁 − 1)) ↔ ((𝑀 − 2) ∈ ℕ0 ∧ (𝑁 − 1) ∈ ℕ0 ∧ (𝑀 − 2) ≤ (𝑁 − 1)))
319285, 310, 317, 318syl3anbrc 1239 . . . . . . . . 9 (𝜑 → (𝑀 − 2) ∈ (0...(𝑁 − 1)))
320 ovex 6577 . . . . . . . . . 10 ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}))) ∈ V
321320a1i 11 . . . . . . . . 9 (𝜑 → ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}))) ∈ V)
322257, 307, 319, 321fvmptd 6197 . . . . . . . 8 (𝜑 → (𝐹‘(𝑀 − 2)) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}))))
323322fveq1d 6105 . . . . . . 7 (𝜑 → ((𝐹‘(𝑀 − 2))‘𝑛) = (((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛))
324323adantr 480 . . . . . 6 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀))) → ((𝐹‘(𝑀 − 2))‘𝑛) = (((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})))‘𝑛))
325 breq1 4586 . . . . . . . . . . . . . 14 (𝑦 = (𝑀 − 1) → (𝑦 < (2nd𝑇) ↔ (𝑀 − 1) < (2nd𝑇)))
326325adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑦 = (𝑀 − 1)) → (𝑦 < (2nd𝑇) ↔ (𝑀 − 1) < (2nd𝑇)))
327 oveq1 6556 . . . . . . . . . . . . . 14 (𝑦 = (𝑀 − 1) → (𝑦 + 1) = ((𝑀 − 1) + 1))
328327, 59sylan9eqr 2666 . . . . . . . . . . . . 13 ((𝜑𝑦 = (𝑀 − 1)) → (𝑦 + 1) = 𝑀)
329326, 328ifbieq2d 4061 . . . . . . . . . . . 12 ((𝜑𝑦 = (𝑀 − 1)) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) = if((𝑀 − 1) < (2nd𝑇), 𝑦, 𝑀))
33062lep1d 10834 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd𝑇) + 1) ≤ (((2nd𝑇) + 1) + 1))
33162, 61, 47, 330, 67letrd 10073 . . . . . . . . . . . . . . 15 (𝜑 → ((2nd𝑇) + 1) ≤ 𝑀)
332 1re 9918 . . . . . . . . . . . . . . . . . 18 1 ∈ ℝ
333 leaddsub 10383 . . . . . . . . . . . . . . . . . 18 (((2nd𝑇) ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑀 ∈ ℝ) → (((2nd𝑇) + 1) ≤ 𝑀 ↔ (2nd𝑇) ≤ (𝑀 − 1)))
334332, 333mp3an2 1404 . . . . . . . . . . . . . . . . 17 (((2nd𝑇) ∈ ℝ ∧ 𝑀 ∈ ℝ) → (((2nd𝑇) + 1) ≤ 𝑀 ↔ (2nd𝑇) ≤ (𝑀 − 1)))
335274, 47, 334syl2anc 691 . . . . . . . . . . . . . . . 16 (𝜑 → (((2nd𝑇) + 1) ≤ 𝑀 ↔ (2nd𝑇) ≤ (𝑀 − 1)))
336274, 128lenltd 10062 . . . . . . . . . . . . . . . 16 (𝜑 → ((2nd𝑇) ≤ (𝑀 − 1) ↔ ¬ (𝑀 − 1) < (2nd𝑇)))
337335, 336bitrd 267 . . . . . . . . . . . . . . 15 (𝜑 → (((2nd𝑇) + 1) ≤ 𝑀 ↔ ¬ (𝑀 − 1) < (2nd𝑇)))
338331, 337mpbid 221 . . . . . . . . . . . . . 14 (𝜑 → ¬ (𝑀 − 1) < (2nd𝑇))
339338iffalsed 4047 . . . . . . . . . . . . 13 (𝜑 → if((𝑀 − 1) < (2nd𝑇), 𝑦, 𝑀) = 𝑀)
340339adantr 480 . . . . . . . . . . . 12 ((𝜑𝑦 = (𝑀 − 1)) → if((𝑀 − 1) < (2nd𝑇), 𝑦, 𝑀) = 𝑀)
341329, 340eqtrd 2644 . . . . . . . . . . 11 ((𝜑𝑦 = (𝑀 − 1)) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) = 𝑀)
342341csbeq1d 3506 . . . . . . . . . 10 ((𝜑𝑦 = (𝑀 − 1)) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = 𝑀 / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
343 oveq2 6557 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑀 → (1...𝑗) = (1...𝑀))
344343imaeq2d 5385 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑀 → ((2nd ‘(1st𝑇)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...𝑀)))
345344xpeq1d 5062 . . . . . . . . . . . . . . 15 (𝑗 = 𝑀 → (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}))
346 oveq1 6556 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑀 → (𝑗 + 1) = (𝑀 + 1))
347346oveq1d 6564 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑀 → ((𝑗 + 1)...𝑁) = ((𝑀 + 1)...𝑁))
348347imaeq2d 5385 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑀 → ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)))
349348xpeq1d 5062 . . . . . . . . . . . . . . 15 (𝑗 = 𝑀 → (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))
350345, 349uneq12d 3730 . . . . . . . . . . . . . 14 (𝑗 = 𝑀 → ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))
351350oveq2d 6565 . . . . . . . . . . . . 13 (𝑗 = 𝑀 → ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
352351adantl 481 . . . . . . . . . . . 12 ((𝜑𝑗 = 𝑀) → ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
35325, 352csbied 3526 . . . . . . . . . . 11 (𝜑𝑀 / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
354353adantr 480 . . . . . . . . . 10 ((𝜑𝑦 = (𝑀 − 1)) → 𝑀 / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
355342, 354eqtrd 2644 . . . . . . . . 9 ((𝜑𝑦 = (𝑀 − 1)) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
356282nnnn0d 11228 . . . . . . . . . 10 (𝜑 → (𝑀 − 1) ∈ ℕ0)
35747, 311, 60, 314lesub1dd 10522 . . . . . . . . . 10 (𝜑 → (𝑀 − 1) ≤ (𝑁 − 1))
358 elfz2nn0 12300 . . . . . . . . . 10 ((𝑀 − 1) ∈ (0...(𝑁 − 1)) ↔ ((𝑀 − 1) ∈ ℕ0 ∧ (𝑁 − 1) ∈ ℕ0 ∧ (𝑀 − 1) ≤ (𝑁 − 1)))
359356, 310, 357, 358syl3anbrc 1239 . . . . . . . . 9 (𝜑 → (𝑀 − 1) ∈ (0...(𝑁 − 1)))
360 ovex 6577 . . . . . . . . . 10 ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) ∈ V
361360a1i 11 . . . . . . . . 9 (𝜑 → ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) ∈ V)
362257, 355, 359, 361fvmptd 6197 . . . . . . . 8 (𝜑 → (𝐹‘(𝑀 − 1)) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
363362fveq1d 6105 . . . . . . 7 (𝜑 → ((𝐹‘(𝑀 − 1))‘𝑛) = (((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛))
364363adantr 480 . . . . . 6 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀))) → ((𝐹‘(𝑀 − 1))‘𝑛) = (((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑛))
365237, 324, 3643eqtr4d 2654 . . . . 5 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀))) → ((𝐹‘(𝑀 − 2))‘𝑛) = ((𝐹‘(𝑀 − 1))‘𝑛))
366365expr 641 . . . 4 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑛 ≠ ((2nd ‘(1st𝑇))‘𝑀) → ((𝐹‘(𝑀 − 2))‘𝑛) = ((𝐹‘(𝑀 − 1))‘𝑛)))
367366necon1d 2804 . . 3 ((𝜑𝑛 ∈ (1...𝑁)) → (((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛) → 𝑛 = ((2nd ‘(1st𝑇))‘𝑀)))
368 elmapi 7765 . . . . . . . . . . 11 ((1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) → (1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾))
36929, 368syl 17 . . . . . . . . . 10 (𝜑 → (1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾))
370369, 27ffvelrnd 6268 . . . . . . . . 9 (𝜑 → ((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) ∈ (0..^𝐾))
371 elfzonn0 12380 . . . . . . . . 9 (((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) ∈ (0..^𝐾) → ((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) ∈ ℕ0)
372370, 371syl 17 . . . . . . . 8 (𝜑 → ((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) ∈ ℕ0)
373372nn0red 11229 . . . . . . 7 (𝜑 → ((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) ∈ ℝ)
374373ltp1d 10833 . . . . . . 7 (𝜑 → ((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) < (((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) + 1))
375373, 374ltned 10052 . . . . . 6 (𝜑 → ((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) ≠ (((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) + 1))
376322fveq1d 6105 . . . . . . 7 (𝜑 → ((𝐹‘(𝑀 − 2))‘((2nd ‘(1st𝑇))‘𝑀)) = (((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})))‘((2nd ‘(1st𝑇))‘𝑀)))
377101a1i 11 . . . . . . . . 9 (𝜑 → (1...𝑁) ∈ V)
378 eqidd 2611 . . . . . . . . 9 ((𝜑 ∧ ((2nd ‘(1st𝑇))‘𝑀) ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) = ((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)))
379 fzss1 12251 . . . . . . . . . . . . . 14 (𝑀 ∈ (ℤ‘1) → (𝑀...𝑁) ⊆ (1...𝑁))
38072, 379syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑀...𝑁) ⊆ (1...𝑁))
381 eluzfz1 12219 . . . . . . . . . . . . . 14 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ (𝑀...𝑁))
38283, 381syl 17 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ (𝑀...𝑁))
383 fnfvima 6400 . . . . . . . . . . . . 13 (((2nd ‘(1st𝑇)) Fn (1...𝑁) ∧ (𝑀...𝑁) ⊆ (1...𝑁) ∧ 𝑀 ∈ (𝑀...𝑁)) → ((2nd ‘(1st𝑇))‘𝑀) ∈ ((2nd ‘(1st𝑇)) “ (𝑀...𝑁)))
384110, 380, 382, 383syl3anc 1318 . . . . . . . . . . . 12 (𝜑 → ((2nd ‘(1st𝑇))‘𝑀) ∈ ((2nd ‘(1st𝑇)) “ (𝑀...𝑁)))
385 fvun2 6180 . . . . . . . . . . . . 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𝑇))‘𝑀)))
38635, 38, 385mp3an12 1406 . . . . . . . . . . . 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𝑇))‘𝑀)))
38754, 384, 386syl2anc 691 . . . . . . . . . . 11 (𝜑 → (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘𝑀)) = ((((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})‘((2nd ‘(1st𝑇))‘𝑀)))
38836fvconst2 6374 . . . . . . . . . . . 12 (((2nd ‘(1st𝑇))‘𝑀) ∈ ((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) → ((((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})‘((2nd ‘(1st𝑇))‘𝑀)) = 0)
389384, 388syl 17 . . . . . . . . . . 11 (𝜑 → ((((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})‘((2nd ‘(1st𝑇))‘𝑀)) = 0)
390387, 389eqtrd 2644 . . . . . . . . . 10 (𝜑 → (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘𝑀)) = 0)
391390adantr 480 . . . . . . . . 9 ((𝜑 ∧ ((2nd ‘(1st𝑇))‘𝑀) ∈ (1...𝑁)) → (((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘𝑀)) = 0)
39231, 99, 377, 377, 103, 378, 391ofval 6804 . . . . . . . 8 ((𝜑 ∧ ((2nd ‘(1st𝑇))‘𝑀) ∈ (1...𝑁)) → (((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})))‘((2nd ‘(1st𝑇))‘𝑀)) = (((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) + 0))
39327, 392mpdan 699 . . . . . . 7 (𝜑 → (((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...(𝑀 − 1))) × {1}) ∪ (((2nd ‘(1st𝑇)) “ (𝑀...𝑁)) × {0})))‘((2nd ‘(1st𝑇))‘𝑀)) = (((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) + 0))
394372nn0cnd 11230 . . . . . . . 8 (𝜑 → ((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) ∈ ℂ)
395394addid1d 10115 . . . . . . 7 (𝜑 → (((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) + 0) = ((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)))
396376, 393, 3953eqtrd 2648 . . . . . 6 (𝜑 → ((𝐹‘(𝑀 − 2))‘((2nd ‘(1st𝑇))‘𝑀)) = ((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)))
397362fveq1d 6105 . . . . . . 7 (𝜑 → ((𝐹‘(𝑀 − 1))‘((2nd ‘(1st𝑇))‘𝑀)) = (((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘((2nd ‘(1st𝑇))‘𝑀)))
398 fzss2 12252 . . . . . . . . . . . . . 14 (𝑁 ∈ (ℤ𝑀) → (1...𝑀) ⊆ (1...𝑁))
39983, 398syl 17 . . . . . . . . . . . . 13 (𝜑 → (1...𝑀) ⊆ (1...𝑁))
400 elfz1end 12242 . . . . . . . . . . . . . 14 (𝑀 ∈ ℕ ↔ 𝑀 ∈ (1...𝑀))
40171, 400sylib 207 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ (1...𝑀))
402 fnfvima 6400 . . . . . . . . . . . . 13 (((2nd ‘(1st𝑇)) Fn (1...𝑁) ∧ (1...𝑀) ⊆ (1...𝑁) ∧ 𝑀 ∈ (1...𝑀)) → ((2nd ‘(1st𝑇))‘𝑀) ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)))
403110, 399, 401, 402syl3anc 1318 . . . . . . . . . . . 12 (𝜑 → ((2nd ‘(1st𝑇))‘𝑀) ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)))
404 fvun1 6179 . . . . . . . . . . . . 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𝑇))‘𝑀)))
405195, 124, 404mp3an12 1406 . . . . . . . . . . . 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𝑇))‘𝑀)))
406203, 403, 405syl2anc 691 . . . . . . . . . . 11 (𝜑 → (((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘𝑀)) = ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1})‘((2nd ‘(1st𝑇))‘𝑀)))
40733fvconst2 6374 . . . . . . . . . . . 12 (((2nd ‘(1st𝑇))‘𝑀) ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1})‘((2nd ‘(1st𝑇))‘𝑀)) = 1)
408403, 407syl 17 . . . . . . . . . . 11 (𝜑 → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1})‘((2nd ‘(1st𝑇))‘𝑀)) = 1)
409406, 408eqtrd 2644 . . . . . . . . . 10 (𝜑 → (((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘𝑀)) = 1)
410409adantr 480 . . . . . . . . 9 ((𝜑 ∧ ((2nd ‘(1st𝑇))‘𝑀) ∈ (1...𝑁)) → (((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘((2nd ‘(1st𝑇))‘𝑀)) = 1)
41131, 211, 377, 377, 103, 378, 410ofval 6804 . . . . . . . 8 ((𝜑 ∧ ((2nd ‘(1st𝑇))‘𝑀) ∈ (1...𝑁)) → (((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘((2nd ‘(1st𝑇))‘𝑀)) = (((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) + 1))
41227, 411mpdan 699 . . . . . . 7 (𝜑 → (((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘((2nd ‘(1st𝑇))‘𝑀)) = (((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) + 1))
413397, 412eqtrd 2644 . . . . . 6 (𝜑 → ((𝐹‘(𝑀 − 1))‘((2nd ‘(1st𝑇))‘𝑀)) = (((1st ‘(1st𝑇))‘((2nd ‘(1st𝑇))‘𝑀)) + 1))
414375, 396, 4133netr4d 2859 . . . . 5 (𝜑 → ((𝐹‘(𝑀 − 2))‘((2nd ‘(1st𝑇))‘𝑀)) ≠ ((𝐹‘(𝑀 − 1))‘((2nd ‘(1st𝑇))‘𝑀)))
415 fveq2 6103 . . . . . 6 (𝑛 = ((2nd ‘(1st𝑇))‘𝑀) → ((𝐹‘(𝑀 − 2))‘𝑛) = ((𝐹‘(𝑀 − 2))‘((2nd ‘(1st𝑇))‘𝑀)))
416 fveq2 6103 . . . . . 6 (𝑛 = ((2nd ‘(1st𝑇))‘𝑀) → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝐹‘(𝑀 − 1))‘((2nd ‘(1st𝑇))‘𝑀)))
417415, 416neeq12d 2843 . . . . 5 (𝑛 = ((2nd ‘(1st𝑇))‘𝑀) → (((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛) ↔ ((𝐹‘(𝑀 − 2))‘((2nd ‘(1st𝑇))‘𝑀)) ≠ ((𝐹‘(𝑀 − 1))‘((2nd ‘(1st𝑇))‘𝑀))))
418414, 417syl5ibrcom 236 . . . 4 (𝜑 → (𝑛 = ((2nd ‘(1st𝑇))‘𝑀) → ((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛)))
419418adantr 480 . . 3 ((𝜑𝑛 ∈ (1...𝑁)) → (𝑛 = ((2nd ‘(1st𝑇))‘𝑀) → ((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛)))
420367, 419impbid 201 . 2 ((𝜑𝑛 ∈ (1...𝑁)) → (((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛) ↔ 𝑛 = ((2nd ‘(1st𝑇))‘𝑀)))
42127, 420riota5 6536 1 (𝜑 → (𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 2))‘𝑛) ≠ ((𝐹‘(𝑀 − 1))‘𝑛)) = ((2nd ‘(1st𝑇))‘𝑀))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195  wa 383   = wceq 1475  wcel 1977  {cab 2596  wne 2780  {crab 2900  Vcvv 3173  csb 3499  cdif 3537  cun 3538  cin 3539  wss 3540  c0 3874  ifcif 4036  {csn 4125   class class class wbr 4583  cmpt 4643   × cxp 5036  ccnv 5037  cima 5041  Fun wfun 5798   Fn wfn 5799  wf 5800  ontowfo 5802  1-1-ontowf1o 5803  cfv 5804  crio 6510  (class class class)co 6549  𝑓 cof 6793  1st c1st 7057  2nd c2nd 7058  𝑚 cmap 7744  cc 9813  cr 9814  0cc0 9815  1c1 9816   + caddc 9818   < clt 9953  cle 9954  cmin 10145  cn 10897  2c2 10947  0cn0 11169  cz 11254  cuz 11563  ...cfz 12197  ..^cfzo 12334
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-n0 11170  df-z 11255  df-uz 11564  df-fz 12198  df-fzo 12335
This theorem is referenced by:  poimirlem8  32587
  Copyright terms: Public domain W3C validator