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 36119
Description: Lemma for poimir 36140 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 3925 . . . . . . 7 (𝑦 ∈ (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∖ ((2nd ‘(1st𝑈)) “ (1...𝑀))) ↔ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀))))
2 imassrn 6029 . . . . . . . . . . . 12 ((2nd ‘(1st𝑇)) “ (1...𝑀)) ⊆ ran (2nd ‘(1st𝑇))
3 poimirlem12.2 . . . . . . . . . . . . . . . 16 (𝜑𝑇𝑆)
4 elrabi 3644 . . . . . . . . . . . . . . . . 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 2856 . . . . . . . . . . . . . . . 16 (𝑇𝑆𝑇 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
7 xp1st 7958 . . . . . . . . . . . . . . . 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 7959 . . . . . . . . . . . . . . 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 6860 . . . . . . . . . . . . . . 15 (2nd ‘(1st𝑇)) ∈ V
12 f1oeq1 6777 . . . . . . . . . . . . . . 15 (𝑓 = (2nd ‘(1st𝑇)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁)))
1311, 12elab 3635 . . . . . . . . . . . . . 14 ((2nd ‘(1st𝑇)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
1410, 13sylib 217 . . . . . . . . . . . . 13 (𝜑 → (2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁))
15 f1of 6789 . . . . . . . . . . . . 13 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)):(1...𝑁)⟶(1...𝑁))
16 frn 6680 . . . . . . . . . . . . 13 ((2nd ‘(1st𝑇)):(1...𝑁)⟶(1...𝑁) → ran (2nd ‘(1st𝑇)) ⊆ (1...𝑁))
1714, 15, 163syl 18 . . . . . . . . . . . 12 (𝜑 → ran (2nd ‘(1st𝑇)) ⊆ (1...𝑁))
182, 17sstrid 3960 . . . . . . . . . . 11 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑀)) ⊆ (1...𝑁))
19 poimirlem12.4 . . . . . . . . . . . . . . 15 (𝜑𝑈𝑆)
20 elrabi 3644 . . . . . . . . . . . . . . . 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 2856 . . . . . . . . . . . . . . 15 (𝑈𝑆𝑈 ∈ ((((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) × (0...𝑁)))
22 xp1st 7958 . . . . . . . . . . . . . . 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 7959 . . . . . . . . . . . . . 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 6860 . . . . . . . . . . . . . 14 (2nd ‘(1st𝑈)) ∈ V
27 f1oeq1 6777 . . . . . . . . . . . . . 14 (𝑓 = (2nd ‘(1st𝑈)) → (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁)))
2826, 27elab 3635 . . . . . . . . . . . . 13 ((2nd ‘(1st𝑈)) ∈ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ↔ (2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁))
2925, 28sylib 217 . . . . . . . . . . . 12 (𝜑 → (2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁))
30 f1ofo 6796 . . . . . . . . . . . 12 ((2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑈)):(1...𝑁)–onto→(1...𝑁))
31 foima 6766 . . . . . . . . . . . 12 ((2nd ‘(1st𝑈)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑈)) “ (1...𝑁)) = (1...𝑁))
3229, 30, 313syl 18 . . . . . . . . . . 11 (𝜑 → ((2nd ‘(1st𝑈)) “ (1...𝑁)) = (1...𝑁))
3318, 32sseqtrrd 3990 . . . . . . . . . 10 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑀)) ⊆ ((2nd ‘(1st𝑈)) “ (1...𝑁)))
3433ssdifd 4105 . . . . . . . . 9 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∖ ((2nd ‘(1st𝑈)) “ (1...𝑀))) ⊆ (((2nd ‘(1st𝑈)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑈)) “ (1...𝑀))))
35 dff1o3 6795 . . . . . . . . . . . 12 ((2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘(1st𝑈)):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd ‘(1st𝑈))))
3635simprbi 498 . . . . . . . . . . 11 ((2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun (2nd ‘(1st𝑈)))
37 imadif 6590 . . . . . . . . . . 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 4445 . . . . . . . . . . . 12 ((((𝑀 + 1)...𝑁) ∪ (1...𝑀)) ∖ (1...𝑀)) = (((𝑀 + 1)...𝑁) ∖ (1...𝑀))
40 poimirlem12.6 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ∈ (0...(𝑁 − 1)))
41 elfznn0 13541 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ (0...(𝑁 − 1)) → 𝑀 ∈ ℕ0)
42 nn0p1nn 12459 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ ℕ0 → (𝑀 + 1) ∈ ℕ)
4340, 41, 423syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑀 + 1) ∈ ℕ)
44 nnuz 12813 . . . . . . . . . . . . . . . 16 ℕ = (ℤ‘1)
4543, 44eleqtrdi 2848 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀 + 1) ∈ (ℤ‘1))
46 poimir.0 . . . . . . . . . . . . . . . . . 18 (𝜑𝑁 ∈ ℕ)
4746nncnd 12176 . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ ℂ)
48 npcan1 11587 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
4947, 48syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
50 elfzuz3 13445 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ (0...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ𝑀))
51 peano2uz 12833 . . . . . . . . . . . . . . . . 17 ((𝑁 − 1) ∈ (ℤ𝑀) → ((𝑁 − 1) + 1) ∈ (ℤ𝑀))
5240, 50, 513syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ𝑀))
5349, 52eqeltrrd 2839 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ (ℤ𝑀))
54 fzsplit2 13473 . . . . . . . . . . . . . . 15 (((𝑀 + 1) ∈ (ℤ‘1) ∧ 𝑁 ∈ (ℤ𝑀)) → (1...𝑁) = ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)))
5545, 53, 54syl2anc 585 . . . . . . . . . . . . . 14 (𝜑 → (1...𝑁) = ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)))
56 uncom 4118 . . . . . . . . . . . . . 14 ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)) = (((𝑀 + 1)...𝑁) ∪ (1...𝑀))
5755, 56eqtrdi 2793 . . . . . . . . . . . . 13 (𝜑 → (1...𝑁) = (((𝑀 + 1)...𝑁) ∪ (1...𝑀)))
5857difeq1d 4086 . . . . . . . . . . . 12 (𝜑 → ((1...𝑁) ∖ (1...𝑀)) = ((((𝑀 + 1)...𝑁) ∪ (1...𝑀)) ∖ (1...𝑀)))
59 incom 4166 . . . . . . . . . . . . . 14 (((𝑀 + 1)...𝑁) ∩ (1...𝑀)) = ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))
6040, 41syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ∈ ℕ0)
6160nn0red 12481 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℝ)
6261ltp1d 12092 . . . . . . . . . . . . . . 15 (𝜑𝑀 < (𝑀 + 1))
63 fzdisj 13475 . . . . . . . . . . . . . . 15 (𝑀 < (𝑀 + 1) → ((1...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅)
6462, 63syl 17 . . . . . . . . . . . . . 14 (𝜑 → ((1...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅)
6559, 64eqtrid 2789 . . . . . . . . . . . . 13 (𝜑 → (((𝑀 + 1)...𝑁) ∩ (1...𝑀)) = ∅)
66 disj3 4418 . . . . . . . . . . . . 13 ((((𝑀 + 1)...𝑁) ∩ (1...𝑀)) = ∅ ↔ ((𝑀 + 1)...𝑁) = (((𝑀 + 1)...𝑁) ∖ (1...𝑀)))
6765, 66sylib 217 . . . . . . . . . . . 12 (𝜑 → ((𝑀 + 1)...𝑁) = (((𝑀 + 1)...𝑁) ∖ (1...𝑀)))
6839, 58, 673eqtr4a 2803 . . . . . . . . . . 11 (𝜑 → ((1...𝑁) ∖ (1...𝑀)) = ((𝑀 + 1)...𝑁))
6968imaeq2d 6018 . . . . . . . . . 10 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑁) ∖ (1...𝑀))) = ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
7038, 69eqtr3d 2779 . . . . . . . . 9 (𝜑 → (((2nd ‘(1st𝑈)) “ (1...𝑁)) ∖ ((2nd ‘(1st𝑈)) “ (1...𝑀))) = ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
7134, 70sseqtrd 3989 . . . . . . . 8 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∖ ((2nd ‘(1st𝑈)) “ (1...𝑀))) ⊆ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
7271sselda 3949 . . . . . . 7 ((𝜑𝑦 ∈ (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∖ ((2nd ‘(1st𝑈)) “ (1...𝑀)))) → 𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
731, 72sylan2br 596 . . . . . 6 ((𝜑 ∧ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀)))) → 𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
74 fveq2 6847 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑈 → (2nd𝑡) = (2nd𝑈))
7574breq2d 5122 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑈 → (𝑦 < (2nd𝑡) ↔ 𝑦 < (2nd𝑈)))
7675ifbid 4514 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑈 → if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd𝑈), 𝑦, (𝑦 + 1)))
7776csbeq1d 3864 . . . . . . . . . . . . . . . 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 6852 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑈 → (1st ‘(1st𝑡)) = (1st ‘(1st𝑈)))
79 2fveq3 6852 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑈 → (2nd ‘(1st𝑡)) = (2nd ‘(1st𝑈)))
8079imaeq1d 6017 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑈 → ((2nd ‘(1st𝑡)) “ (1...𝑗)) = ((2nd ‘(1st𝑈)) “ (1...𝑗)))
8180xpeq1d 5667 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑈 → (((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}))
8279imaeq1d 6017 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑈 → ((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)))
8382xpeq1d 5667 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑈 → (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))
8481, 83uneq12d 4129 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑈 → ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0})))
8578, 84oveq12d 7380 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑈 → ((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))))
8685csbeq2dv 3867 . . . . . . . . . . . . . . . 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 2777 . . . . . . . . . . . . . . 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 5212 . . . . . . . . . . . . . 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 2748 . . . . . . . . . . . . 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 3653 . . . . . . . . . . . 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 498 . . . . . . . . . . 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 5113 . . . . . . . . . . . . . 14 (𝑦 = 𝑀 → (𝑦 < (2nd𝑈) ↔ 𝑀 < (2nd𝑈)))
94 id 22 . . . . . . . . . . . . . 14 (𝑦 = 𝑀𝑦 = 𝑀)
9593, 94ifbieq1d 4515 . . . . . . . . . . . . 13 (𝑦 = 𝑀 → if(𝑦 < (2nd𝑈), 𝑦, (𝑦 + 1)) = if(𝑀 < (2nd𝑈), 𝑀, (𝑦 + 1)))
9646nnred 12175 . . . . . . . . . . . . . . . . 17 (𝜑𝑁 ∈ ℝ)
97 peano2rem 11475 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℝ → (𝑁 − 1) ∈ ℝ)
9896, 97syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 − 1) ∈ ℝ)
99 elfzle2 13452 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ (0...(𝑁 − 1)) → 𝑀 ≤ (𝑁 − 1))
10040, 99syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ≤ (𝑁 − 1))
10196ltm1d 12094 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 − 1) < 𝑁)
10261, 98, 96, 100, 101lelttrd 11320 . . . . . . . . . . . . . . 15 (𝜑𝑀 < 𝑁)
103 poimirlem12.5 . . . . . . . . . . . . . . 15 (𝜑 → (2nd𝑈) = 𝑁)
104102, 103breqtrrd 5138 . . . . . . . . . . . . . 14 (𝜑𝑀 < (2nd𝑈))
105104iftrued 4499 . . . . . . . . . . . . 13 (𝜑 → if(𝑀 < (2nd𝑈), 𝑀, (𝑦 + 1)) = 𝑀)
10695, 105sylan9eqr 2799 . . . . . . . . . . . 12 ((𝜑𝑦 = 𝑀) → if(𝑦 < (2nd𝑈), 𝑦, (𝑦 + 1)) = 𝑀)
107106csbeq1d 3864 . . . . . . . . . . 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 7370 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑀 → (1...𝑗) = (1...𝑀))
109108imaeq2d 6018 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑀 → ((2nd ‘(1st𝑈)) “ (1...𝑗)) = ((2nd ‘(1st𝑈)) “ (1...𝑀)))
110109xpeq1d 5667 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑀 → (((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}))
111 oveq1 7369 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑀 → (𝑗 + 1) = (𝑀 + 1))
112111oveq1d 7377 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑀 → ((𝑗 + 1)...𝑁) = ((𝑀 + 1)...𝑁))
113112imaeq2d 6018 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑀 → ((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
114113xpeq1d 5667 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑀 → (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))
115110, 114uneq12d 4129 . . . . . . . . . . . . . . 15 (𝑗 = 𝑀 → ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})))
116115oveq2d 7378 . . . . . . . . . . . . . 14 (𝑗 = 𝑀 → ((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))))
117116adantl 483 . . . . . . . . . . . . 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 3898 . . . . . . . . . . . 12 (𝜑𝑀 / 𝑗((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))))
119118adantr 482 . . . . . . . . . . 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 2777 . . . . . . . . . 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 7397 . . . . . . . . . 10 (𝜑 → ((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))) ∈ V)
12292, 120, 40, 121fvmptd 6960 . . . . . . . . 9 (𝜑 → (𝐹𝑀) = ((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))))
123122fveq1d 6849 . . . . . . . 8 (𝜑 → ((𝐹𝑀)‘𝑦) = (((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦))
124123adantr 482 . . . . . . 7 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → ((𝐹𝑀)‘𝑦) = (((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦))
125 imassrn 6029 . . . . . . . . . 10 ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) ⊆ ran (2nd ‘(1st𝑈))
126 f1of 6789 . . . . . . . . . . 11 ((2nd ‘(1st𝑈)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑈)):(1...𝑁)⟶(1...𝑁))
127 frn 6680 . . . . . . . . . . 11 ((2nd ‘(1st𝑈)):(1...𝑁)⟶(1...𝑁) → ran (2nd ‘(1st𝑈)) ⊆ (1...𝑁))
12829, 126, 1273syl 18 . . . . . . . . . 10 (𝜑 → ran (2nd ‘(1st𝑈)) ⊆ (1...𝑁))
129125, 128sstrid 3960 . . . . . . . . 9 (𝜑 → ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) ⊆ (1...𝑁))
130129sselda 3949 . . . . . . . 8 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → 𝑦 ∈ (1...𝑁))
131 xp1st 7958 . . . . . . . . . . 11 ((1st𝑈) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(1st𝑈)) ∈ ((0..^𝐾) ↑m (1...𝑁)))
132 elmapfn 8810 . . . . . . . . . . 11 ((1st ‘(1st𝑈)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st ‘(1st𝑈)) Fn (1...𝑁))
13323, 131, 1323syl 18 . . . . . . . . . 10 (𝜑 → (1st ‘(1st𝑈)) Fn (1...𝑁))
134133adantr 482 . . . . . . . . 9 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → (1st ‘(1st𝑈)) Fn (1...𝑁))
135 1ex 11158 . . . . . . . . . . . . . 14 1 ∈ V
136 fnconstg 6735 . . . . . . . . . . . . . 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 11156 . . . . . . . . . . . . . 14 0 ∈ V
139 fnconstg 6735 . . . . . . . . . . . . . 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 472 . . . . . . . . . . . 12 ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) Fn ((2nd ‘(1st𝑈)) “ (1...𝑀)) ∧ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
142 imain 6591 . . . . . . . . . . . . . 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 6018 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ((2nd ‘(1st𝑈)) “ ∅))
145 ima0 6034 . . . . . . . . . . . . . 14 ((2nd ‘(1st𝑈)) “ ∅) = ∅
146144, 145eqtrdi 2793 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ∅)
147143, 146eqtr3d 2779 . . . . . . . . . . . 12 (𝜑 → (((2nd ‘(1st𝑈)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) = ∅)
148 fnun 6619 . . . . . . . . . . . 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 588 . . . . . . . . . . 11 (𝜑 → ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2nd ‘(1st𝑈)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))))
150 imaundi 6107 . . . . . . . . . . . . 13 ((2nd ‘(1st𝑈)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑈)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)))
15155imaeq2d 6018 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑈)) “ (1...𝑁)) = ((2nd ‘(1st𝑈)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))))
152151, 32eqtr3d 2779 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑈)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (1...𝑁))
153150, 152eqtr3id 2791 . . . . . . . . . . . 12 (𝜑 → (((2nd ‘(1st𝑈)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) = (1...𝑁))
154153fneq2d 6601 . . . . . . . . . . 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 231 . . . . . . . . . 10 (𝜑 → ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
156155adantr 482 . . . . . . . . 9 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
157 ovexd 7397 . . . . . . . . 9 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → (1...𝑁) ∈ V)
158 inidm 4183 . . . . . . . . 9 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
159 eqidd 2738 . . . . . . . . 9 (((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) ∧ 𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑈))‘𝑦) = ((1st ‘(1st𝑈))‘𝑦))
160 fvun2 6938 . . . . . . . . . . . . 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 581 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → (((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = ((((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})‘𝑦))
163138fvconst2 7158 . . . . . . . . . . . 12 (𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) → ((((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})‘𝑦) = 0)
164163adantl 483 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → ((((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})‘𝑦) = 0)
165162, 164eqtrd 2777 . . . . . . . . . 10 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → (((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = 0)
166165adantr 482 . . . . . . . . 9 (((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) ∧ 𝑦 ∈ (1...𝑁)) → (((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = 0)
167134, 156, 157, 157, 158, 159, 166ofval 7633 . . . . . . . 8 (((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) ∧ 𝑦 ∈ (1...𝑁)) → (((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦) = (((1st ‘(1st𝑈))‘𝑦) + 0))
168130, 167mpdan 686 . . . . . . 7 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → (((1st ‘(1st𝑈)) ∘f + ((((2nd ‘(1st𝑈)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦) = (((1st ‘(1st𝑈))‘𝑦) + 0))
169 elmapi 8794 . . . . . . . . . . . . 13 ((1st ‘(1st𝑈)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st ‘(1st𝑈)):(1...𝑁)⟶(0..^𝐾))
17023, 131, 1693syl 18 . . . . . . . . . . . 12 (𝜑 → (1st ‘(1st𝑈)):(1...𝑁)⟶(0..^𝐾))
171170ffvelcdmda 7040 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑈))‘𝑦) ∈ (0..^𝐾))
172 elfzonn0 13624 . . . . . . . . . . 11 (((1st ‘(1st𝑈))‘𝑦) ∈ (0..^𝐾) → ((1st ‘(1st𝑈))‘𝑦) ∈ ℕ0)
173171, 172syl 17 . . . . . . . . . 10 ((𝜑𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑈))‘𝑦) ∈ ℕ0)
174173nn0cnd 12482 . . . . . . . . 9 ((𝜑𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑈))‘𝑦) ∈ ℂ)
175174addid1d 11362 . . . . . . . 8 ((𝜑𝑦 ∈ (1...𝑁)) → (((1st ‘(1st𝑈))‘𝑦) + 0) = ((1st ‘(1st𝑈))‘𝑦))
176130, 175syldan 592 . . . . . . 7 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → (((1st ‘(1st𝑈))‘𝑦) + 0) = ((1st ‘(1st𝑈))‘𝑦))
177124, 168, 1763eqtrd 2781 . . . . . 6 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑈)) “ ((𝑀 + 1)...𝑁))) → ((𝐹𝑀)‘𝑦) = ((1st ‘(1st𝑈))‘𝑦))
17873, 177syldan 592 . . . . 5 ((𝜑 ∧ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀)))) → ((𝐹𝑀)‘𝑦) = ((1st ‘(1st𝑈))‘𝑦))
179 fveq2 6847 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑇 → (2nd𝑡) = (2nd𝑇))
180179breq2d 5122 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑇 → (𝑦 < (2nd𝑡) ↔ 𝑦 < (2nd𝑇)))
181180ifbid 4514 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑇 → if(𝑦 < (2nd𝑡), 𝑦, (𝑦 + 1)) = if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)))
182181csbeq1d 3864 . . . . . . . . . . . . . . . 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 6852 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑇 → (1st ‘(1st𝑡)) = (1st ‘(1st𝑇)))
184 2fveq3 6852 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = 𝑇 → (2nd ‘(1st𝑡)) = (2nd ‘(1st𝑇)))
185184imaeq1d 6017 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...𝑗)))
186185xpeq1d 5667 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}))
187184imaeq1d 6017 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = 𝑇 → ((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)))
188187xpeq1d 5667 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑇 → (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))
189186, 188uneq12d 4129 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑇 → ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})))
190183, 189oveq12d 7380 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑇 → ((1st ‘(1st𝑡)) ∘f + ((((2nd ‘(1st𝑡)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑡)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))))
191190csbeq2dv 3867 . . . . . . . . . . . . . . . 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 2777 . . . . . . . . . . . . . . 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 5212 . . . . . . . . . . . . . 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 2748 . . . . . . . . . . . . 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 3653 . . . . . . . . . . . 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 498 . . . . . . . . . . 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 5113 . . . . . . . . . . . . . 14 (𝑦 = 𝑀 → (𝑦 < (2nd𝑇) ↔ 𝑀 < (2nd𝑇)))
199198, 94ifbieq1d 4515 . . . . . . . . . . . . 13 (𝑦 = 𝑀 → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) = if(𝑀 < (2nd𝑇), 𝑀, (𝑦 + 1)))
200 poimirlem12.3 . . . . . . . . . . . . . . 15 (𝜑 → (2nd𝑇) = 𝑁)
201102, 200breqtrrd 5138 . . . . . . . . . . . . . 14 (𝜑𝑀 < (2nd𝑇))
202201iftrued 4499 . . . . . . . . . . . . 13 (𝜑 → if(𝑀 < (2nd𝑇), 𝑀, (𝑦 + 1)) = 𝑀)
203199, 202sylan9eqr 2799 . . . . . . . . . . . 12 ((𝜑𝑦 = 𝑀) → if(𝑦 < (2nd𝑇), 𝑦, (𝑦 + 1)) = 𝑀)
204203csbeq1d 3864 . . . . . . . . . . 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 6018 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑀 → ((2nd ‘(1st𝑇)) “ (1...𝑗)) = ((2nd ‘(1st𝑇)) “ (1...𝑀)))
206205xpeq1d 5667 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑀 → (((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) = (((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}))
207112imaeq2d 6018 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑀 → ((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)))
208207xpeq1d 5667 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑀 → (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))
209206, 208uneq12d 4129 . . . . . . . . . . . . . . 15 (𝑗 = 𝑀 → ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))
210209oveq2d 7378 . . . . . . . . . . . . . 14 (𝑗 = 𝑀 → ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
211210adantl 483 . . . . . . . . . . . . 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 3898 . . . . . . . . . . . 12 (𝜑𝑀 / 𝑗((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
213212adantr 482 . . . . . . . . . . 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 2777 . . . . . . . . . 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 7397 . . . . . . . . . 10 (𝜑 → ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))) ∈ V)
216197, 214, 40, 215fvmptd 6960 . . . . . . . . 9 (𝜑 → (𝐹𝑀) = ((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))))
217216fveq1d 6849 . . . . . . . 8 (𝜑 → ((𝐹𝑀)‘𝑦) = (((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦))
218217adantr 482 . . . . . . 7 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → ((𝐹𝑀)‘𝑦) = (((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦))
21918sselda 3949 . . . . . . . 8 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → 𝑦 ∈ (1...𝑁))
220 xp1st 7958 . . . . . . . . . . 11 ((1st𝑇) ∈ (((0..^𝐾) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)))
221 elmapfn 8810 . . . . . . . . . . 11 ((1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st ‘(1st𝑇)) Fn (1...𝑁))
2228, 220, 2213syl 18 . . . . . . . . . 10 (𝜑 → (1st ‘(1st𝑇)) Fn (1...𝑁))
223222adantr 482 . . . . . . . . 9 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → (1st ‘(1st𝑇)) Fn (1...𝑁))
224 fnconstg 6735 . . . . . . . . . . . . . 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 6735 . . . . . . . . . . . . . 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 472 . . . . . . . . . . . 12 ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) Fn ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}) Fn ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)))
229 dff1o3 6795 . . . . . . . . . . . . . . 15 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) ↔ ((2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁) ∧ Fun (2nd ‘(1st𝑇))))
230229simprbi 498 . . . . . . . . . . . . . 14 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → Fun (2nd ‘(1st𝑇)))
231 imain 6591 . . . . . . . . . . . . . 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 6018 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ((2nd ‘(1st𝑇)) “ ∅))
234 ima0 6034 . . . . . . . . . . . . . 14 ((2nd ‘(1st𝑇)) “ ∅) = ∅
235233, 234eqtrdi 2793 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∩ ((𝑀 + 1)...𝑁))) = ∅)
236232, 235eqtr3d 2779 . . . . . . . . . . . 12 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∩ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))) = ∅)
237 fnun 6619 . . . . . . . . . . . 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 588 . . . . . . . . . . 11 (𝜑 → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))))
239 imaundi 6107 . . . . . . . . . . . . 13 ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)))
24055imaeq2d 6018 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))))
241 f1ofo 6796 . . . . . . . . . . . . . . 15 ((2nd ‘(1st𝑇)):(1...𝑁)–1-1-onto→(1...𝑁) → (2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁))
242 foima 6766 . . . . . . . . . . . . . . 15 ((2nd ‘(1st𝑇)):(1...𝑁)–onto→(1...𝑁) → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
24314, 241, 2423syl 18 . . . . . . . . . . . . . 14 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑁)) = (1...𝑁))
244240, 243eqtr3d 2779 . . . . . . . . . . . . 13 (𝜑 → ((2nd ‘(1st𝑇)) “ ((1...𝑀) ∪ ((𝑀 + 1)...𝑁))) = (1...𝑁))
245239, 244eqtr3id 2791 . . . . . . . . . . . 12 (𝜑 → (((2nd ‘(1st𝑇)) “ (1...𝑀)) ∪ ((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁))) = (1...𝑁))
246245fneq2d 6601 . . . . . . . . . . 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 231 . . . . . . . . . 10 (𝜑 → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
248247adantr 482 . . . . . . . . 9 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})) Fn (1...𝑁))
249 ovexd 7397 . . . . . . . . 9 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → (1...𝑁) ∈ V)
250 eqidd 2738 . . . . . . . . 9 (((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) ∧ 𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑦) = ((1st ‘(1st𝑇))‘𝑦))
251 fvun1 6937 . . . . . . . . . . . . 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 581 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → (((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1})‘𝑦))
254135fvconst2 7158 . . . . . . . . . . . 12 (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1})‘𝑦) = 1)
255254adantl 483 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1})‘𝑦) = 1)
256253, 255eqtrd 2777 . . . . . . . . . 10 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → (((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = 1)
257256adantr 482 . . . . . . . . 9 (((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) ∧ 𝑦 ∈ (1...𝑁)) → (((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0}))‘𝑦) = 1)
258223, 248, 249, 249, 158, 250, 257ofval 7633 . . . . . . . 8 (((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) ∧ 𝑦 ∈ (1...𝑁)) → (((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦) = (((1st ‘(1st𝑇))‘𝑦) + 1))
259219, 258mpdan 686 . . . . . . 7 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → (((1st ‘(1st𝑇)) ∘f + ((((2nd ‘(1st𝑇)) “ (1...𝑀)) × {1}) ∪ (((2nd ‘(1st𝑇)) “ ((𝑀 + 1)...𝑁)) × {0})))‘𝑦) = (((1st ‘(1st𝑇))‘𝑦) + 1))
260218, 259eqtrd 2777 . . . . . 6 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → ((𝐹𝑀)‘𝑦) = (((1st ‘(1st𝑇))‘𝑦) + 1))
261260adantrr 716 . . . . 5 ((𝜑 ∧ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀)))) → ((𝐹𝑀)‘𝑦) = (((1st ‘(1st𝑇))‘𝑦) + 1))
26246nngt0d 12209 . . . . . . . . . 10 (𝜑 → 0 < 𝑁)
263262, 103breqtrrd 5138 . . . . . . . . 9 (𝜑 → 0 < (2nd𝑈))
26446, 5, 19, 263poimirlem5 36112 . . . . . . . 8 (𝜑 → (𝐹‘0) = (1st ‘(1st𝑈)))
265262, 200breqtrrd 5138 . . . . . . . . 9 (𝜑 → 0 < (2nd𝑇))
26646, 5, 3, 265poimirlem5 36112 . . . . . . . 8 (𝜑 → (𝐹‘0) = (1st ‘(1st𝑇)))
267264, 266eqtr3d 2779 . . . . . . 7 (𝜑 → (1st ‘(1st𝑈)) = (1st ‘(1st𝑇)))
268267fveq1d 6849 . . . . . 6 (𝜑 → ((1st ‘(1st𝑈))‘𝑦) = ((1st ‘(1st𝑇))‘𝑦))
269268adantr 482 . . . . 5 ((𝜑 ∧ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀)))) → ((1st ‘(1st𝑈))‘𝑦) = ((1st ‘(1st𝑇))‘𝑦))
270178, 261, 2693eqtr3d 2785 . . . 4 ((𝜑 ∧ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀)))) → (((1st ‘(1st𝑇))‘𝑦) + 1) = ((1st ‘(1st𝑇))‘𝑦))
271 elmapi 8794 . . . . . . . . . . . 12 ((1st ‘(1st𝑇)) ∈ ((0..^𝐾) ↑m (1...𝑁)) → (1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾))
2728, 220, 2713syl 18 . . . . . . . . . . 11 (𝜑 → (1st ‘(1st𝑇)):(1...𝑁)⟶(0..^𝐾))
273272ffvelcdmda 7040 . . . . . . . . . 10 ((𝜑𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑦) ∈ (0..^𝐾))
274 elfzonn0 13624 . . . . . . . . . 10 (((1st ‘(1st𝑇))‘𝑦) ∈ (0..^𝐾) → ((1st ‘(1st𝑇))‘𝑦) ∈ ℕ0)
275273, 274syl 17 . . . . . . . . 9 ((𝜑𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑦) ∈ ℕ0)
276275nn0red 12481 . . . . . . . 8 ((𝜑𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑦) ∈ ℝ)
277276ltp1d 12092 . . . . . . . 8 ((𝜑𝑦 ∈ (1...𝑁)) → ((1st ‘(1st𝑇))‘𝑦) < (((1st ‘(1st𝑇))‘𝑦) + 1))
278276, 277gtned 11297 . . . . . . 7 ((𝜑𝑦 ∈ (1...𝑁)) → (((1st ‘(1st𝑇))‘𝑦) + 1) ≠ ((1st ‘(1st𝑇))‘𝑦))
279219, 278syldan 592 . . . . . 6 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → (((1st ‘(1st𝑇))‘𝑦) + 1) ≠ ((1st ‘(1st𝑇))‘𝑦))
280279neneqd 2949 . . . . 5 ((𝜑𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀))) → ¬ (((1st ‘(1st𝑇))‘𝑦) + 1) = ((1st ‘(1st𝑇))‘𝑦))
281280adantrr 716 . . . 4 ((𝜑 ∧ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀)))) → ¬ (((1st ‘(1st𝑇))‘𝑦) + 1) = ((1st ‘(1st𝑇))‘𝑦))
282270, 281pm2.65da 816 . . 3 (𝜑 → ¬ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀))))
283 iman 403 . . 3 ((𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) → 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀))) ↔ ¬ (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) ∧ ¬ 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀))))
284282, 283sylibr 233 . 2 (𝜑 → (𝑦 ∈ ((2nd ‘(1st𝑇)) “ (1...𝑀)) → 𝑦 ∈ ((2nd ‘(1st𝑈)) “ (1...𝑀))))
285284ssrdv 3955 1 (𝜑 → ((2nd ‘(1st𝑇)) “ (1...𝑀)) ⊆ ((2nd ‘(1st𝑈)) “ (1...𝑀)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397   = wceq 1542  wcel 2107  {cab 2714  wne 2944  {crab 3410  Vcvv 3448  csb 3860  cdif 3912  cun 3913  cin 3914  wss 3915  c0 4287  ifcif 4491  {csn 4591   class class class wbr 5110  cmpt 5193   × cxp 5636  ccnv 5637  ran crn 5639  cima 5641  Fun wfun 6495   Fn wfn 6496  wf 6497  ontowfo 6499  1-1-ontowf1o 6500  cfv 6501  (class class class)co 7362  f cof 7620  1st c1st 7924  2nd c2nd 7925  m cmap 8772  cc 11056  cr 11057  0cc0 11058  1c1 11059   + caddc 11061   < clt 11196  cle 11197  cmin 11392  cn 12160  0cn0 12420  cuz 12770  ...cfz 13431  ..^cfzo 13574
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-of 7622  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-er 8655  df-map 8774  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-nn 12161  df-n0 12421  df-z 12507  df-uz 12771  df-fz 13432  df-fzo 13575
This theorem is referenced by:  poimirlem14  36121
  Copyright terms: Public domain W3C validator