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

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

Proof of Theorem poimirlem12
StepHypRef Expression
1 eldif 3853 . . . . . . 7 (𝑦 ∈ (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∖ ((2nd ‘(1st𝑈)) “ (1...𝑀))) ↔ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀))))
2 imassrn 5914 . . . . . . . . . . . 12 ((2nd ‘(1st𝑇)) “ (1...𝑀)) ⊆ ran (2nd ‘(1st𝑇))
3 poimirlem12.2 . . . . . . . . . . . . . . . 16 (𝜑𝑇𝑆)
4 elrabi 3582 . . . . . . . . . . . . . . . . 17 (𝑇 ∈ {𝑡 ∈ ((((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 . . . . . . . . . . . . . . . . 17 𝑆 = {𝑡 ∈ ((((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 2851 . . . . . . . . . . . . . . . 16 (𝑇𝑆𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
7 xp1st 7746 . . . . . . . . . . . . . . . 16 (𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
83, 6, 73syl 18 . . . . . . . . . . . . . . 15 (𝜑 → (1st𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
9 xp2nd 7747 . . . . . . . . . . . . . . 15 ((1st𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
108, 9syl 17 . . . . . . . . . . . . . 14 (𝜑 → (2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
11 fvex 6687 . . . . . . . . . . . . . . 15 (2nd ‘(1st𝑇)) ∈ V
12 f1oeq1 6606 . . . . . . . . . . . . . . 15 (𝑓 = (2nd ‘(1st𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
1311, 12elab 3573 . . . . . . . . . . . . . 14 ((2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
1410, 13sylib 221 . . . . . . . . . . . . 13 (𝜑 → (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
15 f1of 6618 . . . . . . . . . . . . 13 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)):(1...𝑁)⟶(1...𝑁))
16 frn 6511 . . . . . . . . . . . . 13 ((2nd ‘(1st𝑇)):(1...𝑁)⟶(1...𝑁) → ran (2nd ‘(1st𝑇)) ⊆ (1...𝑁))
1714, 15, 163syl 18 . . . . . . . . . . . 12 (𝜑 → ran (2nd ‘(1st𝑇)) ⊆ (1...𝑁))
182, 17sstrid 3888 . . . . . . . . . . 11 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑀)) ⊆ (1...𝑁))
19 poimirlem12.4 . . . . . . . . . . . . . . 15 (𝜑𝑈𝑆)
20 elrabi 3582 . . . . . . . . . . . . . . . 16 (𝑈 ∈ {𝑡 ∈ ((((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...𝑁)))
2120, 5eleq2s 2851 . . . . . . . . . . . . . . 15 (𝑈𝑆𝑈 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
22 xp1st 7746 . . . . . . . . . . . . . . 15 (𝑈 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)) → (1st𝑈) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
2319, 21, 223syl 18 . . . . . . . . . . . . . 14 (𝜑 → (1st𝑈) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
24 xp2nd 7747 . . . . . . . . . . . . . 14 ((1st𝑈) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (2nd ‘(1st𝑈)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
2523, 24syl 17 . . . . . . . . . . . . 13 (𝜑 → (2nd ‘(1st𝑈)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
26 fvex 6687 . . . . . . . . . . . . . 14 (2nd ‘(1st𝑈)) ∈ V
27 f1oeq1 6606 . . . . . . . . . . . . . 14 (𝑓 = (2nd ‘(1st𝑈)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁)))
2826, 27elab 3573 . . . . . . . . . . . . 13 ((2nd ‘(1st𝑈)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁))
2925, 28sylib 221 . . . . . . . . . . . 12 (𝜑 → (2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁))
30 f1ofo 6625 . . . . . . . . . . . 12 ((2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑈)):(1...𝑁)–onto→(1...𝑁))
31 foima 6597 . . . . . . . . . . . 12 ((2nd ‘(1st𝑈)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑈)) “ (1...𝑁)) = (1...𝑁))
3229, 30, 313syl 18 . . . . . . . . . . 11 (𝜑 → ((2nd ‘(1st𝑈)) “ (1...𝑁)) = (1...𝑁))
3318, 32sseqtrrd 3918 . . . . . . . . . 10 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑀)) ⊆ ((2nd ‘(1st𝑈)) “ (1...𝑁)))
3433ssdifd 4031 . . . . . . . . 9 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∖ ((2nd ‘(1st𝑈)) “ (1...𝑀))) ⊆ (((2nd ‘(1st𝑈)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑈)) “ (1...𝑀))))
35 dff1o3 6624 . . . . . . . . . . . 12 ((2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘(1st𝑈)):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd ‘(1st𝑈))))
3635simprbi 500 . . . . . . . . . . 11 ((2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun (2nd ‘(1st𝑈)))
37 imadif 6423 . . . . . . . . . . 11 (Fun (2nd ‘(1st𝑈)) → ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ (1...𝑀))) = (((2nd ‘(1st𝑈)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑈)) “ (1...𝑀))))
3829, 36, 373syl 18 . . . . . . . . . 10 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ (1...𝑀))) = (((2nd ‘(1st𝑈)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑈)) “ (1...𝑀))))
39 difun2 4370 . . . . . . . . . . . 12 ((((𝑀 + 1)...𝑁) ∪ (1...𝑀)) ∖ (1...𝑀)) = (((𝑀 + 1)...𝑁) ∖ (1...𝑀))
40 poimirlem12.6 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ∈ (0...(𝑁 − 1)))
41 elfznn0 13091 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ (0...(𝑁 − 1)) → 𝑀 ∈ ℕ0)
42 nn0p1nn 12015 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ ℕ0 → (𝑀 + 1) ∈ ℕ)
4340, 41, 423syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑀 + 1) ∈ ℕ)
44 nnuz 12363 . . . . . . . . . . . . . . . 16 ℕ = (ℤ‘1)
4543, 44eleqtrdi 2843 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀 + 1) ∈ (ℤ‘1))
46 poimir.0 . . . . . . . . . . . . . . . . . 18 (𝜑𝑁 ∈ ℕ)
4746nncnd 11732 . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ ℂ)
48 npcan1 11143 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
4947, 48syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
50 elfzuz3 12995 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ (0...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ𝑀))
51 peano2uz 12383 . . . . . . . . . . . . . . . . 17 ((𝑁 − 1) ∈ (ℤ𝑀) → ((𝑁 − 1) + 1) ∈ (ℤ𝑀))
5240, 50, 513syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ𝑀))
5349, 52eqeltrrd 2834 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ (ℤ𝑀))
54 fzsplit2 13023 . . . . . . . . . . . . . . 15 (((𝑀 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ𝑀)) → (1...𝑁) = ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)))
5545, 53, 54syl2anc 587 . . . . . . . . . . . . . 14 (𝜑 → (1...𝑁) = ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)))
56 uncom 4043 . . . . . . . . . . . . . 14 ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)) = (((𝑀 + 1)...𝑁) ∪ (1...𝑀))
5755, 56eqtrdi 2789 . . . . . . . . . . . . 13 (𝜑 → (1...𝑁) = (((𝑀 + 1)...𝑁) ∪ (1...𝑀)))
5857difeq1d 4012 . . . . . . . . . . . 12 (𝜑 → ((1...𝑁) ∖ (1...𝑀)) = ((((𝑀 + 1)...𝑁) ∪ (1...𝑀)) ∖ (1...𝑀)))
59 incom 4091 . . . . . . . . . . . . . 14 (((𝑀 + 1)...𝑁) ∩ (1...𝑀)) = ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))
6040, 41syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ∈ ℕ0)
6160nn0red 12037 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℝ)
6261ltp1d 11648 . . . . . . . . . . . . . . 15 (𝜑𝑀 < (𝑀 + 1))
63 fzdisj 13025 . . . . . . . . . . . . . . 15 (𝑀 < (𝑀 + 1) → ((1...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅)
6462, 63syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((1...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅)
6559, 64syl5eq 2785 . . . . . . . . . . . . 13 (𝜑 → (((𝑀 + 1)...𝑁) ∩ (1...𝑀)) = ∅)
66 disj3 4343 . . . . . . . . . . . . 13 ((((𝑀 + 1)...𝑁) ∩ (1...𝑀)) = ∅ ↔ ((𝑀 + 1)...𝑁) = (((𝑀 + 1)...𝑁) ∖ (1...𝑀)))
6765, 66sylib 221 . . . . . . . . . . . 12 (𝜑 → ((𝑀 + 1)...𝑁) = (((𝑀 + 1)...𝑁) ∖ (1...𝑀)))
6839, 58, 673eqtr4a 2799 . . . . . . . . . . 11 (𝜑 → ((1...𝑁) ∖ (1...𝑀)) = ((𝑀 + 1)...𝑁))
6968imaeq2d 5903 . . . . . . . . . 10 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ (1...𝑀))) = ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
7038, 69eqtr3d 2775 . . . . . . . . 9 (𝜑 → (((2nd ‘(1st𝑈)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑈)) “ (1...𝑀))) = ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
7134, 70sseqtrd 3917 . . . . . . . 8 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∖ ((2nd ‘(1st𝑈)) “ (1...𝑀))) ⊆ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
7271sselda 3877 . . . . . . 7 ((𝜑𝑦 ∈ (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∖ ((2nd ‘(1st𝑈)) “ (1...𝑀)))) → 𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
731, 72sylan2br 598 . . . . . 6 ((𝜑 ∧ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀)))) → 𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
74 fveq2 6674 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑈 → (2nd𝑡) = (2nd𝑈))
7574breq2d 5042 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑈 → (𝑦 < (2nd𝑡) ↔ 𝑦 < (2nd𝑈)))
7675ifbid 4437 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑈 → if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd𝑈), 𝑦, (𝑦 + 1)))
7776csbeq1d 3794 . . . . . . . . . . . . . . . 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}))))
78 2fveq3 6679 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑈 → (1st ‘(1st𝑡)) = (1st ‘(1st𝑈)))
79 2fveq3 6679 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑈 → (2nd ‘(1st𝑡)) = (2nd ‘(1st𝑈)))
8079imaeq1d 5902 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑈 → ((2nd ‘(1st𝑡)) “ (1...𝑗)) = ((2nd ‘(1st𝑈)) “ (1...𝑗)))
8180xpeq1d 5554 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑈 → (((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}))
8279imaeq1d 5902 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑈 → ((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)))
8382xpeq1d 5554 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑈 → (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))
8481, 83uneq12d 4054 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑈 → ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0})))
8578, 84oveq12d 7188 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑈 → ((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))))
8685csbeq2dv 3797 . . . . . . . . . . . . . . . 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}))))
8777, 86eqtrd 2773 . . . . . . . . . . . . . . 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}))))
8887mpteq2dv 5126 . . . . . . . . . . . . . 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})))))
8988eqeq2d 2749 . . . . . . . . . . . . 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}))))))
9089, 5elrab2 3591 . . . . . . . . . . . 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}))))))
9190simprbi 500 . . . . . . . . . . 11 (𝑈𝑆𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑈), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0})))))
9219, 91syl 17 . . . . . . . . . 10 (𝜑𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑈), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0})))))
93 breq1 5033 . . . . . . . . . . . . . 14 (𝑦 = 𝑀 → (𝑦 < (2nd𝑈) ↔ 𝑀 < (2nd𝑈)))
94 id 22 . . . . . . . . . . . . . 14 (𝑦 = 𝑀𝑦 = 𝑀)
9593, 94ifbieq1d 4438 . . . . . . . . . . . . 13 (𝑦 = 𝑀 → if(𝑦 < (2nd𝑈), 𝑦, (𝑦 + 1)) = if(𝑀 < (2nd𝑈), 𝑀, (𝑦 + 1)))
9646nnred 11731 . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ ℝ)
97 peano2rem 11031 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℝ)
9896, 97syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 − 1) ∈ ℝ)
99 elfzle2 13002 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ (0...(𝑁 − 1)) → 𝑀 ≤ (𝑁 − 1))
10040, 99syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ≤ (𝑁 − 1))
10196ltm1d 11650 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 − 1) < 𝑁)
10261, 98, 96, 100, 101lelttrd 10876 . . . . . . . . . . . . . . 15 (𝜑𝑀 < 𝑁)
103 poimirlem12.5 . . . . . . . . . . . . . . 15 (𝜑 → (2nd𝑈) = 𝑁)
104102, 103breqtrrd 5058 . . . . . . . . . . . . . 14 (𝜑𝑀 < (2nd𝑈))
105104iftrued 4422 . . . . . . . . . . . . 13 (𝜑 → if(𝑀 < (2nd𝑈), 𝑀, (𝑦 + 1)) = 𝑀)
10695, 105sylan9eqr 2795 . . . . . . . . . . . 12 ((𝜑𝑦 = 𝑀) → if(𝑦 < (2nd𝑈), 𝑦, (𝑦 + 1)) = 𝑀)
107106csbeq1d 3794 . . . . . . . . . . 11 ((𝜑𝑦 = 𝑀) → 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}))))
108 oveq2 7178 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑀 → (1...𝑗) = (1...𝑀))
109108imaeq2d 5903 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑀 → ((2nd ‘(1st𝑈)) “ (1...𝑗)) = ((2nd ‘(1st𝑈)) “ (1...𝑀)))
110109xpeq1d 5554 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑀 → (((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}))
111 oveq1 7177 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑀 → (𝑗 + 1) = (𝑀 + 1))
112111oveq1d 7185 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑀 → ((𝑗 + 1)...𝑁) = ((𝑀 + 1)...𝑁))
113112imaeq2d 5903 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑀 → ((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
114113xpeq1d 5554 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑀 → (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))
115110, 114uneq12d 4054 . . . . . . . . . . . . . . 15 (𝑗 = 𝑀 → ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})))
116115oveq2d 7186 . . . . . . . . . . . . . 14 (𝑗 = 𝑀 → ((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))))
117116adantl 485 . . . . . . . . . . . . 13 ((𝜑𝑗 = 𝑀) → ((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))))
11840, 117csbied 3826 . . . . . . . . . . . 12 (𝜑𝑀 / 𝑗((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))))
119118adantr 484 . . . . . . . . . . 11 ((𝜑𝑦 = 𝑀) → 𝑀 / 𝑗((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))))
120107, 119eqtrd 2773 . . . . . . . . . 10 ((𝜑𝑦 = 𝑀) → 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}))))
121 ovexd 7205 . . . . . . . . . 10 (𝜑 → ((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))) ∈ V)
12292, 120, 40, 121fvmptd 6782 . . . . . . . . 9 (𝜑 → (𝐹𝑀) = ((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))))
123122fveq1d 6676 . . . . . . . 8 (𝜑 → ((𝐹𝑀)‘𝑦) = (((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦))
124123adantr 484 . . . . . . 7 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → ((𝐹𝑀)‘𝑦) = (((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦))
125 imassrn 5914 . . . . . . . . . 10 ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) ⊆ ran (2nd ‘(1st𝑈))
126 f1of 6618 . . . . . . . . . . 11 ((2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑈)):(1...𝑁)⟶(1...𝑁))
127 frn 6511 . . . . . . . . . . 11 ((2nd ‘(1st𝑈)):(1...𝑁)⟶(1...𝑁) → ran (2nd ‘(1st𝑈)) ⊆ (1...𝑁))
12829, 126, 1273syl 18 . . . . . . . . . 10 (𝜑 → ran (2nd ‘(1st𝑈)) ⊆ (1...𝑁))
129125, 128sstrid 3888 . . . . . . . . 9 (𝜑 → ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) ⊆ (1...𝑁))
130129sselda 3877 . . . . . . . 8 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → 𝑦 ∈ (1...𝑁))
131 xp1st 7746 . . . . . . . . . . 11 ((1st𝑈) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(1st𝑈)) ∈ ((0..^𝐾) ↑m (1...𝑁)))
132 elmapfn 8475 . . . . . . . . . . 11 ((1st ‘(1st𝑈)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st ‘(1st𝑈)) Fn (1...𝑁))
13323, 131, 1323syl 18 . . . . . . . . . 10 (𝜑 → (1st ‘(1st𝑈)) Fn (1...𝑁))
134133adantr 484 . . . . . . . . 9 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → (1st ‘(1st𝑈)) Fn (1...𝑁))
135 1ex 10715 . . . . . . . . . . . . . 14 1 ∈ V
136 fnconstg 6566 . . . . . . . . . . . . . 14 (1 ∈ V → (((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) Fn ((2nd ‘(1st𝑈)) “ (1...𝑀)))
137135, 136ax-mp 5 . . . . . . . . . . . . 13 (((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) Fn ((2nd ‘(1st𝑈)) “ (1...𝑀))
138 c0ex 10713 . . . . . . . . . . . . . 14 0 ∈ V
139 fnconstg 6566 . . . . . . . . . . . . . 14 (0 ∈ V → (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
140138, 139ax-mp 5 . . . . . . . . . . . . 13 (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))
141137, 140pm3.2i 474 . . . . . . . . . . . 12 ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) Fn ((2nd ‘(1st𝑈)) “ (1...𝑀)) ∧ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
142 imain 6424 . . . . . . . . . . . . . 14 (Fun (2nd ‘(1st𝑈)) → ((2nd ‘(1st𝑈)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑈)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))))
14329, 36, 1423syl 18 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑈)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))))
14464imaeq2d 5903 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ((2nd ‘(1st𝑈)) “ ∅))
145 ima0 5919 . . . . . . . . . . . . . 14 ((2nd ‘(1st𝑈)) “ ∅) = ∅
146144, 145eqtrdi 2789 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ∅)
147143, 146eqtr3d 2775 . . . . . . . . . . . 12 (𝜑 → (((2nd ‘(1st𝑈)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) = ∅)
148 fnun 6449 . . . . . . . . . . . 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)...𝑁))))
149141, 147, 148sylancr 590 . . . . . . . . . . 11 (𝜑 → ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2nd ‘(1st𝑈)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))))
150 imaundi 5982 . . . . . . . . . . . . 13 ((2nd ‘(1st𝑈)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑈)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
15155imaeq2d 5903 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑈)) “ (1...𝑁)) = ((2nd ‘(1st𝑈)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))))
152151, 32eqtr3d 2775 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (1...𝑁))
153150, 152eqtr3id 2787 . . . . . . . . . . . 12 (𝜑 → (((2nd ‘(1st𝑈)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) = (1...𝑁))
154153fneq2d 6432 . . . . . . . . . . 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...𝑁)))
155149, 154mpbid 235 . . . . . . . . . 10 (𝜑 → ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
156155adantr 484 . . . . . . . . 9 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
157 ovexd 7205 . . . . . . . . 9 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → (1...𝑁) ∈ V)
158 inidm 4109 . . . . . . . . 9 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
159 eqidd 2739 . . . . . . . . 9 (((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) ∧ 𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑈))‘𝑦) = ((1st ‘(1st𝑈))‘𝑦))
160 fvun2 6760 . . . . . . . . . . . . 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})‘𝑦))
161137, 140, 160mp3an12 1452 . . . . . . . . . . . 12 (((((2nd ‘(1st𝑈)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) = ∅ ∧ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → (((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = ((((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})‘𝑦))
162147, 161sylan 583 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → (((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = ((((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})‘𝑦))
163138fvconst2 6976 . . . . . . . . . . . 12 (𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) → ((((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})‘𝑦) = 0)
164163adantl 485 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → ((((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})‘𝑦) = 0)
165162, 164eqtrd 2773 . . . . . . . . . 10 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → (((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = 0)
166165adantr 484 . . . . . . . . 9 (((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) ∧ 𝑦 ∈ (1...𝑁)) → (((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = 0)
167134, 156, 157, 157, 158, 159, 166ofval 7435 . . . . . . . 8 (((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) ∧ 𝑦 ∈ (1...𝑁)) → (((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦) = (((1st ‘(1st𝑈))‘𝑦) + 0))
168130, 167mpdan 687 . . . . . . 7 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → (((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦) = (((1st ‘(1st𝑈))‘𝑦) + 0))
169 elmapi 8459 . . . . . . . . . . . . 13 ((1st ‘(1st𝑈)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st ‘(1st𝑈)):(1...𝑁)⟶(0..^𝐾))
17023, 131, 1693syl 18 . . . . . . . . . . . 12 (𝜑 → (1st ‘(1st𝑈)):(1...𝑁)⟶(0..^𝐾))
171170ffvelrnda 6861 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑈))‘𝑦) ∈ (0..^𝐾))
172 elfzonn0 13173 . . . . . . . . . . 11 (((1st ‘(1st𝑈))‘𝑦) ∈ (0..^𝐾) → ((1st ‘(1st𝑈))‘𝑦) ∈ ℕ0)
173171, 172syl 17 . . . . . . . . . 10 ((𝜑𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑈))‘𝑦) ∈ ℕ0)
174173nn0cnd 12038 . . . . . . . . 9 ((𝜑𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑈))‘𝑦) ∈ ℂ)
175174addid1d 10918 . . . . . . . 8 ((𝜑𝑦 ∈ (1...𝑁)) → (((1st ‘(1st𝑈))‘𝑦) + 0) = ((1st ‘(1st𝑈))‘𝑦))
176130, 175syldan 594 . . . . . . 7 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → (((1st ‘(1st𝑈))‘𝑦) + 0) = ((1st ‘(1st𝑈))‘𝑦))
177124, 168, 1763eqtrd 2777 . . . . . 6 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → ((𝐹𝑀)‘𝑦) = ((1st ‘(1st𝑈))‘𝑦))
17873, 177syldan 594 . . . . 5 ((𝜑 ∧ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀)))) → ((𝐹𝑀)‘𝑦) = ((1st ‘(1st𝑈))‘𝑦))
179 fveq2 6674 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑇 → (2nd𝑡) = (2nd𝑇))
180179breq2d 5042 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑇 → (𝑦 < (2nd𝑡) ↔ 𝑦 < (2nd𝑇)))
181180ifbid 4437 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑇 → if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)))
182181csbeq1d 3794 . . . . . . . . . . . . . . . 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}))))
183 2fveq3 6679 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑇 → (1st ‘(1st𝑡)) = (1st ‘(1st𝑇)))
184 2fveq3 6679 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑇 → (2nd ‘(1st𝑡)) = (2nd ‘(1st𝑇)))
185184imaeq1d 5902 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...𝑗)))
186185xpeq1d 5554 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}))
187184imaeq1d 5902 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)))
188187xpeq1d 5554 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
189186, 188uneq12d 4054 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑇 → ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))
190183, 189oveq12d 7188 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑇 → ((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
191190csbeq2dv 3797 . . . . . . . . . . . . . . . 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}))))
192182, 191eqtrd 2773 . . . . . . . . . . . . . . 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}))))
193192mpteq2dv 5126 . . . . . . . . . . . . . 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})))))
194193eqeq2d 2749 . . . . . . . . . . . . 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}))))))
195194, 5elrab2 3591 . . . . . . . . . . . 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}))))))
196195simprbi 500 . . . . . . . . . . 11 (𝑇𝑆𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
1973, 196syl 17 . . . . . . . . . 10 (𝜑𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))))
198 breq1 5033 . . . . . . . . . . . . . 14 (𝑦 = 𝑀 → (𝑦 < (2nd𝑇) ↔ 𝑀 < (2nd𝑇)))
199198, 94ifbieq1d 4438 . . . . . . . . . . . . 13 (𝑦 = 𝑀 → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) = if(𝑀 < (2nd𝑇), 𝑀, (𝑦 + 1)))
200 poimirlem12.3 . . . . . . . . . . . . . . 15 (𝜑 → (2nd𝑇) = 𝑁)
201102, 200breqtrrd 5058 . . . . . . . . . . . . . 14 (𝜑𝑀 < (2nd𝑇))
202201iftrued 4422 . . . . . . . . . . . . 13 (𝜑 → if(𝑀 < (2nd𝑇), 𝑀, (𝑦 + 1)) = 𝑀)
203199, 202sylan9eqr 2795 . . . . . . . . . . . 12 ((𝜑𝑦 = 𝑀) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) = 𝑀)
204203csbeq1d 3794 . . . . . . . . . . 11 ((𝜑𝑦 = 𝑀) → 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}))))
205108imaeq2d 5903 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑀 → ((2nd ‘(1st𝑇)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...𝑀)))
206205xpeq1d 5554 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑀 → (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}))
207112imaeq2d 5903 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑀 → ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)))
208207xpeq1d 5554 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑀 → (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))
209206, 208uneq12d 4054 . . . . . . . . . . . . . . 15 (𝑗 = 𝑀 → ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))
210209oveq2d 7186 . . . . . . . . . . . . . 14 (𝑗 = 𝑀 → ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
211210adantl 485 . . . . . . . . . . . . 13 ((𝜑𝑗 = 𝑀) → ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
21240, 211csbied 3826 . . . . . . . . . . . 12 (𝜑𝑀 / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
213212adantr 484 . . . . . . . . . . 11 ((𝜑𝑦 = 𝑀) → 𝑀 / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
214204, 213eqtrd 2773 . . . . . . . . . 10 ((𝜑𝑦 = 𝑀) → 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}))))
215 ovexd 7205 . . . . . . . . . 10 (𝜑 → ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) ∈ V)
216197, 214, 40, 215fvmptd 6782 . . . . . . . . 9 (𝜑 → (𝐹𝑀) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
217216fveq1d 6676 . . . . . . . 8 (𝜑 → ((𝐹𝑀)‘𝑦) = (((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦))
218217adantr 484 . . . . . . 7 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → ((𝐹𝑀)‘𝑦) = (((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦))
21918sselda 3877 . . . . . . . 8 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → 𝑦 ∈ (1...𝑁))
220 xp1st 7746 . . . . . . . . . . 11 ((1st𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)))
221 elmapfn 8475 . . . . . . . . . . 11 ((1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st ‘(1st𝑇)) Fn (1...𝑁))
2228, 220, 2213syl 18 . . . . . . . . . 10 (𝜑 → (1st ‘(1st𝑇)) Fn (1...𝑁))
223222adantr 484 . . . . . . . . 9 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → (1st ‘(1st𝑇)) Fn (1...𝑁))
224 fnconstg 6566 . . . . . . . . . . . . . 14 (1 ∈ V → (((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...𝑀)))
225135, 224ax-mp 5 . . . . . . . . . . . . 13 (((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...𝑀))
226 fnconstg 6566 . . . . . . . . . . . . . 14 (0 ∈ V → (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)))
227138, 226ax-mp 5 . . . . . . . . . . . . 13 (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))
228225, 227pm3.2i 474 . . . . . . . . . . . 12 ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)))
229 dff1o3 6624 . . . . . . . . . . . . . . 15 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd ‘(1st𝑇))))
230229simprbi 500 . . . . . . . . . . . . . 14 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun (2nd ‘(1st𝑇)))
231 imain 6424 . . . . . . . . . . . . . 14 (Fun (2nd ‘(1st𝑇)) → ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))))
23214, 230, 2313syl 18 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))))
23364imaeq2d 5903 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ((2nd ‘(1st𝑇)) “ ∅))
234 ima0 5919 . . . . . . . . . . . . . 14 ((2nd ‘(1st𝑇)) “ ∅) = ∅
235233, 234eqtrdi 2789 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ∅)
236232, 235eqtr3d 2775 . . . . . . . . . . . 12 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅)
237 fnun 6449 . . . . . . . . . . . 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)...𝑁))))
238228, 236, 237sylancr 590 . . . . . . . . . . 11 (𝜑 → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))))
239 imaundi 5982 . . . . . . . . . . . . 13 ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)))
24055imaeq2d 5903 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))))
241 f1ofo 6625 . . . . . . . . . . . . . . 15 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁))
242 foima 6597 . . . . . . . . . . . . . . 15 ((2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
24314, 241, 2423syl 18 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
244240, 243eqtr3d 2775 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (1...𝑁))
245239, 244eqtr3id 2787 . . . . . . . . . . . 12 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))) = (1...𝑁))
246245fneq2d 6432 . . . . . . . . . . 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...𝑁)))
247238, 246mpbid 235 . . . . . . . . . 10 (𝜑 → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
248247adantr 484 . . . . . . . . 9 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
249 ovexd 7205 . . . . . . . . 9 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → (1...𝑁) ∈ V)
250 eqidd 2739 . . . . . . . . 9 (((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) ∧ 𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑦) = ((1st ‘(1st𝑇))‘𝑦))
251 fvun1 6759 . . . . . . . . . . . . 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})‘𝑦))
252225, 227, 251mp3an12 1452 . . . . . . . . . . . 12 (((((2nd ‘(1st𝑇)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅ ∧ 𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → (((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1})‘𝑦))
253236, 252sylan 583 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → (((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1})‘𝑦))
254135fvconst2 6976 . . . . . . . . . . . 12 (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1})‘𝑦) = 1)
255254adantl 485 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1})‘𝑦) = 1)
256253, 255eqtrd 2773 . . . . . . . . . 10 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → (((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = 1)
257256adantr 484 . . . . . . . . 9 (((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) ∧ 𝑦 ∈ (1...𝑁)) → (((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = 1)
258223, 248, 249, 249, 158, 250, 257ofval 7435 . . . . . . . 8 (((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) ∧ 𝑦 ∈ (1...𝑁)) → (((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦) = (((1st ‘(1st𝑇))‘𝑦) + 1))
259219, 258mpdan 687 . . . . . . 7 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → (((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦) = (((1st ‘(1st𝑇))‘𝑦) + 1))
260218, 259eqtrd 2773 . . . . . 6 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → ((𝐹𝑀)‘𝑦) = (((1st ‘(1st𝑇))‘𝑦) + 1))
261260adantrr 717 . . . . 5 ((𝜑 ∧ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀)))) → ((𝐹𝑀)‘𝑦) = (((1st ‘(1st𝑇))‘𝑦) + 1))
26246nngt0d 11765 . . . . . . . . . 10 (𝜑 → 0 < 𝑁)
263262, 103breqtrrd 5058 . . . . . . . . 9 (𝜑 → 0 < (2nd𝑈))
26446, 5, 19, 263poimirlem5 35405 . . . . . . . 8 (𝜑 → (𝐹‘0) = (1st ‘(1st𝑈)))
265262, 200breqtrrd 5058 . . . . . . . . 9 (𝜑 → 0 < (2nd𝑇))
26646, 5, 3, 265poimirlem5 35405 . . . . . . . 8 (𝜑 → (𝐹‘0) = (1st ‘(1st𝑇)))
267264, 266eqtr3d 2775 . . . . . . 7 (𝜑 → (1st ‘(1st𝑈)) = (1st ‘(1st𝑇)))
268267fveq1d 6676 . . . . . 6 (𝜑 → ((1st ‘(1st𝑈))‘𝑦) = ((1st ‘(1st𝑇))‘𝑦))
269268adantr 484 . . . . 5 ((𝜑 ∧ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀)))) → ((1st ‘(1st𝑈))‘𝑦) = ((1st ‘(1st𝑇))‘𝑦))
270178, 261, 2693eqtr3d 2781 . . . 4 ((𝜑 ∧ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀)))) → (((1st ‘(1st𝑇))‘𝑦) + 1) = ((1st ‘(1st𝑇))‘𝑦))
271 elmapi 8459 . . . . . . . . . . . 12 ((1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾))
2728, 220, 2713syl 18 . . . . . . . . . . 11 (𝜑 → (1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾))
273272ffvelrnda 6861 . . . . . . . . . 10 ((𝜑𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑦) ∈ (0..^𝐾))
274 elfzonn0 13173 . . . . . . . . . 10 (((1st ‘(1st𝑇))‘𝑦) ∈ (0..^𝐾) → ((1st ‘(1st𝑇))‘𝑦) ∈ ℕ0)
275273, 274syl 17 . . . . . . . . 9 ((𝜑𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑦) ∈ ℕ0)
276275nn0red 12037 . . . . . . . 8 ((𝜑𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑦) ∈ ℝ)
277276ltp1d 11648 . . . . . . . 8 ((𝜑𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑦) < (((1st ‘(1st𝑇))‘𝑦) + 1))
278276, 277gtned 10853 . . . . . . 7 ((𝜑𝑦 ∈ (1...𝑁)) → (((1st ‘(1st𝑇))‘𝑦) + 1) ≠ ((1st ‘(1st𝑇))‘𝑦))
279219, 278syldan 594 . . . . . 6 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → (((1st ‘(1st𝑇))‘𝑦) + 1) ≠ ((1st ‘(1st𝑇))‘𝑦))
280279neneqd 2939 . . . . 5 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → ¬ (((1st ‘(1st𝑇))‘𝑦) + 1) = ((1st ‘(1st𝑇))‘𝑦))
281280adantrr 717 . . . 4 ((𝜑 ∧ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀)))) → ¬ (((1st ‘(1st𝑇))‘𝑦) + 1) = ((1st ‘(1st𝑇))‘𝑦))
282270, 281pm2.65da 817 . . 3 (𝜑 → ¬ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀))))
283 iman 405 . . 3 ((𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) → 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀))) ↔ ¬ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀))))
284282, 283sylibr 237 . 2 (𝜑 → (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) → 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀))))
285284ssrdv 3883 1 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑀)) ⊆ ((2nd ‘(1st𝑈)) “ (1...𝑀)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399   = wceq 1542  wcel 2114  {cab 2716  wne 2934  {crab 3057  Vcvv 3398  csb 3790  cdif 3840  cun 3841  cin 3842  wss 3843  c0 4211  ifcif 4414  {csn 4516   class class class wbr 5030  cmpt 5110   × cxp 5523  ccnv 5524  ran crn 5526  cima 5528  Fun wfun 6333   Fn wfn 6334  wf 6335  ontowfo 6337  1-1-ontowf1o 6338  cfv 6339  (class class class)co 7170  f cof 7423  1st c1st 7712  2nd c2nd 7713  m cmap 8437  cc 10613  cr 10614  0cc0 10615  1c1 10616   + caddc 10618   < clt 10753  cle 10754  cmin 10948  cn 11716  0cn0 11976  cuz 12324  ...cfz 12981  ..^cfzo 13124
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7479  ax-cnex 10671  ax-resscn 10672  ax-1cn 10673  ax-icn 10674  ax-addcl 10675  ax-addrcl 10676  ax-mulcl 10677  ax-mulrcl 10678  ax-mulcom 10679  ax-addass 10680  ax-mulass 10681  ax-distr 10682  ax-i2m1 10683  ax-1ne0 10684  ax-1rid 10685  ax-rnegex 10686  ax-rrecex 10687  ax-cnre 10688  ax-pre-lttri 10689  ax-pre-lttrn 10690  ax-pre-ltadd 10691  ax-pre-mulgt0 10692
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rab 3062  df-v 3400  df-sbc 3681  df-csb 3791  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-pss 3862  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-tp 4521  df-op 4523  df-uni 4797  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5483  df-we 5485  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6129  df-ord 6175  df-on 6176  df-lim 6177  df-suc 6178  df-iota 6297  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-riota 7127  df-ov 7173  df-oprab 7174  df-mpo 7175  df-of 7425  df-om 7600  df-1st 7714  df-2nd 7715  df-wrecs 7976  df-recs 8037  df-rdg 8075  df-er 8320  df-map 8439  df-en 8556  df-dom 8557  df-sdom 8558  df-pnf 10755  df-mnf 10756  df-xr 10757  df-ltxr 10758  df-le 10759  df-sub 10950  df-neg 10951  df-nn 11717  df-n0 11977  df-z 12063  df-uz 12325  df-fz 12982  df-fzo 13125
This theorem is referenced by:  poimirlem14  35414
  Copyright terms: Public domain W3C validator