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

Theorem poimirlem11 34785
Description: Lemma for poimir 34807 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..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
poimirlem22.1 (𝜑𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (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 3945 . . . . . . 7 (𝑦 ∈ (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∖ ((2nd ‘(1st𝑈)) “ (1...𝑀))) ↔ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀))))
2 imassrn 5934 . . . . . . . . . . . 12 ((2nd ‘(1st𝑇)) “ (1...𝑀)) ⊆ ran (2nd ‘(1st𝑇))
3 poimirlem12.2 . . . . . . . . . . . . . . . . . 18 (𝜑𝑇𝑆)
4 elrabi 3674 . . . . . . . . . . . . . . . . . . 19 (𝑇 ∈ {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
5 poimirlem22.s . . . . . . . . . . . . . . . . . . 19 𝑆 = {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))}
64, 5eleq2s 2931 . . . . . . . . . . . . . . . . . 18 (𝑇𝑆𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
73, 6syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
8 xp1st 7712 . . . . . . . . . . . . . . . . 17 (𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
97, 8syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (1st𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
10 xp2nd 7713 . . . . . . . . . . . . . . . 16 ((1st𝑇) ∈ (((0..^𝐾) ↑m (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 6677 . . . . . . . . . . . . . . . 16 (2nd ‘(1st𝑇)) ∈ V
13 f1oeq1 6598 . . . . . . . . . . . . . . . 16 (𝑓 = (2nd ‘(1st𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
1412, 13elab 3666 . . . . . . . . . . . . . . 15 ((2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
1511, 14sylib 219 . . . . . . . . . . . . . 14 (𝜑 → (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
16 f1of 6609 . . . . . . . . . . . . . 14 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)):(1...𝑁)⟶(1...𝑁))
1715, 16syl 17 . . . . . . . . . . . . 13 (𝜑 → (2nd ‘(1st𝑇)):(1...𝑁)⟶(1...𝑁))
1817frnd 6515 . . . . . . . . . . . 12 (𝜑 → ran (2nd ‘(1st𝑇)) ⊆ (1...𝑁))
192, 18sstrid 3977 . . . . . . . . . . 11 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑀)) ⊆ (1...𝑁))
20 poimirlem11.4 . . . . . . . . . . . . . . . . 17 (𝜑𝑈𝑆)
21 elrabi 3674 . . . . . . . . . . . . . . . . . 18 (𝑈 ∈ {𝑡 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∣ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))} → 𝑈 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
2221, 5eleq2s 2931 . . . . . . . . . . . . . . . . 17 (𝑈𝑆𝑈 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
2320, 22syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑈 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
24 xp1st 7712 . . . . . . . . . . . . . . . 16 (𝑈 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑈) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
2523, 24syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (1st𝑈) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
26 xp2nd 7713 . . . . . . . . . . . . . . 15 ((1st𝑈) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd ‘(1st𝑈)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
2725, 26syl 17 . . . . . . . . . . . . . 14 (𝜑 → (2nd ‘(1st𝑈)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
28 fvex 6677 . . . . . . . . . . . . . . 15 (2nd ‘(1st𝑈)) ∈ V
29 f1oeq1 6598 . . . . . . . . . . . . . . 15 (𝑓 = (2nd ‘(1st𝑈)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁)))
3028, 29elab 3666 . . . . . . . . . . . . . 14 ((2nd ‘(1st𝑈)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁))
3127, 30sylib 219 . . . . . . . . . . . . 13 (𝜑 → (2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁))
32 f1ofo 6616 . . . . . . . . . . . . 13 ((2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑈)):(1...𝑁)–onto→(1...𝑁))
3331, 32syl 17 . . . . . . . . . . . 12 (𝜑 → (2nd ‘(1st𝑈)):(1...𝑁)–onto→(1...𝑁))
34 foima 6589 . . . . . . . . . . . 12 ((2nd ‘(1st𝑈)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑈)) “ (1...𝑁)) = (1...𝑁))
3533, 34syl 17 . . . . . . . . . . 11 (𝜑 → ((2nd ‘(1st𝑈)) “ (1...𝑁)) = (1...𝑁))
3619, 35sseqtrrd 4007 . . . . . . . . . 10 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑀)) ⊆ ((2nd ‘(1st𝑈)) “ (1...𝑁)))
3736ssdifd 4116 . . . . . . . . 9 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∖ ((2nd ‘(1st𝑈)) “ (1...𝑀))) ⊆ (((2nd ‘(1st𝑈)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑈)) “ (1...𝑀))))
38 dff1o3 6615 . . . . . . . . . . . . 13 ((2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘(1st𝑈)):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd ‘(1st𝑈))))
3938simprbi 497 . . . . . . . . . . . 12 ((2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun (2nd ‘(1st𝑈)))
4031, 39syl 17 . . . . . . . . . . 11 (𝜑 → Fun (2nd ‘(1st𝑈)))
41 imadif 6432 . . . . . . . . . . 11 (Fun (2nd ‘(1st𝑈)) → ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ (1...𝑀))) = (((2nd ‘(1st𝑈)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑈)) “ (1...𝑀))))
4240, 41syl 17 . . . . . . . . . 10 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ (1...𝑀))) = (((2nd ‘(1st𝑈)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑈)) “ (1...𝑀))))
43 difun2 4427 . . . . . . . . . . . 12 ((((𝑀 + 1)...𝑁) ∪ (1...𝑀)) ∖ (1...𝑀)) = (((𝑀 + 1)...𝑁) ∖ (1...𝑀))
44 poimirlem11.6 . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ (1...𝑁))
45 fzsplit 12923 . . . . . . . . . . . . . . 15 (𝑀 ∈ (1...𝑁) → (1...𝑁) = ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)))
4644, 45syl 17 . . . . . . . . . . . . . 14 (𝜑 → (1...𝑁) = ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)))
47 uncom 4128 . . . . . . . . . . . . . 14 ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)) = (((𝑀 + 1)...𝑁) ∪ (1...𝑀))
4846, 47syl6eq 2872 . . . . . . . . . . . . 13 (𝜑 → (1...𝑁) = (((𝑀 + 1)...𝑁) ∪ (1...𝑀)))
4948difeq1d 4097 . . . . . . . . . . . 12 (𝜑 → ((1...𝑁) ∖ (1...𝑀)) = ((((𝑀 + 1)...𝑁) ∪ (1...𝑀)) ∖ (1...𝑀)))
50 incom 4177 . . . . . . . . . . . . . 14 (((𝑀 + 1)...𝑁) ∩ (1...𝑀)) = ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))
51 elfznn 12926 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ (1...𝑁) → 𝑀 ∈ ℕ)
5244, 51syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ∈ ℕ)
5352nnred 11642 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℝ)
5453ltp1d 11559 . . . . . . . . . . . . . . 15 (𝜑𝑀 < (𝑀 + 1))
55 fzdisj 12924 . . . . . . . . . . . . . . 15 (𝑀 < (𝑀 + 1) → ((1...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅)
5654, 55syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((1...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅)
5750, 56syl5eq 2868 . . . . . . . . . . . . 13 (𝜑 → (((𝑀 + 1)...𝑁) ∩ (1...𝑀)) = ∅)
58 disj3 4401 . . . . . . . . . . . . 13 ((((𝑀 + 1)...𝑁) ∩ (1...𝑀)) = ∅ ↔ ((𝑀 + 1)...𝑁) = (((𝑀 + 1)...𝑁) ∖ (1...𝑀)))
5957, 58sylib 219 . . . . . . . . . . . 12 (𝜑 → ((𝑀 + 1)...𝑁) = (((𝑀 + 1)...𝑁) ∖ (1...𝑀)))
6043, 49, 593eqtr4a 2882 . . . . . . . . . . 11 (𝜑 → ((1...𝑁) ∖ (1...𝑀)) = ((𝑀 + 1)...𝑁))
6160imaeq2d 5923 . . . . . . . . . 10 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ (1...𝑀))) = ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
6242, 61eqtr3d 2858 . . . . . . . . 9 (𝜑 → (((2nd ‘(1st𝑈)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑈)) “ (1...𝑀))) = ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
6337, 62sseqtrd 4006 . . . . . . . 8 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∖ ((2nd ‘(1st𝑈)) “ (1...𝑀))) ⊆ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
6463sselda 3966 . . . . . . 7 ((𝜑𝑦 ∈ (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∖ ((2nd ‘(1st𝑈)) “ (1...𝑀)))) → 𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
651, 64sylan2br 594 . . . . . 6 ((𝜑 ∧ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀)))) → 𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
66 fveq2 6664 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑈 → (2nd𝑡) = (2nd𝑈))
6766breq2d 5070 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑈 → (𝑦 < (2nd𝑡) ↔ 𝑦 < (2nd𝑈)))
6867ifbid 4487 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑈 → if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd𝑈), 𝑦, (𝑦 + 1)))
6968csbeq1d 3886 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑈if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑈), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))
70 2fveq3 6669 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑈 → (1st ‘(1st𝑡)) = (1st ‘(1st𝑈)))
71 2fveq3 6669 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑈 → (2nd ‘(1st𝑡)) = (2nd ‘(1st𝑈)))
7271imaeq1d 5922 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑈 → ((2nd ‘(1st𝑡)) “ (1...𝑗)) = ((2nd ‘(1st𝑈)) “ (1...𝑗)))
7372xpeq1d 5578 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑈 → (((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}))
7471imaeq1d 5922 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑈 → ((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)))
7574xpeq1d 5578 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑈 → (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))
7673, 75uneq12d 4139 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑈 → ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0})))
7770, 76oveq12d 7163 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑈 → ((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))))
7877csbeq2dv 3889 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑈if(𝑦 < (2nd𝑈), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑈), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))))
7969, 78eqtrd 2856 . . . . . . . . . . . . . . 15 (𝑡 = 𝑈if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑈), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))))
8079mpteq2dv 5154 . . . . . . . . . . . . . 14 (𝑡 = 𝑈 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑈), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0})))))
8180eqeq2d 2832 . . . . . . . . . . . . 13 (𝑡 = 𝑈 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑈), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
8281, 5elrab2 3682 . . . . . . . . . . . 12 (𝑈𝑆 ↔ (𝑈 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑈), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
8382simprbi 497 . . . . . . . . . . 11 (𝑈𝑆𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑈), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0})))))
8420, 83syl 17 . . . . . . . . . 10 (𝜑𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑈), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0})))))
85 poimirlem11.5 . . . . . . . . . . . . . . . 16 (𝜑 → (2nd𝑈) = 0)
86 breq12 5063 . . . . . . . . . . . . . . . 16 ((𝑦 = (𝑀 − 1) ∧ (2nd𝑈) = 0) → (𝑦 < (2nd𝑈) ↔ (𝑀 − 1) < 0))
8785, 86sylan2 592 . . . . . . . . . . . . . . 15 ((𝑦 = (𝑀 − 1) ∧ 𝜑) → (𝑦 < (2nd𝑈) ↔ (𝑀 − 1) < 0))
8887ancoms 459 . . . . . . . . . . . . . 14 ((𝜑𝑦 = (𝑀 − 1)) → (𝑦 < (2nd𝑈) ↔ (𝑀 − 1) < 0))
89 oveq1 7152 . . . . . . . . . . . . . . 15 (𝑦 = (𝑀 − 1) → (𝑦 + 1) = ((𝑀 − 1) + 1))
9052nncnd 11643 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℂ)
91 npcan1 11054 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℂ → ((𝑀 − 1) + 1) = 𝑀)
9290, 91syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑀 − 1) + 1) = 𝑀)
9389, 92sylan9eqr 2878 . . . . . . . . . . . . . 14 ((𝜑𝑦 = (𝑀 − 1)) → (𝑦 + 1) = 𝑀)
9488, 93ifbieq2d 4490 . . . . . . . . . . . . 13 ((𝜑𝑦 = (𝑀 − 1)) → if(𝑦 < (2nd𝑈), 𝑦, (𝑦 + 1)) = if((𝑀 − 1) < 0, 𝑦, 𝑀))
9552nnzd 12075 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑀 ∈ ℤ)
96 poimir.0 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑁 ∈ ℕ)
9796nnzd 12075 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ ℤ)
98 elfzm1b 12975 . . . . . . . . . . . . . . . . . . 19 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∈ (1...𝑁) ↔ (𝑀 − 1) ∈ (0...(𝑁 − 1))))
9995, 97, 98syl2anc 584 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑀 ∈ (1...𝑁) ↔ (𝑀 − 1) ∈ (0...(𝑁 − 1))))
10044, 99mpbid 233 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑀 − 1) ∈ (0...(𝑁 − 1)))
101 elfzle1 12900 . . . . . . . . . . . . . . . . 17 ((𝑀 − 1) ∈ (0...(𝑁 − 1)) → 0 ≤ (𝑀 − 1))
102100, 101syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ≤ (𝑀 − 1))
103 0red 10633 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 ∈ ℝ)
104 nnm1nn0 11927 . . . . . . . . . . . . . . . . . . 19 (𝑀 ∈ ℕ → (𝑀 − 1) ∈ ℕ0)
10552, 104syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑀 − 1) ∈ ℕ0)
106105nn0red 11945 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑀 − 1) ∈ ℝ)
107103, 106lenltd 10775 . . . . . . . . . . . . . . . 16 (𝜑 → (0 ≤ (𝑀 − 1) ↔ ¬ (𝑀 − 1) < 0))
108102, 107mpbid 233 . . . . . . . . . . . . . . 15 (𝜑 → ¬ (𝑀 − 1) < 0)
109108iffalsed 4476 . . . . . . . . . . . . . 14 (𝜑 → if((𝑀 − 1) < 0, 𝑦, 𝑀) = 𝑀)
110109adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑦 = (𝑀 − 1)) → if((𝑀 − 1) < 0, 𝑦, 𝑀) = 𝑀)
11194, 110eqtrd 2856 . . . . . . . . . . . 12 ((𝜑𝑦 = (𝑀 − 1)) → if(𝑦 < (2nd𝑈), 𝑦, (𝑦 + 1)) = 𝑀)
112111csbeq1d 3886 . . . . . . . . . . 11 ((𝜑𝑦 = (𝑀 − 1)) → if(𝑦 < (2nd𝑈), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))) = 𝑀 / 𝑗((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))))
113 oveq2 7153 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑀 → (1...𝑗) = (1...𝑀))
114113imaeq2d 5923 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑀 → ((2nd ‘(1st𝑈)) “ (1...𝑗)) = ((2nd ‘(1st𝑈)) “ (1...𝑀)))
115114xpeq1d 5578 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑀 → (((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}))
116 oveq1 7152 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑀 → (𝑗 + 1) = (𝑀 + 1))
117116oveq1d 7160 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑀 → ((𝑗 + 1)...𝑁) = ((𝑀 + 1)...𝑁))
118117imaeq2d 5923 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑀 → ((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
119118xpeq1d 5578 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑀 → (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))
120115, 119uneq12d 4139 . . . . . . . . . . . . . . 15 (𝑗 = 𝑀 → ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})))
121120oveq2d 7161 . . . . . . . . . . . . . 14 (𝑗 = 𝑀 → ((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))))
122121adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑗 = 𝑀) → ((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))))
12344, 122csbied 3918 . . . . . . . . . . . 12 (𝜑𝑀 / 𝑗((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))))
124123adantr 481 . . . . . . . . . . 11 ((𝜑𝑦 = (𝑀 − 1)) → 𝑀 / 𝑗((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))))
125112, 124eqtrd 2856 . . . . . . . . . 10 ((𝜑𝑦 = (𝑀 − 1)) → if(𝑦 < (2nd𝑈), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))))
126 ovexd 7180 . . . . . . . . . 10 (𝜑 → ((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))) ∈ V)
12784, 125, 100, 126fvmptd 6768 . . . . . . . . 9 (𝜑 → (𝐹‘(𝑀 − 1)) = ((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))))
128127fveq1d 6666 . . . . . . . 8 (𝜑 → ((𝐹‘(𝑀 − 1))‘𝑦) = (((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦))
129128adantr 481 . . . . . . 7 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → ((𝐹‘(𝑀 − 1))‘𝑦) = (((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦))
130 imassrn 5934 . . . . . . . . . 10 ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) ⊆ ran (2nd ‘(1st𝑈))
131 f1of 6609 . . . . . . . . . . . 12 ((2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑈)):(1...𝑁)⟶(1...𝑁))
13231, 131syl 17 . . . . . . . . . . 11 (𝜑 → (2nd ‘(1st𝑈)):(1...𝑁)⟶(1...𝑁))
133132frnd 6515 . . . . . . . . . 10 (𝜑 → ran (2nd ‘(1st𝑈)) ⊆ (1...𝑁))
134130, 133sstrid 3977 . . . . . . . . 9 (𝜑 → ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) ⊆ (1...𝑁))
135134sselda 3966 . . . . . . . 8 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → 𝑦 ∈ (1...𝑁))
136 xp1st 7712 . . . . . . . . . . . 12 ((1st𝑈) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(1st𝑈)) ∈ ((0..^𝐾) ↑m (1...𝑁)))
13725, 136syl 17 . . . . . . . . . . 11 (𝜑 → (1st ‘(1st𝑈)) ∈ ((0..^𝐾) ↑m (1...𝑁)))
138 elmapfn 8419 . . . . . . . . . . 11 ((1st ‘(1st𝑈)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st ‘(1st𝑈)) Fn (1...𝑁))
139137, 138syl 17 . . . . . . . . . 10 (𝜑 → (1st ‘(1st𝑈)) Fn (1...𝑁))
140139adantr 481 . . . . . . . . 9 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → (1st ‘(1st𝑈)) Fn (1...𝑁))
141 1ex 10626 . . . . . . . . . . . . . 14 1 ∈ V
142 fnconstg 6561 . . . . . . . . . . . . . 14 (1 ∈ V → (((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) Fn ((2nd ‘(1st𝑈)) “ (1...𝑀)))
143141, 142ax-mp 5 . . . . . . . . . . . . 13 (((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) Fn ((2nd ‘(1st𝑈)) “ (1...𝑀))
144 c0ex 10624 . . . . . . . . . . . . . 14 0 ∈ V
145 fnconstg 6561 . . . . . . . . . . . . . 14 (0 ∈ V → (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
146144, 145ax-mp 5 . . . . . . . . . . . . 13 (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))
147143, 146pm3.2i 471 . . . . . . . . . . . 12 ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) Fn ((2nd ‘(1st𝑈)) “ (1...𝑀)) ∧ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
148 imain 6433 . . . . . . . . . . . . . 14 (Fun (2nd ‘(1st𝑈)) → ((2nd ‘(1st𝑈)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑈)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))))
14940, 148syl 17 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑈)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))))
15056imaeq2d 5923 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ((2nd ‘(1st𝑈)) “ ∅))
151 ima0 5939 . . . . . . . . . . . . . 14 ((2nd ‘(1st𝑈)) “ ∅) = ∅
152150, 151syl6eq 2872 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ∅)
153149, 152eqtr3d 2858 . . . . . . . . . . . 12 (𝜑 → (((2nd ‘(1st𝑈)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) = ∅)
154 fnun 6457 . . . . . . . . . . . 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)...𝑁))))
155147, 153, 154sylancr 587 . . . . . . . . . . 11 (𝜑 → ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2nd ‘(1st𝑈)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))))
156 imaundi 6002 . . . . . . . . . . . . 13 ((2nd ‘(1st𝑈)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑈)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
15746imaeq2d 5923 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑈)) “ (1...𝑁)) = ((2nd ‘(1st𝑈)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))))
158157, 35eqtr3d 2858 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (1...𝑁))
159156, 158syl5eqr 2870 . . . . . . . . . . . 12 (𝜑 → (((2nd ‘(1st𝑈)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) = (1...𝑁))
160159fneq2d 6441 . . . . . . . . . . 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...𝑁)))
161155, 160mpbid 233 . . . . . . . . . 10 (𝜑 → ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
162161adantr 481 . . . . . . . . 9 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
163 ovexd 7180 . . . . . . . . 9 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → (1...𝑁) ∈ V)
164 inidm 4194 . . . . . . . . 9 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
165 eqidd 2822 . . . . . . . . 9 (((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) ∧ 𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑈))‘𝑦) = ((1st ‘(1st𝑈))‘𝑦))
166 fvun2 6749 . . . . . . . . . . . . 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})‘𝑦))
167143, 146, 166mp3an12 1442 . . . . . . . . . . . 12 (((((2nd ‘(1st𝑈)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) = ∅ ∧ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → (((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = ((((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})‘𝑦))
168153, 167sylan 580 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → (((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = ((((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})‘𝑦))
169144fvconst2 6959 . . . . . . . . . . . 12 (𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) → ((((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})‘𝑦) = 0)
170169adantl 482 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → ((((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})‘𝑦) = 0)
171168, 170eqtrd 2856 . . . . . . . . . 10 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → (((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = 0)
172171adantr 481 . . . . . . . . 9 (((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) ∧ 𝑦 ∈ (1...𝑁)) → (((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = 0)
173140, 162, 163, 163, 164, 165, 172ofval 7407 . . . . . . . 8 (((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) ∧ 𝑦 ∈ (1...𝑁)) → (((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦) = (((1st ‘(1st𝑈))‘𝑦) + 0))
174135, 173mpdan 683 . . . . . . 7 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → (((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦) = (((1st ‘(1st𝑈))‘𝑦) + 0))
175 elmapi 8418 . . . . . . . . . . . . 13 ((1st ‘(1st𝑈)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st ‘(1st𝑈)):(1...𝑁)⟶(0..^𝐾))
176137, 175syl 17 . . . . . . . . . . . 12 (𝜑 → (1st ‘(1st𝑈)):(1...𝑁)⟶(0..^𝐾))
177176ffvelrnda 6844 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑈))‘𝑦) ∈ (0..^𝐾))
178 elfzonn0 13072 . . . . . . . . . . 11 (((1st ‘(1st𝑈))‘𝑦) ∈ (0..^𝐾) → ((1st ‘(1st𝑈))‘𝑦) ∈ ℕ0)
179177, 178syl 17 . . . . . . . . . 10 ((𝜑𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑈))‘𝑦) ∈ ℕ0)
180179nn0cnd 11946 . . . . . . . . 9 ((𝜑𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑈))‘𝑦) ∈ ℂ)
181135, 180syldan 591 . . . . . . . 8 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → ((1st ‘(1st𝑈))‘𝑦) ∈ ℂ)
182181addid1d 10829 . . . . . . 7 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → (((1st ‘(1st𝑈))‘𝑦) + 0) = ((1st ‘(1st𝑈))‘𝑦))
183129, 174, 1823eqtrd 2860 . . . . . 6 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → ((𝐹‘(𝑀 − 1))‘𝑦) = ((1st ‘(1st𝑈))‘𝑦))
18465, 183syldan 591 . . . . 5 ((𝜑 ∧ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀)))) → ((𝐹‘(𝑀 − 1))‘𝑦) = ((1st ‘(1st𝑈))‘𝑦))
185 fveq2 6664 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑇 → (2nd𝑡) = (2nd𝑇))
186185breq2d 5070 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑇 → (𝑦 < (2nd𝑡) ↔ 𝑦 < (2nd𝑇)))
187186ifbid 4487 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑇 → if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)))
188187csbeq1d 3886 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑇if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))))
189 2fveq3 6669 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑇 → (1st ‘(1st𝑡)) = (1st ‘(1st𝑇)))
190 2fveq3 6669 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑇 → (2nd ‘(1st𝑡)) = (2nd ‘(1st𝑇)))
191190imaeq1d 5922 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...𝑗)))
192191xpeq1d 5578 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}))
193190imaeq1d 5922 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)))
194193xpeq1d 5578 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
195192, 194uneq12d 4139 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑇 → ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))
196189, 195oveq12d 7163 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑇 → ((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
197196csbeq2dv 3889 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑇if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
198188, 197eqtrd 2856 . . . . . . . . . . . . . . 15 (𝑡 = 𝑇if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
199198mpteq2dv 5154 . . . . . . . . . . . . . 14 (𝑡 = 𝑇 → (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
200199eqeq2d 2832 . . . . . . . . . . . . 13 (𝑡 = 𝑇 → (𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})))) ↔ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
201200, 5elrab2 3682 . . . . . . . . . . . 12 (𝑇𝑆 ↔ (𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) ∧ 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))))
202201simprbi 497 . . . . . . . . . . 11 (𝑇𝑆𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
2033, 202syl 17 . . . . . . . . . 10 (𝜑𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
204 poimirlem11.3 . . . . . . . . . . . . . . . 16 (𝜑 → (2nd𝑇) = 0)
205 breq12 5063 . . . . . . . . . . . . . . . 16 ((𝑦 = (𝑀 − 1) ∧ (2nd𝑇) = 0) → (𝑦 < (2nd𝑇) ↔ (𝑀 − 1) < 0))
206204, 205sylan2 592 . . . . . . . . . . . . . . 15 ((𝑦 = (𝑀 − 1) ∧ 𝜑) → (𝑦 < (2nd𝑇) ↔ (𝑀 − 1) < 0))
207206ancoms 459 . . . . . . . . . . . . . 14 ((𝜑𝑦 = (𝑀 − 1)) → (𝑦 < (2nd𝑇) ↔ (𝑀 − 1) < 0))
208207, 93ifbieq2d 4490 . . . . . . . . . . . . 13 ((𝜑𝑦 = (𝑀 − 1)) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) = if((𝑀 − 1) < 0, 𝑦, 𝑀))
209208, 110eqtrd 2856 . . . . . . . . . . . 12 ((𝜑𝑦 = (𝑀 − 1)) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) = 𝑀)
210209csbeq1d 3886 . . . . . . . . . . 11 ((𝜑𝑦 = (𝑀 − 1)) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = 𝑀 / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
211113imaeq2d 5923 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑀 → ((2nd ‘(1st𝑇)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...𝑀)))
212211xpeq1d 5578 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑀 → (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}))
213117imaeq2d 5923 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑀 → ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)))
214213xpeq1d 5578 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑀 → (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))
215212, 214uneq12d 4139 . . . . . . . . . . . . . . 15 (𝑗 = 𝑀 → ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))
216215oveq2d 7161 . . . . . . . . . . . . . 14 (𝑗 = 𝑀 → ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
217216adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑗 = 𝑀) → ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
21844, 217csbied 3918 . . . . . . . . . . . 12 (𝜑𝑀 / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
219218adantr 481 . . . . . . . . . . 11 ((𝜑𝑦 = (𝑀 − 1)) → 𝑀 / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
220210, 219eqtrd 2856 . . . . . . . . . 10 ((𝜑𝑦 = (𝑀 − 1)) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
221 ovexd 7180 . . . . . . . . . 10 (𝜑 → ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) ∈ V)
222203, 220, 100, 221fvmptd 6768 . . . . . . . . 9 (𝜑 → (𝐹‘(𝑀 − 1)) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
223222fveq1d 6666 . . . . . . . 8 (𝜑 → ((𝐹‘(𝑀 − 1))‘𝑦) = (((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦))
224223adantr 481 . . . . . . 7 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → ((𝐹‘(𝑀 − 1))‘𝑦) = (((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦))
22519sselda 3966 . . . . . . . 8 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → 𝑦 ∈ (1...𝑁))
226 xp1st 7712 . . . . . . . . . . . 12 ((1st𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)))
2279, 226syl 17 . . . . . . . . . . 11 (𝜑 → (1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)))
228 elmapfn 8419 . . . . . . . . . . 11 ((1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st ‘(1st𝑇)) Fn (1...𝑁))
229227, 228syl 17 . . . . . . . . . 10 (𝜑 → (1st ‘(1st𝑇)) Fn (1...𝑁))
230229adantr 481 . . . . . . . . 9 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → (1st ‘(1st𝑇)) Fn (1...𝑁))
231 fnconstg 6561 . . . . . . . . . . . . . 14 (1 ∈ V → (((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...𝑀)))
232141, 231ax-mp 5 . . . . . . . . . . . . 13 (((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...𝑀))
233 fnconstg 6561 . . . . . . . . . . . . . 14 (0 ∈ V → (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)))
234144, 233ax-mp 5 . . . . . . . . . . . . 13 (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))
235232, 234pm3.2i 471 . . . . . . . . . . . 12 ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)))
236 dff1o3 6615 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd ‘(1st𝑇))))
237236simprbi 497 . . . . . . . . . . . . . . 15 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun (2nd ‘(1st𝑇)))
23815, 237syl 17 . . . . . . . . . . . . . 14 (𝜑 → Fun (2nd ‘(1st𝑇)))
239 imain 6433 . . . . . . . . . . . . . 14 (Fun (2nd ‘(1st𝑇)) → ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))))
240238, 239syl 17 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))))
24156imaeq2d 5923 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ((2nd ‘(1st𝑇)) “ ∅))
242 ima0 5939 . . . . . . . . . . . . . 14 ((2nd ‘(1st𝑇)) “ ∅) = ∅
243241, 242syl6eq 2872 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ∅)
244240, 243eqtr3d 2858 . . . . . . . . . . . 12 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅)
245 fnun 6457 . . . . . . . . . . . 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)...𝑁))))
246235, 244, 245sylancr 587 . . . . . . . . . . 11 (𝜑 → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))))
247 imaundi 6002 . . . . . . . . . . . . 13 ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)))
24846imaeq2d 5923 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))))
249 f1ofo 6616 . . . . . . . . . . . . . . . 16 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁))
25015, 249syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁))
251 foima 6589 . . . . . . . . . . . . . . 15 ((2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
252250, 251syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
253248, 252eqtr3d 2858 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (1...𝑁))
254247, 253syl5eqr 2870 . . . . . . . . . . . 12 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))) = (1...𝑁))
255254fneq2d 6441 . . . . . . . . . . 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...𝑁)))
256246, 255mpbid 233 . . . . . . . . . 10 (𝜑 → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
257256adantr 481 . . . . . . . . 9 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
258 ovexd 7180 . . . . . . . . 9 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → (1...𝑁) ∈ V)
259 eqidd 2822 . . . . . . . . 9 (((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) ∧ 𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑦) = ((1st ‘(1st𝑇))‘𝑦))
260 fvun1 6748 . . . . . . . . . . . . 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})‘𝑦))
261232, 234, 260mp3an12 1442 . . . . . . . . . . . 12 (((((2nd ‘(1st𝑇)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅ ∧ 𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → (((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1})‘𝑦))
262244, 261sylan 580 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → (((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1})‘𝑦))
263141fvconst2 6959 . . . . . . . . . . . 12 (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1})‘𝑦) = 1)
264263adantl 482 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1})‘𝑦) = 1)
265262, 264eqtrd 2856 . . . . . . . . . 10 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → (((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = 1)
266265adantr 481 . . . . . . . . 9 (((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) ∧ 𝑦 ∈ (1...𝑁)) → (((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = 1)
267230, 257, 258, 258, 164, 259, 266ofval 7407 . . . . . . . 8 (((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) ∧ 𝑦 ∈ (1...𝑁)) → (((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦) = (((1st ‘(1st𝑇))‘𝑦) + 1))
268225, 267mpdan 683 . . . . . . 7 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → (((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦) = (((1st ‘(1st𝑇))‘𝑦) + 1))
269224, 268eqtrd 2856 . . . . . 6 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → ((𝐹‘(𝑀 − 1))‘𝑦) = (((1st ‘(1st𝑇))‘𝑦) + 1))
270269adantrr 713 . . . . 5 ((𝜑 ∧ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀)))) → ((𝐹‘(𝑀 − 1))‘𝑦) = (((1st ‘(1st𝑇))‘𝑦) + 1))
271 poimirlem22.1 . . . . . . . . 9 (𝜑𝐹:(0...(𝑁 − 1))⟶((0...𝐾) ↑m (1...𝑁)))
27296, 5, 271, 20, 85poimirlem10 34784 . . . . . . . 8 (𝜑 → ((𝐹‘(𝑁 − 1)) ∘f − ((1...𝑁) × {1})) = (1st ‘(1st𝑈)))
27396, 5, 271, 3, 204poimirlem10 34784 . . . . . . . 8 (𝜑 → ((𝐹‘(𝑁 − 1)) ∘f − ((1...𝑁) × {1})) = (1st ‘(1st𝑇)))
274272, 273eqtr3d 2858 . . . . . . 7 (𝜑 → (1st ‘(1st𝑈)) = (1st ‘(1st𝑇)))
275274fveq1d 6666 . . . . . 6 (𝜑 → ((1st ‘(1st𝑈))‘𝑦) = ((1st ‘(1st𝑇))‘𝑦))
276275adantr 481 . . . . 5 ((𝜑 ∧ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀)))) → ((1st ‘(1st𝑈))‘𝑦) = ((1st ‘(1st𝑇))‘𝑦))
277184, 270, 2763eqtr3d 2864 . . . 4 ((𝜑 ∧ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀)))) → (((1st ‘(1st𝑇))‘𝑦) + 1) = ((1st ‘(1st𝑇))‘𝑦))
278 elmapi 8418 . . . . . . . . . . . 12 ((1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾))
279227, 278syl 17 . . . . . . . . . . 11 (𝜑 → (1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾))
280279ffvelrnda 6844 . . . . . . . . . 10 ((𝜑𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑦) ∈ (0..^𝐾))
281 elfzonn0 13072 . . . . . . . . . 10 (((1st ‘(1st𝑇))‘𝑦) ∈ (0..^𝐾) → ((1st ‘(1st𝑇))‘𝑦) ∈ ℕ0)
282280, 281syl 17 . . . . . . . . 9 ((𝜑𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑦) ∈ ℕ0)
283282nn0red 11945 . . . . . . . 8 ((𝜑𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑦) ∈ ℝ)
284283ltp1d 11559 . . . . . . . 8 ((𝜑𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑦) < (((1st ‘(1st𝑇))‘𝑦) + 1))
285283, 284gtned 10764 . . . . . . 7 ((𝜑𝑦 ∈ (1...𝑁)) → (((1st ‘(1st𝑇))‘𝑦) + 1) ≠ ((1st ‘(1st𝑇))‘𝑦))
286225, 285syldan 591 . . . . . 6 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → (((1st ‘(1st𝑇))‘𝑦) + 1) ≠ ((1st ‘(1st𝑇))‘𝑦))
287286neneqd 3021 . . . . 5 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → ¬ (((1st ‘(1st𝑇))‘𝑦) + 1) = ((1st ‘(1st𝑇))‘𝑦))
288287adantrr 713 . . . 4 ((𝜑 ∧ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀)))) → ¬ (((1st ‘(1st𝑇))‘𝑦) + 1) = ((1st ‘(1st𝑇))‘𝑦))
289277, 288pm2.65da 813 . . 3 (𝜑 → ¬ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀))))
290 iman 402 . . 3 ((𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) → 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀))) ↔ ¬ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀))))
291289, 290sylibr 235 . 2 (𝜑 → (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) → 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀))))
292291ssrdv 3972 1 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑀)) ⊆ ((2nd ‘(1st𝑈)) “ (1...𝑀)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396   = wceq 1528  wcel 2105  {cab 2799  wne 3016  {crab 3142  Vcvv 3495  csb 3882  cdif 3932  cun 3933  cin 3934  wss 3935  c0 4290  ifcif 4465  {csn 4559   class class class wbr 5058  cmpt 5138   × cxp 5547  ccnv 5548  ran crn 5550  cima 5552  Fun wfun 6343   Fn wfn 6344  wf 6345  ontowfo 6347  1-1-ontowf1o 6348  cfv 6349  (class class class)co 7145  f cof 7396  1st c1st 7678  2nd c2nd 7679  m cmap 8396  cc 10524  0cc0 10526  1c1 10527   + caddc 10529   < clt 10664  cle 10665  cmin 10859  cn 11627  0cn0 11886  cz 11970  ...cfz 12882  ..^cfzo 13023
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4833  df-iun 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-of 7398  df-om 7569  df-1st 7680  df-2nd 7681  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-er 8279  df-map 8398  df-en 8499  df-dom 8500  df-sdom 8501  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11628  df-n0 11887  df-z 11971  df-uz 12233  df-fz 12883  df-fzo 13024
This theorem is referenced by:  poimirlem13  34787
  Copyright terms: Public domain W3C validator