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

Theorem poimirlem32 33441
Description: Lemma for poimir 33442, combining poimirlem28 33437, poimirlem30 33439, and poimirlem31 33440 to get Equation (1) of [Kulpa] p. 547. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0 (𝜑𝑁 ∈ ℕ)
poimir.i 𝐼 = ((0[,]1) ↑𝑚 (1...𝑁))
poimir.r 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))
poimir.1 (𝜑𝐹 ∈ ((𝑅t 𝐼) Cn 𝑅))
poimir.2 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧𝐼 ∧ (𝑧𝑛) = 0)) → ((𝐹𝑧)‘𝑛) ≤ 0)
poimir.3 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧𝐼 ∧ (𝑧𝑛) = 1)) → 0 ≤ ((𝐹𝑧)‘𝑛))
Assertion
Ref Expression
poimirlem32 (𝜑 → ∃𝑐𝐼𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
Distinct variable groups:   𝑧,𝑛,𝜑   𝑛,𝐹   𝑛,𝑁   𝜑,𝑧   𝑧,𝐹   𝑧,𝑁   𝑛,𝑐,𝑟,𝑣,𝑧,𝜑   𝐹,𝑐,𝑟,𝑣   𝐼,𝑐,𝑛,𝑟,𝑣,𝑧   𝑁,𝑐,𝑟,𝑣   𝑅,𝑐,𝑛,𝑟,𝑣,𝑧

Proof of Theorem poimirlem32
Dummy variables 𝑓 𝑖 𝑗 𝑘 𝑚 𝑝 𝑞 𝑠 𝑔 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 poimir.0 . . . . . . 7 (𝜑𝑁 ∈ ℕ)
21adantr 481 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 𝑁 ∈ ℕ)
3 oveq1 6657 . . . . . . . . . . . . . 14 (𝑝 = ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝑝𝑓 / ((1...𝑁) × {𝑘})) = (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))
43fveq2d 6195 . . . . . . . . . . . . 13 (𝑝 = ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘}))) = (𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))))
54fveq1d 6193 . . . . . . . . . . . 12 (𝑝 = ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) = ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏))
65breq2d 4665 . . . . . . . . . . 11 (𝑝 = ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ↔ 0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏)))
7 fveq1 6190 . . . . . . . . . . . 12 (𝑝 = ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝑝𝑏) = (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏))
87neeq1d 2853 . . . . . . . . . . 11 (𝑝 = ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → ((𝑝𝑏) ≠ 0 ↔ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0))
96, 8anbi12d 747 . . . . . . . . . 10 (𝑝 = ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → ((0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ (0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)))
109ralbidv 2986 . . . . . . . . 9 (𝑝 = ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)))
1110rabbidv 3189 . . . . . . . 8 (𝑝 = ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} = {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)})
1211uneq2d 3767 . . . . . . 7 (𝑝 = ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) = ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}))
1312supeq1d 8352 . . . . . 6 (𝑝 = ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))
141nnnn0d 11351 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℕ0)
15 0elfz 12436 . . . . . . . . . . 11 (𝑁 ∈ ℕ0 → 0 ∈ (0...𝑁))
1614, 15syl 17 . . . . . . . . . 10 (𝜑 → 0 ∈ (0...𝑁))
1716snssd 4340 . . . . . . . . 9 (𝜑 → {0} ⊆ (0...𝑁))
18 ssrab2 3687 . . . . . . . . . . 11 {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ⊆ (1...𝑁)
19 1eluzge0 11732 . . . . . . . . . . . 12 1 ∈ (ℤ‘0)
20 fzss1 12380 . . . . . . . . . . . 12 (1 ∈ (ℤ‘0) → (1...𝑁) ⊆ (0...𝑁))
2119, 20ax-mp 5 . . . . . . . . . . 11 (1...𝑁) ⊆ (0...𝑁)
2218, 21sstri 3612 . . . . . . . . . 10 {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ⊆ (0...𝑁)
2322a1i 11 . . . . . . . . 9 (𝜑 → {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ⊆ (0...𝑁))
2417, 23unssd 3789 . . . . . . . 8 (𝜑 → ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ⊆ (0...𝑁))
25 ltso 10118 . . . . . . . . 9 < Or ℝ
26 snfi 8038 . . . . . . . . . . 11 {0} ∈ Fin
27 fzfi 12771 . . . . . . . . . . . 12 (1...𝑁) ∈ Fin
28 rabfi 8185 . . . . . . . . . . . 12 ((1...𝑁) ∈ Fin → {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ∈ Fin)
2927, 28ax-mp 5 . . . . . . . . . . 11 {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ∈ Fin
30 unfi 8227 . . . . . . . . . . 11 (({0} ∈ Fin ∧ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ∈ Fin) → ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ∈ Fin)
3126, 29, 30mp2an 708 . . . . . . . . . 10 ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ∈ Fin
32 c0ex 10034 . . . . . . . . . . . 12 0 ∈ V
3332snid 4208 . . . . . . . . . . 11 0 ∈ {0}
34 elun1 3780 . . . . . . . . . . 11 (0 ∈ {0} → 0 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}))
35 ne0i 3921 . . . . . . . . . . 11 (0 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ≠ ∅)
3633, 34, 35mp2b 10 . . . . . . . . . 10 ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ≠ ∅
37 0red 10041 . . . . . . . . . . . . 13 ((𝜑𝑁 ∈ ℕ) → 0 ∈ ℝ)
3837snssd 4340 . . . . . . . . . . . 12 ((𝜑𝑁 ∈ ℕ) → {0} ⊆ ℝ)
391, 38ax-mp 5 . . . . . . . . . . 11 {0} ⊆ ℝ
40 elfzelz 12342 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℤ)
4140ssriv 3607 . . . . . . . . . . . . 13 (1...𝑁) ⊆ ℤ
42 zssre 11384 . . . . . . . . . . . . 13 ℤ ⊆ ℝ
4341, 42sstri 3612 . . . . . . . . . . . 12 (1...𝑁) ⊆ ℝ
4418, 43sstri 3612 . . . . . . . . . . 11 {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ⊆ ℝ
4539, 44unssi 3788 . . . . . . . . . 10 ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ⊆ ℝ
4631, 36, 453pm3.2i 1239 . . . . . . . . 9 (({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ∈ Fin ∧ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ≠ ∅ ∧ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ⊆ ℝ)
47 fisupcl 8375 . . . . . . . . 9 (( < Or ℝ ∧ (({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ∈ Fin ∧ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ≠ ∅ ∧ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ⊆ ℝ)) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}))
4825, 46, 47mp2an 708 . . . . . . . 8 sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})
49 ssel 3597 . . . . . . . 8 (({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ⊆ (0...𝑁) → (sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ∈ (0...𝑁)))
5024, 48, 49mpisyl 21 . . . . . . 7 (𝜑 → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ∈ (0...𝑁))
5150ad2antrr 762 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑝:(1...𝑁)⟶(0...𝑘)) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ∈ (0...𝑁))
52 elfznn 12370 . . . . . . . . 9 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ)
53 nngt0 11049 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → 0 < 𝑛)
5453adantr 481 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) → 0 < 𝑛)
55 simpr 477 . . . . . . . . . . . . . 14 ((0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → (𝑝𝑏) ≠ 0)
5655ralimi 2952 . . . . . . . . . . . . 13 (∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑠)(𝑝𝑏) ≠ 0)
57 elfznn 12370 . . . . . . . . . . . . . 14 (𝑠 ∈ (1...𝑁) → 𝑠 ∈ ℕ)
58 nnre 11027 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
59 nnre 11027 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ℕ → 𝑠 ∈ ℝ)
60 lenlt 10116 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℝ ∧ 𝑠 ∈ ℝ) → (𝑛𝑠 ↔ ¬ 𝑠 < 𝑛))
6158, 59, 60syl2an 494 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ) → (𝑛𝑠 ↔ ¬ 𝑠 < 𝑛))
62 elfz1b 12409 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ (1...𝑠) ↔ (𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ ∧ 𝑛𝑠))
6362biimpri 218 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ ∧ 𝑛𝑠) → 𝑛 ∈ (1...𝑠))
64633expia 1267 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ) → (𝑛𝑠𝑛 ∈ (1...𝑠)))
6561, 64sylbird 250 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ) → (¬ 𝑠 < 𝑛𝑛 ∈ (1...𝑠)))
66 fveq2 6191 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = 𝑛 → (𝑝𝑏) = (𝑝𝑛))
6766eqeq1d 2624 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = 𝑛 → ((𝑝𝑏) = 0 ↔ (𝑝𝑛) = 0))
6867rspcev 3309 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ (1...𝑠) ∧ (𝑝𝑛) = 0) → ∃𝑏 ∈ (1...𝑠)(𝑝𝑏) = 0)
6968expcom 451 . . . . . . . . . . . . . . . . . 18 ((𝑝𝑛) = 0 → (𝑛 ∈ (1...𝑠) → ∃𝑏 ∈ (1...𝑠)(𝑝𝑏) = 0))
7065, 69sylan9 689 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ) ∧ (𝑝𝑛) = 0) → (¬ 𝑠 < 𝑛 → ∃𝑏 ∈ (1...𝑠)(𝑝𝑏) = 0))
7170an32s 846 . . . . . . . . . . . . . . . 16 (((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) ∧ 𝑠 ∈ ℕ) → (¬ 𝑠 < 𝑛 → ∃𝑏 ∈ (1...𝑠)(𝑝𝑏) = 0))
72 nne 2798 . . . . . . . . . . . . . . . . . 18 (¬ (𝑝𝑏) ≠ 0 ↔ (𝑝𝑏) = 0)
7372rexbii 3041 . . . . . . . . . . . . . . . . 17 (∃𝑏 ∈ (1...𝑠) ¬ (𝑝𝑏) ≠ 0 ↔ ∃𝑏 ∈ (1...𝑠)(𝑝𝑏) = 0)
74 rexnal 2995 . . . . . . . . . . . . . . . . 17 (∃𝑏 ∈ (1...𝑠) ¬ (𝑝𝑏) ≠ 0 ↔ ¬ ∀𝑏 ∈ (1...𝑠)(𝑝𝑏) ≠ 0)
7573, 74bitr3i 266 . . . . . . . . . . . . . . . 16 (∃𝑏 ∈ (1...𝑠)(𝑝𝑏) = 0 ↔ ¬ ∀𝑏 ∈ (1...𝑠)(𝑝𝑏) ≠ 0)
7671, 75syl6ib 241 . . . . . . . . . . . . . . 15 (((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) ∧ 𝑠 ∈ ℕ) → (¬ 𝑠 < 𝑛 → ¬ ∀𝑏 ∈ (1...𝑠)(𝑝𝑏) ≠ 0))
7776con4d 114 . . . . . . . . . . . . . 14 (((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) ∧ 𝑠 ∈ ℕ) → (∀𝑏 ∈ (1...𝑠)(𝑝𝑏) ≠ 0 → 𝑠 < 𝑛))
7857, 77sylan2 491 . . . . . . . . . . . . 13 (((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) ∧ 𝑠 ∈ (1...𝑁)) → (∀𝑏 ∈ (1...𝑠)(𝑝𝑏) ≠ 0 → 𝑠 < 𝑛))
7956, 78syl5 34 . . . . . . . . . . . 12 (((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) ∧ 𝑠 ∈ (1...𝑁)) → (∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → 𝑠 < 𝑛))
8079ralrimiva 2966 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) → ∀𝑠 ∈ (1...𝑁)(∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → 𝑠 < 𝑛))
81 ralunb 3794 . . . . . . . . . . . 12 (∀𝑠 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})𝑠 < 𝑛 ↔ (∀𝑠 ∈ {0}𝑠 < 𝑛 ∧ ∀𝑠 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}𝑠 < 𝑛))
82 breq1 4656 . . . . . . . . . . . . . 14 (𝑠 = 0 → (𝑠 < 𝑛 ↔ 0 < 𝑛))
8332, 82ralsn 4222 . . . . . . . . . . . . 13 (∀𝑠 ∈ {0}𝑠 < 𝑛 ↔ 0 < 𝑛)
84 oveq2 6658 . . . . . . . . . . . . . . 15 (𝑎 = 𝑠 → (1...𝑎) = (1...𝑠))
8584raleqdv 3144 . . . . . . . . . . . . . 14 (𝑎 = 𝑠 → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
8685ralrab 3368 . . . . . . . . . . . . 13 (∀𝑠 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}𝑠 < 𝑛 ↔ ∀𝑠 ∈ (1...𝑁)(∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → 𝑠 < 𝑛))
8783, 86anbi12i 733 . . . . . . . . . . . 12 ((∀𝑠 ∈ {0}𝑠 < 𝑛 ∧ ∀𝑠 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}𝑠 < 𝑛) ↔ (0 < 𝑛 ∧ ∀𝑠 ∈ (1...𝑁)(∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → 𝑠 < 𝑛)))
8881, 87bitri 264 . . . . . . . . . . 11 (∀𝑠 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})𝑠 < 𝑛 ↔ (0 < 𝑛 ∧ ∀𝑠 ∈ (1...𝑁)(∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → 𝑠 < 𝑛)))
8954, 80, 88sylanbrc 698 . . . . . . . . . 10 ((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) → ∀𝑠 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})𝑠 < 𝑛)
90 breq1 4656 . . . . . . . . . . 11 (𝑠 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) → (𝑠 < 𝑛 ↔ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < 𝑛))
9190rspcva 3307 . . . . . . . . . 10 ((sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ∧ ∀𝑠 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})𝑠 < 𝑛) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < 𝑛)
9248, 89, 91sylancr 695 . . . . . . . . 9 ((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < 𝑛)
9352, 92sylan 488 . . . . . . . 8 ((𝑛 ∈ (1...𝑁) ∧ (𝑝𝑛) = 0) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < 𝑛)
94933adant2 1080 . . . . . . 7 ((𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 0) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < 𝑛)
9594adantl 482 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 0)) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < 𝑛)
9640zred 11482 . . . . . . . . . . 11 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℝ)
97963ad2ant1 1082 . . . . . . . . . 10 ((𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) → 𝑛 ∈ ℝ)
9897adantl 482 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → 𝑛 ∈ ℝ)
99 simpr1 1067 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → 𝑛 ∈ (1...𝑁))
100 simpll 790 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → 𝜑)
101 simplr 792 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → 𝑘 ∈ ℕ)
102 elfzelz 12342 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ (0...𝑘) → 𝑖 ∈ ℤ)
103102zred 11482 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ (0...𝑘) → 𝑖 ∈ ℝ)
104 nndivre 11056 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ ℝ)
105103, 104sylan 488 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ ℝ)
106 elfzle1 12344 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ (0...𝑘) → 0 ≤ 𝑖)
107103, 106jca 554 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ (0...𝑘) → (𝑖 ∈ ℝ ∧ 0 ≤ 𝑖))
108 nnrp 11842 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
109108rpregt0d 11878 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ ℕ → (𝑘 ∈ ℝ ∧ 0 < 𝑘))
110 divge0 10892 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑖 ∈ ℝ ∧ 0 ≤ 𝑖) ∧ (𝑘 ∈ ℝ ∧ 0 < 𝑘)) → 0 ≤ (𝑖 / 𝑘))
111107, 109, 110syl2an 494 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝑖 / 𝑘))
112 elfzle2 12345 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ (0...𝑘) → 𝑖𝑘)
113112adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑖𝑘)
114103adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑖 ∈ ℝ)
115 1red 10055 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 1 ∈ ℝ)
116108adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ+)
117114, 115, 116ledivmuld 11925 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑖 / 𝑘) ≤ 1 ↔ 𝑖 ≤ (𝑘 · 1)))
118 nncn 11028 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
119118mulid1d 10057 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ ℕ → (𝑘 · 1) = 𝑘)
120119breq2d 4665 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ ℕ → (𝑖 ≤ (𝑘 · 1) ↔ 𝑖𝑘))
121120adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 ≤ (𝑘 · 1) ↔ 𝑖𝑘))
122117, 121bitrd 268 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑖 / 𝑘) ≤ 1 ↔ 𝑖𝑘))
123113, 122mpbird 247 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ≤ 1)
124 0re 10040 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ ℝ
125 1re 10039 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℝ
126124, 125elicc2i 12239 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖 / 𝑘) ∈ (0[,]1) ↔ ((𝑖 / 𝑘) ∈ ℝ ∧ 0 ≤ (𝑖 / 𝑘) ∧ (𝑖 / 𝑘) ≤ 1))
127105, 111, 123, 126syl3anbrc 1246 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ (0[,]1))
128127ancoms 469 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑘)) → (𝑖 / 𝑘) ∈ (0[,]1))
129 elsni 4194 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ {𝑘} → 𝑗 = 𝑘)
130129oveq2d 6666 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ {𝑘} → (𝑖 / 𝑗) = (𝑖 / 𝑘))
131130eleq1d 2686 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ {𝑘} → ((𝑖 / 𝑗) ∈ (0[,]1) ↔ (𝑖 / 𝑘) ∈ (0[,]1)))
132128, 131syl5ibrcom 237 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑘)) → (𝑗 ∈ {𝑘} → (𝑖 / 𝑗) ∈ (0[,]1)))
133132impr 649 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ ∧ (𝑖 ∈ (0...𝑘) ∧ 𝑗 ∈ {𝑘})) → (𝑖 / 𝑗) ∈ (0[,]1))
134101, 133sylan 488 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) ∧ (𝑖 ∈ (0...𝑘) ∧ 𝑗 ∈ {𝑘})) → (𝑖 / 𝑗) ∈ (0[,]1))
135 simprr 796 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → 𝑝:(1...𝑁)⟶(0...𝑘))
136 vex 3203 . . . . . . . . . . . . . . . . . 18 𝑘 ∈ V
137136fconst 6091 . . . . . . . . . . . . . . . . 17 ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘}
138137a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘})
139 fzfid 12772 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → (1...𝑁) ∈ Fin)
140 inidm 3822 . . . . . . . . . . . . . . . 16 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
141134, 135, 138, 139, 139, 140off 6912 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → (𝑝𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
142 poimir.i . . . . . . . . . . . . . . . . 17 𝐼 = ((0[,]1) ↑𝑚 (1...𝑁))
143142eleq2i 2693 . . . . . . . . . . . . . . . 16 ((𝑝𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ (𝑝𝑓 / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑𝑚 (1...𝑁)))
144 ovex 6678 . . . . . . . . . . . . . . . . 17 (0[,]1) ∈ V
145 ovex 6678 . . . . . . . . . . . . . . . . 17 (1...𝑁) ∈ V
146144, 145elmap 7886 . . . . . . . . . . . . . . . 16 ((𝑝𝑓 / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑𝑚 (1...𝑁)) ↔ (𝑝𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
147143, 146bitri 264 . . . . . . . . . . . . . . 15 ((𝑝𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ (𝑝𝑓 / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
148141, 147sylibr 224 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → (𝑝𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼)
1491483adantr3 1222 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → (𝑝𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼)
150 3anass 1042 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) ↔ (𝑛 ∈ (1...𝑁) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)))
151 ancom 466 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (1...𝑁) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) ↔ ((𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) ∧ 𝑛 ∈ (1...𝑁)))
152150, 151bitri 264 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) ↔ ((𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) ∧ 𝑛 ∈ (1...𝑁)))
153 ffn 6045 . . . . . . . . . . . . . . . . . 18 (𝑝:(1...𝑁)⟶(0...𝑘) → 𝑝 Fn (1...𝑁))
154153ad2antrl 764 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → 𝑝 Fn (1...𝑁))
155 fnconstg 6093 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ V → ((1...𝑁) × {𝑘}) Fn (1...𝑁))
156136, 155mp1i 13 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ((1...𝑁) × {𝑘}) Fn (1...𝑁))
157 fzfid 12772 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → (1...𝑁) ∈ Fin)
158 simplrr 801 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑝𝑛) = 𝑘)
159136fvconst2 6469 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {𝑘})‘𝑛) = 𝑘)
160159adantl 482 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {𝑘})‘𝑛) = 𝑘)
161154, 156, 157, 157, 140, 158, 160ofval 6906 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑝𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = (𝑘 / 𝑘))
162161anasss 679 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ) ∧ ((𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) ∧ 𝑛 ∈ (1...𝑁))) → ((𝑝𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = (𝑘 / 𝑘))
163152, 162sylan2b 492 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ((𝑝𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = (𝑘 / 𝑘))
164 nnne0 11053 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ → 𝑘 ≠ 0)
165118, 164dividd 10799 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ → (𝑘 / 𝑘) = 1)
166165ad2antlr 763 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → (𝑘 / 𝑘) = 1)
167163, 166eqtrd 2656 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ((𝑝𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = 1)
168 ovex 6678 . . . . . . . . . . . . . 14 (𝑝𝑓 / ((1...𝑁) × {𝑘})) ∈ V
169 eleq1 2689 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑝𝑓 / ((1...𝑁) × {𝑘})) → (𝑧𝐼 ↔ (𝑝𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼))
170 fveq1 6190 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑝𝑓 / ((1...𝑁) × {𝑘})) → (𝑧𝑛) = ((𝑝𝑓 / ((1...𝑁) × {𝑘}))‘𝑛))
171170eqeq1d 2624 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑝𝑓 / ((1...𝑁) × {𝑘})) → ((𝑧𝑛) = 1 ↔ ((𝑝𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = 1))
172169, 1713anbi23d 1402 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑝𝑓 / ((1...𝑁) × {𝑘})) → ((𝑛 ∈ (1...𝑁) ∧ 𝑧𝐼 ∧ (𝑧𝑛) = 1) ↔ (𝑛 ∈ (1...𝑁) ∧ (𝑝𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 ∧ ((𝑝𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = 1)))
173172anbi2d 740 . . . . . . . . . . . . . . 15 (𝑧 = (𝑝𝑓 / ((1...𝑁) × {𝑘})) → ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧𝐼 ∧ (𝑧𝑛) = 1)) ↔ (𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ (𝑝𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 ∧ ((𝑝𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = 1))))
174 fveq2 6191 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑝𝑓 / ((1...𝑁) × {𝑘})) → (𝐹𝑧) = (𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘}))))
175174fveq1d 6193 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑝𝑓 / ((1...𝑁) × {𝑘})) → ((𝐹𝑧)‘𝑛) = ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑛))
176175breq2d 4665 . . . . . . . . . . . . . . 15 (𝑧 = (𝑝𝑓 / ((1...𝑁) × {𝑘})) → (0 ≤ ((𝐹𝑧)‘𝑛) ↔ 0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
177173, 176imbi12d 334 . . . . . . . . . . . . . 14 (𝑧 = (𝑝𝑓 / ((1...𝑁) × {𝑘})) → (((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧𝐼 ∧ (𝑧𝑛) = 1)) → 0 ≤ ((𝐹𝑧)‘𝑛)) ↔ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ (𝑝𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 ∧ ((𝑝𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = 1)) → 0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑛))))
178 poimir.3 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧𝐼 ∧ (𝑧𝑛) = 1)) → 0 ≤ ((𝐹𝑧)‘𝑛))
179168, 177, 178vtocl 3259 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ (𝑝𝑓 / ((1...𝑁) × {𝑘})) ∈ 𝐼 ∧ ((𝑝𝑓 / ((1...𝑁) × {𝑘}))‘𝑛) = 1)) → 0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑛))
180100, 99, 149, 167, 179syl13anc 1328 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → 0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑛))
181 simpr 477 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
182 simp3 1063 . . . . . . . . . . . . 13 ((𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) → (𝑝𝑛) = 𝑘)
183 neeq1 2856 . . . . . . . . . . . . . . 15 ((𝑝𝑛) = 𝑘 → ((𝑝𝑛) ≠ 0 ↔ 𝑘 ≠ 0))
184164, 183syl5ibrcom 237 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → ((𝑝𝑛) = 𝑘 → (𝑝𝑛) ≠ 0))
185184imp 445 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ∧ (𝑝𝑛) = 𝑘) → (𝑝𝑛) ≠ 0)
186181, 182, 185syl2an 494 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → (𝑝𝑛) ≠ 0)
187 vex 3203 . . . . . . . . . . . . 13 𝑛 ∈ V
188 fveq2 6191 . . . . . . . . . . . . . . 15 (𝑏 = 𝑛 → ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) = ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑛))
189188breq2d 4665 . . . . . . . . . . . . . 14 (𝑏 = 𝑛 → (0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ↔ 0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑛)))
19066neeq1d 2853 . . . . . . . . . . . . . 14 (𝑏 = 𝑛 → ((𝑝𝑏) ≠ 0 ↔ (𝑝𝑛) ≠ 0))
191189, 190anbi12d 747 . . . . . . . . . . . . 13 (𝑏 = 𝑛 → ((0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ (0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∧ (𝑝𝑛) ≠ 0)))
192187, 191ralsn 4222 . . . . . . . . . . . 12 (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ (0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑛) ∧ (𝑝𝑛) ≠ 0))
193180, 186, 192sylanbrc 698 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))
19440zcnd 11483 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ)
195 1cnd 10056 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...𝑁) → 1 ∈ ℂ)
196194, 195subeq0ad 10402 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) = 0 ↔ 𝑛 = 1))
197196biimpcd 239 . . . . . . . . . . . . . . . . 17 ((𝑛 − 1) = 0 → (𝑛 ∈ (1...𝑁) → 𝑛 = 1))
198 1z 11407 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℤ
199 fzsn 12383 . . . . . . . . . . . . . . . . . . . . 21 (1 ∈ ℤ → (1...1) = {1})
200198, 199ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (1...1) = {1}
201 oveq2 6658 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 1 → (1...𝑛) = (1...1))
202 sneq 4187 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 1 → {𝑛} = {1})
203200, 201, 2023eqtr4a 2682 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 1 → (1...𝑛) = {𝑛})
204203raleqdv 3144 . . . . . . . . . . . . . . . . . 18 (𝑛 = 1 → (∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
205204biimprd 238 . . . . . . . . . . . . . . . . 17 (𝑛 = 1 → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
206197, 205syl6 35 . . . . . . . . . . . . . . . 16 ((𝑛 − 1) = 0 → (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
207 ralun 3795 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)) → ∀𝑏 ∈ ((1...(𝑛 − 1)) ∪ {𝑛})(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))
208 npcan1 10455 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ℂ → ((𝑛 − 1) + 1) = 𝑛)
209194, 208syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) + 1) = 𝑛)
210 elfzuz 12338 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ (ℤ‘1))
211209, 210eqeltrd 2701 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) + 1) ∈ (ℤ‘1))
212 peano2zm 11420 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ℤ → (𝑛 − 1) ∈ ℤ)
213 uzid 11702 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 − 1) ∈ ℤ → (𝑛 − 1) ∈ (ℤ‘(𝑛 − 1)))
214 peano2uz 11741 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 − 1) ∈ (ℤ‘(𝑛 − 1)) → ((𝑛 − 1) + 1) ∈ (ℤ‘(𝑛 − 1)))
21540, 212, 213, 2144syl 19 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) + 1) ∈ (ℤ‘(𝑛 − 1)))
216209, 215eqeltrrd 2702 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ (ℤ‘(𝑛 − 1)))
217 fzsplit2 12366 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑛 − 1) + 1) ∈ (ℤ‘1) ∧ 𝑛 ∈ (ℤ‘(𝑛 − 1))) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)))
218211, 216, 217syl2anc 693 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (1...𝑁) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)))
219209oveq1d 6665 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...𝑁) → (((𝑛 − 1) + 1)...𝑛) = (𝑛...𝑛))
220 fzsn 12383 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ℤ → (𝑛...𝑛) = {𝑛})
22140, 220syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...𝑁) → (𝑛...𝑛) = {𝑛})
222219, 221eqtrd 2656 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (1...𝑁) → (((𝑛 − 1) + 1)...𝑛) = {𝑛})
223222uneq2d 3767 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (1...𝑁) → ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)) = ((1...(𝑛 − 1)) ∪ {𝑛}))
224218, 223eqtrd 2656 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ (1...𝑁) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ {𝑛}))
225224raleqdv 3144 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ ∀𝑏 ∈ ((1...(𝑛 − 1)) ∪ {𝑛})(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
226207, 225syl5ibr 236 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...𝑁) → ((∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
227226expd 452 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
228227com12 32 . . . . . . . . . . . . . . . . 17 (∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
229228adantl 482 . . . . . . . . . . . . . . . 16 (((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)) → (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
230206, 229jaoi 394 . . . . . . . . . . . . . . 15 (((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))) → (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
231230imdistand 728 . . . . . . . . . . . . . 14 (((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))) → ((𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)) → (𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
232231com12 32 . . . . . . . . . . . . 13 ((𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)) → (((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))) → (𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
233 elun 3753 . . . . . . . . . . . . . 14 ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ↔ ((𝑛 − 1) ∈ {0} ∨ (𝑛 − 1) ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}))
234 ovex 6678 . . . . . . . . . . . . . . . 16 (𝑛 − 1) ∈ V
235234elsn 4192 . . . . . . . . . . . . . . 15 ((𝑛 − 1) ∈ {0} ↔ (𝑛 − 1) = 0)
236 oveq2 6658 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑛 − 1) → (1...𝑎) = (1...(𝑛 − 1)))
237236raleqdv 3144 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑛 − 1) → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
238237elrab 3363 . . . . . . . . . . . . . . 15 ((𝑛 − 1) ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ↔ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
239235, 238orbi12i 543 . . . . . . . . . . . . . 14 (((𝑛 − 1) ∈ {0} ∨ (𝑛 − 1) ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ↔ ((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
240233, 239bitri 264 . . . . . . . . . . . . 13 ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ↔ ((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
241 oveq2 6658 . . . . . . . . . . . . . . 15 (𝑎 = 𝑛 → (1...𝑎) = (1...𝑛))
242241raleqdv 3144 . . . . . . . . . . . . . 14 (𝑎 = 𝑛 → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
243242elrab 3363 . . . . . . . . . . . . 13 (𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ↔ (𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
244232, 240, 2433imtr4g 285 . . . . . . . . . . . 12 ((𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)) → ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → 𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}))
245 elun2 3781 . . . . . . . . . . . 12 (𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} → 𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}))
246244, 245syl6 35 . . . . . . . . . . 11 ((𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)) → ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → 𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})))
24799, 193, 246syl2anc 693 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → 𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})))
248 fimaxre2 10969 . . . . . . . . . . . . 13 ((({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ⊆ ℝ ∧ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ∈ Fin) → ∃𝑖 ∈ ℝ ∀𝑗 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})𝑗𝑖)
24945, 31, 248mp2an 708 . . . . . . . . . . . 12 𝑖 ∈ ℝ ∀𝑗 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})𝑗𝑖
25045, 36, 2493pm3.2i 1239 . . . . . . . . . . 11 (({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ⊆ ℝ ∧ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ≠ ∅ ∧ ∃𝑖 ∈ ℝ ∀𝑗 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})𝑗𝑖)
251250suprubii 10998 . . . . . . . . . 10 (𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → 𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ))
252247, 251syl6 35 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → 𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )))
253 ltm1 10863 . . . . . . . . . 10 (𝑛 ∈ ℝ → (𝑛 − 1) < 𝑛)
254 peano2rem 10348 . . . . . . . . . . 11 (𝑛 ∈ ℝ → (𝑛 − 1) ∈ ℝ)
25545, 48sselii 3600 . . . . . . . . . . . 12 sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ∈ ℝ
256 ltletr 10129 . . . . . . . . . . . 12 (((𝑛 − 1) ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ∈ ℝ) → (((𝑛 − 1) < 𝑛𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )) → (𝑛 − 1) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )))
257255, 256mp3an3 1413 . . . . . . . . . . 11 (((𝑛 − 1) ∈ ℝ ∧ 𝑛 ∈ ℝ) → (((𝑛 − 1) < 𝑛𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )) → (𝑛 − 1) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )))
258254, 257mpancom 703 . . . . . . . . . 10 (𝑛 ∈ ℝ → (((𝑛 − 1) < 𝑛𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )) → (𝑛 − 1) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )))
259253, 258mpand 711 . . . . . . . . 9 (𝑛 ∈ ℝ → (𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) → (𝑛 − 1) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )))
26098, 252, 259sylsyld 61 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → (𝑛 − 1) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )))
261255ltnri 10146 . . . . . . . . . 10 ¬ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )
262 breq1 4656 . . . . . . . . . 10 (sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) = (𝑛 − 1) → (sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ↔ (𝑛 − 1) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )))
263261, 262mtbii 316 . . . . . . . . 9 (sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) = (𝑛 − 1) → ¬ (𝑛 − 1) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ))
264263necon2ai 2823 . . . . . . . 8 ((𝑛 − 1) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ≠ (𝑛 − 1))
265260, 264syl6 35 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ≠ (𝑛 − 1)))
266 eleq1 2689 . . . . . . . . 9 (sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) = (𝑛 − 1) → (sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ↔ (𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})))
26748, 266mpbii 223 . . . . . . . 8 (sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) = (𝑛 − 1) → (𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}))
268267necon3bi 2820 . . . . . . 7 (¬ (𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ≠ (𝑛 − 1))
269265, 268pm2.61d1 171 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ≠ (𝑛 − 1))
2702, 13, 51, 95, 269, 181poimirlem28 33437 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ∃𝑠 ∈ (((0..^𝑘) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))
271 nn0ex 11298 . . . . . . . . . . . 12 0 ∈ V
272 fzo0ssnn0 12548 . . . . . . . . . . . 12 (0..^𝑘) ⊆ ℕ0
273 mapss 7900 . . . . . . . . . . . 12 ((ℕ0 ∈ V ∧ (0..^𝑘) ⊆ ℕ0) → ((0..^𝑘) ↑𝑚 (1...𝑁)) ⊆ (ℕ0𝑚 (1...𝑁)))
274271, 272, 273mp2an 708 . . . . . . . . . . 11 ((0..^𝑘) ↑𝑚 (1...𝑁)) ⊆ (ℕ0𝑚 (1...𝑁))
275 xpss1 5228 . . . . . . . . . . 11 (((0..^𝑘) ↑𝑚 (1...𝑁)) ⊆ (ℕ0𝑚 (1...𝑁)) → (((0..^𝑘) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ⊆ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
276274, 275ax-mp 5 . . . . . . . . . 10 (((0..^𝑘) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ⊆ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
277276sseli 3599 . . . . . . . . 9 (𝑠 ∈ (((0..^𝑘) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → 𝑠 ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
278 xp1st 7198 . . . . . . . . . 10 (𝑠 ∈ (((0..^𝑘) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st𝑠) ∈ ((0..^𝑘) ↑𝑚 (1...𝑁)))
279 elmapi 7879 . . . . . . . . . 10 ((1st𝑠) ∈ ((0..^𝑘) ↑𝑚 (1...𝑁)) → (1st𝑠):(1...𝑁)⟶(0..^𝑘))
280 frn 6053 . . . . . . . . . 10 ((1st𝑠):(1...𝑁)⟶(0..^𝑘) → ran (1st𝑠) ⊆ (0..^𝑘))
281278, 279, 2803syl 18 . . . . . . . . 9 (𝑠 ∈ (((0..^𝑘) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → ran (1st𝑠) ⊆ (0..^𝑘))
282277, 281jca 554 . . . . . . . 8 (𝑠 ∈ (((0..^𝑘) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (𝑠 ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ran (1st𝑠) ⊆ (0..^𝑘)))
283282anim1i 592 . . . . . . 7 ((𝑠 ∈ (((0..^𝑘) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) → ((𝑠 ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ran (1st𝑠) ⊆ (0..^𝑘)) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))
284 anass 681 . . . . . . 7 (((𝑠 ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ran (1st𝑠) ⊆ (0..^𝑘)) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) ↔ (𝑠 ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ (ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))))
285283, 284sylib 208 . . . . . 6 ((𝑠 ∈ (((0..^𝑘) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) → (𝑠 ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ (ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))))
286285reximi2 3010 . . . . 5 (∃𝑠 ∈ (((0..^𝑘) ↑𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) → ∃𝑠 ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})(ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))
287270, 286syl 17 . . . 4 ((𝜑𝑘 ∈ ℕ) → ∃𝑠 ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})(ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))
288287ralrimiva 2966 . . 3 (𝜑 → ∀𝑘 ∈ ℕ ∃𝑠 ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})(ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))
289 nnex 11026 . . . 4 ℕ ∈ V
290145, 271ixpconst 7918 . . . . . . 7 X𝑛 ∈ (1...𝑁)ℕ0 = (ℕ0𝑚 (1...𝑁))
291 omelon 8543 . . . . . . . . . 10 ω ∈ On
292 nn0ennn 12778 . . . . . . . . . . 11 0 ≈ ℕ
293 nnenom 12779 . . . . . . . . . . 11 ℕ ≈ ω
294292, 293entr2i 8011 . . . . . . . . . 10 ω ≈ ℕ0
295 isnumi 8772 . . . . . . . . . 10 ((ω ∈ On ∧ ω ≈ ℕ0) → ℕ0 ∈ dom card)
296291, 294, 295mp2an 708 . . . . . . . . 9 0 ∈ dom card
297296rgenw 2924 . . . . . . . 8 𝑛 ∈ (1...𝑁)ℕ0 ∈ dom card
298 finixpnum 33394 . . . . . . . 8 (((1...𝑁) ∈ Fin ∧ ∀𝑛 ∈ (1...𝑁)ℕ0 ∈ dom card) → X𝑛 ∈ (1...𝑁)ℕ0 ∈ dom card)
29927, 297, 298mp2an 708 . . . . . . 7 X𝑛 ∈ (1...𝑁)ℕ0 ∈ dom card
300290, 299eqeltrri 2698 . . . . . 6 (ℕ0𝑚 (1...𝑁)) ∈ dom card
301145, 145mapval 7869 . . . . . . . . 9 ((1...𝑁) ↑𝑚 (1...𝑁)) = {𝑓𝑓:(1...𝑁)⟶(1...𝑁)}
302 mapfi 8262 . . . . . . . . . 10 (((1...𝑁) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((1...𝑁) ↑𝑚 (1...𝑁)) ∈ Fin)
30327, 27, 302mp2an 708 . . . . . . . . 9 ((1...𝑁) ↑𝑚 (1...𝑁)) ∈ Fin
304301, 303eqeltrri 2698 . . . . . . . 8 {𝑓𝑓:(1...𝑁)⟶(1...𝑁)} ∈ Fin
305 f1of 6137 . . . . . . . . 9 (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑓:(1...𝑁)⟶(1...𝑁))
306305ss2abi 3674 . . . . . . . 8 {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ⊆ {𝑓𝑓:(1...𝑁)⟶(1...𝑁)}
307 ssfi 8180 . . . . . . . 8 (({𝑓𝑓:(1...𝑁)⟶(1...𝑁)} ∈ Fin ∧ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ⊆ {𝑓𝑓:(1...𝑁)⟶(1...𝑁)}) → {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ∈ Fin)
308304, 306, 307mp2an 708 . . . . . . 7 {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ∈ Fin
309 finnum 8774 . . . . . . 7 ({𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ∈ Fin → {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ∈ dom card)
310308, 309ax-mp 5 . . . . . 6 {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ∈ dom card
311 xpnum 8777 . . . . . 6 (((ℕ0𝑚 (1...𝑁)) ∈ dom card ∧ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ∈ dom card) → ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∈ dom card)
312300, 310, 311mp2an 708 . . . . 5 ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∈ dom card
313 ssrab2 3687 . . . . . . . 8 {𝑠 ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))} ⊆ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
314313rgenw 2924 . . . . . . 7 𝑘 ∈ ℕ {𝑠 ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))} ⊆ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
315 ss2iun 4536 . . . . . . 7 (∀𝑘 ∈ ℕ {𝑠 ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))} ⊆ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → 𝑘 ∈ ℕ {𝑠 ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))} ⊆ 𝑘 ∈ ℕ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
316314, 315ax-mp 5 . . . . . 6 𝑘 ∈ ℕ {𝑠 ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))} ⊆ 𝑘 ∈ ℕ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
317 1nn 11031 . . . . . . 7 1 ∈ ℕ
318 ne0i 3921 . . . . . . 7 (1 ∈ ℕ → ℕ ≠ ∅)
319 iunconst 4529 . . . . . . 7 (ℕ ≠ ∅ → 𝑘 ∈ ℕ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) = ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
320317, 318, 319mp2b 10 . . . . . 6 𝑘 ∈ ℕ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) = ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
321316, 320sseqtri 3637 . . . . 5 𝑘 ∈ ℕ {𝑠 ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))} ⊆ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
322 ssnum 8862 . . . . 5 ((((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∈ dom card ∧ 𝑘 ∈ ℕ {𝑠 ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))} ⊆ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) → 𝑘 ∈ ℕ {𝑠 ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))} ∈ dom card)
323312, 321, 322mp2an 708 . . . 4 𝑘 ∈ ℕ {𝑠 ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))} ∈ dom card
324 fveq2 6191 . . . . . . . 8 (𝑠 = (𝑔𝑘) → (1st𝑠) = (1st ‘(𝑔𝑘)))
325324rneqd 5353 . . . . . . 7 (𝑠 = (𝑔𝑘) → ran (1st𝑠) = ran (1st ‘(𝑔𝑘)))
326325sseq1d 3632 . . . . . 6 (𝑠 = (𝑔𝑘) → (ran (1st𝑠) ⊆ (0..^𝑘) ↔ ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘)))
327 fveq2 6191 . . . . . . . . . . . . . . . . . . . . . 22 (𝑠 = (𝑔𝑘) → (2nd𝑠) = (2nd ‘(𝑔𝑘)))
328327imaeq1d 5465 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = (𝑔𝑘) → ((2nd𝑠) “ (1...𝑗)) = ((2nd ‘(𝑔𝑘)) “ (1...𝑗)))
329328xpeq1d 5138 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = (𝑔𝑘) → (((2nd𝑠) “ (1...𝑗)) × {1}) = (((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}))
330327imaeq1d 5465 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = (𝑔𝑘) → ((2nd𝑠) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)))
331330xpeq1d 5138 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = (𝑔𝑘) → (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))
332329, 331uneq12d 3768 . . . . . . . . . . . . . . . . . . 19 (𝑠 = (𝑔𝑘) → ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
333324, 332oveq12d 6668 . . . . . . . . . . . . . . . . . 18 (𝑠 = (𝑔𝑘) → ((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))))
334333oveq1d 6665 . . . . . . . . . . . . . . . . 17 (𝑠 = (𝑔𝑘) → (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) = (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))
335334fveq2d 6195 . . . . . . . . . . . . . . . 16 (𝑠 = (𝑔𝑘) → (𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))) = (𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))))
336335fveq1d 6193 . . . . . . . . . . . . . . 15 (𝑠 = (𝑔𝑘) → ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) = ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏))
337336breq2d 4665 . . . . . . . . . . . . . 14 (𝑠 = (𝑔𝑘) → (0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ↔ 0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏)))
338333fveq1d 6193 . . . . . . . . . . . . . . 15 (𝑠 = (𝑔𝑘) → (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) = (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏))
339338neeq1d 2853 . . . . . . . . . . . . . 14 (𝑠 = (𝑔𝑘) → ((((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0 ↔ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0))
340337, 339anbi12d 747 . . . . . . . . . . . . 13 (𝑠 = (𝑔𝑘) → ((0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0) ↔ (0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)))
341340ralbidv 2986 . . . . . . . . . . . 12 (𝑠 = (𝑔𝑘) → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)))
342341rabbidv 3189 . . . . . . . . . . 11 (𝑠 = (𝑔𝑘) → {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)} = {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)})
343342uneq2d 3767 . . . . . . . . . 10 (𝑠 = (𝑔𝑘) → ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}) = ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}))
344343supeq1d 8352 . . . . . . . . 9 (𝑠 = (𝑔𝑘) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))
345344eqeq2d 2632 . . . . . . . 8 (𝑠 = (𝑔𝑘) → (𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) ↔ 𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))
346345rexbidv 3052 . . . . . . 7 (𝑠 = (𝑔𝑘) → (∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) ↔ ∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))
347346ralbidv 2986 . . . . . 6 (𝑠 = (𝑔𝑘) → (∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) ↔ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))
348326, 347anbi12d 747 . . . . 5 (𝑠 = (𝑔𝑘) → ((ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) ↔ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))))
349348ac6num 9301 . . . 4 ((ℕ ∈ V ∧ 𝑘 ∈ ℕ {𝑠 ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))} ∈ dom card ∧ ∀𝑘 ∈ ℕ ∃𝑠 ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})(ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) → ∃𝑔(𝑔:ℕ⟶((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))))
350289, 323, 349mp3an12 1414 . . 3 (∀𝑘 ∈ ℕ ∃𝑠 ∈ ((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})(ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘𝑓 + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) → ∃𝑔(𝑔:ℕ⟶((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))))
351288, 350syl 17 . 2 (𝜑 → ∃𝑔(𝑔:ℕ⟶((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))))
3521ad2antrr 762 . . . 4 (((𝜑𝑔:ℕ⟶((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) → 𝑁 ∈ ℕ)
353 poimir.r . . . 4 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))
354 poimir.1 . . . . 5 (𝜑𝐹 ∈ ((𝑅t 𝐼) Cn 𝑅))
355354ad2antrr 762 . . . 4 (((𝜑𝑔:ℕ⟶((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) → 𝐹 ∈ ((𝑅t 𝐼) Cn 𝑅))
356 eqid 2622 . . . 4 ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑛) = ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑛)
357 simplr 792 . . . 4 (((𝜑𝑔:ℕ⟶((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) → 𝑔:ℕ⟶((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
358 simpl 473 . . . . . . 7 ((ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) → ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘))
359358ralimi 2952 . . . . . 6 (∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) → ∀𝑘 ∈ ℕ ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘))
360359adantl 482 . . . . 5 (((𝜑𝑔:ℕ⟶((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) → ∀𝑘 ∈ ℕ ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘))
361 fveq2 6191 . . . . . . . . 9 (𝑘 = 𝑝 → (𝑔𝑘) = (𝑔𝑝))
362361fveq2d 6195 . . . . . . . 8 (𝑘 = 𝑝 → (1st ‘(𝑔𝑘)) = (1st ‘(𝑔𝑝)))
363362rneqd 5353 . . . . . . 7 (𝑘 = 𝑝 → ran (1st ‘(𝑔𝑘)) = ran (1st ‘(𝑔𝑝)))
364 oveq2 6658 . . . . . . 7 (𝑘 = 𝑝 → (0..^𝑘) = (0..^𝑝))
365363, 364sseq12d 3634 . . . . . 6 (𝑘 = 𝑝 → (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ↔ ran (1st ‘(𝑔𝑝)) ⊆ (0..^𝑝)))
366365rspccva 3308 . . . . 5 ((∀𝑘 ∈ ℕ ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ 𝑝 ∈ ℕ) → ran (1st ‘(𝑔𝑝)) ⊆ (0..^𝑝))
367360, 366sylan 488 . . . 4 ((((𝜑𝑔:ℕ⟶((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) ∧ 𝑝 ∈ ℕ) → ran (1st ‘(𝑔𝑝)) ⊆ (0..^𝑝))
368 simpll 790 . . . . . 6 (((𝜑𝑔:ℕ⟶((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) → 𝜑)
369 poimir.2 . . . . . 6 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧𝐼 ∧ (𝑧𝑛) = 0)) → ((𝐹𝑧)‘𝑛) ≤ 0)
370368, 369sylan 488 . . . . 5 ((((𝜑𝑔:ℕ⟶((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧𝐼 ∧ (𝑧𝑛) = 0)) → ((𝐹𝑧)‘𝑛) ≤ 0)
371 eqid 2622 . . . . 5 ((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) = ((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))
372 simpr 477 . . . . . . . 8 ((ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) → ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))
373372ralimi 2952 . . . . . . 7 (∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) → ∀𝑘 ∈ ℕ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))
374373adantl 482 . . . . . 6 (((𝜑𝑔:ℕ⟶((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) → ∀𝑘 ∈ ℕ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))
375361fveq2d 6195 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 𝑝 → (2nd ‘(𝑔𝑘)) = (2nd ‘(𝑔𝑝)))
376375imaeq1d 5465 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑝 → ((2nd ‘(𝑔𝑘)) “ (1...𝑗)) = ((2nd ‘(𝑔𝑝)) “ (1...𝑗)))
377376xpeq1d 5138 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑝 → (((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) = (((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}))
378375imaeq1d 5465 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑝 → ((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)))
379378xpeq1d 5138 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑝 → (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))
380377, 379uneq12d 3768 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑝 → ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))
381362, 380oveq12d 6668 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑝 → ((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))))
382 sneq 4187 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑝 → {𝑘} = {𝑝})
383382xpeq2d 5139 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑝 → ((1...𝑁) × {𝑘}) = ((1...𝑁) × {𝑝}))
384381, 383oveq12d 6668 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑝 → (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})) = (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))
385384fveq2d 6195 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑝 → (𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘}))) = (𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝}))))
386385fveq1d 6193 . . . . . . . . . . . . . . 15 (𝑘 = 𝑝 → ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) = ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏))
387386breq2d 4665 . . . . . . . . . . . . . 14 (𝑘 = 𝑝 → (0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ↔ 0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏)))
388381fveq1d 6193 . . . . . . . . . . . . . . 15 (𝑘 = 𝑝 → (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) = (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏))
389388neeq1d 2853 . . . . . . . . . . . . . 14 (𝑘 = 𝑝 → ((((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0 ↔ (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0))
390387, 389anbi12d 747 . . . . . . . . . . . . 13 (𝑘 = 𝑝 → ((0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0) ↔ (0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)))
391390ralbidv 2986 . . . . . . . . . . . 12 (𝑘 = 𝑝 → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)))
392391rabbidv 3189 . . . . . . . . . . 11 (𝑘 = 𝑝 → {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)} = {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)})
393392uneq2d 3767 . . . . . . . . . 10 (𝑘 = 𝑝 → ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}) = ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}))
394393supeq1d 8352 . . . . . . . . 9 (𝑘 = 𝑝 → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))
395394eqeq2d 2632 . . . . . . . 8 (𝑘 = 𝑝 → (𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) ↔ 𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))
396395rexbidv 3052 . . . . . . 7 (𝑘 = 𝑝 → (∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) ↔ ∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))
397 eqeq1 2626 . . . . . . . . 9 (𝑖 = 𝑞 → (𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) ↔ 𝑞 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))
398397rexbidv 3052 . . . . . . . 8 (𝑖 = 𝑞 → (∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) ↔ ∃𝑗 ∈ (0...𝑁)𝑞 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))
399 oveq2 6658 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑚 → (1...𝑗) = (1...𝑚))
400399imaeq2d 5466 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑚 → ((2nd ‘(𝑔𝑝)) “ (1...𝑗)) = ((2nd ‘(𝑔𝑝)) “ (1...𝑚)))
401400xpeq1d 5138 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑚 → (((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) = (((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}))
402 oveq1 6657 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = 𝑚 → (𝑗 + 1) = (𝑚 + 1))
403402oveq1d 6665 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑚 → ((𝑗 + 1)...𝑁) = ((𝑚 + 1)...𝑁))
404403imaeq2d 5466 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑚 → ((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)))
405404xpeq1d 5138 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑚 → (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))
406401, 405uneq12d 3768 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑚 → ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))
407406oveq2d 6666 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑚 → ((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))))
408407oveq1d 6665 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑚 → (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})) = (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))
409408fveq2d 6195 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑚 → (𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝}))) = (𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝}))))
410409fveq1d 6193 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑚 → ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏) = ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏))
411410breq2d 4665 . . . . . . . . . . . . . . 15 (𝑗 = 𝑚 → (0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏) ↔ 0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏)))
412407fveq1d 6193 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑚 → (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) = (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏))
413412neeq1d 2853 . . . . . . . . . . . . . . 15 (𝑗 = 𝑚 → ((((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0 ↔ (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0))
414411, 413anbi12d 747 . . . . . . . . . . . . . 14 (𝑗 = 𝑚 → ((0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0) ↔ (0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)))
415414ralbidv 2986 . . . . . . . . . . . . 13 (𝑗 = 𝑚 → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)))
416415rabbidv 3189 . . . . . . . . . . . 12 (𝑗 = 𝑚 → {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)} = {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)})
417416uneq2d 3767 . . . . . . . . . . 11 (𝑗 = 𝑚 → ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}) = ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}))
418417supeq1d 8352 . . . . . . . . . 10 (𝑗 = 𝑚 → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))
419418eqeq2d 2632 . . . . . . . . 9 (𝑗 = 𝑚 → (𝑞 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) ↔ 𝑞 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))
420419cbvrexv 3172 . . . . . . . 8 (∃𝑗 ∈ (0...𝑁)𝑞 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) ↔ ∃𝑚 ∈ (0...𝑁)𝑞 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))
421398, 420syl6bb 276 . . . . . . 7 (𝑖 = 𝑞 → (∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) ↔ ∃𝑚 ∈ (0...𝑁)𝑞 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))
422396, 421rspc2v 3322 . . . . . 6 ((𝑝 ∈ ℕ ∧ 𝑞 ∈ (0...𝑁)) → (∀𝑘 ∈ ℕ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) → ∃𝑚 ∈ (0...𝑁)𝑞 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))
423374, 422mpan9 486 . . . . 5 ((((𝜑𝑔:ℕ⟶((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ (0...𝑁))) → ∃𝑚 ∈ (0...𝑁)𝑞 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))
424352, 142, 353, 355, 370, 371, 357, 367, 423poimirlem31 33440 . . . 4 ((((𝜑𝑔:ℕ⟶((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) ∧ (𝑝 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ≤ })) → ∃𝑚 ∈ (0...𝑁)0𝑟((𝐹‘(((1st ‘(𝑔𝑝)) ∘𝑓 + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑝})))‘𝑛))
425352, 142, 353, 355, 356, 357, 367, 424poimirlem30 33439 . . 3 (((𝜑𝑔:ℕ⟶((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) → ∃𝑐𝐼𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
426425anasss 679 . 2 ((𝜑 ∧ (𝑔:ℕ⟶((ℕ0𝑚 (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘𝑓 / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘𝑓 + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))) → ∃𝑐𝐼𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
427351, 426exlimddv 1863 1 (𝜑 → ∃𝑐𝐼𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  w3a 1037   = wceq 1483  wex 1704  wcel 1990  {cab 2608  wne 2794  wral 2912  wrex 2913  {crab 2916  Vcvv 3200  cun 3572  wss 3574  c0 3915  {csn 4177  {cpr 4179   ciun 4520   class class class wbr 4653   Or wor 5034   × cxp 5112  ccnv 5113  dom cdm 5114  ran crn 5115  cima 5117  Oncon0 5723   Fn wfn 5883  wf 5884  1-1-ontowf1o 5887  cfv 5888  (class class class)co 6650  𝑓 cof 6895  ωcom 7065  1st c1st 7166  2nd c2nd 7167  𝑚 cmap 7857  Xcixp 7908  cen 7952  Fincfn 7955  supcsup 8346  cardccrd 8761  cc 9934  cr 9935  0cc0 9936  1c1 9937   + caddc 9939   · cmul 9941   < clt 10074  cle 10075  cmin 10266   / cdiv 10684  cn 11020  0cn0 11292  cz 11377  cuz 11687  +crp 11832  (,)cioo 12175  [,]cicc 12178  ...cfz 12326  ..^cfzo 12465  t crest 16081  topGenctg 16098  tcpt 16099   Cn ccn 21028
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-disj 4621  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-omul 7565  df-er 7742  df-map 7859  df-pm 7860  df-ixp 7909  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fi 8317  df-sup 8348  df-inf 8349  df-oi 8415  df-card 8765  df-acn 8768  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-n0 11293  df-xnn0 11364  df-z 11378  df-uz 11688  df-q 11789  df-rp 11833  df-xneg 11946  df-xadd 11947  df-xmul 11948  df-ioo 12179  df-icc 12182  df-fz 12327  df-fzo 12466  df-fl 12593  df-seq 12802  df-exp 12861  df-fac 13061  df-bc 13090  df-hash 13118  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-clim 14219  df-sum 14417  df-dvds 14984  df-rest 16083  df-topgen 16104  df-pt 16105  df-psmet 19738  df-xmet 19739  df-met 19740  df-bl 19741  df-mopn 19742  df-top 20699  df-topon 20716  df-bases 20750  df-cld 20823  df-ntr 20824  df-cls 20825  df-lp 20940  df-cn 21031  df-cnp 21032  df-t1 21118  df-haus 21119  df-cmp 21190  df-tx 21365  df-hmeo 21558  df-hmph 21559  df-ii 22680
This theorem is referenced by:  poimir  33442
  Copyright terms: Public domain W3C validator