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

Theorem poimirlem32 35108
 Description: Lemma for poimir 35109, combining poimirlem28 35104, poimirlem30 35106, and poimirlem31 35107 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 484 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 𝑁 ∈ ℕ)
3 fvoveq1 7159 . . . . . . . . . . . . 13 (𝑝 = ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝐹‘(𝑝f / ((1...𝑁) × {𝑘}))) = (𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))))
43fveq1d 6648 . . . . . . . . . . . 12 (𝑝 = ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) = ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏))
54breq2d 5043 . . . . . . . . . . 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 6645 . . . . . . . . . . . 12 (𝑝 = ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝑝𝑏) = (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏))
76neeq1d 3046 . . . . . . . . . . 11 (𝑝 = ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → ((𝑝𝑏) ≠ 0 ↔ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0))
85, 7anbi12d 633 . . . . . . . . . 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 3162 . . . . . . . . 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 3427 . . . . . . . 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 4090 . . . . . . 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 8897 . . . . . 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 11946 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℕ0)
14 0elfz 13002 . . . . . . . . . . 11 (𝑁 ∈ ℕ0 → 0 ∈ (0...𝑁))
1513, 14syl 17 . . . . . . . . . 10 (𝜑 → 0 ∈ (0...𝑁))
1615snssd 4702 . . . . . . . . 9 (𝜑 → {0} ⊆ (0...𝑁))
17 ssrab2 4007 . . . . . . . . . . 11 {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ⊆ (1...𝑁)
18 fz1ssfz0 13001 . . . . . . . . . . 11 (1...𝑁) ⊆ (0...𝑁)
1917, 18sstri 3924 . . . . . . . . . 10 {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ⊆ (0...𝑁)
2019a1i 11 . . . . . . . . 9 (𝜑 → {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ⊆ (0...𝑁))
2116, 20unssd 4113 . . . . . . . 8 (𝜑 → ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ⊆ (0...𝑁))
22 ltso 10713 . . . . . . . . 9 < Or ℝ
23 snfi 8580 . . . . . . . . . . 11 {0} ∈ Fin
24 fzfi 13338 . . . . . . . . . . . 12 (1...𝑁) ∈ Fin
25 rabfi 8730 . . . . . . . . . . . 12 ((1...𝑁) ∈ Fin → {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ∈ Fin)
2624, 25ax-mp 5 . . . . . . . . . . 11 {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ∈ Fin
27 unfi 8772 . . . . . . . . . . 11 (({0} ∈ Fin ∧ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ∈ Fin) → ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ∈ Fin)
2823, 26, 27mp2an 691 . . . . . . . . . 10 ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ∈ Fin
29 c0ex 10627 . . . . . . . . . . . 12 0 ∈ V
3029snid 4561 . . . . . . . . . . 11 0 ∈ {0}
31 elun1 4103 . . . . . . . . . . 11 (0 ∈ {0} → 0 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}))
32 ne0i 4250 . . . . . . . . . . 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 10636 . . . . . . . . . . . . 13 ((𝜑𝑁 ∈ ℕ) → 0 ∈ ℝ)
3534snssd 4702 . . . . . . . . . . . 12 ((𝜑𝑁 ∈ ℕ) → {0} ⊆ ℝ)
361, 35ax-mp 5 . . . . . . . . . . 11 {0} ⊆ ℝ
37 elfzelz 12905 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℤ)
3837ssriv 3919 . . . . . . . . . . . . 13 (1...𝑁) ⊆ ℤ
39 zssre 11979 . . . . . . . . . . . . 13 ℤ ⊆ ℝ
4038, 39sstri 3924 . . . . . . . . . . . 12 (1...𝑁) ⊆ ℝ
4117, 40sstri 3924 . . . . . . . . . . 11 {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ⊆ ℝ
4236, 41unssi 4112 . . . . . . . . . 10 ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ⊆ ℝ
4328, 33, 423pm3.2i 1336 . . . . . . . . 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 8920 . . . . . . . . 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 691 . . . . . . . 8 sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})
46 ssel 3908 . . . . . . . 8 (({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ⊆ (0...𝑁) → (sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ∈ (0...𝑁)))
4721, 45, 46mpisyl 21 . . . . . . 7 (𝜑 → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ∈ (0...𝑁))
4847ad2antrr 725 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑝:(1...𝑁)⟶(0...𝑘)) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ∈ (0...𝑁))
49 elfznn 12934 . . . . . . . . 9 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ)
50 nngt0 11659 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → 0 < 𝑛)
5150adantr 484 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) → 0 < 𝑛)
52 simpr 488 . . . . . . . . . . . . . 14 ((0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → (𝑝𝑏) ≠ 0)
5352ralimi 3128 . . . . . . . . . . . . 13 (∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑠)(𝑝𝑏) ≠ 0)
54 elfznn 12934 . . . . . . . . . . . . . 14 (𝑠 ∈ (1...𝑁) → 𝑠 ∈ ℕ)
55 nnre 11635 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
56 nnre 11635 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ℕ → 𝑠 ∈ ℝ)
57 lenlt 10711 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℝ ∧ 𝑠 ∈ ℝ) → (𝑛𝑠 ↔ ¬ 𝑠 < 𝑛))
5855, 56, 57syl2an 598 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ) → (𝑛𝑠 ↔ ¬ 𝑠 < 𝑛))
59 elfz1b 12974 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ (1...𝑠) ↔ (𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ ∧ 𝑛𝑠))
6059biimpri 231 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ ∧ 𝑛𝑠) → 𝑛 ∈ (1...𝑠))
61603expia 1118 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ) → (𝑛𝑠𝑛 ∈ (1...𝑠)))
6258, 61sylbird 263 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ) → (¬ 𝑠 < 𝑛𝑛 ∈ (1...𝑠)))
63 fveq2 6646 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = 𝑛 → (𝑝𝑏) = (𝑝𝑛))
6463eqeq1d 2800 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = 𝑛 → ((𝑝𝑏) = 0 ↔ (𝑝𝑛) = 0))
6564rspcev 3571 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ (1...𝑠) ∧ (𝑝𝑛) = 0) → ∃𝑏 ∈ (1...𝑠)(𝑝𝑏) = 0)
6665expcom 417 . . . . . . . . . . . . . . . . . 18 ((𝑝𝑛) = 0 → (𝑛 ∈ (1...𝑠) → ∃𝑏 ∈ (1...𝑠)(𝑝𝑏) = 0))
6762, 66sylan9 511 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ) ∧ (𝑝𝑛) = 0) → (¬ 𝑠 < 𝑛 → ∃𝑏 ∈ (1...𝑠)(𝑝𝑏) = 0))
6867an32s 651 . . . . . . . . . . . . . . . 16 (((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) ∧ 𝑠 ∈ ℕ) → (¬ 𝑠 < 𝑛 → ∃𝑏 ∈ (1...𝑠)(𝑝𝑏) = 0))
69 nne 2991 . . . . . . . . . . . . . . . . . 18 (¬ (𝑝𝑏) ≠ 0 ↔ (𝑝𝑏) = 0)
7069rexbii 3210 . . . . . . . . . . . . . . . . 17 (∃𝑏 ∈ (1...𝑠) ¬ (𝑝𝑏) ≠ 0 ↔ ∃𝑏 ∈ (1...𝑠)(𝑝𝑏) = 0)
71 rexnal 3201 . . . . . . . . . . . . . . . . 17 (∃𝑏 ∈ (1...𝑠) ¬ (𝑝𝑏) ≠ 0 ↔ ¬ ∀𝑏 ∈ (1...𝑠)(𝑝𝑏) ≠ 0)
7270, 71bitr3i 280 . . . . . . . . . . . . . . . 16 (∃𝑏 ∈ (1...𝑠)(𝑝𝑏) = 0 ↔ ¬ ∀𝑏 ∈ (1...𝑠)(𝑝𝑏) ≠ 0)
7368, 72syl6ib 254 . . . . . . . . . . . . . . 15 (((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) ∧ 𝑠 ∈ ℕ) → (¬ 𝑠 < 𝑛 → ¬ ∀𝑏 ∈ (1...𝑠)(𝑝𝑏) ≠ 0))
7473con4d 115 . . . . . . . . . . . . . 14 (((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) ∧ 𝑠 ∈ ℕ) → (∀𝑏 ∈ (1...𝑠)(𝑝𝑏) ≠ 0 → 𝑠 < 𝑛))
7554, 74sylan2 595 . . . . . . . . . . . . 13 (((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) ∧ 𝑠 ∈ (1...𝑁)) → (∀𝑏 ∈ (1...𝑠)(𝑝𝑏) ≠ 0 → 𝑠 < 𝑛))
7653, 75syl5 34 . . . . . . . . . . . 12 (((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) ∧ 𝑠 ∈ (1...𝑁)) → (∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → 𝑠 < 𝑛))
7776ralrimiva 3149 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) → ∀𝑠 ∈ (1...𝑁)(∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → 𝑠 < 𝑛))
78 ralunb 4118 . . . . . . . . . . . 12 (∀𝑠 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})𝑠 < 𝑛 ↔ (∀𝑠 ∈ {0}𝑠 < 𝑛 ∧ ∀𝑠 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}𝑠 < 𝑛))
79 breq1 5034 . . . . . . . . . . . . . 14 (𝑠 = 0 → (𝑠 < 𝑛 ↔ 0 < 𝑛))
8029, 79ralsn 4579 . . . . . . . . . . . . 13 (∀𝑠 ∈ {0}𝑠 < 𝑛 ↔ 0 < 𝑛)
81 oveq2 7144 . . . . . . . . . . . . . . 15 (𝑎 = 𝑠 → (1...𝑎) = (1...𝑠))
8281raleqdv 3364 . . . . . . . . . . . . . 14 (𝑎 = 𝑠 → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
8382ralrab 3633 . . . . . . . . . . . . 13 (∀𝑠 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}𝑠 < 𝑛 ↔ ∀𝑠 ∈ (1...𝑁)(∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → 𝑠 < 𝑛))
8480, 83anbi12i 629 . . . . . . . . . . . 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 586 . . . . . . . . . 10 ((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) → ∀𝑠 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})𝑠 < 𝑛)
87 breq1 5034 . . . . . . . . . . 11 (𝑠 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) → (𝑠 < 𝑛 ↔ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < 𝑛))
8887rspcva 3569 . . . . . . . . . 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 590 . . . . . . . . 9 ((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < 𝑛)
9049, 89sylan 583 . . . . . . . 8 ((𝑛 ∈ (1...𝑁) ∧ (𝑝𝑛) = 0) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < 𝑛)
91903adant2 1128 . . . . . . 7 ((𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 0) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < 𝑛)
9291adantl 485 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 0)) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < 𝑛)
9337zred 12078 . . . . . . . . . . 11 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℝ)
94933ad2ant1 1130 . . . . . . . . . 10 ((𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) → 𝑛 ∈ ℝ)
9594adantl 485 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → 𝑛 ∈ ℝ)
96 simpr1 1191 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → 𝑛 ∈ (1...𝑁))
97 simpll 766 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → 𝜑)
98 simplr 768 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → 𝑘 ∈ ℕ)
99 elfzelz 12905 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ (0...𝑘) → 𝑖 ∈ ℤ)
10099zred 12078 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ (0...𝑘) → 𝑖 ∈ ℝ)
101 nndivre 11669 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ ℝ)
102100, 101sylan 583 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ ℝ)
103 elfzle1 12908 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ (0...𝑘) → 0 ≤ 𝑖)
104100, 103jca 515 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ (0...𝑘) → (𝑖 ∈ ℝ ∧ 0 ≤ 𝑖))
105 nnrp 12391 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
106105rpregt0d 12428 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ ℕ → (𝑘 ∈ ℝ ∧ 0 < 𝑘))
107 divge0 11501 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑖 ∈ ℝ ∧ 0 ≤ 𝑖) ∧ (𝑘 ∈ ℝ ∧ 0 < 𝑘)) → 0 ≤ (𝑖 / 𝑘))
108104, 106, 107syl2an 598 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝑖 / 𝑘))
109 elfzle2 12909 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ (0...𝑘) → 𝑖𝑘)
110109adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑖𝑘)
111100adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑖 ∈ ℝ)
112 1red 10634 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 1 ∈ ℝ)
113105adantl 485 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ+)
114111, 112, 113ledivmuld 12475 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑖 / 𝑘) ≤ 1 ↔ 𝑖 ≤ (𝑘 · 1)))
115 nncn 11636 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
116115mulid1d 10650 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ ℕ → (𝑘 · 1) = 𝑘)
117116breq2d 5043 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ ℕ → (𝑖 ≤ (𝑘 · 1) ↔ 𝑖𝑘))
118117adantl 485 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 ≤ (𝑘 · 1) ↔ 𝑖𝑘))
119114, 118bitrd 282 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑖 / 𝑘) ≤ 1 ↔ 𝑖𝑘))
120110, 119mpbird 260 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ≤ 1)
121 elicc01 12847 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖 / 𝑘) ∈ (0[,]1) ↔ ((𝑖 / 𝑘) ∈ ℝ ∧ 0 ≤ (𝑖 / 𝑘) ∧ (𝑖 / 𝑘) ≤ 1))
122102, 108, 120, 121syl3anbrc 1340 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ (0[,]1))
123122ancoms 462 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑘)) → (𝑖 / 𝑘) ∈ (0[,]1))
124 elsni 4542 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ {𝑘} → 𝑗 = 𝑘)
125124oveq2d 7152 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ {𝑘} → (𝑖 / 𝑗) = (𝑖 / 𝑘))
126125eleq1d 2874 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ {𝑘} → ((𝑖 / 𝑗) ∈ (0[,]1) ↔ (𝑖 / 𝑘) ∈ (0[,]1)))
127123, 126syl5ibrcom 250 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑘)) → (𝑗 ∈ {𝑘} → (𝑖 / 𝑗) ∈ (0[,]1)))
128127impr 458 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ ∧ (𝑖 ∈ (0...𝑘) ∧ 𝑗 ∈ {𝑘})) → (𝑖 / 𝑗) ∈ (0[,]1))
12998, 128sylan 583 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) ∧ (𝑖 ∈ (0...𝑘) ∧ 𝑗 ∈ {𝑘})) → (𝑖 / 𝑗) ∈ (0[,]1))
130 simprr 772 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → 𝑝:(1...𝑁)⟶(0...𝑘))
131 vex 3444 . . . . . . . . . . . . . . . . . 18 𝑘 ∈ V
132131fconst 6540 . . . . . . . . . . . . . . . . 17 ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘}
133132a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘})
134 fzfid 13339 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → (1...𝑁) ∈ Fin)
135 inidm 4145 . . . . . . . . . . . . . . . 16 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
136129, 130, 133, 134, 134, 135off 7407 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → (𝑝f / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
137 poimir.i . . . . . . . . . . . . . . . . 17 𝐼 = ((0[,]1) ↑m (1...𝑁))
138137eleq2i 2881 . . . . . . . . . . . . . . . 16 ((𝑝f / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ (𝑝f / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑m (1...𝑁)))
139 ovex 7169 . . . . . . . . . . . . . . . . 17 (0[,]1) ∈ V
140 ovex 7169 . . . . . . . . . . . . . . . . 17 (1...𝑁) ∈ V
141139, 140elmap 8421 . . . . . . . . . . . . . . . 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 1168 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → (𝑝f / ((1...𝑁) × {𝑘})) ∈ 𝐼)
145 3anass 1092 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) ↔ (𝑛 ∈ (1...𝑁) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)))
146 ancom 464 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (1...𝑁) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) ↔ ((𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) ∧ 𝑛 ∈ (1...𝑁)))
147145, 146bitri 278 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) ↔ ((𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) ∧ 𝑛 ∈ (1...𝑁)))
148 ffn 6488 . . . . . . . . . . . . . . . . . 18 (𝑝:(1...𝑁)⟶(0...𝑘) → 𝑝 Fn (1...𝑁))
149148ad2antrl 727 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → 𝑝 Fn (1...𝑁))
150 fnconstg 6542 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ V → ((1...𝑁) × {𝑘}) Fn (1...𝑁))
151131, 150mp1i 13 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ((1...𝑁) × {𝑘}) Fn (1...𝑁))
152 fzfid 13339 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → (1...𝑁) ∈ Fin)
153 simplrr 777 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑝𝑛) = 𝑘)
154131fvconst2 6944 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {𝑘})‘𝑛) = 𝑘)
155154adantl 485 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {𝑘})‘𝑛) = 𝑘)
156149, 151, 152, 152, 135, 153, 155ofval 7400 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = (𝑘 / 𝑘))
157156anasss 470 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ) ∧ ((𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) ∧ 𝑛 ∈ (1...𝑁))) → ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = (𝑘 / 𝑘))
158147, 157sylan2b 596 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = (𝑘 / 𝑘))
159 nnne0 11662 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ → 𝑘 ≠ 0)
160115, 159dividd 11406 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ → (𝑘 / 𝑘) = 1)
161160ad2antlr 726 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → (𝑘 / 𝑘) = 1)
162158, 161eqtrd 2833 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = 1)
163 ovex 7169 . . . . . . . . . . . . . 14 (𝑝f / ((1...𝑁) × {𝑘})) ∈ V
164 eleq1 2877 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → (𝑧𝐼 ↔ (𝑝f / ((1...𝑁) × {𝑘})) ∈ 𝐼))
165 fveq1 6645 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → (𝑧𝑛) = ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛))
166165eqeq1d 2800 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → ((𝑧𝑛) = 1 ↔ ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = 1))
167164, 1663anbi23d 1436 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → ((𝑛 ∈ (1...𝑁) ∧ 𝑧𝐼 ∧ (𝑧𝑛) = 1) ↔ (𝑛 ∈ (1...𝑁) ∧ (𝑝f / ((1...𝑁) × {𝑘})) ∈ 𝐼 ∧ ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = 1)))
168167anbi2d 631 . . . . . . . . . . . . . . 15 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧𝐼 ∧ (𝑧𝑛) = 1)) ↔ (𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ (𝑝f / ((1...𝑁) × {𝑘})) ∈ 𝐼 ∧ ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = 1))))
169 fveq2 6646 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → (𝐹𝑧) = (𝐹‘(𝑝f / ((1...𝑁) × {𝑘}))))
170169fveq1d 6648 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → ((𝐹𝑧)‘𝑛) = ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛))
171170breq2d 5043 . . . . . . . . . . . . . . 15 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → (0 ≤ ((𝐹𝑧)‘𝑛) ↔ 0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛)))
172168, 171imbi12d 348 . . . . . . . . . . . . . 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 3507 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ (𝑝f / ((1...𝑁) × {𝑘})) ∈ 𝐼 ∧ ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = 1)) → 0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛))
17597, 96, 144, 162, 174syl13anc 1369 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → 0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛))
176 simpr 488 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
177 simp3 1135 . . . . . . . . . . . . 13 ((𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) → (𝑝𝑛) = 𝑘)
178 neeq1 3049 . . . . . . . . . . . . . . 15 ((𝑝𝑛) = 𝑘 → ((𝑝𝑛) ≠ 0 ↔ 𝑘 ≠ 0))
179159, 178syl5ibrcom 250 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → ((𝑝𝑛) = 𝑘 → (𝑝𝑛) ≠ 0))
180179imp 410 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ∧ (𝑝𝑛) = 𝑘) → (𝑝𝑛) ≠ 0)
181176, 177, 180syl2an 598 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → (𝑝𝑛) ≠ 0)
182 vex 3444 . . . . . . . . . . . . 13 𝑛 ∈ V
183 fveq2 6646 . . . . . . . . . . . . . . 15 (𝑏 = 𝑛 → ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) = ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛))
184183breq2d 5043 . . . . . . . . . . . . . 14 (𝑏 = 𝑛 → (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ↔ 0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛)))
18563neeq1d 3046 . . . . . . . . . . . . . 14 (𝑏 = 𝑛 → ((𝑝𝑏) ≠ 0 ↔ (𝑝𝑛) ≠ 0))
186184, 185anbi12d 633 . . . . . . . . . . . . 13 (𝑏 = 𝑛 → ((0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛) ∧ (𝑝𝑛) ≠ 0)))
187182, 186ralsn 4579 . . . . . . . . . . . 12 (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛) ∧ (𝑝𝑛) ≠ 0))
188175, 181, 187sylanbrc 586 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))
18937zcnd 12079 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ)
190 1cnd 10628 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...𝑁) → 1 ∈ ℂ)
191189, 190subeq0ad 10999 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) = 0 ↔ 𝑛 = 1))
192191biimpcd 252 . . . . . . . . . . . . . . . . 17 ((𝑛 − 1) = 0 → (𝑛 ∈ (1...𝑁) → 𝑛 = 1))
193 1z 12003 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℤ
194 fzsn 12947 . . . . . . . . . . . . . . . . . . . . 21 (1 ∈ ℤ → (1...1) = {1})
195193, 194ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (1...1) = {1}
196 oveq2 7144 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 1 → (1...𝑛) = (1...1))
197 sneq 4535 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 1 → {𝑛} = {1})
198195, 196, 1973eqtr4a 2859 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 1 → (1...𝑛) = {𝑛})
199198raleqdv 3364 . . . . . . . . . . . . . . . . . 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 35 . . . . . . . . . . . . . . . 16 ((𝑛 − 1) = 0 → (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
202 ralun 4119 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)) → ∀𝑏 ∈ ((1...(𝑛 − 1)) ∪ {𝑛})(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))
203 npcan1 11057 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ℂ → ((𝑛 − 1) + 1) = 𝑛)
204189, 203syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) + 1) = 𝑛)
205 elfzuz 12901 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ (ℤ‘1))
206204, 205eqeltrd 2890 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) + 1) ∈ (ℤ‘1))
207 peano2zm 12016 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ℤ → (𝑛 − 1) ∈ ℤ)
208 uzid 12249 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 − 1) ∈ ℤ → (𝑛 − 1) ∈ (ℤ‘(𝑛 − 1)))
209 peano2uz 12292 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 − 1) ∈ (ℤ‘(𝑛 − 1)) → ((𝑛 − 1) + 1) ∈ (ℤ‘(𝑛 − 1)))
21037, 207, 208, 2094syl 19 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) + 1) ∈ (ℤ‘(𝑛 − 1)))
211204, 210eqeltrrd 2891 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ (ℤ‘(𝑛 − 1)))
212 fzsplit2 12930 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑛 − 1) + 1) ∈ (ℤ‘1) ∧ 𝑛 ∈ (ℤ‘(𝑛 − 1))) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)))
213206, 211, 212syl2anc 587 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (1...𝑁) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)))
214204oveq1d 7151 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...𝑁) → (((𝑛 − 1) + 1)...𝑛) = (𝑛...𝑛))
215 fzsn 12947 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ℤ → (𝑛...𝑛) = {𝑛})
21637, 215syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...𝑁) → (𝑛...𝑛) = {𝑛})
217214, 216eqtrd 2833 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (1...𝑁) → (((𝑛 − 1) + 1)...𝑛) = {𝑛})
218217uneq2d 4090 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (1...𝑁) → ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)) = ((1...(𝑛 − 1)) ∪ {𝑛}))
219213, 218eqtrd 2833 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ (1...𝑁) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ {𝑛}))
220219raleqdv 3364 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ ∀𝑏 ∈ ((1...(𝑛 − 1)) ∪ {𝑛})(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
221202, 220syl5ibr 249 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...𝑁) → ((∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
222221expd 419 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
223222com12 32 . . . . . . . . . . . . . . . . 17 (∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
224223adantl 485 . . . . . . . . . . . . . . . 16 (((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)) → (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
225201, 224jaoi 854 . . . . . . . . . . . . . . 15 (((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))) → (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
226225imdistand 574 . . . . . . . . . . . . . 14 (((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))) → ((𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)) → (𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
227226com12 32 . . . . . . . . . . . . 13 ((𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)) → (((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))) → (𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
228 elun 4076 . . . . . . . . . . . . . 14 ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ↔ ((𝑛 − 1) ∈ {0} ∨ (𝑛 − 1) ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}))
229 ovex 7169 . . . . . . . . . . . . . . . 16 (𝑛 − 1) ∈ V
230229elsn 4540 . . . . . . . . . . . . . . 15 ((𝑛 − 1) ∈ {0} ↔ (𝑛 − 1) = 0)
231 oveq2 7144 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑛 − 1) → (1...𝑎) = (1...(𝑛 − 1)))
232231raleqdv 3364 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑛 − 1) → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
233232elrab 3628 . . . . . . . . . . . . . . 15 ((𝑛 − 1) ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ↔ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
234230, 233orbi12i 912 . . . . . . . . . . . . . 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 7144 . . . . . . . . . . . . . . 15 (𝑎 = 𝑛 → (1...𝑎) = (1...𝑛))
237236raleqdv 3364 . . . . . . . . . . . . . 14 (𝑎 = 𝑛 → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
238237elrab 3628 . . . . . . . . . . . . 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 4104 . . . . . . . . . . . 12 (𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} → 𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}))
241239, 240syl6 35 . . . . . . . . . . 11 ((𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)) → ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → 𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})))
24296, 188, 241syl2anc 587 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → 𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})))
243 fimaxre2 11577 . . . . . . . . . . . . 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 691 . . . . . . . . . . . 12 𝑖 ∈ ℝ ∀𝑗 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})𝑗𝑖
24542, 33, 2443pm3.2i 1336 . . . . . . . . . . 11 (({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ⊆ ℝ ∧ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ≠ ∅ ∧ ∃𝑖 ∈ ℝ ∀𝑗 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})𝑗𝑖)
246245suprubii 11606 . . . . . . . . . 10 (𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → 𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ))
247242, 246syl6 35 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → 𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )))
248 ltm1 11474 . . . . . . . . . 10 (𝑛 ∈ ℝ → (𝑛 − 1) < 𝑛)
249 peano2rem 10945 . . . . . . . . . . 11 (𝑛 ∈ ℝ → (𝑛 − 1) ∈ ℝ)
25042, 45sselii 3912 . . . . . . . . . . . 12 sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ∈ ℝ
251 ltletr 10724 . . . . . . . . . . . 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 1447 . . . . . . . . . . 11 (((𝑛 − 1) ∈ ℝ ∧ 𝑛 ∈ ℝ) → (((𝑛 − 1) < 𝑛𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )) → (𝑛 − 1) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )))
253249, 252mpancom 687 . . . . . . . . . 10 (𝑛 ∈ ℝ → (((𝑛 − 1) < 𝑛𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )) → (𝑛 − 1) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )))
254248, 253mpand 694 . . . . . . . . 9 (𝑛 ∈ ℝ → (𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) → (𝑛 − 1) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )))
25595, 247, 254sylsyld 61 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → (𝑛 − 1) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )))
256250ltnri 10741 . . . . . . . . . 10 ¬ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )
257 breq1 5034 . . . . . . . . . 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 3016 . . . . . . . 8 ((𝑛 − 1) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ≠ (𝑛 − 1))
260255, 259syl6 35 . . . . . . 7 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ≠ (𝑛 − 1)))
261 eleq1 2877 . . . . . . . . 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 3013 . . . . . . 7 (¬ (𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ≠ (𝑛 − 1))
264260, 263pm2.61d1 183 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ≠ (𝑛 − 1))
2652, 12, 48, 92, 264, 176poimirlem28 35104 . . . . 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 11894 . . . . . . . . . . . 12 0 ∈ V
267 fzo0ssnn0 13116 . . . . . . . . . . . 12 (0..^𝑘) ⊆ ℕ0
268 mapss 8439 . . . . . . . . . . . 12 ((ℕ0 ∈ V ∧ (0..^𝑘) ⊆ ℕ0) → ((0..^𝑘) ↑m (1...𝑁)) ⊆ (ℕ0m (1...𝑁)))
269266, 267, 268mp2an 691 . . . . . . . . . . 11 ((0..^𝑘) ↑m (1...𝑁)) ⊆ (ℕ0m (1...𝑁))
270 xpss1 5539 . . . . . . . . . . 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 3911 . . . . . . . . 9 (𝑠 ∈ (((0..^𝑘) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → 𝑠 ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
273 xp1st 7706 . . . . . . . . . 10 (𝑠 ∈ (((0..^𝑘) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st𝑠) ∈ ((0..^𝑘) ↑m (1...𝑁)))
274 elmapi 8414 . . . . . . . . . 10 ((1st𝑠) ∈ ((0..^𝑘) ↑m (1...𝑁)) → (1st𝑠):(1...𝑁)⟶(0..^𝑘))
275 frn 6494 . . . . . . . . . 10 ((1st𝑠):(1...𝑁)⟶(0..^𝑘) → ran (1st𝑠) ⊆ (0..^𝑘))
276273, 274, 2753syl 18 . . . . . . . . 9 (𝑠 ∈ (((0..^𝑘) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → ran (1st𝑠) ⊆ (0..^𝑘))
277272, 276jca 515 . . . . . . . 8 (𝑠 ∈ (((0..^𝑘) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (𝑠 ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ran (1st𝑠) ⊆ (0..^𝑘)))
278277anim1i 617 . . . . . . 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 472 . . . . . . 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 3207 . . . . 5 (∃𝑠 ∈ (((0..^𝑘) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) → ∃𝑠 ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})(ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))
282265, 281syl 17 . . . 4 ((𝜑𝑘 ∈ ℕ) → ∃𝑠 ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})(ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))
283282ralrimiva 3149 . . 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 11634 . . . 4 ℕ ∈ V
285140, 266ixpconst 8457 . . . . . . 7 X𝑛 ∈ (1...𝑁)ℕ0 = (ℕ0m (1...𝑁))
286 omelon 9096 . . . . . . . . . 10 ω ∈ On
287 nn0ennn 13345 . . . . . . . . . . 11 0 ≈ ℕ
288 nnenom 13346 . . . . . . . . . . 11 ℕ ≈ ω
289287, 288entr2i 8550 . . . . . . . . . 10 ω ≈ ℕ0
290 isnumi 9362 . . . . . . . . . 10 ((ω ∈ On ∧ ω ≈ ℕ0) → ℕ0 ∈ dom card)
291286, 289, 290mp2an 691 . . . . . . . . 9 0 ∈ dom card
292291rgenw 3118 . . . . . . . 8 𝑛 ∈ (1...𝑁)ℕ0 ∈ dom card
293 finixpnum 35061 . . . . . . . 8 (((1...𝑁) ∈ Fin ∧ ∀𝑛 ∈ (1...𝑁)ℕ0 ∈ dom card) → X𝑛 ∈ (1...𝑁)ℕ0 ∈ dom card)
29424, 292, 293mp2an 691 . . . . . . 7 X𝑛 ∈ (1...𝑁)ℕ0 ∈ dom card
295285, 294eqeltrri 2887 . . . . . 6 (ℕ0m (1...𝑁)) ∈ dom card
296140, 140mapval 8404 . . . . . . . . 9 ((1...𝑁) ↑m (1...𝑁)) = {𝑓𝑓:(1...𝑁)⟶(1...𝑁)}
297 mapfi 8807 . . . . . . . . . 10 (((1...𝑁) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((1...𝑁) ↑m (1...𝑁)) ∈ Fin)
29824, 24, 297mp2an 691 . . . . . . . . 9 ((1...𝑁) ↑m (1...𝑁)) ∈ Fin
299296, 298eqeltrri 2887 . . . . . . . 8 {𝑓𝑓:(1...𝑁)⟶(1...𝑁)} ∈ Fin
300 f1of 6591 . . . . . . . . 9 (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑓:(1...𝑁)⟶(1...𝑁))
301300ss2abi 3994 . . . . . . . 8 {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ⊆ {𝑓𝑓:(1...𝑁)⟶(1...𝑁)}
302 ssfi 8725 . . . . . . . 8 (({𝑓𝑓:(1...𝑁)⟶(1...𝑁)} ∈ Fin ∧ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ⊆ {𝑓𝑓:(1...𝑁)⟶(1...𝑁)}) → {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ∈ Fin)
303299, 301, 302mp2an 691 . . . . . . 7 {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ∈ Fin
304 finnum 9364 . . . . . . 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 9367 . . . . . 6 (((ℕ0m (1...𝑁)) ∈ dom card ∧ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ∈ dom card) → ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∈ dom card)
307295, 305, 306mp2an 691 . . . . 5 ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∈ dom card
308 ssrab2 4007 . . . . . . . 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 3118 . . . . . . 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 4900 . . . . . . 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 11639 . . . . . . 7 1 ∈ ℕ
313 ne0i 4250 . . . . . . 7 (1 ∈ ℕ → ℕ ≠ ∅)
314 iunconst 4891 . . . . . . 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 3951 . . . . 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 9453 . . . . 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 691 . . . 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 6646 . . . . . . . 8 (𝑠 = (𝑔𝑘) → (1st𝑠) = (1st ‘(𝑔𝑘)))
320319rneqd 5773 . . . . . . 7 (𝑠 = (𝑔𝑘) → ran (1st𝑠) = ran (1st ‘(𝑔𝑘)))
321320sseq1d 3946 . . . . . 6 (𝑠 = (𝑔𝑘) → (ran (1st𝑠) ⊆ (0..^𝑘) ↔ ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘)))
322 fveq2 6646 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = (𝑔𝑘) → (2nd𝑠) = (2nd ‘(𝑔𝑘)))
323322imaeq1d 5896 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = (𝑔𝑘) → ((2nd𝑠) “ (1...𝑗)) = ((2nd ‘(𝑔𝑘)) “ (1...𝑗)))
324323xpeq1d 5549 . . . . . . . . . . . . . . . . . . 19 (𝑠 = (𝑔𝑘) → (((2nd𝑠) “ (1...𝑗)) × {1}) = (((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}))
325322imaeq1d 5896 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = (𝑔𝑘) → ((2nd𝑠) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)))
326325xpeq1d 5549 . . . . . . . . . . . . . . . . . . 19 (𝑠 = (𝑔𝑘) → (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))
327324, 326uneq12d 4091 . . . . . . . . . . . . . . . . . 18 (𝑠 = (𝑔𝑘) → ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
328319, 327oveq12d 7154 . . . . . . . . . . . . . . . . 17 (𝑠 = (𝑔𝑘) → ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))))
329328fvoveq1d 7158 . . . . . . . . . . . . . . . 16 (𝑠 = (𝑔𝑘) → (𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))) = (𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))))
330329fveq1d 6648 . . . . . . . . . . . . . . 15 (𝑠 = (𝑔𝑘) → ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) = ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏))
331330breq2d 5043 . . . . . . . . . . . . . 14 (𝑠 = (𝑔𝑘) → (0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ↔ 0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏)))
332328fveq1d 6648 . . . . . . . . . . . . . . 15 (𝑠 = (𝑔𝑘) → (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) = (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏))
333332neeq1d 3046 . . . . . . . . . . . . . 14 (𝑠 = (𝑔𝑘) → ((((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0 ↔ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0))
334331, 333anbi12d 633 . . . . . . . . . . . . 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 3162 . . . . . . . . . . . 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 3427 . . . . . . . . . . 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 4090 . . . . . . . . . 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 8897 . . . . . . . . 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 2809 . . . . . . . 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 3256 . . . . . . 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 3162 . . . . . 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 633 . . . . 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 9893 . . . 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 1448 . . 3 (∀𝑘 ∈ ℕ ∃𝑠 ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})(ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) → ∃𝑔(𝑔:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))))
345283, 344syl 17 . 2 (𝜑 → ∃𝑔(𝑔:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))))
3461ad2antrr 725 . . . 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 725 . . . 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 2798 . . . 4 ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑛) = ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑛)
351 simplr 768 . . . 4 (((𝜑𝑔:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) → 𝑔:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
352 simpl 486 . . . . . . 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 3128 . . . . . 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 485 . . . . 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 6651 . . . . . . . 8 (𝑘 = 𝑝 → (1st ‘(𝑔𝑘)) = (1st ‘(𝑔𝑝)))
356355rneqd 5773 . . . . . . 7 (𝑘 = 𝑝 → ran (1st ‘(𝑔𝑘)) = ran (1st ‘(𝑔𝑝)))
357 oveq2 7144 . . . . . . 7 (𝑘 = 𝑝 → (0..^𝑘) = (0..^𝑝))
358356, 357sseq12d 3948 . . . . . 6 (𝑘 = 𝑝 → (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ↔ ran (1st ‘(𝑔𝑝)) ⊆ (0..^𝑝)))
359358rspccva 3570 . . . . 5 ((∀𝑘 ∈ ℕ ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ 𝑝 ∈ ℕ) → ran (1st ‘(𝑔𝑝)) ⊆ (0..^𝑝))
360354, 359sylan 583 . . . 4 ((((𝜑𝑔:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) ∧ 𝑝 ∈ ℕ) → ran (1st ‘(𝑔𝑝)) ⊆ (0..^𝑝))
361 simpll 766 . . . . . 6 (((𝜑𝑔:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) → 𝜑)
362 poimir.2 . . . . . 6 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧𝐼 ∧ (𝑧𝑛) = 0)) → ((𝐹𝑧)‘𝑛) ≤ 0)
363361, 362sylan 583 . . . . 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 2798 . . . . 5 ((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) = ((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))
365 simpr 488 . . . . . . . 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 3128 . . . . . . 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 485 . . . . . 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 6651 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 𝑝 → (2nd ‘(𝑔𝑘)) = (2nd ‘(𝑔𝑝)))
369368imaeq1d 5896 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑝 → ((2nd ‘(𝑔𝑘)) “ (1...𝑗)) = ((2nd ‘(𝑔𝑝)) “ (1...𝑗)))
370369xpeq1d 5549 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑝 → (((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) = (((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}))
371368imaeq1d 5896 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑝 → ((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)))
372371xpeq1d 5549 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑝 → (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))
373370, 372uneq12d 4091 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑝 → ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))
374355, 373oveq12d 7154 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑝 → ((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))))
375 sneq 4535 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑝 → {𝑘} = {𝑝})
376375xpeq2d 5550 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑝 → ((1...𝑁) × {𝑘}) = ((1...𝑁) × {𝑝}))
377374, 376oveq12d 7154 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑝 → (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) = (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))
378377fveq2d 6650 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑝 → (𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))) = (𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝}))))
379378fveq1d 6648 . . . . . . . . . . . . . . 15 (𝑘 = 𝑝 → ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) = ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏))
380379breq2d 5043 . . . . . . . . . . . . . 14 (𝑘 = 𝑝 → (0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ↔ 0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏)))
381374fveq1d 6648 . . . . . . . . . . . . . . 15 (𝑘 = 𝑝 → (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) = (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏))
382381neeq1d 3046 . . . . . . . . . . . . . 14 (𝑘 = 𝑝 → ((((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0 ↔ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0))
383380, 382anbi12d 633 . . . . . . . . . . . . 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 3162 . . . . . . . . . . . 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 3427 . . . . . . . . . . 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 4090 . . . . . . . . . 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 8897 . . . . . . . . 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 2809 . . . . . . . 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 3256 . . . . . . 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 2802 . . . . . . . . 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 3256 . . . . . . . 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 7144 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑚 → (1...𝑗) = (1...𝑚))
393392imaeq2d 5897 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑚 → ((2nd ‘(𝑔𝑝)) “ (1...𝑗)) = ((2nd ‘(𝑔𝑝)) “ (1...𝑚)))
394393xpeq1d 5549 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑚 → (((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) = (((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}))
395 oveq1 7143 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑚 → (𝑗 + 1) = (𝑚 + 1))
396395oveq1d 7151 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑚 → ((𝑗 + 1)...𝑁) = ((𝑚 + 1)...𝑁))
397396imaeq2d 5897 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑚 → ((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)))
398397xpeq1d 5549 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑚 → (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))
399394, 398uneq12d 4091 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑚 → ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))
400399oveq2d 7152 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑚 → ((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))))
401400fvoveq1d 7158 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑚 → (𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝}))) = (𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝}))))
402401fveq1d 6648 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑚 → ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) = ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏))
403402breq2d 5043 . . . . . . . . . . . . . . 15 (𝑗 = 𝑚 → (0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ↔ 0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏)))
404400fveq1d 6648 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑚 → (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) = (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏))
405404neeq1d 3046 . . . . . . . . . . . . . . 15 (𝑗 = 𝑚 → ((((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0 ↔ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0))
406403, 405anbi12d 633 . . . . . . . . . . . . . 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 3162 . . . . . . . . . . . . 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 3427 . . . . . . . . . . . 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 4090 . . . . . . . . . . 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 8897 . . . . . . . . . 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 2809 . . . . . . . . 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 3397 . . . . . . . 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, 412syl6bb 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 3581 . . . . . 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 510 . . . . 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 35107 . . . 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 35106 . . 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 470 . 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 1936 1 (𝜑 → ∃𝑐𝐼𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2111  {cab 2776   ≠ wne 2987  ∀wral 3106  ∃wrex 3107  {crab 3110  Vcvv 3441   ∪ cun 3879   ⊆ wss 3881  ∅c0 4243  {csn 4525  {cpr 4527  ∪ ciun 4882   class class class wbr 5031   Or wor 5438   × cxp 5518  ◡ccnv 5519  dom cdm 5520  ran crn 5521   “ cima 5523  Oncon0 6160   Fn wfn 6320  ⟶wf 6321  –1-1-onto→wf1o 6324  ‘cfv 6325  (class class class)co 7136   ∘f cof 7389  ωcom 7563  1st c1st 7672  2nd c2nd 7673   ↑m cmap 8392  Xcixp 8447   ≈ cen 8492  Fincfn 8495  supcsup 8891  cardccrd 9351  ℂcc 10527  ℝcr 10528  0cc0 10529  1c1 10530   + caddc 10532   · cmul 10534   < clt 10667   ≤ cle 10668   − cmin 10862   / cdiv 11289  ℕcn 11628  ℕ0cn0 11888  ℤcz 11972  ℤ≥cuz 12234  ℝ+crp 12380  (,)cioo 12729  [,]cicc 12732  ...cfz 12888  ..^cfzo 13031   ↾t crest 16689  topGenctg 16706  ∏tcpt 16707   Cn ccn 21839 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7444  ax-inf2 9091  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4840  df-iun 4884  df-iin 4885  df-disj 4997  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5426  df-eprel 5431  df-po 5439  df-so 5440  df-fr 5479  df-se 5480  df-we 5481  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-pred 6117  df-ord 6163  df-on 6164  df-lim 6165  df-suc 6166  df-iota 6284  df-fun 6327  df-fn 6328  df-f 6329  df-f1 6330  df-fo 6331  df-f1o 6332  df-fv 6333  df-isom 6334  df-riota 7094  df-ov 7139  df-oprab 7140  df-mpo 7141  df-of 7391  df-om 7564  df-1st 7674  df-2nd 7675  df-wrecs 7933  df-recs 7994  df-rdg 8032  df-1o 8088  df-2o 8089  df-oadd 8092  df-omul 8093  df-er 8275  df-map 8394  df-pm 8395  df-ixp 8448  df-en 8496  df-dom 8497  df-sdom 8498  df-fin 8499  df-fi 8862  df-sup 8893  df-inf 8894  df-oi 8961  df-dju 9317  df-card 9355  df-acn 9358  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11629  df-2 11691  df-3 11692  df-n0 11889  df-xnn0 11959  df-z 11973  df-uz 12235  df-q 12340  df-rp 12381  df-xneg 12498  df-xadd 12499  df-xmul 12500  df-ioo 12733  df-icc 12736  df-fz 12889  df-fzo 13032  df-fl 13160  df-seq 13368  df-exp 13429  df-fac 13633  df-bc 13662  df-hash 13690  df-cj 14453  df-re 14454  df-im 14455  df-sqrt 14589  df-abs 14590  df-clim 14840  df-sum 15038  df-dvds 15603  df-rest 16691  df-topgen 16712  df-pt 16713  df-psmet 20087  df-xmet 20088  df-met 20089  df-bl 20090  df-mopn 20091  df-top 21509  df-topon 21526  df-bases 21561  df-cld 21634  df-ntr 21635  df-cls 21636  df-lp 21751  df-cn 21842  df-cnp 21843  df-t1 21929  df-haus 21930  df-cmp 22002  df-tx 22177  df-hmeo 22370  df-hmph 22371  df-ii 23492 This theorem is referenced by:  poimir  35109
 Copyright terms: Public domain W3C validator