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 37622
Description: Lemma for poimir 37623, combining poimirlem28 37618, poimirlem30 37620, and poimirlem31 37621 to get Equation (1) of [Kulpa] p. 547. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0 (𝜑𝑁 ∈ ℕ)
poimir.i 𝐼 = ((0[,]1) ↑m (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 480 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 𝑁 ∈ ℕ)
3 fvoveq1 7426 . . . . . . . . . . . . 13 (𝑝 = ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝐹‘(𝑝f / ((1...𝑁) × {𝑘}))) = (𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))))
43fveq1d 6877 . . . . . . . . . . . 12 (𝑝 = ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) = ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏))
54breq2d 5131 . . . . . . . . . . 11 (𝑝 = ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ↔ 0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏)))
6 fveq1 6874 . . . . . . . . . . . 12 (𝑝 = ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝑝𝑏) = (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏))
76neeq1d 2991 . . . . . . . . . . 11 (𝑝 = ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → ((𝑝𝑏) ≠ 0 ↔ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0))
85, 7anbi12d 632 . . . . . . . . . 10 (𝑝 = ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → ((0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ (0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)))
98ralbidv 3163 . . . . . . . . 9 (𝑝 = ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)))
109rabbidv 3423 . . . . . . . 8 (𝑝 = ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} = {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)})
1110uneq2d 4143 . . . . . . 7 (𝑝 = ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) = ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}))
1211supeq1d 9456 . . . . . 6 (𝑝 = ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))
131nnnn0d 12560 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℕ0)
14 0elfz 13639 . . . . . . . . . . 11 (𝑁 ∈ ℕ0 → 0 ∈ (0...𝑁))
1513, 14syl 17 . . . . . . . . . 10 (𝜑 → 0 ∈ (0...𝑁))
1615snssd 4785 . . . . . . . . 9 (𝜑 → {0} ⊆ (0...𝑁))
17 ssrab2 4055 . . . . . . . . . . 11 {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ⊆ (1...𝑁)
18 fz1ssfz0 13638 . . . . . . . . . . 11 (1...𝑁) ⊆ (0...𝑁)
1917, 18sstri 3968 . . . . . . . . . 10 {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ⊆ (0...𝑁)
2019a1i 11 . . . . . . . . 9 (𝜑 → {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ⊆ (0...𝑁))
2116, 20unssd 4167 . . . . . . . 8 (𝜑 → ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ⊆ (0...𝑁))
22 ltso 11313 . . . . . . . . 9 < Or ℝ
23 snfi 9055 . . . . . . . . . . 11 {0} ∈ Fin
24 fzfi 13988 . . . . . . . . . . . 12 (1...𝑁) ∈ Fin
25 rabfi 9273 . . . . . . . . . . . 12 ((1...𝑁) ∈ Fin → {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ∈ Fin)
2624, 25ax-mp 5 . . . . . . . . . . 11 {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ∈ Fin
27 unfi 9183 . . . . . . . . . . 11 (({0} ∈ Fin ∧ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ∈ Fin) → ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ∈ Fin)
2823, 26, 27mp2an 692 . . . . . . . . . 10 ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ∈ Fin
29 c0ex 11227 . . . . . . . . . . . 12 0 ∈ V
3029snid 4638 . . . . . . . . . . 11 0 ∈ {0}
31 elun1 4157 . . . . . . . . . . 11 (0 ∈ {0} → 0 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}))
32 ne0i 4316 . . . . . . . . . . 11 (0 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ≠ ∅)
3330, 31, 32mp2b 10 . . . . . . . . . 10 ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ≠ ∅
34 0red 11236 . . . . . . . . . . . . 13 ((𝜑𝑁 ∈ ℕ) → 0 ∈ ℝ)
3534snssd 4785 . . . . . . . . . . . 12 ((𝜑𝑁 ∈ ℕ) → {0} ⊆ ℝ)
361, 35ax-mp 5 . . . . . . . . . . 11 {0} ⊆ ℝ
37 elfzelz 13539 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℤ)
3837ssriv 3962 . . . . . . . . . . . . 13 (1...𝑁) ⊆ ℤ
39 zssre 12593 . . . . . . . . . . . . 13 ℤ ⊆ ℝ
4038, 39sstri 3968 . . . . . . . . . . . 12 (1...𝑁) ⊆ ℝ
4117, 40sstri 3968 . . . . . . . . . . 11 {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ⊆ ℝ
4236, 41unssi 4166 . . . . . . . . . 10 ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ⊆ ℝ
4328, 33, 423pm3.2i 1340 . . . . . . . . 9 (({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ∈ Fin ∧ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ≠ ∅ ∧ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ⊆ ℝ)
44 fisupcl 9480 . . . . . . . . 9 (( < Or ℝ ∧ (({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ∈ Fin ∧ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ≠ ∅ ∧ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ⊆ ℝ)) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}))
4522, 43, 44mp2an 692 . . . . . . . 8 sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})
46 ssel 3952 . . . . . . . 8 (({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ⊆ (0...𝑁) → (sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ∈ (0...𝑁)))
4721, 45, 46mpisyl 21 . . . . . . 7 (𝜑 → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ∈ (0...𝑁))
4847ad2antrr 726 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑝:(1...𝑁)⟶(0...𝑘)) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ∈ (0...𝑁))
49 elfznn 13568 . . . . . . . . 9 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ)
50 nngt0 12269 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → 0 < 𝑛)
5150adantr 480 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) → 0 < 𝑛)
52 simpr 484 . . . . . . . . . . . . . 14 ((0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → (𝑝𝑏) ≠ 0)
5352ralimi 3073 . . . . . . . . . . . . 13 (∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑠)(𝑝𝑏) ≠ 0)
54 elfznn 13568 . . . . . . . . . . . . . 14 (𝑠 ∈ (1...𝑁) → 𝑠 ∈ ℕ)
55 nnre 12245 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
56 nnre 12245 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ℕ → 𝑠 ∈ ℝ)
57 lenlt 11311 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℝ ∧ 𝑠 ∈ ℝ) → (𝑛𝑠 ↔ ¬ 𝑠 < 𝑛))
5855, 56, 57syl2an 596 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ) → (𝑛𝑠 ↔ ¬ 𝑠 < 𝑛))
59 elfz1b 13608 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ (1...𝑠) ↔ (𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ ∧ 𝑛𝑠))
6059biimpri 228 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ ∧ 𝑛𝑠) → 𝑛 ∈ (1...𝑠))
61603expia 1121 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ) → (𝑛𝑠𝑛 ∈ (1...𝑠)))
6258, 61sylbird 260 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ) → (¬ 𝑠 < 𝑛𝑛 ∈ (1...𝑠)))
63 fveq2 6875 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = 𝑛 → (𝑝𝑏) = (𝑝𝑛))
6463eqeq1d 2737 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = 𝑛 → ((𝑝𝑏) = 0 ↔ (𝑝𝑛) = 0))
6564rspcev 3601 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ (1...𝑠) ∧ (𝑝𝑛) = 0) → ∃𝑏 ∈ (1...𝑠)(𝑝𝑏) = 0)
6665expcom 413 . . . . . . . . . . . . . . . . . 18 ((𝑝𝑛) = 0 → (𝑛 ∈ (1...𝑠) → ∃𝑏 ∈ (1...𝑠)(𝑝𝑏) = 0))
6762, 66sylan9 507 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ) ∧ (𝑝𝑛) = 0) → (¬ 𝑠 < 𝑛 → ∃𝑏 ∈ (1...𝑠)(𝑝𝑏) = 0))
6867an32s 652 . . . . . . . . . . . . . . . 16 (((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) ∧ 𝑠 ∈ ℕ) → (¬ 𝑠 < 𝑛 → ∃𝑏 ∈ (1...𝑠)(𝑝𝑏) = 0))
69 nne 2936 . . . . . . . . . . . . . . . . . 18 (¬ (𝑝𝑏) ≠ 0 ↔ (𝑝𝑏) = 0)
7069rexbii 3083 . . . . . . . . . . . . . . . . 17 (∃𝑏 ∈ (1...𝑠) ¬ (𝑝𝑏) ≠ 0 ↔ ∃𝑏 ∈ (1...𝑠)(𝑝𝑏) = 0)
71 rexnal 3089 . . . . . . . . . . . . . . . . 17 (∃𝑏 ∈ (1...𝑠) ¬ (𝑝𝑏) ≠ 0 ↔ ¬ ∀𝑏 ∈ (1...𝑠)(𝑝𝑏) ≠ 0)
7270, 71bitr3i 277 . . . . . . . . . . . . . . . 16 (∃𝑏 ∈ (1...𝑠)(𝑝𝑏) = 0 ↔ ¬ ∀𝑏 ∈ (1...𝑠)(𝑝𝑏) ≠ 0)
7368, 72imbitrdi 251 . . . . . . . . . . . . . . 15 (((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) ∧ 𝑠 ∈ ℕ) → (¬ 𝑠 < 𝑛 → ¬ ∀𝑏 ∈ (1...𝑠)(𝑝𝑏) ≠ 0))
7473con4d 115 . . . . . . . . . . . . . 14 (((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) ∧ 𝑠 ∈ ℕ) → (∀𝑏 ∈ (1...𝑠)(𝑝𝑏) ≠ 0 → 𝑠 < 𝑛))
7554, 74sylan2 593 . . . . . . . . . . . . 13 (((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) ∧ 𝑠 ∈ (1...𝑁)) → (∀𝑏 ∈ (1...𝑠)(𝑝𝑏) ≠ 0 → 𝑠 < 𝑛))
7653, 75syl5 34 . . . . . . . . . . . 12 (((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) ∧ 𝑠 ∈ (1...𝑁)) → (∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → 𝑠 < 𝑛))
7776ralrimiva 3132 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) → ∀𝑠 ∈ (1...𝑁)(∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → 𝑠 < 𝑛))
78 ralunb 4172 . . . . . . . . . . . 12 (∀𝑠 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})𝑠 < 𝑛 ↔ (∀𝑠 ∈ {0}𝑠 < 𝑛 ∧ ∀𝑠 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}𝑠 < 𝑛))
79 breq1 5122 . . . . . . . . . . . . . 14 (𝑠 = 0 → (𝑠 < 𝑛 ↔ 0 < 𝑛))
8029, 79ralsn 4657 . . . . . . . . . . . . 13 (∀𝑠 ∈ {0}𝑠 < 𝑛 ↔ 0 < 𝑛)
81 oveq2 7411 . . . . . . . . . . . . . . 15 (𝑎 = 𝑠 → (1...𝑎) = (1...𝑠))
8281raleqdv 3305 . . . . . . . . . . . . . 14 (𝑎 = 𝑠 → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
8382ralrab 3677 . . . . . . . . . . . . 13 (∀𝑠 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}𝑠 < 𝑛 ↔ ∀𝑠 ∈ (1...𝑁)(∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → 𝑠 < 𝑛))
8480, 83anbi12i 628 . . . . . . . . . . . 12 ((∀𝑠 ∈ {0}𝑠 < 𝑛 ∧ ∀𝑠 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}𝑠 < 𝑛) ↔ (0 < 𝑛 ∧ ∀𝑠 ∈ (1...𝑁)(∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → 𝑠 < 𝑛)))
8578, 84bitri 275 . . . . . . . . . . 11 (∀𝑠 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})𝑠 < 𝑛 ↔ (0 < 𝑛 ∧ ∀𝑠 ∈ (1...𝑁)(∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → 𝑠 < 𝑛)))
8651, 77, 85sylanbrc 583 . . . . . . . . . 10 ((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) → ∀𝑠 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})𝑠 < 𝑛)
87 breq1 5122 . . . . . . . . . . 11 (𝑠 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) → (𝑠 < 𝑛 ↔ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < 𝑛))
8887rspcva 3599 . . . . . . . . . 10 ((sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ∧ ∀𝑠 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})𝑠 < 𝑛) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < 𝑛)
8945, 86, 88sylancr 587 . . . . . . . . 9 ((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < 𝑛)
9049, 89sylan 580 . . . . . . . 8 ((𝑛 ∈ (1...𝑁) ∧ (𝑝𝑛) = 0) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < 𝑛)
91903adant2 1131 . . . . . . 7 ((𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 0) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < 𝑛)
9291adantl 481 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 0)) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < 𝑛)
9337zred 12695 . . . . . . . . . . 11 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℝ)
94933ad2ant1 1133 . . . . . . . . . 10 ((𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) → 𝑛 ∈ ℝ)
9594adantl 481 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → 𝑛 ∈ ℝ)
96 simpr1 1195 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → 𝑛 ∈ (1...𝑁))
97 simpll 766 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → 𝜑)
98 simplr 768 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → 𝑘 ∈ ℕ)
99 elfzelz 13539 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ (0...𝑘) → 𝑖 ∈ ℤ)
10099zred 12695 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ (0...𝑘) → 𝑖 ∈ ℝ)
101 nndivre 12279 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ ℝ)
102100, 101sylan 580 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ ℝ)
103 elfzle1 13542 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ (0...𝑘) → 0 ≤ 𝑖)
104100, 103jca 511 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ (0...𝑘) → (𝑖 ∈ ℝ ∧ 0 ≤ 𝑖))
105 nnrp 13018 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
106105rpregt0d 13055 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ ℕ → (𝑘 ∈ ℝ ∧ 0 < 𝑘))
107 divge0 12109 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑖 ∈ ℝ ∧ 0 ≤ 𝑖) ∧ (𝑘 ∈ ℝ ∧ 0 < 𝑘)) → 0 ≤ (𝑖 / 𝑘))
108104, 106, 107syl2an 596 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝑖 / 𝑘))
109 elfzle2 13543 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ (0...𝑘) → 𝑖𝑘)
110109adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑖𝑘)
111100adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑖 ∈ ℝ)
112 1red 11234 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 1 ∈ ℝ)
113105adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ+)
114111, 112, 113ledivmuld 13102 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑖 / 𝑘) ≤ 1 ↔ 𝑖 ≤ (𝑘 · 1)))
115 nncn 12246 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
116115mulridd 11250 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ ℕ → (𝑘 · 1) = 𝑘)
117116breq2d 5131 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ ℕ → (𝑖 ≤ (𝑘 · 1) ↔ 𝑖𝑘))
118117adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 ≤ (𝑘 · 1) ↔ 𝑖𝑘))
119114, 118bitrd 279 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑖 / 𝑘) ≤ 1 ↔ 𝑖𝑘))
120110, 119mpbird 257 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ≤ 1)
121 elicc01 13481 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖 / 𝑘) ∈ (0[,]1) ↔ ((𝑖 / 𝑘) ∈ ℝ ∧ 0 ≤ (𝑖 / 𝑘) ∧ (𝑖 / 𝑘) ≤ 1))
122102, 108, 120, 121syl3anbrc 1344 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ (0[,]1))
123122ancoms 458 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑘)) → (𝑖 / 𝑘) ∈ (0[,]1))
124 elsni 4618 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ {𝑘} → 𝑗 = 𝑘)
125124oveq2d 7419 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ {𝑘} → (𝑖 / 𝑗) = (𝑖 / 𝑘))
126125eleq1d 2819 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ {𝑘} → ((𝑖 / 𝑗) ∈ (0[,]1) ↔ (𝑖 / 𝑘) ∈ (0[,]1)))
127123, 126syl5ibrcom 247 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑘)) → (𝑗 ∈ {𝑘} → (𝑖 / 𝑗) ∈ (0[,]1)))
128127impr 454 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ ∧ (𝑖 ∈ (0...𝑘) ∧ 𝑗 ∈ {𝑘})) → (𝑖 / 𝑗) ∈ (0[,]1))
12998, 128sylan 580 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) ∧ (𝑖 ∈ (0...𝑘) ∧ 𝑗 ∈ {𝑘})) → (𝑖 / 𝑗) ∈ (0[,]1))
130 simprr 772 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → 𝑝:(1...𝑁)⟶(0...𝑘))
131 vex 3463 . . . . . . . . . . . . . . . . . 18 𝑘 ∈ V
132131fconst 6763 . . . . . . . . . . . . . . . . 17 ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘}
133132a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘})
134 fzfid 13989 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → (1...𝑁) ∈ Fin)
135 inidm 4202 . . . . . . . . . . . . . . . 16 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
136129, 130, 133, 134, 134, 135off 7687 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → (𝑝f / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
137 poimir.i . . . . . . . . . . . . . . . . 17 𝐼 = ((0[,]1) ↑m (1...𝑁))
138137eleq2i 2826 . . . . . . . . . . . . . . . 16 ((𝑝f / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ (𝑝f / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑m (1...𝑁)))
139 ovex 7436 . . . . . . . . . . . . . . . . 17 (0[,]1) ∈ V
140 ovex 7436 . . . . . . . . . . . . . . . . 17 (1...𝑁) ∈ V
141139, 140elmap 8883 . . . . . . . . . . . . . . . 16 ((𝑝f / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑m (1...𝑁)) ↔ (𝑝f / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
142138, 141bitri 275 . . . . . . . . . . . . . . 15 ((𝑝f / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ (𝑝f / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
143136, 142sylibr 234 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → (𝑝f / ((1...𝑁) × {𝑘})) ∈ 𝐼)
1441433adantr3 1172 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → (𝑝f / ((1...𝑁) × {𝑘})) ∈ 𝐼)
145 3anass 1094 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) ↔ (𝑛 ∈ (1...𝑁) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)))
146 ancom 460 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (1...𝑁) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) ↔ ((𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) ∧ 𝑛 ∈ (1...𝑁)))
147145, 146bitri 275 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) ↔ ((𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) ∧ 𝑛 ∈ (1...𝑁)))
148 ffn 6705 . . . . . . . . . . . . . . . . . 18 (𝑝:(1...𝑁)⟶(0...𝑘) → 𝑝 Fn (1...𝑁))
149148ad2antrl 728 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → 𝑝 Fn (1...𝑁))
150 fnconstg 6765 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ V → ((1...𝑁) × {𝑘}) Fn (1...𝑁))
151131, 150mp1i 13 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ((1...𝑁) × {𝑘}) Fn (1...𝑁))
152 fzfid 13989 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → (1...𝑁) ∈ Fin)
153 simplrr 777 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑝𝑛) = 𝑘)
154131fvconst2 7195 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {𝑘})‘𝑛) = 𝑘)
155154adantl 481 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {𝑘})‘𝑛) = 𝑘)
156149, 151, 152, 152, 135, 153, 155ofval 7680 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = (𝑘 / 𝑘))
157156anasss 466 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ) ∧ ((𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) ∧ 𝑛 ∈ (1...𝑁))) → ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = (𝑘 / 𝑘))
158147, 157sylan2b 594 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = (𝑘 / 𝑘))
159 nnne0 12272 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ → 𝑘 ≠ 0)
160115, 159dividd 12013 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ → (𝑘 / 𝑘) = 1)
161160ad2antlr 727 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → (𝑘 / 𝑘) = 1)
162158, 161eqtrd 2770 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = 1)
163 ovex 7436 . . . . . . . . . . . . . 14 (𝑝f / ((1...𝑁) × {𝑘})) ∈ V
164 eleq1 2822 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → (𝑧𝐼 ↔ (𝑝f / ((1...𝑁) × {𝑘})) ∈ 𝐼))
165 fveq1 6874 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → (𝑧𝑛) = ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛))
166165eqeq1d 2737 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → ((𝑧𝑛) = 1 ↔ ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = 1))
167164, 1663anbi23d 1441 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → ((𝑛 ∈ (1...𝑁) ∧ 𝑧𝐼 ∧ (𝑧𝑛) = 1) ↔ (𝑛 ∈ (1...𝑁) ∧ (𝑝f / ((1...𝑁) × {𝑘})) ∈ 𝐼 ∧ ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = 1)))
168167anbi2d 630 . . . . . . . . . . . . . . 15 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧𝐼 ∧ (𝑧𝑛) = 1)) ↔ (𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ (𝑝f / ((1...𝑁) × {𝑘})) ∈ 𝐼 ∧ ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = 1))))
169 fveq2 6875 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → (𝐹𝑧) = (𝐹‘(𝑝f / ((1...𝑁) × {𝑘}))))
170169fveq1d 6877 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → ((𝐹𝑧)‘𝑛) = ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛))
171170breq2d 5131 . . . . . . . . . . . . . . 15 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → (0 ≤ ((𝐹𝑧)‘𝑛) ↔ 0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛)))
172168, 171imbi12d 344 . . . . . . . . . . . . . 14 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → (((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧𝐼 ∧ (𝑧𝑛) = 1)) → 0 ≤ ((𝐹𝑧)‘𝑛)) ↔ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ (𝑝f / ((1...𝑁) × {𝑘})) ∈ 𝐼 ∧ ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = 1)) → 0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛))))
173 poimir.3 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧𝐼 ∧ (𝑧𝑛) = 1)) → 0 ≤ ((𝐹𝑧)‘𝑛))
174163, 172, 173vtocl 3537 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ (𝑝f / ((1...𝑁) × {𝑘})) ∈ 𝐼 ∧ ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = 1)) → 0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛))
17597, 96, 144, 162, 174syl13anc 1374 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → 0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛))
176 simpr 484 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
177 simp3 1138 . . . . . . . . . . . . 13 ((𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) → (𝑝𝑛) = 𝑘)
178 neeq1 2994 . . . . . . . . . . . . . . 15 ((𝑝𝑛) = 𝑘 → ((𝑝𝑛) ≠ 0 ↔ 𝑘 ≠ 0))
179159, 178syl5ibrcom 247 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → ((𝑝𝑛) = 𝑘 → (𝑝𝑛) ≠ 0))
180179imp 406 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ∧ (𝑝𝑛) = 𝑘) → (𝑝𝑛) ≠ 0)
181176, 177, 180syl2an 596 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → (𝑝𝑛) ≠ 0)
182 vex 3463 . . . . . . . . . . . . 13 𝑛 ∈ V
183 fveq2 6875 . . . . . . . . . . . . . . 15 (𝑏 = 𝑛 → ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) = ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛))
184183breq2d 5131 . . . . . . . . . . . . . 14 (𝑏 = 𝑛 → (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ↔ 0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛)))
18563neeq1d 2991 . . . . . . . . . . . . . 14 (𝑏 = 𝑛 → ((𝑝𝑏) ≠ 0 ↔ (𝑝𝑛) ≠ 0))
186184, 185anbi12d 632 . . . . . . . . . . . . 13 (𝑏 = 𝑛 → ((0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛) ∧ (𝑝𝑛) ≠ 0)))
187182, 186ralsn 4657 . . . . . . . . . . . 12 (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛) ∧ (𝑝𝑛) ≠ 0))
188175, 181, 187sylanbrc 583 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))
18937zcnd 12696 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ)
190 1cnd 11228 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...𝑁) → 1 ∈ ℂ)
191189, 190subeq0ad 11602 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) = 0 ↔ 𝑛 = 1))
192191biimpcd 249 . . . . . . . . . . . . . . . . 17 ((𝑛 − 1) = 0 → (𝑛 ∈ (1...𝑁) → 𝑛 = 1))
193 1z 12620 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℤ
194 fzsn 13581 . . . . . . . . . . . . . . . . . . . . 21 (1 ∈ ℤ → (1...1) = {1})
195193, 194ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (1...1) = {1}
196 oveq2 7411 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 1 → (1...𝑛) = (1...1))
197 sneq 4611 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 1 → {𝑛} = {1})
198195, 196, 1973eqtr4a 2796 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 1 → (1...𝑛) = {𝑛})
199198raleqdv 3305 . . . . . . . . . . . . . . . . . 18 (𝑛 = 1 → (∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
200199biimprd 248 . . . . . . . . . . . . . . . . 17 (𝑛 = 1 → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
201192, 200syl6 35 . . . . . . . . . . . . . . . 16 ((𝑛 − 1) = 0 → (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
202 ralun 4173 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)) → ∀𝑏 ∈ ((1...(𝑛 − 1)) ∪ {𝑛})(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))
203 npcan1 11660 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ℂ → ((𝑛 − 1) + 1) = 𝑛)
204189, 203syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) + 1) = 𝑛)
205 elfzuz 13535 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ (ℤ‘1))
206204, 205eqeltrd 2834 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) + 1) ∈ (ℤ‘1))
207 peano2zm 12633 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ℤ → (𝑛 − 1) ∈ ℤ)
208 uzid 12865 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 − 1) ∈ ℤ → (𝑛 − 1) ∈ (ℤ‘(𝑛 − 1)))
209 peano2uz 12915 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 − 1) ∈ (ℤ‘(𝑛 − 1)) → ((𝑛 − 1) + 1) ∈ (ℤ‘(𝑛 − 1)))
21037, 207, 208, 2094syl 19 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) + 1) ∈ (ℤ‘(𝑛 − 1)))
211204, 210eqeltrrd 2835 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ (ℤ‘(𝑛 − 1)))
212 fzsplit2 13564 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑛 − 1) + 1) ∈ (ℤ‘1) ∧ 𝑛 ∈ (ℤ‘(𝑛 − 1))) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)))
213206, 211, 212syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (1...𝑁) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)))
214204oveq1d 7418 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...𝑁) → (((𝑛 − 1) + 1)...𝑛) = (𝑛...𝑛))
215 fzsn 13581 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ℤ → (𝑛...𝑛) = {𝑛})
21637, 215syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...𝑁) → (𝑛...𝑛) = {𝑛})
217214, 216eqtrd 2770 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (1...𝑁) → (((𝑛 − 1) + 1)...𝑛) = {𝑛})
218217uneq2d 4143 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (1...𝑁) → ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)) = ((1...(𝑛 − 1)) ∪ {𝑛}))
219213, 218eqtrd 2770 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ (1...𝑁) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ {𝑛}))
220219raleqdv 3305 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ ∀𝑏 ∈ ((1...(𝑛 − 1)) ∪ {𝑛})(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
221202, 220imbitrrid 246 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...𝑁) → ((∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
222221expd 415 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
223222com12 32 . . . . . . . . . . . . . . . . 17 (∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
224223adantl 481 . . . . . . . . . . . . . . . 16 (((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)) → (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
225201, 224jaoi 857 . . . . . . . . . . . . . . 15 (((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))) → (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
226225imdistand 570 . . . . . . . . . . . . . 14 (((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))) → ((𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)) → (𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
227226com12 32 . . . . . . . . . . . . 13 ((𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)) → (((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))) → (𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
228 elun 4128 . . . . . . . . . . . . . 14 ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ↔ ((𝑛 − 1) ∈ {0} ∨ (𝑛 − 1) ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}))
229 ovex 7436 . . . . . . . . . . . . . . . 16 (𝑛 − 1) ∈ V
230229elsn 4616 . . . . . . . . . . . . . . 15 ((𝑛 − 1) ∈ {0} ↔ (𝑛 − 1) = 0)
231 oveq2 7411 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑛 − 1) → (1...𝑎) = (1...(𝑛 − 1)))
232231raleqdv 3305 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑛 − 1) → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
233232elrab 3671 . . . . . . . . . . . . . . 15 ((𝑛 − 1) ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ↔ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
234230, 233orbi12i 914 . . . . . . . . . . . . . 14 (((𝑛 − 1) ∈ {0} ∨ (𝑛 − 1) ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ↔ ((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
235228, 234bitri 275 . . . . . . . . . . . . 13 ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ↔ ((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
236 oveq2 7411 . . . . . . . . . . . . . . 15 (𝑎 = 𝑛 → (1...𝑎) = (1...𝑛))
237236raleqdv 3305 . . . . . . . . . . . . . 14 (𝑎 = 𝑛 → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
238237elrab 3671 . . . . . . . . . . . . 13 (𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ↔ (𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
239227, 235, 2383imtr4g 296 . . . . . . . . . . . 12 ((𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)) → ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → 𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}))
240 elun2 4158 . . . . . . . . . . . 12 (𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} → 𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}))
241239, 240syl6 35 . . . . . . . . . . 11 ((𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)) → ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → 𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})))
24296, 188, 241syl2anc 584 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → 𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})))
243 fimaxre2 12185 . . . . . . . . . . . . 13 ((({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ⊆ ℝ ∧ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ∈ Fin) → ∃𝑖 ∈ ℝ ∀𝑗 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})𝑗𝑖)
24442, 28, 243mp2an 692 . . . . . . . . . . . 12 𝑖 ∈ ℝ ∀𝑗 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})𝑗𝑖
24542, 33, 2443pm3.2i 1340 . . . . . . . . . . 11 (({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ⊆ ℝ ∧ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ≠ ∅ ∧ ∃𝑖 ∈ ℝ ∀𝑗 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})𝑗𝑖)
246245suprubii 12215 . . . . . . . . . 10 (𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → 𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ))
247242, 246syl6 35 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → 𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )))
248 ltm1 12081 . . . . . . . . . 10 (𝑛 ∈ ℝ → (𝑛 − 1) < 𝑛)
249 peano2rem 11548 . . . . . . . . . . 11 (𝑛 ∈ ℝ → (𝑛 − 1) ∈ ℝ)
25042, 45sselii 3955 . . . . . . . . . . . 12 sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ∈ ℝ
251 ltletr 11325 . . . . . . . . . . . 12 (((𝑛 − 1) ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ∈ ℝ) → (((𝑛 − 1) < 𝑛𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )) → (𝑛 − 1) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )))
252250, 251mp3an3 1452 . . . . . . . . . . 11 (((𝑛 − 1) ∈ ℝ ∧ 𝑛 ∈ ℝ) → (((𝑛 − 1) < 𝑛𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )) → (𝑛 − 1) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )))
253249, 252mpancom 688 . . . . . . . . . 10 (𝑛 ∈ ℝ → (((𝑛 − 1) < 𝑛𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )) → (𝑛 − 1) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )))
254248, 253mpand 695 . . . . . . . . 9 (𝑛 ∈ ℝ → (𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) → (𝑛 − 1) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )))
25595, 247, 254sylsyld 61 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → (𝑛 − 1) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )))
256250ltnri 11342 . . . . . . . . . 10 ¬ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )
257 breq1 5122 . . . . . . . . . 10 (sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) = (𝑛 − 1) → (sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ↔ (𝑛 − 1) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )))
258256, 257mtbii 326 . . . . . . . . 9 (sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) = (𝑛 − 1) → ¬ (𝑛 − 1) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ))
259258necon2ai 2961 . . . . . . . 8 ((𝑛 − 1) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ≠ (𝑛 − 1))
260255, 259syl6 35 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ≠ (𝑛 − 1)))
261 eleq1 2822 . . . . . . . . 9 (sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) = (𝑛 − 1) → (sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ↔ (𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})))
26245, 261mpbii 233 . . . . . . . 8 (sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) = (𝑛 − 1) → (𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}))
263262necon3bi 2958 . . . . . . 7 (¬ (𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ≠ (𝑛 − 1))
264260, 263pm2.61d1 180 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ≠ (𝑛 − 1))
2652, 12, 48, 92, 264, 176poimirlem28 37618 . . . . 5 ((𝜑𝑘 ∈ ℕ) → ∃𝑠 ∈ (((0..^𝑘) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))
266 nn0ex 12505 . . . . . . . . . . . 12 0 ∈ V
267 fzo0ssnn0 13760 . . . . . . . . . . . 12 (0..^𝑘) ⊆ ℕ0
268 mapss 8901 . . . . . . . . . . . 12 ((ℕ0 ∈ V ∧ (0..^𝑘) ⊆ ℕ0) → ((0..^𝑘) ↑m (1...𝑁)) ⊆ (ℕ0m (1...𝑁)))
269266, 267, 268mp2an 692 . . . . . . . . . . 11 ((0..^𝑘) ↑m (1...𝑁)) ⊆ (ℕ0m (1...𝑁))
270 xpss1 5673 . . . . . . . . . . 11 (((0..^𝑘) ↑m (1...𝑁)) ⊆ (ℕ0m (1...𝑁)) → (((0..^𝑘) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ⊆ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
271269, 270ax-mp 5 . . . . . . . . . 10 (((0..^𝑘) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ⊆ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
272271sseli 3954 . . . . . . . . 9 (𝑠 ∈ (((0..^𝑘) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → 𝑠 ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
273 xp1st 8018 . . . . . . . . . 10 (𝑠 ∈ (((0..^𝑘) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st𝑠) ∈ ((0..^𝑘) ↑m (1...𝑁)))
274 elmapi 8861 . . . . . . . . . 10 ((1st𝑠) ∈ ((0..^𝑘) ↑m (1...𝑁)) → (1st𝑠):(1...𝑁)⟶(0..^𝑘))
275 frn 6712 . . . . . . . . . 10 ((1st𝑠):(1...𝑁)⟶(0..^𝑘) → ran (1st𝑠) ⊆ (0..^𝑘))
276273, 274, 2753syl 18 . . . . . . . . 9 (𝑠 ∈ (((0..^𝑘) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → ran (1st𝑠) ⊆ (0..^𝑘))
277272, 276jca 511 . . . . . . . 8 (𝑠 ∈ (((0..^𝑘) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (𝑠 ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ran (1st𝑠) ⊆ (0..^𝑘)))
278277anim1i 615 . . . . . . 7 ((𝑠 ∈ (((0..^𝑘) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) → ((𝑠 ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ran (1st𝑠) ⊆ (0..^𝑘)) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))
279 anass 468 . . . . . . 7 (((𝑠 ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ran (1st𝑠) ⊆ (0..^𝑘)) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) ↔ (𝑠 ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ (ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))))
280278, 279sylib 218 . . . . . 6 ((𝑠 ∈ (((0..^𝑘) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) → (𝑠 ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ (ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))))
281280reximi2 3069 . . . . 5 (∃𝑠 ∈ (((0..^𝑘) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) → ∃𝑠 ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})(ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))
282265, 281syl 17 . . . 4 ((𝜑𝑘 ∈ ℕ) → ∃𝑠 ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})(ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))
283282ralrimiva 3132 . . 3 (𝜑 → ∀𝑘 ∈ ℕ ∃𝑠 ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})(ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))
284 nnex 12244 . . . 4 ℕ ∈ V
285140, 266ixpconst 8919 . . . . . . 7 X𝑛 ∈ (1...𝑁)ℕ0 = (ℕ0m (1...𝑁))
286 omelon 9658 . . . . . . . . . 10 ω ∈ On
287 nn0ennn 13995 . . . . . . . . . . 11 0 ≈ ℕ
288 nnenom 13996 . . . . . . . . . . 11 ℕ ≈ ω
289287, 288entr2i 9021 . . . . . . . . . 10 ω ≈ ℕ0
290 isnumi 9958 . . . . . . . . . 10 ((ω ∈ On ∧ ω ≈ ℕ0) → ℕ0 ∈ dom card)
291286, 289, 290mp2an 692 . . . . . . . . 9 0 ∈ dom card
292291rgenw 3055 . . . . . . . 8 𝑛 ∈ (1...𝑁)ℕ0 ∈ dom card
293 finixpnum 37575 . . . . . . . 8 (((1...𝑁) ∈ Fin ∧ ∀𝑛 ∈ (1...𝑁)ℕ0 ∈ dom card) → X𝑛 ∈ (1...𝑁)ℕ0 ∈ dom card)
29424, 292, 293mp2an 692 . . . . . . 7 X𝑛 ∈ (1...𝑁)ℕ0 ∈ dom card
295285, 294eqeltrri 2831 . . . . . 6 (ℕ0m (1...𝑁)) ∈ dom card
296140, 140mapval 8850 . . . . . . . . 9 ((1...𝑁) ↑m (1...𝑁)) = {𝑓𝑓:(1...𝑁)⟶(1...𝑁)}
297 mapfi 9358 . . . . . . . . . 10 (((1...𝑁) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((1...𝑁) ↑m (1...𝑁)) ∈ Fin)
29824, 24, 297mp2an 692 . . . . . . . . 9 ((1...𝑁) ↑m (1...𝑁)) ∈ Fin
299296, 298eqeltrri 2831 . . . . . . . 8 {𝑓𝑓:(1...𝑁)⟶(1...𝑁)} ∈ Fin
300 f1of 6817 . . . . . . . . 9 (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑓:(1...𝑁)⟶(1...𝑁))
301300ss2abi 4042 . . . . . . . 8 {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ⊆ {𝑓𝑓:(1...𝑁)⟶(1...𝑁)}
302 ssfi 9185 . . . . . . . 8 (({𝑓𝑓:(1...𝑁)⟶(1...𝑁)} ∈ Fin ∧ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ⊆ {𝑓𝑓:(1...𝑁)⟶(1...𝑁)}) → {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ∈ Fin)
303299, 301, 302mp2an 692 . . . . . . 7 {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ∈ Fin
304 finnum 9960 . . . . . . 7 ({𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ∈ Fin → {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ∈ dom card)
305303, 304ax-mp 5 . . . . . 6 {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ∈ dom card
306 xpnum 9963 . . . . . 6 (((ℕ0m (1...𝑁)) ∈ dom card ∧ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ∈ dom card) → ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∈ dom card)
307295, 305, 306mp2an 692 . . . . 5 ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∈ dom card
308 ssrab2 4055 . . . . . . . 8 {𝑠 ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))} ⊆ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
309308rgenw 3055 . . . . . . 7 𝑘 ∈ ℕ {𝑠 ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))} ⊆ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
310 ss2iun 4986 . . . . . . 7 (∀𝑘 ∈ ℕ {𝑠 ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))} ⊆ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → 𝑘 ∈ ℕ {𝑠 ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))} ⊆ 𝑘 ∈ ℕ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
311309, 310ax-mp 5 . . . . . 6 𝑘 ∈ ℕ {𝑠 ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))} ⊆ 𝑘 ∈ ℕ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
312 1nn 12249 . . . . . . 7 1 ∈ ℕ
313 ne0i 4316 . . . . . . 7 (1 ∈ ℕ → ℕ ≠ ∅)
314 iunconst 4977 . . . . . . 7 (ℕ ≠ ∅ → 𝑘 ∈ ℕ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) = ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
315312, 313, 314mp2b 10 . . . . . 6 𝑘 ∈ ℕ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) = ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
316311, 315sseqtri 4007 . . . . 5 𝑘 ∈ ℕ {𝑠 ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))} ⊆ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})
317 ssnum 10051 . . . . 5 ((((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∈ dom card ∧ 𝑘 ∈ ℕ {𝑠 ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))} ⊆ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) → 𝑘 ∈ ℕ {𝑠 ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))} ∈ dom card)
318307, 316, 317mp2an 692 . . . 4 𝑘 ∈ ℕ {𝑠 ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))} ∈ dom card
319 fveq2 6875 . . . . . . . 8 (𝑠 = (𝑔𝑘) → (1st𝑠) = (1st ‘(𝑔𝑘)))
320319rneqd 5918 . . . . . . 7 (𝑠 = (𝑔𝑘) → ran (1st𝑠) = ran (1st ‘(𝑔𝑘)))
321320sseq1d 3990 . . . . . 6 (𝑠 = (𝑔𝑘) → (ran (1st𝑠) ⊆ (0..^𝑘) ↔ ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘)))
322 fveq2 6875 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = (𝑔𝑘) → (2nd𝑠) = (2nd ‘(𝑔𝑘)))
323322imaeq1d 6046 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = (𝑔𝑘) → ((2nd𝑠) “ (1...𝑗)) = ((2nd ‘(𝑔𝑘)) “ (1...𝑗)))
324323xpeq1d 5683 . . . . . . . . . . . . . . . . . . 19 (𝑠 = (𝑔𝑘) → (((2nd𝑠) “ (1...𝑗)) × {1}) = (((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}))
325322imaeq1d 6046 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = (𝑔𝑘) → ((2nd𝑠) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)))
326325xpeq1d 5683 . . . . . . . . . . . . . . . . . . 19 (𝑠 = (𝑔𝑘) → (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))
327324, 326uneq12d 4144 . . . . . . . . . . . . . . . . . 18 (𝑠 = (𝑔𝑘) → ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
328319, 327oveq12d 7421 . . . . . . . . . . . . . . . . 17 (𝑠 = (𝑔𝑘) → ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))))
329328fvoveq1d 7425 . . . . . . . . . . . . . . . 16 (𝑠 = (𝑔𝑘) → (𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))) = (𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))))
330329fveq1d 6877 . . . . . . . . . . . . . . 15 (𝑠 = (𝑔𝑘) → ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) = ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏))
331330breq2d 5131 . . . . . . . . . . . . . 14 (𝑠 = (𝑔𝑘) → (0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ↔ 0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏)))
332328fveq1d 6877 . . . . . . . . . . . . . . 15 (𝑠 = (𝑔𝑘) → (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) = (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏))
333332neeq1d 2991 . . . . . . . . . . . . . 14 (𝑠 = (𝑔𝑘) → ((((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0 ↔ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0))
334331, 333anbi12d 632 . . . . . . . . . . . . 13 (𝑠 = (𝑔𝑘) → ((0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0) ↔ (0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)))
335334ralbidv 3163 . . . . . . . . . . . 12 (𝑠 = (𝑔𝑘) → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)))
336335rabbidv 3423 . . . . . . . . . . 11 (𝑠 = (𝑔𝑘) → {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)} = {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)})
337336uneq2d 4143 . . . . . . . . . 10 (𝑠 = (𝑔𝑘) → ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}) = ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}))
338337supeq1d 9456 . . . . . . . . 9 (𝑠 = (𝑔𝑘) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))
339338eqeq2d 2746 . . . . . . . 8 (𝑠 = (𝑔𝑘) → (𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) ↔ 𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))
340339rexbidv 3164 . . . . . . 7 (𝑠 = (𝑔𝑘) → (∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) ↔ ∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))
341340ralbidv 3163 . . . . . 6 (𝑠 = (𝑔𝑘) → (∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) ↔ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))
342321, 341anbi12d 632 . . . . 5 (𝑠 = (𝑔𝑘) → ((ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) ↔ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))))
343342ac6num 10491 . . . 4 ((ℕ ∈ V ∧ 𝑘 ∈ ℕ {𝑠 ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∣ (ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))} ∈ dom card ∧ ∀𝑘 ∈ ℕ ∃𝑠 ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})(ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) → ∃𝑔(𝑔:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))))
344284, 318, 343mp3an12 1453 . . 3 (∀𝑘 ∈ ℕ ∃𝑠 ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})(ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) → ∃𝑔(𝑔:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))))
345283, 344syl 17 . 2 (𝜑 → ∃𝑔(𝑔:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))))
3461ad2antrr 726 . . . 4 (((𝜑𝑔:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) → 𝑁 ∈ ℕ)
347 poimir.r . . . 4 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))
348 poimir.1 . . . . 5 (𝜑𝐹 ∈ ((𝑅t 𝐼) Cn 𝑅))
349348ad2antrr 726 . . . 4 (((𝜑𝑔:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) → 𝐹 ∈ ((𝑅t 𝐼) Cn 𝑅))
350 eqid 2735 . . . 4 ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑛) = ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑛)
351 simplr 768 . . . 4 (((𝜑𝑔:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) → 𝑔:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
352 simpl 482 . . . . . . 7 ((ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) → ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘))
353352ralimi 3073 . . . . . 6 (∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) → ∀𝑘 ∈ ℕ ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘))
354353adantl 481 . . . . 5 (((𝜑𝑔:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) → ∀𝑘 ∈ ℕ ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘))
355 2fveq3 6880 . . . . . . . 8 (𝑘 = 𝑝 → (1st ‘(𝑔𝑘)) = (1st ‘(𝑔𝑝)))
356355rneqd 5918 . . . . . . 7 (𝑘 = 𝑝 → ran (1st ‘(𝑔𝑘)) = ran (1st ‘(𝑔𝑝)))
357 oveq2 7411 . . . . . . 7 (𝑘 = 𝑝 → (0..^𝑘) = (0..^𝑝))
358356, 357sseq12d 3992 . . . . . 6 (𝑘 = 𝑝 → (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ↔ ran (1st ‘(𝑔𝑝)) ⊆ (0..^𝑝)))
359358rspccva 3600 . . . . 5 ((∀𝑘 ∈ ℕ ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ 𝑝 ∈ ℕ) → ran (1st ‘(𝑔𝑝)) ⊆ (0..^𝑝))
360354, 359sylan 580 . . . 4 ((((𝜑𝑔:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) ∧ 𝑝 ∈ ℕ) → ran (1st ‘(𝑔𝑝)) ⊆ (0..^𝑝))
361 simpll 766 . . . . . 6 (((𝜑𝑔:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) → 𝜑)
362 poimir.2 . . . . . 6 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧𝐼 ∧ (𝑧𝑛) = 0)) → ((𝐹𝑧)‘𝑛) ≤ 0)
363361, 362sylan 580 . . . . 5 ((((𝜑𝑔:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧𝐼 ∧ (𝑧𝑛) = 0)) → ((𝐹𝑧)‘𝑛) ≤ 0)
364 eqid 2735 . . . . 5 ((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) = ((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))
365 simpr 484 . . . . . . . 8 ((ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) → ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))
366365ralimi 3073 . . . . . . 7 (∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) → ∀𝑘 ∈ ℕ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))
367366adantl 481 . . . . . 6 (((𝜑𝑔:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) → ∀𝑘 ∈ ℕ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))
368 2fveq3 6880 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 𝑝 → (2nd ‘(𝑔𝑘)) = (2nd ‘(𝑔𝑝)))
369368imaeq1d 6046 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑝 → ((2nd ‘(𝑔𝑘)) “ (1...𝑗)) = ((2nd ‘(𝑔𝑝)) “ (1...𝑗)))
370369xpeq1d 5683 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑝 → (((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) = (((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}))
371368imaeq1d 6046 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑝 → ((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)))
372371xpeq1d 5683 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑝 → (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))
373370, 372uneq12d 4144 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑝 → ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))
374355, 373oveq12d 7421 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑝 → ((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))))
375 sneq 4611 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑝 → {𝑘} = {𝑝})
376375xpeq2d 5684 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑝 → ((1...𝑁) × {𝑘}) = ((1...𝑁) × {𝑝}))
377374, 376oveq12d 7421 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑝 → (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) = (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))
378377fveq2d 6879 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑝 → (𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))) = (𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝}))))
379378fveq1d 6877 . . . . . . . . . . . . . . 15 (𝑘 = 𝑝 → ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) = ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏))
380379breq2d 5131 . . . . . . . . . . . . . 14 (𝑘 = 𝑝 → (0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ↔ 0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏)))
381374fveq1d 6877 . . . . . . . . . . . . . . 15 (𝑘 = 𝑝 → (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) = (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏))
382381neeq1d 2991 . . . . . . . . . . . . . 14 (𝑘 = 𝑝 → ((((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0 ↔ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0))
383380, 382anbi12d 632 . . . . . . . . . . . . 13 (𝑘 = 𝑝 → ((0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0) ↔ (0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)))
384383ralbidv 3163 . . . . . . . . . . . 12 (𝑘 = 𝑝 → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)))
385384rabbidv 3423 . . . . . . . . . . 11 (𝑘 = 𝑝 → {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)} = {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)})
386385uneq2d 4143 . . . . . . . . . 10 (𝑘 = 𝑝 → ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}) = ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}))
387386supeq1d 9456 . . . . . . . . 9 (𝑘 = 𝑝 → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))
388387eqeq2d 2746 . . . . . . . 8 (𝑘 = 𝑝 → (𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) ↔ 𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))
389388rexbidv 3164 . . . . . . 7 (𝑘 = 𝑝 → (∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) ↔ ∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))
390 eqeq1 2739 . . . . . . . . 9 (𝑖 = 𝑞 → (𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) ↔ 𝑞 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))
391390rexbidv 3164 . . . . . . . 8 (𝑖 = 𝑞 → (∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) ↔ ∃𝑗 ∈ (0...𝑁)𝑞 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))
392 oveq2 7411 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑚 → (1...𝑗) = (1...𝑚))
393392imaeq2d 6047 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑚 → ((2nd ‘(𝑔𝑝)) “ (1...𝑗)) = ((2nd ‘(𝑔𝑝)) “ (1...𝑚)))
394393xpeq1d 5683 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑚 → (((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) = (((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}))
395 oveq1 7410 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑚 → (𝑗 + 1) = (𝑚 + 1))
396395oveq1d 7418 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑚 → ((𝑗 + 1)...𝑁) = ((𝑚 + 1)...𝑁))
397396imaeq2d 6047 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑚 → ((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)))
398397xpeq1d 5683 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑚 → (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))
399394, 398uneq12d 4144 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑚 → ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))
400399oveq2d 7419 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑚 → ((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))))
401400fvoveq1d 7425 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑚 → (𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝}))) = (𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝}))))
402401fveq1d 6877 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑚 → ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) = ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏))
403402breq2d 5131 . . . . . . . . . . . . . . 15 (𝑗 = 𝑚 → (0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ↔ 0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏)))
404400fveq1d 6877 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑚 → (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) = (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏))
405404neeq1d 2991 . . . . . . . . . . . . . . 15 (𝑗 = 𝑚 → ((((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0 ↔ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0))
406403, 405anbi12d 632 . . . . . . . . . . . . . 14 (𝑗 = 𝑚 → ((0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0) ↔ (0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)))
407406ralbidv 3163 . . . . . . . . . . . . 13 (𝑗 = 𝑚 → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)))
408407rabbidv 3423 . . . . . . . . . . . 12 (𝑗 = 𝑚 → {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)} = {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)})
409408uneq2d 4143 . . . . . . . . . . 11 (𝑗 = 𝑚 → ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}) = ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}))
410409supeq1d 9456 . . . . . . . . . 10 (𝑗 = 𝑚 → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))
411410eqeq2d 2746 . . . . . . . . 9 (𝑗 = 𝑚 → (𝑞 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) ↔ 𝑞 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))
412411cbvrexvw 3221 . . . . . . . 8 (∃𝑗 ∈ (0...𝑁)𝑞 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) ↔ ∃𝑚 ∈ (0...𝑁)𝑞 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))
413391, 412bitrdi 287 . . . . . . 7 (𝑖 = 𝑞 → (∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) ↔ ∃𝑚 ∈ (0...𝑁)𝑞 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))
414389, 413rspc2v 3612 . . . . . 6 ((𝑝 ∈ ℕ ∧ 𝑞 ∈ (0...𝑁)) → (∀𝑘 ∈ ℕ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) → ∃𝑚 ∈ (0...𝑁)𝑞 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))
415367, 414mpan9 506 . . . . 5 ((((𝜑𝑔:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ (0...𝑁))) → ∃𝑚 ∈ (0...𝑁)𝑞 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))
416346, 137, 347, 349, 363, 364, 351, 360, 415poimirlem31 37621 . . . 4 ((((𝜑𝑔:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) ∧ (𝑝 ∈ ℕ ∧ 𝑛 ∈ (1...𝑁) ∧ 𝑟 ∈ { ≤ , ≤ })) → ∃𝑚 ∈ (0...𝑁)0𝑟((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑛))
417346, 137, 347, 349, 350, 351, 360, 416poimirlem30 37620 . . 3 (((𝜑𝑔:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) → ∃𝑐𝐼𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
418417anasss 466 . 2 ((𝜑 ∧ (𝑔:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))) → ∃𝑐𝐼𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
419345, 418exlimddv 1935 1 (𝜑 → ∃𝑐𝐼𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847  w3a 1086   = wceq 1540  wex 1779  wcel 2108  {cab 2713  wne 2932  wral 3051  wrex 3060  {crab 3415  Vcvv 3459  cun 3924  wss 3926  c0 4308  {csn 4601  {cpr 4603   ciun 4967   class class class wbr 5119   Or wor 5560   × cxp 5652  ccnv 5653  dom cdm 5654  ran crn 5655  cima 5657  Oncon0 6352   Fn wfn 6525  wf 6526  1-1-ontowf1o 6529  cfv 6530  (class class class)co 7403  f cof 7667  ωcom 7859  1st c1st 7984  2nd c2nd 7985  m cmap 8838  Xcixp 8909  cen 8954  Fincfn 8957  supcsup 9450  cardccrd 9947  cc 11125  cr 11126  0cc0 11127  1c1 11128   + caddc 11130   · cmul 11132   < clt 11267  cle 11268  cmin 11464   / cdiv 11892  cn 12238  0cn0 12499  cz 12586  cuz 12850  +crp 13006  (,)cioo 13360  [,]cicc 13363  ...cfz 13522  ..^cfzo 13669  t crest 17432  topGenctg 17449  tcpt 17450   Cn ccn 23160
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5249  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-inf2 9653  ax-cnex 11183  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204  ax-pre-sup 11205
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3359  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-tp 4606  df-op 4608  df-uni 4884  df-int 4923  df-iun 4969  df-iin 4970  df-disj 5087  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-se 5607  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-isom 6539  df-riota 7360  df-ov 7406  df-oprab 7407  df-mpo 7408  df-of 7669  df-om 7860  df-1st 7986  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8383  df-rdg 8422  df-1o 8478  df-2o 8479  df-oadd 8482  df-omul 8483  df-er 8717  df-map 8840  df-pm 8841  df-ixp 8910  df-en 8958  df-dom 8959  df-sdom 8960  df-fin 8961  df-fi 9421  df-sup 9452  df-inf 9453  df-oi 9522  df-dju 9913  df-card 9951  df-acn 9954  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11466  df-neg 11467  df-div 11893  df-nn 12239  df-2 12301  df-3 12302  df-n0 12500  df-xnn0 12573  df-z 12587  df-uz 12851  df-q 12963  df-rp 13007  df-xneg 13126  df-xadd 13127  df-xmul 13128  df-ioo 13364  df-icc 13367  df-fz 13523  df-fzo 13670  df-fl 13807  df-seq 14018  df-exp 14078  df-fac 14290  df-bc 14319  df-hash 14347  df-cj 15116  df-re 15117  df-im 15118  df-sqrt 15252  df-abs 15253  df-clim 15502  df-sum 15701  df-dvds 16271  df-rest 17434  df-topgen 17455  df-pt 17456  df-psmet 21305  df-xmet 21306  df-met 21307  df-bl 21308  df-mopn 21309  df-top 22830  df-topon 22847  df-bases 22882  df-cld 22955  df-ntr 22956  df-cls 22957  df-lp 23072  df-cn 23163  df-cnp 23164  df-t1 23250  df-haus 23251  df-cmp 23323  df-tx 23498  df-hmeo 23691  df-hmph 23692  df-ii 24819
This theorem is referenced by:  poimir  37623
  Copyright terms: Public domain W3C validator