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 38226
Description: Lemma for poimir 38227, combining poimirlem28 38222, poimirlem30 38224, and poimirlem31 38225 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 485 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 𝑁 ∈ ℕ)
3 fvoveq1 7434 . . . . . . . . . . . . 13 (𝑝 = ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝐹‘(𝑝f / ((1...𝑁) × {𝑘}))) = (𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))))
43fveq1d 6884 . . . . . . . . . . . 12 (𝑝 = ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) = ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏))
54breq2d 5123 . . . . . . . . . . 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 6881 . . . . . . . . . . . 12 (𝑝 = ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝑝𝑏) = (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏))
76neeq1d 3023 . . . . . . . . . . 11 (𝑝 = ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → ((𝑝𝑏) ≠ 0 ↔ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0))
85, 7anbi12d 643 . . . . . . . . . 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 3194 . . . . . . . . 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 3429 . . . . . . . 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 4128 . . . . . . 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 9406 . . . . . 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 12565 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℕ0)
14 0elfz 13652 . . . . . . . . . . 11 (𝑁 ∈ ℕ0 → 0 ∈ (0...𝑁))
1513, 14syl 18 . . . . . . . . . 10 (𝜑 → 0 ∈ (0...𝑁))
1615snssd 4755 . . . . . . . . 9 (𝜑 → {0} ⊆ (0...𝑁))
17 ssrab2 4040 . . . . . . . . . . 11 {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ⊆ (1...𝑁)
18 fz1ssfz0 13651 . . . . . . . . . . 11 (1...𝑁) ⊆ (0...𝑁)
1917, 18sstri 3952 . . . . . . . . . 10 {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ⊆ (0...𝑁)
2019a1i 11 . . . . . . . . 9 (𝜑 → {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ⊆ (0...𝑁))
2116, 20unssd 4151 . . . . . . . 8 (𝜑 → ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ⊆ (0...𝑁))
22 ltso 11290 . . . . . . . . 9 < Or ℝ
23 snfi 9040 . . . . . . . . . . 11 {0} ∈ Fin
24 fzfi 14008 . . . . . . . . . . . 12 (1...𝑁) ∈ Fin
25 rabfi 9231 . . . . . . . . . . . 12 ((1...𝑁) ∈ Fin → {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ∈ Fin)
2624, 25ax-mp 5 . . . . . . . . . . 11 {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ∈ Fin
27 unfi 9155 . . . . . . . . . . 11 (({0} ∈ Fin ∧ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ∈ Fin) → ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ∈ Fin)
2823, 26, 27mp2an 704 . . . . . . . . . 10 ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ∈ Fin
29 c0ex 11200 . . . . . . . . . . . 12 0 ∈ V
3029snid 4631 . . . . . . . . . . 11 0 ∈ {0}
31 elun1 4141 . . . . . . . . . . 11 (0 ∈ {0} → 0 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}))
32 ne0i 4300 . . . . . . . . . . 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 11211 . . . . . . . . . . . . 13 ((𝜑𝑁 ∈ ℕ) → 0 ∈ ℝ)
3534snssd 4755 . . . . . . . . . . . 12 ((𝜑𝑁 ∈ ℕ) → {0} ⊆ ℝ)
361, 35ax-mp 5 . . . . . . . . . . 11 {0} ⊆ ℝ
37 elfzelz 13552 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℤ)
3837ssriv 3947 . . . . . . . . . . . . 13 (1...𝑁) ⊆ ℤ
39 zssre 12598 . . . . . . . . . . . . 13 ℤ ⊆ ℝ
4038, 39sstri 3952 . . . . . . . . . . . 12 (1...𝑁) ⊆ ℝ
4117, 40sstri 3952 . . . . . . . . . . 11 {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ⊆ ℝ
4236, 41unssi 4150 . . . . . . . . . 10 ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ⊆ ℝ
4328, 33, 423pm3.2i 1356 . . . . . . . . 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 9430 . . . . . . . . 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 704 . . . . . . . 8 sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})
46 ssel 3937 . . . . . . . 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 22 . . . . . . 7 (𝜑 → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ∈ (0...𝑁))
4847ad2antrr 738 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑝:(1...𝑁)⟶(0...𝑘)) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ∈ (0...𝑁))
49 elfznn 13581 . . . . . . . . 9 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ)
50 nngt0 12267 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → 0 < 𝑛)
5150adantr 485 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) → 0 < 𝑛)
52 simpr 489 . . . . . . . . . . . . . 14 ((0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → (𝑝𝑏) ≠ 0)
5352ralimi 3108 . . . . . . . . . . . . 13 (∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑠)(𝑝𝑏) ≠ 0)
54 elfznn 13581 . . . . . . . . . . . . . 14 (𝑠 ∈ (1...𝑁) → 𝑠 ∈ ℕ)
55 nnre 12240 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
56 nnre 12240 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ℕ → 𝑠 ∈ ℝ)
57 lenlt 11288 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℝ ∧ 𝑠 ∈ ℝ) → (𝑛𝑠 ↔ ¬ 𝑠 < 𝑛))
5855, 56, 57syl2an 607 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ) → (𝑛𝑠 ↔ ¬ 𝑠 < 𝑛))
59 elfz1b 13621 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ (1...𝑠) ↔ (𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ ∧ 𝑛𝑠))
6059biimpri 231 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ ∧ 𝑛𝑠) → 𝑛 ∈ (1...𝑠))
61603expia 1137 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ) → (𝑛𝑠𝑛 ∈ (1...𝑠)))
6258, 61sylbird 263 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ) → (¬ 𝑠 < 𝑛𝑛 ∈ (1...𝑠)))
63 fveq2 6882 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = 𝑛 → (𝑝𝑏) = (𝑝𝑛))
6463eqeq1d 2771 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = 𝑛 → ((𝑝𝑏) = 0 ↔ (𝑝𝑛) = 0))
6564rspcev 3588 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ (1...𝑠) ∧ (𝑝𝑛) = 0) → ∃𝑏 ∈ (1...𝑠)(𝑝𝑏) = 0)
6665expcom 418 . . . . . . . . . . . . . . . . . 18 ((𝑝𝑛) = 0 → (𝑛 ∈ (1...𝑠) → ∃𝑏 ∈ (1...𝑠)(𝑝𝑏) = 0))
6762, 66sylan9 516 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ) ∧ (𝑝𝑛) = 0) → (¬ 𝑠 < 𝑛 → ∃𝑏 ∈ (1...𝑠)(𝑝𝑏) = 0))
6867an32s 664 . . . . . . . . . . . . . . . 16 (((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) ∧ 𝑠 ∈ ℕ) → (¬ 𝑠 < 𝑛 → ∃𝑏 ∈ (1...𝑠)(𝑝𝑏) = 0))
69 nne 2968 . . . . . . . . . . . . . . . . . 18 (¬ (𝑝𝑏) ≠ 0 ↔ (𝑝𝑏) = 0)
7069rexbii 3118 . . . . . . . . . . . . . . . . 17 (∃𝑏 ∈ (1...𝑠) ¬ (𝑝𝑏) ≠ 0 ↔ ∃𝑏 ∈ (1...𝑠)(𝑝𝑏) = 0)
71 rexnal 3123 . . . . . . . . . . . . . . . . 17 (∃𝑏 ∈ (1...𝑠) ¬ (𝑝𝑏) ≠ 0 ↔ ¬ ∀𝑏 ∈ (1...𝑠)(𝑝𝑏) ≠ 0)
7270, 71bitr3i 280 . . . . . . . . . . . . . . . 16 (∃𝑏 ∈ (1...𝑠)(𝑝𝑏) = 0 ↔ ¬ ∀𝑏 ∈ (1...𝑠)(𝑝𝑏) ≠ 0)
7368, 72imbitrdi 254 . . . . . . . . . . . . . . 15 (((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) ∧ 𝑠 ∈ ℕ) → (¬ 𝑠 < 𝑛 → ¬ ∀𝑏 ∈ (1...𝑠)(𝑝𝑏) ≠ 0))
7473con4d 116 . . . . . . . . . . . . . 14 (((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) ∧ 𝑠 ∈ ℕ) → (∀𝑏 ∈ (1...𝑠)(𝑝𝑏) ≠ 0 → 𝑠 < 𝑛))
7554, 74sylan2 604 . . . . . . . . . . . . 13 (((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) ∧ 𝑠 ∈ (1...𝑁)) → (∀𝑏 ∈ (1...𝑠)(𝑝𝑏) ≠ 0 → 𝑠 < 𝑛))
7653, 75syl5 35 . . . . . . . . . . . 12 (((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) ∧ 𝑠 ∈ (1...𝑁)) → (∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → 𝑠 < 𝑛))
7776ralrimiva 3163 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) → ∀𝑠 ∈ (1...𝑁)(∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → 𝑠 < 𝑛))
78 ralunb 4156 . . . . . . . . . . . 12 (∀𝑠 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})𝑠 < 𝑛 ↔ (∀𝑠 ∈ {0}𝑠 < 𝑛 ∧ ∀𝑠 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}𝑠 < 𝑛))
79 breq1 5114 . . . . . . . . . . . . . 14 (𝑠 = 0 → (𝑠 < 𝑛 ↔ 0 < 𝑛))
8029, 79ralsn 4650 . . . . . . . . . . . . 13 (∀𝑠 ∈ {0}𝑠 < 𝑛 ↔ 0 < 𝑛)
81 oveq2 7419 . . . . . . . . . . . . . . 15 (𝑎 = 𝑠 → (1...𝑎) = (1...𝑠))
8281raleqdv 3329 . . . . . . . . . . . . . 14 (𝑎 = 𝑠 → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
8382ralrab 3664 . . . . . . . . . . . . 13 (∀𝑠 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}𝑠 < 𝑛 ↔ ∀𝑠 ∈ (1...𝑁)(∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → 𝑠 < 𝑛))
8480, 83anbi12i 639 . . . . . . . . . . . 12 ((∀𝑠 ∈ {0}𝑠 < 𝑛 ∧ ∀𝑠 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}𝑠 < 𝑛) ↔ (0 < 𝑛 ∧ ∀𝑠 ∈ (1...𝑁)(∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → 𝑠 < 𝑛)))
8578, 84bitri 278 . . . . . . . . . . 11 (∀𝑠 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})𝑠 < 𝑛 ↔ (0 < 𝑛 ∧ ∀𝑠 ∈ (1...𝑁)(∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → 𝑠 < 𝑛)))
8651, 77, 85sylanbrc 594 . . . . . . . . . 10 ((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) → ∀𝑠 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})𝑠 < 𝑛)
87 breq1 5114 . . . . . . . . . . 11 (𝑠 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) → (𝑠 < 𝑛 ↔ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < 𝑛))
8887rspcva 3586 . . . . . . . . . 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 598 . . . . . . . . 9 ((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < 𝑛)
9049, 89sylan 591 . . . . . . . 8 ((𝑛 ∈ (1...𝑁) ∧ (𝑝𝑛) = 0) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < 𝑛)
91903adant2 1147 . . . . . . 7 ((𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 0) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < 𝑛)
9291adantl 486 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 0)) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < 𝑛)
9337zred 12700 . . . . . . . . . . 11 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℝ)
94933ad2ant1 1149 . . . . . . . . . 10 ((𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) → 𝑛 ∈ ℝ)
9594adantl 486 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → 𝑛 ∈ ℝ)
96 simpr1 1211 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → 𝑛 ∈ (1...𝑁))
97 simpll 778 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → 𝜑)
98 simplr 780 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → 𝑘 ∈ ℕ)
99 elfzelz 13552 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ (0...𝑘) → 𝑖 ∈ ℤ)
10099zred 12700 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ (0...𝑘) → 𝑖 ∈ ℝ)
101 nndivre 12277 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ ℝ)
102100, 101sylan 591 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ ℝ)
103 elfzle1 13555 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ (0...𝑘) → 0 ≤ 𝑖)
104100, 103jca 520 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ (0...𝑘) → (𝑖 ∈ ℝ ∧ 0 ≤ 𝑖))
105 nnrp 13028 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
106105rpregt0d 13066 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ ℕ → (𝑘 ∈ ℝ ∧ 0 < 𝑘))
107 divge0 12084 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑖 ∈ ℝ ∧ 0 ≤ 𝑖) ∧ (𝑘 ∈ ℝ ∧ 0 < 𝑘)) → 0 ≤ (𝑖 / 𝑘))
108104, 106, 107syl2an 607 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝑖 / 𝑘))
109 elfzle2 13556 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ (0...𝑘) → 𝑖𝑘)
110109adantr 485 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑖𝑘)
111100adantr 485 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑖 ∈ ℝ)
112 1red 11209 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 1 ∈ ℝ)
113105adantl 486 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ+)
114111, 112, 113ledivmuld 13113 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑖 / 𝑘) ≤ 1 ↔ 𝑖 ≤ (𝑘 · 1)))
115 nncn 12241 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
116115mulridd 11226 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ ℕ → (𝑘 · 1) = 𝑘)
117116breq2d 5123 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ ℕ → (𝑖 ≤ (𝑘 · 1) ↔ 𝑖𝑘))
118117adantl 486 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 ≤ (𝑘 · 1) ↔ 𝑖𝑘))
119114, 118bitrd 282 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑖 / 𝑘) ≤ 1 ↔ 𝑖𝑘))
120110, 119mpbird 260 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ≤ 1)
121 elicc01 13493 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖 / 𝑘) ∈ (0[,]1) ↔ ((𝑖 / 𝑘) ∈ ℝ ∧ 0 ≤ (𝑖 / 𝑘) ∧ (𝑖 / 𝑘) ≤ 1))
122102, 108, 120, 121syl3anbrc 1360 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ (0[,]1))
123122ancoms 463 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑘)) → (𝑖 / 𝑘) ∈ (0[,]1))
124 elsni 4609 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ {𝑘} → 𝑗 = 𝑘)
125124oveq2d 7427 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ {𝑘} → (𝑖 / 𝑗) = (𝑖 / 𝑘))
126125eleq1d 2854 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ {𝑘} → ((𝑖 / 𝑗) ∈ (0[,]1) ↔ (𝑖 / 𝑘) ∈ (0[,]1)))
127123, 126syl5ibrcom 250 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑘)) → (𝑗 ∈ {𝑘} → (𝑖 / 𝑗) ∈ (0[,]1)))
128127impr 459 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ ∧ (𝑖 ∈ (0...𝑘) ∧ 𝑗 ∈ {𝑘})) → (𝑖 / 𝑗) ∈ (0[,]1))
12998, 128sylan 591 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) ∧ (𝑖 ∈ (0...𝑘) ∧ 𝑗 ∈ {𝑘})) → (𝑖 / 𝑗) ∈ (0[,]1))
130 simprr 784 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → 𝑝:(1...𝑁)⟶(0...𝑘))
131 vex 3465 . . . . . . . . . . . . . . . . . 18 𝑘 ∈ V
132131fconst 6765 . . . . . . . . . . . . . . . . 17 ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘}
133132a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘})
134 fzfid 14009 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → (1...𝑁) ∈ Fin)
135 inidm 4185 . . . . . . . . . . . . . . . 16 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
136129, 130, 133, 134, 134, 135off 7693 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → (𝑝f / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
137 poimir.i . . . . . . . . . . . . . . . . 17 𝐼 = ((0[,]1) ↑m (1...𝑁))
138137eleq2i 2861 . . . . . . . . . . . . . . . 16 ((𝑝f / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ (𝑝f / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑m (1...𝑁)))
139 ovex 7444 . . . . . . . . . . . . . . . . 17 (0[,]1) ∈ V
140 ovex 7444 . . . . . . . . . . . . . . . . 17 (1...𝑁) ∈ V
141139, 140elmap 8869 . . . . . . . . . . . . . . . 16 ((𝑝f / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑m (1...𝑁)) ↔ (𝑝f / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
142138, 141bitri 278 . . . . . . . . . . . . . . 15 ((𝑝f / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ (𝑝f / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
143136, 142sylibr 237 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → (𝑝f / ((1...𝑁) × {𝑘})) ∈ 𝐼)
1441433adantr3 1188 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → (𝑝f / ((1...𝑁) × {𝑘})) ∈ 𝐼)
145 3anass 1109 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) ↔ (𝑛 ∈ (1...𝑁) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)))
146 ancom 465 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (1...𝑁) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) ↔ ((𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) ∧ 𝑛 ∈ (1...𝑁)))
147145, 146bitri 278 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) ↔ ((𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) ∧ 𝑛 ∈ (1...𝑁)))
148 ffn 6706 . . . . . . . . . . . . . . . . . 18 (𝑝:(1...𝑁)⟶(0...𝑘) → 𝑝 Fn (1...𝑁))
149148ad2antrl 740 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → 𝑝 Fn (1...𝑁))
150 fnconstg 6767 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ V → ((1...𝑁) × {𝑘}) Fn (1...𝑁))
151131, 150mp1i 14 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ((1...𝑁) × {𝑘}) Fn (1...𝑁))
152 fzfid 14009 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → (1...𝑁) ∈ Fin)
153 simplrr 789 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑝𝑛) = 𝑘)
154131fvconst2 7203 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {𝑘})‘𝑛) = 𝑘)
155154adantl 486 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {𝑘})‘𝑛) = 𝑘)
156149, 151, 152, 152, 135, 153, 155ofval 7686 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = (𝑘 / 𝑘))
157156anasss 471 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ) ∧ ((𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) ∧ 𝑛 ∈ (1...𝑁))) → ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = (𝑘 / 𝑘))
158147, 157sylan2b 605 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = (𝑘 / 𝑘))
159 nnne0 12270 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ → 𝑘 ≠ 0)
160115, 159dividd 11989 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ → (𝑘 / 𝑘) = 1)
161160ad2antlr 739 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → (𝑘 / 𝑘) = 1)
162158, 161eqtrd 2804 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = 1)
163 ovex 7444 . . . . . . . . . . . . . 14 (𝑝f / ((1...𝑁) × {𝑘})) ∈ V
164 eleq1 2857 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → (𝑧𝐼 ↔ (𝑝f / ((1...𝑁) × {𝑘})) ∈ 𝐼))
165 fveq1 6881 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → (𝑧𝑛) = ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛))
166165eqeq1d 2771 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → ((𝑧𝑛) = 1 ↔ ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = 1))
167164, 1663anbi23d 1465 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → ((𝑛 ∈ (1...𝑁) ∧ 𝑧𝐼 ∧ (𝑧𝑛) = 1) ↔ (𝑛 ∈ (1...𝑁) ∧ (𝑝f / ((1...𝑁) × {𝑘})) ∈ 𝐼 ∧ ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = 1)))
168167anbi2d 641 . . . . . . . . . . . . . . 15 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧𝐼 ∧ (𝑧𝑛) = 1)) ↔ (𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ (𝑝f / ((1...𝑁) × {𝑘})) ∈ 𝐼 ∧ ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = 1))))
169 fveq2 6882 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → (𝐹𝑧) = (𝐹‘(𝑝f / ((1...𝑁) × {𝑘}))))
170169fveq1d 6884 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → ((𝐹𝑧)‘𝑛) = ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛))
171170breq2d 5123 . . . . . . . . . . . . . . 15 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → (0 ≤ ((𝐹𝑧)‘𝑛) ↔ 0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛)))
172168, 171imbi12d 347 . . . . . . . . . . . . . 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 3532 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ (𝑝f / ((1...𝑁) × {𝑘})) ∈ 𝐼 ∧ ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = 1)) → 0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛))
17597, 96, 144, 162, 174syl13anc 1397 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → 0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛))
176 simpr 489 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
177 simp3 1154 . . . . . . . . . . . . 13 ((𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) → (𝑝𝑛) = 𝑘)
178 neeq1 3026 . . . . . . . . . . . . . . 15 ((𝑝𝑛) = 𝑘 → ((𝑝𝑛) ≠ 0 ↔ 𝑘 ≠ 0))
179159, 178syl5ibrcom 250 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → ((𝑝𝑛) = 𝑘 → (𝑝𝑛) ≠ 0))
180179imp 411 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ∧ (𝑝𝑛) = 𝑘) → (𝑝𝑛) ≠ 0)
181176, 177, 180syl2an 607 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → (𝑝𝑛) ≠ 0)
182 vex 3465 . . . . . . . . . . . . 13 𝑛 ∈ V
183 fveq2 6882 . . . . . . . . . . . . . . 15 (𝑏 = 𝑛 → ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) = ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛))
184183breq2d 5123 . . . . . . . . . . . . . 14 (𝑏 = 𝑛 → (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ↔ 0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛)))
18563neeq1d 3023 . . . . . . . . . . . . . 14 (𝑏 = 𝑛 → ((𝑝𝑏) ≠ 0 ↔ (𝑝𝑛) ≠ 0))
186184, 185anbi12d 643 . . . . . . . . . . . . 13 (𝑏 = 𝑛 → ((0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛) ∧ (𝑝𝑛) ≠ 0)))
187182, 186ralsn 4650 . . . . . . . . . . . 12 (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛) ∧ (𝑝𝑛) ≠ 0))
188175, 181, 187sylanbrc 594 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))
18937zcnd 12701 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ)
190 1cnd 11202 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...𝑁) → 1 ∈ ℂ)
191189, 190subeq0ad 11579 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) = 0 ↔ 𝑛 = 1))
192191biimpcd 252 . . . . . . . . . . . . . . . . 17 ((𝑛 − 1) = 0 → (𝑛 ∈ (1...𝑁) → 𝑛 = 1))
193 1z 12624 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℤ
194 fzsn 13594 . . . . . . . . . . . . . . . . . . . . 21 (1 ∈ ℤ → (1...1) = {1})
195193, 194ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (1...1) = {1}
196 oveq2 7419 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 1 → (1...𝑛) = (1...1))
197 sneq 4602 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 1 → {𝑛} = {1})
198195, 196, 1973eqtr4a 2830 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 1 → (1...𝑛) = {𝑛})
199198raleqdv 3329 . . . . . . . . . . . . . . . . . 18 (𝑛 = 1 → (∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
200199biimprd 251 . . . . . . . . . . . . . . . . 17 (𝑛 = 1 → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
201192, 200syl6 36 . . . . . . . . . . . . . . . 16 ((𝑛 − 1) = 0 → (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
202 ralun 4157 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)) → ∀𝑏 ∈ ((1...(𝑛 − 1)) ∪ {𝑛})(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))
203 npcan1 11639 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ℂ → ((𝑛 − 1) + 1) = 𝑛)
204189, 203syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) + 1) = 𝑛)
205 elfzuz 13548 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ (ℤ‘1))
206204, 205eqeltrd 2869 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) + 1) ∈ (ℤ‘1))
207 peano2zm 12637 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ℤ → (𝑛 − 1) ∈ ℤ)
208 uzid 12877 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 − 1) ∈ ℤ → (𝑛 − 1) ∈ (ℤ‘(𝑛 − 1)))
209 peano2uz 12925 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 − 1) ∈ (ℤ‘(𝑛 − 1)) → ((𝑛 − 1) + 1) ∈ (ℤ‘(𝑛 − 1)))
21037, 207, 208, 2094syl 20 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) + 1) ∈ (ℤ‘(𝑛 − 1)))
211204, 210eqeltrrd 2870 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ (ℤ‘(𝑛 − 1)))
212 fzsplit2 13577 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑛 − 1) + 1) ∈ (ℤ‘1) ∧ 𝑛 ∈ (ℤ‘(𝑛 − 1))) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)))
213206, 211, 212syl2anc 595 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (1...𝑁) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)))
214204oveq1d 7426 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...𝑁) → (((𝑛 − 1) + 1)...𝑛) = (𝑛...𝑛))
215 fzsn 13594 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ℤ → (𝑛...𝑛) = {𝑛})
21637, 215syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...𝑁) → (𝑛...𝑛) = {𝑛})
217214, 216eqtrd 2804 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (1...𝑁) → (((𝑛 − 1) + 1)...𝑛) = {𝑛})
218217uneq2d 4128 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (1...𝑁) → ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)) = ((1...(𝑛 − 1)) ∪ {𝑛}))
219213, 218eqtrd 2804 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ (1...𝑁) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ {𝑛}))
220219raleqdv 3329 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ ∀𝑏 ∈ ((1...(𝑛 − 1)) ∪ {𝑛})(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
221202, 220imbitrrid 249 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...𝑁) → ((∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
222221expd 420 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
223222com12 33 . . . . . . . . . . . . . . . . 17 (∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
224223adantl 486 . . . . . . . . . . . . . . . 16 (((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)) → (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
225201, 224jaoi 870 . . . . . . . . . . . . . . 15 (((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))) → (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
226225imdistand 580 . . . . . . . . . . . . . 14 (((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))) → ((𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)) → (𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
227226com12 33 . . . . . . . . . . . . 13 ((𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)) → (((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))) → (𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
228 elun 4113 . . . . . . . . . . . . . 14 ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ↔ ((𝑛 − 1) ∈ {0} ∨ (𝑛 − 1) ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}))
229 ovex 7444 . . . . . . . . . . . . . . . 16 (𝑛 − 1) ∈ V
230229elsn 4607 . . . . . . . . . . . . . . 15 ((𝑛 − 1) ∈ {0} ↔ (𝑛 − 1) = 0)
231 oveq2 7419 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑛 − 1) → (1...𝑎) = (1...(𝑛 − 1)))
232231raleqdv 3329 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑛 − 1) → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
233232elrab 3657 . . . . . . . . . . . . . . 15 ((𝑛 − 1) ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ↔ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
234230, 233orbi12i 927 . . . . . . . . . . . . . 14 (((𝑛 − 1) ∈ {0} ∨ (𝑛 − 1) ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ↔ ((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
235228, 234bitri 278 . . . . . . . . . . . . 13 ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ↔ ((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
236 oveq2 7419 . . . . . . . . . . . . . . 15 (𝑎 = 𝑛 → (1...𝑎) = (1...𝑛))
237236raleqdv 3329 . . . . . . . . . . . . . 14 (𝑎 = 𝑛 → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
238237elrab 3657 . . . . . . . . . . . . 13 (𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ↔ (𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
239227, 235, 2383imtr4g 299 . . . . . . . . . . . 12 ((𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)) → ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → 𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}))
240 elun2 4142 . . . . . . . . . . . 12 (𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} → 𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}))
241239, 240syl6 36 . . . . . . . . . . 11 ((𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)) → ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → 𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})))
24296, 188, 241syl2anc 595 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → 𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})))
243 fimaxre2 12160 . . . . . . . . . . . . 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 704 . . . . . . . . . . . 12 𝑖 ∈ ℝ ∀𝑗 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})𝑗𝑖
24542, 33, 2443pm3.2i 1356 . . . . . . . . . . 11 (({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ⊆ ℝ ∧ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ≠ ∅ ∧ ∃𝑖 ∈ ℝ ∀𝑗 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})𝑗𝑖)
246245suprubii 12190 . . . . . . . . . 10 (𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → 𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ))
247242, 246syl6 36 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → 𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )))
248 ltm1 12057 . . . . . . . . . 10 (𝑛 ∈ ℝ → (𝑛 − 1) < 𝑛)
249 peano2rem 11525 . . . . . . . . . . 11 (𝑛 ∈ ℝ → (𝑛 − 1) ∈ ℝ)
25042, 45sselii 3940 . . . . . . . . . . . 12 sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ∈ ℝ
251 ltletr 11302 . . . . . . . . . . . 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 1476 . . . . . . . . . . 11 (((𝑛 − 1) ∈ ℝ ∧ 𝑛 ∈ ℝ) → (((𝑛 − 1) < 𝑛𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )) → (𝑛 − 1) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )))
253249, 252mpancom 700 . . . . . . . . . 10 (𝑛 ∈ ℝ → (((𝑛 − 1) < 𝑛𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )) → (𝑛 − 1) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )))
254248, 253mpand 707 . . . . . . . . 9 (𝑛 ∈ ℝ → (𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) → (𝑛 − 1) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )))
25595, 247, 254sylsyld 62 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → (𝑛 − 1) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )))
256250ltnri 11319 . . . . . . . . . 10 ¬ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )
257 breq1 5114 . . . . . . . . . 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 329 . . . . . . . . 9 (sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) = (𝑛 − 1) → ¬ (𝑛 − 1) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ))
259258necon2ai 2993 . . . . . . . 8 ((𝑛 − 1) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ≠ (𝑛 − 1))
260255, 259syl6 36 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ≠ (𝑛 − 1)))
261 eleq1 2857 . . . . . . . . 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 236 . . . . . . . 8 (sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) = (𝑛 − 1) → (𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}))
263262necon3bi 2990 . . . . . . 7 (¬ (𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ≠ (𝑛 − 1))
264260, 263pm2.61d1 182 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ≠ (𝑛 − 1))
2652, 12, 48, 92, 264, 176poimirlem28 38222 . . . . 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 12510 . . . . . . . . . . . 12 0 ∈ V
267 fzo0ssnn0 13775 . . . . . . . . . . . 12 (0..^𝑘) ⊆ ℕ0
268 mapss 8887 . . . . . . . . . . . 12 ((ℕ0 ∈ V ∧ (0..^𝑘) ⊆ ℕ0) → ((0..^𝑘) ↑m (1...𝑁)) ⊆ (ℕ0m (1...𝑁)))
269266, 267, 268mp2an 704 . . . . . . . . . . 11 ((0..^𝑘) ↑m (1...𝑁)) ⊆ (ℕ0m (1...𝑁))
270 xpss1 5681 . . . . . . . . . . 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 3939 . . . . . . . . 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 8846 . . . . . . . . . 10 ((1st𝑠) ∈ ((0..^𝑘) ↑m (1...𝑁)) → (1st𝑠):(1...𝑁)⟶(0..^𝑘))
275 frn 6714 . . . . . . . . . 10 ((1st𝑠):(1...𝑁)⟶(0..^𝑘) → ran (1st𝑠) ⊆ (0..^𝑘))
276273, 274, 2753syl 19 . . . . . . . . 9 (𝑠 ∈ (((0..^𝑘) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → ran (1st𝑠) ⊆ (0..^𝑘))
277272, 276jca 520 . . . . . . . 8 (𝑠 ∈ (((0..^𝑘) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (𝑠 ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ran (1st𝑠) ⊆ (0..^𝑘)))
278277anim1i 626 . . . . . . 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 473 . . . . . . 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 221 . . . . . 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 3104 . . . . 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 18 . . . 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 3163 . . 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 12239 . . . 4 ℕ ∈ V
285140, 266ixpconst 8905 . . . . . . 7 X𝑛 ∈ (1...𝑁)ℕ0 = (ℕ0m (1...𝑁))
286 omelon 9615 . . . . . . . . . 10 ω ∈ On
287 nn0ennn 14015 . . . . . . . . . . 11 0 ≈ ℕ
288 nnenom 14016 . . . . . . . . . . 11 ℕ ≈ ω
289287, 288entr2i 9006 . . . . . . . . . 10 ω ≈ ℕ0
290 isnumi 9932 . . . . . . . . . 10 ((ω ∈ On ∧ ω ≈ ℕ0) → ℕ0 ∈ dom card)
291286, 289, 290mp2an 704 . . . . . . . . 9 0 ∈ dom card
292291rgenw 3089 . . . . . . . 8 𝑛 ∈ (1...𝑁)ℕ0 ∈ dom card
293 finixpnum 38179 . . . . . . . 8 (((1...𝑁) ∈ Fin ∧ ∀𝑛 ∈ (1...𝑁)ℕ0 ∈ dom card) → X𝑛 ∈ (1...𝑁)ℕ0 ∈ dom card)
29424, 292, 293mp2an 704 . . . . . . 7 X𝑛 ∈ (1...𝑁)ℕ0 ∈ dom card
295285, 294eqeltrri 2866 . . . . . 6 (ℕ0m (1...𝑁)) ∈ dom card
296140, 140mapval 8835 . . . . . . . . 9 ((1...𝑁) ↑m (1...𝑁)) = {𝑓𝑓:(1...𝑁)⟶(1...𝑁)}
297 mapfi 9305 . . . . . . . . . 10 (((1...𝑁) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((1...𝑁) ↑m (1...𝑁)) ∈ Fin)
29824, 24, 297mp2an 704 . . . . . . . . 9 ((1...𝑁) ↑m (1...𝑁)) ∈ Fin
299296, 298eqeltrri 2866 . . . . . . . 8 {𝑓𝑓:(1...𝑁)⟶(1...𝑁)} ∈ Fin
300 f1of 6821 . . . . . . . . 9 (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑓:(1...𝑁)⟶(1...𝑁))
301300ss2abi 4026 . . . . . . . 8 {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ⊆ {𝑓𝑓:(1...𝑁)⟶(1...𝑁)}
302 ssfi 9157 . . . . . . . 8 (({𝑓𝑓:(1...𝑁)⟶(1...𝑁)} ∈ Fin ∧ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ⊆ {𝑓𝑓:(1...𝑁)⟶(1...𝑁)}) → {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ∈ Fin)
303299, 301, 302mp2an 704 . . . . . . 7 {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ∈ Fin
304 finnum 9934 . . . . . . 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 9937 . . . . . 6 (((ℕ0m (1...𝑁)) ∈ dom card ∧ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ∈ dom card) → ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∈ dom card)
307295, 305, 306mp2an 704 . . . . 5 ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∈ dom card
308 ssrab2 4040 . . . . . . . 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 3089 . . . . . . 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 4977 . . . . . . 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 12244 . . . . . . 7 1 ∈ ℕ
313 ne0i 4300 . . . . . . 7 (1 ∈ ℕ → ℕ ≠ ∅)
314 iunconst 4968 . . . . . . 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 3991 . . . . 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 10023 . . . . 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 704 . . . 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 6882 . . . . . . . 8 (𝑠 = (𝑔𝑘) → (1st𝑠) = (1st ‘(𝑔𝑘)))
320319rneqd 5929 . . . . . . 7 (𝑠 = (𝑔𝑘) → ran (1st𝑠) = ran (1st ‘(𝑔𝑘)))
321320sseq1d 3974 . . . . . 6 (𝑠 = (𝑔𝑘) → (ran (1st𝑠) ⊆ (0..^𝑘) ↔ ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘)))
322 fveq2 6882 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = (𝑔𝑘) → (2nd𝑠) = (2nd ‘(𝑔𝑘)))
323322imaeq1d 6062 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = (𝑔𝑘) → ((2nd𝑠) “ (1...𝑗)) = ((2nd ‘(𝑔𝑘)) “ (1...𝑗)))
324323xpeq1d 5691 . . . . . . . . . . . . . . . . . . 19 (𝑠 = (𝑔𝑘) → (((2nd𝑠) “ (1...𝑗)) × {1}) = (((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}))
325322imaeq1d 6062 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = (𝑔𝑘) → ((2nd𝑠) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)))
326325xpeq1d 5691 . . . . . . . . . . . . . . . . . . 19 (𝑠 = (𝑔𝑘) → (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))
327324, 326uneq12d 4129 . . . . . . . . . . . . . . . . . 18 (𝑠 = (𝑔𝑘) → ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
328319, 327oveq12d 7429 . . . . . . . . . . . . . . . . 17 (𝑠 = (𝑔𝑘) → ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))))
329328fvoveq1d 7433 . . . . . . . . . . . . . . . 16 (𝑠 = (𝑔𝑘) → (𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))) = (𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))))
330329fveq1d 6884 . . . . . . . . . . . . . . 15 (𝑠 = (𝑔𝑘) → ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) = ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏))
331330breq2d 5123 . . . . . . . . . . . . . 14 (𝑠 = (𝑔𝑘) → (0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ↔ 0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏)))
332328fveq1d 6884 . . . . . . . . . . . . . . 15 (𝑠 = (𝑔𝑘) → (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) = (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏))
333332neeq1d 3023 . . . . . . . . . . . . . 14 (𝑠 = (𝑔𝑘) → ((((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0 ↔ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0))
334331, 333anbi12d 643 . . . . . . . . . . . . 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 3194 . . . . . . . . . . . 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 3429 . . . . . . . . . . 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 4128 . . . . . . . . . 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 9406 . . . . . . . . 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 2780 . . . . . . . 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 3195 . . . . . . 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 3194 . . . . . 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 643 . . . . 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 10463 . . . 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 1477 . . 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 18 . 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 738 . . . 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 738 . . . 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 2769 . . . 4 ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑛) = ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑛)
351 simplr 780 . . . 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 487 . . . . . . 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 3108 . . . . . 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 486 . . . . 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 6887 . . . . . . . 8 (𝑘 = 𝑝 → (1st ‘(𝑔𝑘)) = (1st ‘(𝑔𝑝)))
356355rneqd 5929 . . . . . . 7 (𝑘 = 𝑝 → ran (1st ‘(𝑔𝑘)) = ran (1st ‘(𝑔𝑝)))
357 oveq2 7419 . . . . . . 7 (𝑘 = 𝑝 → (0..^𝑘) = (0..^𝑝))
358356, 357sseq12d 3976 . . . . . 6 (𝑘 = 𝑝 → (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ↔ ran (1st ‘(𝑔𝑝)) ⊆ (0..^𝑝)))
359358rspccva 3587 . . . . 5 ((∀𝑘 ∈ ℕ ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ 𝑝 ∈ ℕ) → ran (1st ‘(𝑔𝑝)) ⊆ (0..^𝑝))
360354, 359sylan 591 . . . 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 778 . . . . . 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 591 . . . . 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 2769 . . . . 5 ((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) = ((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))
365 simpr 489 . . . . . . . 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 3108 . . . . . . 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 486 . . . . . 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 6887 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 𝑝 → (2nd ‘(𝑔𝑘)) = (2nd ‘(𝑔𝑝)))
369368imaeq1d 6062 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑝 → ((2nd ‘(𝑔𝑘)) “ (1...𝑗)) = ((2nd ‘(𝑔𝑝)) “ (1...𝑗)))
370369xpeq1d 5691 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑝 → (((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) = (((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}))
371368imaeq1d 6062 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑝 → ((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)))
372371xpeq1d 5691 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑝 → (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))
373370, 372uneq12d 4129 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑝 → ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))
374355, 373oveq12d 7429 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑝 → ((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))))
375 sneq 4602 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑝 → {𝑘} = {𝑝})
376375xpeq2d 5692 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑝 → ((1...𝑁) × {𝑘}) = ((1...𝑁) × {𝑝}))
377374, 376oveq12d 7429 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑝 → (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) = (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))
378377fveq2d 6886 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑝 → (𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))) = (𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝}))))
379378fveq1d 6884 . . . . . . . . . . . . . . 15 (𝑘 = 𝑝 → ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) = ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏))
380379breq2d 5123 . . . . . . . . . . . . . 14 (𝑘 = 𝑝 → (0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ↔ 0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏)))
381374fveq1d 6884 . . . . . . . . . . . . . . 15 (𝑘 = 𝑝 → (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) = (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏))
382381neeq1d 3023 . . . . . . . . . . . . . 14 (𝑘 = 𝑝 → ((((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0 ↔ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0))
383380, 382anbi12d 643 . . . . . . . . . . . . 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 3194 . . . . . . . . . . . 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 3429 . . . . . . . . . . 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 4128 . . . . . . . . . 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 9406 . . . . . . . . 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 2780 . . . . . . . 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 3195 . . . . . . 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 2773 . . . . . . . . 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 3195 . . . . . . . 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 7419 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑚 → (1...𝑗) = (1...𝑚))
393392imaeq2d 6063 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑚 → ((2nd ‘(𝑔𝑝)) “ (1...𝑗)) = ((2nd ‘(𝑔𝑝)) “ (1...𝑚)))
394393xpeq1d 5691 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑚 → (((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) = (((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}))
395 oveq1 7418 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑚 → (𝑗 + 1) = (𝑚 + 1))
396395oveq1d 7426 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑚 → ((𝑗 + 1)...𝑁) = ((𝑚 + 1)...𝑁))
397396imaeq2d 6063 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑚 → ((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)))
398397xpeq1d 5691 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑚 → (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))
399394, 398uneq12d 4129 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑚 → ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))
400399oveq2d 7427 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑚 → ((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))))
401400fvoveq1d 7433 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑚 → (𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝}))) = (𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝}))))
402401fveq1d 6884 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑚 → ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) = ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏))
403402breq2d 5123 . . . . . . . . . . . . . . 15 (𝑗 = 𝑚 → (0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ↔ 0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏)))
404400fveq1d 6884 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑚 → (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) = (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏))
405404neeq1d 3023 . . . . . . . . . . . . . . 15 (𝑗 = 𝑚 → ((((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0 ↔ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0))
406403, 405anbi12d 643 . . . . . . . . . . . . . 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 3194 . . . . . . . . . . . . 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 3429 . . . . . . . . . . . 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 4128 . . . . . . . . . . 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 9406 . . . . . . . . . 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 2780 . . . . . . . . 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 3250 . . . . . . . 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 290 . . . . . . 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 3599 . . . . . 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 515 . . . . 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 38225 . . . 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 38224 . . 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 471 . 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 1962 1 (𝜑 → ∃𝑐𝐼𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 400  wo 860  w3a 1101   = wceq 1567  wex 1806  wcel 2149  {cab 2747  wne 2964  wral 3085  wrex 3095  {crab 3422  Vcvv 3461  cun 3909  wss 3911  c0 4292  {csn 4592  {cpr 4594   ciun 4958   class class class wbr 5111   Or wor 5569   × cxp 5660  ccnv 5661  dom cdm 5662  ran crn 5663  cima 5665  Oncon0 6361   Fn wfn 6532  wf 6533  1-1-ontowf1o 6536  cfv 6537  (class class class)co 7411  f cof 7673  ωcom 7862  1st c1st 7984  2nd c2nd 7985  m cmap 8824  Xcixp 8895  cen 8940  Fincfn 8943  supcsup 9400  cardccrd 9921  cc 11098  cr 11099  0cc0 11100  1c1 11101   + caddc 11103   · cmul 11105   < clt 11243  cle 11244  cmin 11441   / cdiv 11871  cn 12233  0cn0 12504  cz 12591  cuz 12862  +crp 13016  (,)cioo 13372  [,]cicc 13375  ...cfz 13535  ..^cfzo 13682  t crest 17473  topGenctg 17490  tcpt 17491   Cn ccn 23350
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-inf2 9610  ax-cnex 11156  ax-resscn 11157  ax-1cn 11158  ax-icn 11159  ax-addcl 11160  ax-addrcl 11161  ax-mulcl 11162  ax-mulrcl 11163  ax-mulcom 11164  ax-addass 11165  ax-mulass 11166  ax-distr 11167  ax-i2m1 11168  ax-1ne0 11169  ax-1rid 11170  ax-rnegex 11171  ax-rrecex 11172  ax-cnre 11173  ax-pre-lttri 11174  ax-pre-lttrn 11175  ax-pre-ltadd 11176  ax-pre-mulgt0 11177  ax-pre-sup 11178
This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rmo 3375  df-reu 3376  df-rab 3423  df-v 3463  df-sbc 3752  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4491  df-pw 4567  df-sn 4593  df-pr 4595  df-tp 4597  df-op 4599  df-uni 4875  df-int 4915  df-iun 4960  df-iin 4961  df-disj 5079  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-se 5616  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-of 7675  df-om 7863  df-1st 7986  df-2nd 7987  df-frecs 8278  df-wrecs 8309  df-recs 8358  df-rdg 8397  df-1o 8453  df-2o 8454  df-oadd 8457  df-omul 8458  df-er 8694  df-map 8826  df-pm 8827  df-ixp 8896  df-en 8944  df-dom 8945  df-sdom 8946  df-fin 8947  df-fi 9371  df-sup 9402  df-inf 9403  df-oi 9472  df-dju 9887  df-card 9925  df-acn 9928  df-pnf 11245  df-mnf 11246  df-xr 11247  df-ltxr 11248  df-le 11249  df-sub 11443  df-neg 11444  df-div 11872  df-nn 12234  df-2 12303  df-3 12304  df-n0 12505  df-xnn0 12578  df-z 12592  df-uz 12863  df-q 12973  df-rp 13017  df-xneg 13137  df-xadd 13138  df-xmul 13139  df-ioo 13376  df-icc 13379  df-fz 13536  df-fzo 13683  df-fl 13825  df-seq 14038  df-exp 14098  df-fac 14310  df-bc 14339  df-hash 14367  df-cj 15150  df-re 15151  df-im 15152  df-sqrt 15286  df-abs 15287  df-clim 15539  df-sum 15738  df-dvds 16311  df-rest 17475  df-topgen 17496  df-pt 17497  df-psmet 21483  df-xmet 21484  df-met 21485  df-bl 21486  df-mopn 21487  df-top 23020  df-topon 23037  df-bases 23072  df-cld 23145  df-ntr 23146  df-cls 23147  df-lp 23262  df-cn 23353  df-cnp 23354  df-t1 23440  df-haus 23441  df-cmp 23513  df-tx 23688  df-hmeo 23881  df-hmph 23882  df-ii 25005
This theorem is referenced by:  poimir  38227
  Copyright terms: Public domain W3C validator