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

Theorem poimirlem11 33550
 Description: Lemma for poimir 33572 connecting walks that could yield from a given cube a given face opposite the first vertex of the walk. (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}))))}
poimirlem22.1 (𝜑𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))
poimirlem12.2 (𝜑𝑇𝑆)
poimirlem11.3 (𝜑 → (2nd𝑇) = 0)
poimirlem11.4 (𝜑𝑈𝑆)
poimirlem11.5 (𝜑 → (2nd𝑈) = 0)
poimirlem11.6 (𝜑𝑀 ∈ (1...𝑁))
Assertion
Ref Expression
poimirlem11 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑀)) ⊆ ((2nd ‘(1st𝑈)) “ (1...𝑀)))
Distinct variable groups:   𝑓,𝑗,𝑡,𝑦   𝜑,𝑗,𝑦   𝑗,𝐹,𝑦   𝑗,𝑀,𝑦   𝑗,𝑁,𝑦   𝑇,𝑗,𝑦   𝑈,𝑗,𝑦   𝜑,𝑡   𝑓,𝐾,𝑗,𝑡   𝑓,𝑀,𝑡   𝑓,𝑁,𝑡   𝑇,𝑓   𝑈,𝑓   𝑓,𝐹,𝑡   𝑡,𝑇   𝑡,𝑈   𝑆,𝑗,𝑡,𝑦
Allowed substitution hints:   𝜑(𝑓)   𝑆(𝑓)   𝐾(𝑦)

Proof of Theorem poimirlem11
StepHypRef Expression
1 eldif 3617 . . . . . . 7 (𝑦 ∈ (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∖ ((2nd ‘(1st𝑈)) “ (1...𝑀))) ↔ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀))))
2 imassrn 5512 . . . . . . . . . . . 12 ((2nd ‘(1st𝑇)) “ (1...𝑀)) ⊆ ran (2nd ‘(1st𝑇))
3 poimirlem12.2 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇𝑆)
4 elrabi 3391 . . . . . . . . . . . . . . . . . . 19 (𝑇 ∈ {𝑡 ∈ ((((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...𝑁)))
5 poimirlem22.s . . . . . . . . . . . . . . . . . . 19 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
64, 5eleq2s 2748 . . . . . . . . . . . . . . . . . 18 (𝑇𝑆𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
73, 6syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
8 xp1st 7242 . . . . . . . . . . . . . . . . 17 (𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
97, 8syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
10 xp2nd 7243 . . . . . . . . . . . . . . . 16 ((1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
119, 10syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
12 fvex 6239 . . . . . . . . . . . . . . . 16 (2nd ‘(1st𝑇)) ∈ V
13 f1oeq1 6165 . . . . . . . . . . . . . . . 16 (𝑓 = (2nd ‘(1st𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
1412, 13elab 3382 . . . . . . . . . . . . . . 15 ((2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
1511, 14sylib 208 . . . . . . . . . . . . . 14 (𝜑 → (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
16 f1of 6175 . . . . . . . . . . . . . 14 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)):(1...𝑁)⟶(1...𝑁))
1715, 16syl 17 . . . . . . . . . . . . 13 (𝜑 → (2nd ‘(1st𝑇)):(1...𝑁)⟶(1...𝑁))
18 frn 6091 . . . . . . . . . . . . 13 ((2nd ‘(1st𝑇)):(1...𝑁)⟶(1...𝑁) → ran (2nd ‘(1st𝑇)) ⊆ (1...𝑁))
1917, 18syl 17 . . . . . . . . . . . 12 (𝜑 → ran (2nd ‘(1st𝑇)) ⊆ (1...𝑁))
202, 19syl5ss 3647 . . . . . . . . . . 11 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑀)) ⊆ (1...𝑁))
21 poimirlem11.4 . . . . . . . . . . . . . . . . 17 (𝜑𝑈𝑆)
22 elrabi 3391 . . . . . . . . . . . . . . . . . 18 (𝑈 ∈ {𝑡 ∈ ((((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...𝑁)))
2322, 5eleq2s 2748 . . . . . . . . . . . . . . . . 17 (𝑈𝑆𝑈 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
2421, 23syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑈 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
25 xp1st 7242 . . . . . . . . . . . . . . . 16 (𝑈 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑈) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
2624, 25syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (1st𝑈) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
27 xp2nd 7243 . . . . . . . . . . . . . . 15 ((1st𝑈) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd ‘(1st𝑈)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
2826, 27syl 17 . . . . . . . . . . . . . 14 (𝜑 → (2nd ‘(1st𝑈)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
29 fvex 6239 . . . . . . . . . . . . . . 15 (2nd ‘(1st𝑈)) ∈ V
30 f1oeq1 6165 . . . . . . . . . . . . . . 15 (𝑓 = (2nd ‘(1st𝑈)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁)))
3129, 30elab 3382 . . . . . . . . . . . . . 14 ((2nd ‘(1st𝑈)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁))
3228, 31sylib 208 . . . . . . . . . . . . 13 (𝜑 → (2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁))
33 f1ofo 6182 . . . . . . . . . . . . 13 ((2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑈)):(1...𝑁)–onto→(1...𝑁))
3432, 33syl 17 . . . . . . . . . . . 12 (𝜑 → (2nd ‘(1st𝑈)):(1...𝑁)–onto→(1...𝑁))
35 foima 6158 . . . . . . . . . . . 12 ((2nd ‘(1st𝑈)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑈)) “ (1...𝑁)) = (1...𝑁))
3634, 35syl 17 . . . . . . . . . . 11 (𝜑 → ((2nd ‘(1st𝑈)) “ (1...𝑁)) = (1...𝑁))
3720, 36sseqtr4d 3675 . . . . . . . . . 10 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑀)) ⊆ ((2nd ‘(1st𝑈)) “ (1...𝑁)))
3837ssdifd 3779 . . . . . . . . 9 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∖ ((2nd ‘(1st𝑈)) “ (1...𝑀))) ⊆ (((2nd ‘(1st𝑈)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑈)) “ (1...𝑀))))
39 dff1o3 6181 . . . . . . . . . . . . 13 ((2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘(1st𝑈)):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd ‘(1st𝑈))))
4039simprbi 479 . . . . . . . . . . . 12 ((2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun (2nd ‘(1st𝑈)))
4132, 40syl 17 . . . . . . . . . . 11 (𝜑 → Fun (2nd ‘(1st𝑈)))
42 imadif 6011 . . . . . . . . . . 11 (Fun (2nd ‘(1st𝑈)) → ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ (1...𝑀))) = (((2nd ‘(1st𝑈)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑈)) “ (1...𝑀))))
4341, 42syl 17 . . . . . . . . . 10 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ (1...𝑀))) = (((2nd ‘(1st𝑈)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑈)) “ (1...𝑀))))
44 difun2 4081 . . . . . . . . . . . 12 ((((𝑀 + 1)...𝑁) ∪ (1...𝑀)) ∖ (1...𝑀)) = (((𝑀 + 1)...𝑁) ∖ (1...𝑀))
45 poimirlem11.6 . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ (1...𝑁))
46 fzsplit 12405 . . . . . . . . . . . . . . 15 (𝑀 ∈ (1...𝑁) → (1...𝑁) = ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)))
4745, 46syl 17 . . . . . . . . . . . . . 14 (𝜑 → (1...𝑁) = ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)))
48 uncom 3790 . . . . . . . . . . . . . 14 ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)) = (((𝑀 + 1)...𝑁) ∪ (1...𝑀))
4947, 48syl6eq 2701 . . . . . . . . . . . . 13 (𝜑 → (1...𝑁) = (((𝑀 + 1)...𝑁) ∪ (1...𝑀)))
5049difeq1d 3760 . . . . . . . . . . . 12 (𝜑 → ((1...𝑁) ∖ (1...𝑀)) = ((((𝑀 + 1)...𝑁) ∪ (1...𝑀)) ∖ (1...𝑀)))
51 incom 3838 . . . . . . . . . . . . . 14 (((𝑀 + 1)...𝑁) ∩ (1...𝑀)) = ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))
52 elfznn 12408 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ (1...𝑁) → 𝑀 ∈ ℕ)
5345, 52syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ∈ ℕ)
5453nnred 11073 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℝ)
5554ltp1d 10992 . . . . . . . . . . . . . . 15 (𝜑𝑀 < (𝑀 + 1))
56 fzdisj 12406 . . . . . . . . . . . . . . 15 (𝑀 < (𝑀 + 1) → ((1...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅)
5755, 56syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((1...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅)
5851, 57syl5eq 2697 . . . . . . . . . . . . 13 (𝜑 → (((𝑀 + 1)...𝑁) ∩ (1...𝑀)) = ∅)
59 disj3 4054 . . . . . . . . . . . . 13 ((((𝑀 + 1)...𝑁) ∩ (1...𝑀)) = ∅ ↔ ((𝑀 + 1)...𝑁) = (((𝑀 + 1)...𝑁) ∖ (1...𝑀)))
6058, 59sylib 208 . . . . . . . . . . . 12 (𝜑 → ((𝑀 + 1)...𝑁) = (((𝑀 + 1)...𝑁) ∖ (1...𝑀)))
6144, 50, 603eqtr4a 2711 . . . . . . . . . . 11 (𝜑 → ((1...𝑁) ∖ (1...𝑀)) = ((𝑀 + 1)...𝑁))
6261imaeq2d 5501 . . . . . . . . . 10 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ (1...𝑀))) = ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
6343, 62eqtr3d 2687 . . . . . . . . 9 (𝜑 → (((2nd ‘(1st𝑈)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑈)) “ (1...𝑀))) = ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
6438, 63sseqtrd 3674 . . . . . . . 8 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∖ ((2nd ‘(1st𝑈)) “ (1...𝑀))) ⊆ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
6564sselda 3636 . . . . . . 7 ((𝜑𝑦 ∈ (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∖ ((2nd ‘(1st𝑈)) “ (1...𝑀)))) → 𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
661, 65sylan2br 492 . . . . . 6 ((𝜑 ∧ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀)))) → 𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
67 fveq2 6229 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑈 → (2nd𝑡) = (2nd𝑈))
6867breq2d 4697 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑈 → (𝑦 < (2nd𝑡) ↔ 𝑦 < (2nd𝑈)))
6968ifbid 4141 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑈 → if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd𝑈), 𝑦, (𝑦 + 1)))
7069csbeq1d 3573 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑈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}))))
71 fveq2 6229 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑈 → (1st𝑡) = (1st𝑈))
7271fveq2d 6233 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑈 → (1st ‘(1st𝑡)) = (1st ‘(1st𝑈)))
7371fveq2d 6233 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑈 → (2nd ‘(1st𝑡)) = (2nd ‘(1st𝑈)))
7473imaeq1d 5500 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑈 → ((2nd ‘(1st𝑡)) “ (1...𝑗)) = ((2nd ‘(1st𝑈)) “ (1...𝑗)))
7574xpeq1d 5172 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑈 → (((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}))
7673imaeq1d 5500 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑈 → ((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)))
7776xpeq1d 5172 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑈 → (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))
7875, 77uneq12d 3801 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑈 → ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0})))
7972, 78oveq12d 6708 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑈 → ((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑈)) ∘𝑓 + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))))
8079csbeq2dv 4025 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑈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}))))
8170, 80eqtrd 2685 . . . . . . . . . . . . . . 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}))))
8281mpteq2dv 4778 . . . . . . . . . . . . . 14 (𝑡 = 𝑈 → (𝑦 ∈ (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})))))
8382eqeq2d 2661 . . . . . . . . . . . . 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}))))))
8483, 5elrab2 3399 . . . . . . . . . . . 12 (𝑈𝑆 ↔ (𝑈 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑈), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑈)) ∘𝑓 + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
8584simprbi 479 . . . . . . . . . . 11 (𝑈𝑆𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑈), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑈)) ∘𝑓 + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0})))))
8621, 85syl 17 . . . . . . . . . 10 (𝜑𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑈), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑈)) ∘𝑓 + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0})))))
87 poimirlem11.5 . . . . . . . . . . . . . . . 16 (𝜑 → (2nd𝑈) = 0)
88 breq12 4690 . . . . . . . . . . . . . . . 16 ((𝑦 = (𝑀 − 1) ∧ (2nd𝑈) = 0) → (𝑦 < (2nd𝑈) ↔ (𝑀 − 1) < 0))
8987, 88sylan2 490 . . . . . . . . . . . . . . 15 ((𝑦 = (𝑀 − 1) ∧ 𝜑) → (𝑦 < (2nd𝑈) ↔ (𝑀 − 1) < 0))
9089ancoms 468 . . . . . . . . . . . . . 14 ((𝜑𝑦 = (𝑀 − 1)) → (𝑦 < (2nd𝑈) ↔ (𝑀 − 1) < 0))
91 oveq1 6697 . . . . . . . . . . . . . . 15 (𝑦 = (𝑀 − 1) → (𝑦 + 1) = ((𝑀 − 1) + 1))
9253nncnd 11074 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℂ)
93 npcan1 10493 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℂ → ((𝑀 − 1) + 1) = 𝑀)
9492, 93syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑀 − 1) + 1) = 𝑀)
9591, 94sylan9eqr 2707 . . . . . . . . . . . . . 14 ((𝜑𝑦 = (𝑀 − 1)) → (𝑦 + 1) = 𝑀)
9690, 95ifbieq2d 4144 . . . . . . . . . . . . 13 ((𝜑𝑦 = (𝑀 − 1)) → if(𝑦 < (2nd𝑈), 𝑦, (𝑦 + 1)) = if((𝑀 − 1) < 0, 𝑦, 𝑀))
9753nnzd 11519 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑀 ∈ ℤ)
98 poimir.0 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑁 ∈ ℕ)
9998nnzd 11519 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ ℤ)
100 elfzm1b 12456 . . . . . . . . . . . . . . . . . . 19 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∈ (1...𝑁) ↔ (𝑀 − 1) ∈ (0...(𝑁 − 1))))
10197, 99, 100syl2anc 694 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑀 ∈ (1...𝑁) ↔ (𝑀 − 1) ∈ (0...(𝑁 − 1))))
10245, 101mpbid 222 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑀 − 1) ∈ (0...(𝑁 − 1)))
103 elfzle1 12382 . . . . . . . . . . . . . . . . 17 ((𝑀 − 1) ∈ (0...(𝑁 − 1)) → 0 ≤ (𝑀 − 1))
104102, 103syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ≤ (𝑀 − 1))
105 0red 10079 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 ∈ ℝ)
106 nnm1nn0 11372 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ ℕ → (𝑀 − 1) ∈ ℕ0)
10753, 106syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑀 − 1) ∈ ℕ0)
108107nn0red 11390 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑀 − 1) ∈ ℝ)
109105, 108lenltd 10221 . . . . . . . . . . . . . . . 16 (𝜑 → (0 ≤ (𝑀 − 1) ↔ ¬ (𝑀 − 1) < 0))
110104, 109mpbid 222 . . . . . . . . . . . . . . 15 (𝜑 → ¬ (𝑀 − 1) < 0)
111110iffalsed 4130 . . . . . . . . . . . . . 14 (𝜑 → if((𝑀 − 1) < 0, 𝑦, 𝑀) = 𝑀)
112111adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑦 = (𝑀 − 1)) → if((𝑀 − 1) < 0, 𝑦, 𝑀) = 𝑀)
11396, 112eqtrd 2685 . . . . . . . . . . . 12 ((𝜑𝑦 = (𝑀 − 1)) → if(𝑦 < (2nd𝑈), 𝑦, (𝑦 + 1)) = 𝑀)
114113csbeq1d 3573 . . . . . . . . . . 11 ((𝜑𝑦 = (𝑀 − 1)) → if(𝑦 < (2nd𝑈), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑈)) ∘𝑓 + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))) = 𝑀 / 𝑗((1st ‘(1st𝑈)) ∘𝑓 + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))))
115 oveq2 6698 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑀 → (1...𝑗) = (1...𝑀))
116115imaeq2d 5501 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑀 → ((2nd ‘(1st𝑈)) “ (1...𝑗)) = ((2nd ‘(1st𝑈)) “ (1...𝑀)))
117116xpeq1d 5172 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑀 → (((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}))
118 oveq1 6697 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑀 → (𝑗 + 1) = (𝑀 + 1))
119118oveq1d 6705 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑀 → ((𝑗 + 1)...𝑁) = ((𝑀 + 1)...𝑁))
120119imaeq2d 5501 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑀 → ((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
121120xpeq1d 5172 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑀 → (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))
122117, 121uneq12d 3801 . . . . . . . . . . . . . . 15 (𝑗 = 𝑀 → ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})))
123122oveq2d 6706 . . . . . . . . . . . . . 14 (𝑗 = 𝑀 → ((1st ‘(1st𝑈)) ∘𝑓 + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑈)) ∘𝑓 + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))))
124123adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑗 = 𝑀) → ((1st ‘(1st𝑈)) ∘𝑓 + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑈)) ∘𝑓 + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))))
12545, 124csbied 3593 . . . . . . . . . . . 12 (𝜑𝑀 / 𝑗((1st ‘(1st𝑈)) ∘𝑓 + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑈)) ∘𝑓 + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))))
126125adantr 480 . . . . . . . . . . 11 ((𝜑𝑦 = (𝑀 − 1)) → 𝑀 / 𝑗((1st ‘(1st𝑈)) ∘𝑓 + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑈)) ∘𝑓 + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))))
127114, 126eqtrd 2685 . . . . . . . . . 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}))))
128 ovexd 6720 . . . . . . . . . 10 (𝜑 → ((1st ‘(1st𝑈)) ∘𝑓 + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))) ∈ V)
12986, 127, 102, 128fvmptd 6327 . . . . . . . . 9 (𝜑 → (𝐹‘(𝑀 − 1)) = ((1st ‘(1st𝑈)) ∘𝑓 + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))))
130129fveq1d 6231 . . . . . . . 8 (𝜑 → ((𝐹‘(𝑀 − 1))‘𝑦) = (((1st ‘(1st𝑈)) ∘𝑓 + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦))
131130adantr 480 . . . . . . 7 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → ((𝐹‘(𝑀 − 1))‘𝑦) = (((1st ‘(1st𝑈)) ∘𝑓 + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦))
132 imassrn 5512 . . . . . . . . . 10 ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) ⊆ ran (2nd ‘(1st𝑈))
133 f1of 6175 . . . . . . . . . . . 12 ((2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑈)):(1...𝑁)⟶(1...𝑁))
13432, 133syl 17 . . . . . . . . . . 11 (𝜑 → (2nd ‘(1st𝑈)):(1...𝑁)⟶(1...𝑁))
135 frn 6091 . . . . . . . . . . 11 ((2nd ‘(1st𝑈)):(1...𝑁)⟶(1...𝑁) → ran (2nd ‘(1st𝑈)) ⊆ (1...𝑁))
136134, 135syl 17 . . . . . . . . . 10 (𝜑 → ran (2nd ‘(1st𝑈)) ⊆ (1...𝑁))
137132, 136syl5ss 3647 . . . . . . . . 9 (𝜑 → ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) ⊆ (1...𝑁))
138137sselda 3636 . . . . . . . 8 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → 𝑦 ∈ (1...𝑁))
139 xp1st 7242 . . . . . . . . . . . 12 ((1st𝑈) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(1st𝑈)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
14026, 139syl 17 . . . . . . . . . . 11 (𝜑 → (1st ‘(1st𝑈)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
141 elmapfn 7922 . . . . . . . . . . 11 ((1st ‘(1st𝑈)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) → (1st ‘(1st𝑈)) Fn (1...𝑁))
142140, 141syl 17 . . . . . . . . . 10 (𝜑 → (1st ‘(1st𝑈)) Fn (1...𝑁))
143142adantr 480 . . . . . . . . 9 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → (1st ‘(1st𝑈)) Fn (1...𝑁))
144 1ex 10073 . . . . . . . . . . . . . 14 1 ∈ V
145 fnconstg 6131 . . . . . . . . . . . . . 14 (1 ∈ V → (((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) Fn ((2nd ‘(1st𝑈)) “ (1...𝑀)))
146144, 145ax-mp 5 . . . . . . . . . . . . 13 (((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) Fn ((2nd ‘(1st𝑈)) “ (1...𝑀))
147 c0ex 10072 . . . . . . . . . . . . . 14 0 ∈ V
148 fnconstg 6131 . . . . . . . . . . . . . 14 (0 ∈ V → (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
149147, 148ax-mp 5 . . . . . . . . . . . . 13 (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))
150146, 149pm3.2i 470 . . . . . . . . . . . 12 ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) Fn ((2nd ‘(1st𝑈)) “ (1...𝑀)) ∧ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
151 imain 6012 . . . . . . . . . . . . . 14 (Fun (2nd ‘(1st𝑈)) → ((2nd ‘(1st𝑈)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑈)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))))
15241, 151syl 17 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑈)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))))
15357imaeq2d 5501 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ((2nd ‘(1st𝑈)) “ ∅))
154 ima0 5516 . . . . . . . . . . . . . 14 ((2nd ‘(1st𝑈)) “ ∅) = ∅
155153, 154syl6eq 2701 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ∅)
156152, 155eqtr3d 2687 . . . . . . . . . . . 12 (𝜑 → (((2nd ‘(1st𝑈)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) = ∅)
157 fnun 6035 . . . . . . . . . . . 12 ((((((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)...𝑁))))
158150, 156, 157sylancr 696 . . . . . . . . . . 11 (𝜑 → ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2nd ‘(1st𝑈)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))))
159 imaundi 5580 . . . . . . . . . . . . 13 ((2nd ‘(1st𝑈)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑈)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
16047imaeq2d 5501 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑈)) “ (1...𝑁)) = ((2nd ‘(1st𝑈)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))))
161160, 36eqtr3d 2687 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (1...𝑁))
162159, 161syl5eqr 2699 . . . . . . . . . . . 12 (𝜑 → (((2nd ‘(1st𝑈)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) = (1...𝑁))
163162fneq2d 6020 . . . . . . . . . . 11 (𝜑 → (((((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...𝑁)))
164158, 163mpbid 222 . . . . . . . . . 10 (𝜑 → ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
165164adantr 480 . . . . . . . . 9 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
166 ovexd 6720 . . . . . . . . 9 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → (1...𝑁) ∈ V)
167 inidm 3855 . . . . . . . . 9 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
168 eqidd 2652 . . . . . . . . 9 (((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) ∧ 𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑈))‘𝑦) = ((1st ‘(1st𝑈))‘𝑦))
169 fvun2 6309 . . . . . . . . . . . . 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)...𝑁)))) → (((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = ((((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})‘𝑦))
170146, 149, 169mp3an12 1454 . . . . . . . . . . . 12 (((((2nd ‘(1st𝑈)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) = ∅ ∧ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → (((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = ((((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})‘𝑦))
171156, 170sylan 487 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → (((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = ((((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})‘𝑦))
172147fvconst2 6510 . . . . . . . . . . . 12 (𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) → ((((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})‘𝑦) = 0)
173172adantl 481 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → ((((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})‘𝑦) = 0)
174171, 173eqtrd 2685 . . . . . . . . . 10 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → (((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = 0)
175174adantr 480 . . . . . . . . 9 (((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) ∧ 𝑦 ∈ (1...𝑁)) → (((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = 0)
176143, 165, 166, 166, 167, 168, 175ofval 6948 . . . . . . . 8 (((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) ∧ 𝑦 ∈ (1...𝑁)) → (((1st ‘(1st𝑈)) ∘𝑓 + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦) = (((1st ‘(1st𝑈))‘𝑦) + 0))
177138, 176mpdan 703 . . . . . . 7 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → (((1st ‘(1st𝑈)) ∘𝑓 + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦) = (((1st ‘(1st𝑈))‘𝑦) + 0))
178 elmapi 7921 . . . . . . . . . . . . 13 ((1st ‘(1st𝑈)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) → (1st ‘(1st𝑈)):(1...𝑁)⟶(0..^𝐾))
179140, 178syl 17 . . . . . . . . . . . 12 (𝜑 → (1st ‘(1st𝑈)):(1...𝑁)⟶(0..^𝐾))
180179ffvelrnda 6399 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑈))‘𝑦) ∈ (0..^𝐾))
181 elfzonn0 12552 . . . . . . . . . . 11 (((1st ‘(1st𝑈))‘𝑦) ∈ (0..^𝐾) → ((1st ‘(1st𝑈))‘𝑦) ∈ ℕ0)
182180, 181syl 17 . . . . . . . . . 10 ((𝜑𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑈))‘𝑦) ∈ ℕ0)
183182nn0cnd 11391 . . . . . . . . 9 ((𝜑𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑈))‘𝑦) ∈ ℂ)
184138, 183syldan 486 . . . . . . . 8 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → ((1st ‘(1st𝑈))‘𝑦) ∈ ℂ)
185184addid1d 10274 . . . . . . 7 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → (((1st ‘(1st𝑈))‘𝑦) + 0) = ((1st ‘(1st𝑈))‘𝑦))
186131, 177, 1853eqtrd 2689 . . . . . 6 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → ((𝐹‘(𝑀 − 1))‘𝑦) = ((1st ‘(1st𝑈))‘𝑦))
18766, 186syldan 486 . . . . 5 ((𝜑 ∧ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀)))) → ((𝐹‘(𝑀 − 1))‘𝑦) = ((1st ‘(1st𝑈))‘𝑦))
188 fveq2 6229 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑇 → (2nd𝑡) = (2nd𝑇))
189188breq2d 4697 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑇 → (𝑦 < (2nd𝑡) ↔ 𝑦 < (2nd𝑇)))
190189ifbid 4141 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑇 → if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)))
191190csbeq1d 3573 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑇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}))))
192 fveq2 6229 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑇 → (1st𝑡) = (1st𝑇))
193192fveq2d 6233 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑇 → (1st ‘(1st𝑡)) = (1st ‘(1st𝑇)))
194192fveq2d 6233 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑇 → (2nd ‘(1st𝑡)) = (2nd ‘(1st𝑇)))
195194imaeq1d 5500 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...𝑗)))
196195xpeq1d 5172 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}))
197194imaeq1d 5500 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)))
198197xpeq1d 5172 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
199196, 198uneq12d 3801 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑇 → ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))
200193, 199oveq12d 6708 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑇 → ((1st ‘(1st𝑡)) ∘𝑓 + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
201200csbeq2dv 4025 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑇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}))))
202191, 201eqtrd 2685 . . . . . . . . . . . . . . 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}))))
203202mpteq2dv 4778 . . . . . . . . . . . . . 14 (𝑡 = 𝑇 → (𝑦 ∈ (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})))))
204203eqeq2d 2661 . . . . . . . . . . . . 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}))))))
205204, 5elrab2 3399 . . . . . . . . . . . 12 (𝑇𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
206205simprbi 479 . . . . . . . . . . 11 (𝑇𝑆𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
2073, 206syl 17 . . . . . . . . . 10 (𝜑𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
208 poimirlem11.3 . . . . . . . . . . . . . . . 16 (𝜑 → (2nd𝑇) = 0)
209 breq12 4690 . . . . . . . . . . . . . . . 16 ((𝑦 = (𝑀 − 1) ∧ (2nd𝑇) = 0) → (𝑦 < (2nd𝑇) ↔ (𝑀 − 1) < 0))
210208, 209sylan2 490 . . . . . . . . . . . . . . 15 ((𝑦 = (𝑀 − 1) ∧ 𝜑) → (𝑦 < (2nd𝑇) ↔ (𝑀 − 1) < 0))
211210ancoms 468 . . . . . . . . . . . . . 14 ((𝜑𝑦 = (𝑀 − 1)) → (𝑦 < (2nd𝑇) ↔ (𝑀 − 1) < 0))
212211, 95ifbieq2d 4144 . . . . . . . . . . . . 13 ((𝜑𝑦 = (𝑀 − 1)) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) = if((𝑀 − 1) < 0, 𝑦, 𝑀))
213212, 112eqtrd 2685 . . . . . . . . . . . 12 ((𝜑𝑦 = (𝑀 − 1)) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) = 𝑀)
214213csbeq1d 3573 . . . . . . . . . . 11 ((𝜑𝑦 = (𝑀 − 1)) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = 𝑀 / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
215115imaeq2d 5501 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑀 → ((2nd ‘(1st𝑇)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...𝑀)))
216215xpeq1d 5172 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑀 → (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}))
217119imaeq2d 5501 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑀 → ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)))
218217xpeq1d 5172 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑀 → (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))
219216, 218uneq12d 3801 . . . . . . . . . . . . . . 15 (𝑗 = 𝑀 → ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))
220219oveq2d 6706 . . . . . . . . . . . . . 14 (𝑗 = 𝑀 → ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
221220adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑗 = 𝑀) → ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
22245, 221csbied 3593 . . . . . . . . . . . 12 (𝜑𝑀 / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
223222adantr 480 . . . . . . . . . . 11 ((𝜑𝑦 = (𝑀 − 1)) → 𝑀 / 𝑗((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
224214, 223eqtrd 2685 . . . . . . . . . 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}))))
225 ovexd 6720 . . . . . . . . . 10 (𝜑 → ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) ∈ V)
226207, 224, 102, 225fvmptd 6327 . . . . . . . . 9 (𝜑 → (𝐹‘(𝑀 − 1)) = ((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
227226fveq1d 6231 . . . . . . . 8 (𝜑 → ((𝐹‘(𝑀 − 1))‘𝑦) = (((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦))
228227adantr 480 . . . . . . 7 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → ((𝐹‘(𝑀 − 1))‘𝑦) = (((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦))
22920sselda 3636 . . . . . . . 8 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → 𝑦 ∈ (1...𝑁))
230 xp1st 7242 . . . . . . . . . . . 12 ((1st𝑇) ∈ (((0..^𝐾) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
2319, 230syl 17 . . . . . . . . . . 11 (𝜑 → (1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)))
232 elmapfn 7922 . . . . . . . . . . 11 ((1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) → (1st ‘(1st𝑇)) Fn (1...𝑁))
233231, 232syl 17 . . . . . . . . . 10 (𝜑 → (1st ‘(1st𝑇)) Fn (1...𝑁))
234233adantr 480 . . . . . . . . 9 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → (1st ‘(1st𝑇)) Fn (1...𝑁))
235 fnconstg 6131 . . . . . . . . . . . . . 14 (1 ∈ V → (((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...𝑀)))
236144, 235ax-mp 5 . . . . . . . . . . . . 13 (((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...𝑀))
237 fnconstg 6131 . . . . . . . . . . . . . 14 (0 ∈ V → (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)))
238147, 237ax-mp 5 . . . . . . . . . . . . 13 (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))
239236, 238pm3.2i 470 . . . . . . . . . . . 12 ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)))
240 dff1o3 6181 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd ‘(1st𝑇))))
241240simprbi 479 . . . . . . . . . . . . . . 15 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun (2nd ‘(1st𝑇)))
24215, 241syl 17 . . . . . . . . . . . . . 14 (𝜑 → Fun (2nd ‘(1st𝑇)))
243 imain 6012 . . . . . . . . . . . . . 14 (Fun (2nd ‘(1st𝑇)) → ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))))
244242, 243syl 17 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))))
24557imaeq2d 5501 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ((2nd ‘(1st𝑇)) “ ∅))
246 ima0 5516 . . . . . . . . . . . . . 14 ((2nd ‘(1st𝑇)) “ ∅) = ∅
247245, 246syl6eq 2701 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ∅)
248244, 247eqtr3d 2687 . . . . . . . . . . . 12 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅)
249 fnun 6035 . . . . . . . . . . . 12 ((((((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)...𝑁))))
250239, 248, 249sylancr 696 . . . . . . . . . . 11 (𝜑 → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))))
251 imaundi 5580 . . . . . . . . . . . . 13 ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)))
25247imaeq2d 5501 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))))
253 f1ofo 6182 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁))
25415, 253syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁))
255 foima 6158 . . . . . . . . . . . . . . 15 ((2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
256254, 255syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
257252, 256eqtr3d 2687 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (1...𝑁))
258251, 257syl5eqr 2699 . . . . . . . . . . . 12 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))) = (1...𝑁))
259258fneq2d 6020 . . . . . . . . . . 11 (𝜑 → (((((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...𝑁)))
260250, 259mpbid 222 . . . . . . . . . 10 (𝜑 → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
261260adantr 480 . . . . . . . . 9 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
262 ovexd 6720 . . . . . . . . 9 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → (1...𝑁) ∈ V)
263 eqidd 2652 . . . . . . . . 9 (((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) ∧ 𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑦) = ((1st ‘(1st𝑇))‘𝑦))
264 fvun1 6308 . . . . . . . . . . . . 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...𝑀)))) → (((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1})‘𝑦))
265236, 238, 264mp3an12 1454 . . . . . . . . . . . 12 (((((2nd ‘(1st𝑇)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅ ∧ 𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → (((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1})‘𝑦))
266248, 265sylan 487 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → (((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1})‘𝑦))
267144fvconst2 6510 . . . . . . . . . . . 12 (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1})‘𝑦) = 1)
268267adantl 481 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1})‘𝑦) = 1)
269266, 268eqtrd 2685 . . . . . . . . . 10 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → (((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = 1)
270269adantr 480 . . . . . . . . 9 (((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) ∧ 𝑦 ∈ (1...𝑁)) → (((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = 1)
271234, 261, 262, 262, 167, 263, 270ofval 6948 . . . . . . . 8 (((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) ∧ 𝑦 ∈ (1...𝑁)) → (((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦) = (((1st ‘(1st𝑇))‘𝑦) + 1))
272229, 271mpdan 703 . . . . . . 7 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → (((1st ‘(1st𝑇)) ∘𝑓 + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦) = (((1st ‘(1st𝑇))‘𝑦) + 1))
273228, 272eqtrd 2685 . . . . . 6 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → ((𝐹‘(𝑀 − 1))‘𝑦) = (((1st ‘(1st𝑇))‘𝑦) + 1))
274273adantrr 753 . . . . 5 ((𝜑 ∧ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀)))) → ((𝐹‘(𝑀 − 1))‘𝑦) = (((1st ‘(1st𝑇))‘𝑦) + 1))
275 poimirlem22.1 . . . . . . . . 9 (𝜑𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑𝑚 (1...𝑁)))
27698, 5, 275, 21, 87poimirlem10 33549 . . . . . . . 8 (𝜑 → ((𝐹‘(𝑁 − 1)) ∘𝑓 − ((1...𝑁) × {1})) = (1st ‘(1st𝑈)))
27798, 5, 275, 3, 208poimirlem10 33549 . . . . . . . 8 (𝜑 → ((𝐹‘(𝑁 − 1)) ∘𝑓 − ((1...𝑁) × {1})) = (1st ‘(1st𝑇)))
278276, 277eqtr3d 2687 . . . . . . 7 (𝜑 → (1st ‘(1st𝑈)) = (1st ‘(1st𝑇)))
279278fveq1d 6231 . . . . . 6 (𝜑 → ((1st ‘(1st𝑈))‘𝑦) = ((1st ‘(1st𝑇))‘𝑦))
280279adantr 480 . . . . 5 ((𝜑 ∧ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀)))) → ((1st ‘(1st𝑈))‘𝑦) = ((1st ‘(1st𝑇))‘𝑦))
281187, 274, 2803eqtr3d 2693 . . . 4 ((𝜑 ∧ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀)))) → (((1st ‘(1st𝑇))‘𝑦) + 1) = ((1st ‘(1st𝑇))‘𝑦))
282 elmapi 7921 . . . . . . . . . . . 12 ((1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑𝑚 (1...𝑁)) → (1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾))
283231, 282syl 17 . . . . . . . . . . 11 (𝜑 → (1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾))
284283ffvelrnda 6399 . . . . . . . . . 10 ((𝜑𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑦) ∈ (0..^𝐾))
285 elfzonn0 12552 . . . . . . . . . 10 (((1st ‘(1st𝑇))‘𝑦) ∈ (0..^𝐾) → ((1st ‘(1st𝑇))‘𝑦) ∈ ℕ0)
286284, 285syl 17 . . . . . . . . 9 ((𝜑𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑦) ∈ ℕ0)
287286nn0red 11390 . . . . . . . 8 ((𝜑𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑦) ∈ ℝ)
288287ltp1d 10992 . . . . . . . 8 ((𝜑𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑦) < (((1st ‘(1st𝑇))‘𝑦) + 1))
289287, 288gtned 10210 . . . . . . 7 ((𝜑𝑦 ∈ (1...𝑁)) → (((1st ‘(1st𝑇))‘𝑦) + 1) ≠ ((1st ‘(1st𝑇))‘𝑦))
290229, 289syldan 486 . . . . . 6 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → (((1st ‘(1st𝑇))‘𝑦) + 1) ≠ ((1st ‘(1st𝑇))‘𝑦))
291290neneqd 2828 . . . . 5 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → ¬ (((1st ‘(1st𝑇))‘𝑦) + 1) = ((1st ‘(1st𝑇))‘𝑦))
292291adantrr 753 . . . 4 ((𝜑 ∧ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀)))) → ¬ (((1st ‘(1st𝑇))‘𝑦) + 1) = ((1st ‘(1st𝑇))‘𝑦))
293281, 292pm2.65da 599 . . 3 (𝜑 → ¬ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀))))
294 iman 439 . . 3 ((𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) → 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀))) ↔ ¬ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀))))
295293, 294sylibr 224 . 2 (𝜑 → (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) → 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀))))
296295ssrdv 3642 1 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑀)) ⊆ ((2nd ‘(1st𝑈)) “ (1...𝑀)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1523   ∈ wcel 2030  {cab 2637   ≠ wne 2823  {crab 2945  Vcvv 3231  ⦋csb 3566   ∖ cdif 3604   ∪ cun 3605   ∩ cin 3606   ⊆ wss 3607  ∅c0 3948  ifcif 4119  {csn 4210   class class class wbr 4685   ↦ cmpt 4762   × cxp 5141  ◡ccnv 5142  ran crn 5144   “ cima 5146  Fun wfun 5920   Fn wfn 5921  ⟶wf 5922  –onto→wfo 5924  –1-1-onto→wf1o 5925  ‘cfv 5926  (class class class)co 6690   ∘𝑓 cof 6937  1st c1st 7208  2nd c2nd 7209   ↑𝑚 cmap 7899  ℂcc 9972  0cc0 9974  1c1 9975   + caddc 9977   < clt 10112   ≤ cle 10113   − cmin 10304  ℕcn 11058  ℕ0cn0 11330  ℤcz 11415  ...cfz 12364  ..^cfzo 12504 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-er 7787  df-map 7901  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-n0 11331  df-z 11416  df-uz 11726  df-fz 12365  df-fzo 12505 This theorem is referenced by:  poimirlem13  33552
 Copyright terms: Public domain W3C validator