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

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

Proof of Theorem poimirlem32
Dummy variables 𝑓 𝑖 𝑗 𝑘 𝑚 𝑝 𝑞 𝑠 𝑔 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 poimir.0 . . . . . . 7 (𝜑𝑁 ∈ ℕ)
21adantr 480 . . . . . 6 ((𝜑𝑘 ∈ ℕ) → 𝑁 ∈ ℕ)
3 fvoveq1 7278 . . . . . . . . . . . . 13 (𝑝 = ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝐹‘(𝑝f / ((1...𝑁) × {𝑘}))) = (𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))))
43fveq1d 6758 . . . . . . . . . . . 12 (𝑝 = ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) = ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏))
54breq2d 5082 . . . . . . . . . . 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 6755 . . . . . . . . . . . 12 (𝑝 = ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝑝𝑏) = (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏))
76neeq1d 3002 . . . . . . . . . . 11 (𝑝 = ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) → ((𝑝𝑏) ≠ 0 ↔ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0))
85, 7anbi12d 630 . . . . . . . . . 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 3120 . . . . . . . . 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 3404 . . . . . . . 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 4093 . . . . . . 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 9135 . . . . . 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 12223 . . . . . . . . . . 11 (𝜑𝑁 ∈ ℕ0)
14 0elfz 13282 . . . . . . . . . . 11 (𝑁 ∈ ℕ0 → 0 ∈ (0...𝑁))
1513, 14syl 17 . . . . . . . . . 10 (𝜑 → 0 ∈ (0...𝑁))
1615snssd 4739 . . . . . . . . 9 (𝜑 → {0} ⊆ (0...𝑁))
17 ssrab2 4009 . . . . . . . . . . 11 {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ⊆ (1...𝑁)
18 fz1ssfz0 13281 . . . . . . . . . . 11 (1...𝑁) ⊆ (0...𝑁)
1917, 18sstri 3926 . . . . . . . . . 10 {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ⊆ (0...𝑁)
2019a1i 11 . . . . . . . . 9 (𝜑 → {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ⊆ (0...𝑁))
2116, 20unssd 4116 . . . . . . . 8 (𝜑 → ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ⊆ (0...𝑁))
22 ltso 10986 . . . . . . . . 9 < Or ℝ
23 snfi 8788 . . . . . . . . . . 11 {0} ∈ Fin
24 fzfi 13620 . . . . . . . . . . . 12 (1...𝑁) ∈ Fin
25 rabfi 8973 . . . . . . . . . . . 12 ((1...𝑁) ∈ Fin → {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ∈ Fin)
2624, 25ax-mp 5 . . . . . . . . . . 11 {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ∈ Fin
27 unfi 8917 . . . . . . . . . . 11 (({0} ∈ Fin ∧ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ∈ Fin) → ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ∈ Fin)
2823, 26, 27mp2an 688 . . . . . . . . . 10 ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ∈ Fin
29 c0ex 10900 . . . . . . . . . . . 12 0 ∈ V
3029snid 4594 . . . . . . . . . . 11 0 ∈ {0}
31 elun1 4106 . . . . . . . . . . 11 (0 ∈ {0} → 0 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}))
32 ne0i 4265 . . . . . . . . . . 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 10909 . . . . . . . . . . . . 13 ((𝜑𝑁 ∈ ℕ) → 0 ∈ ℝ)
3534snssd 4739 . . . . . . . . . . . 12 ((𝜑𝑁 ∈ ℕ) → {0} ⊆ ℝ)
361, 35ax-mp 5 . . . . . . . . . . 11 {0} ⊆ ℝ
37 elfzelz 13185 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℤ)
3837ssriv 3921 . . . . . . . . . . . . 13 (1...𝑁) ⊆ ℤ
39 zssre 12256 . . . . . . . . . . . . 13 ℤ ⊆ ℝ
4038, 39sstri 3926 . . . . . . . . . . . 12 (1...𝑁) ⊆ ℝ
4117, 40sstri 3926 . . . . . . . . . . 11 {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ⊆ ℝ
4236, 41unssi 4115 . . . . . . . . . 10 ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ⊆ ℝ
4328, 33, 423pm3.2i 1337 . . . . . . . . 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 9158 . . . . . . . . 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 688 . . . . . . . 8 sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})
46 ssel 3910 . . . . . . . 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 722 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑝:(1...𝑁)⟶(0...𝑘)) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ∈ (0...𝑁))
49 elfznn 13214 . . . . . . . . 9 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ)
50 nngt0 11934 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → 0 < 𝑛)
5150adantr 480 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) → 0 < 𝑛)
52 simpr 484 . . . . . . . . . . . . . 14 ((0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → (𝑝𝑏) ≠ 0)
5352ralimi 3086 . . . . . . . . . . . . 13 (∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑠)(𝑝𝑏) ≠ 0)
54 elfznn 13214 . . . . . . . . . . . . . 14 (𝑠 ∈ (1...𝑁) → 𝑠 ∈ ℕ)
55 nnre 11910 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ ℕ → 𝑛 ∈ ℝ)
56 nnre 11910 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ ℕ → 𝑠 ∈ ℝ)
57 lenlt 10984 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℝ ∧ 𝑠 ∈ ℝ) → (𝑛𝑠 ↔ ¬ 𝑠 < 𝑛))
5855, 56, 57syl2an 595 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ) → (𝑛𝑠 ↔ ¬ 𝑠 < 𝑛))
59 elfz1b 13254 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ (1...𝑠) ↔ (𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ ∧ 𝑛𝑠))
6059biimpri 227 . . . . . . . . . . . . . . . . . . . 20 ((𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ ∧ 𝑛𝑠) → 𝑛 ∈ (1...𝑠))
61603expia 1119 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ) → (𝑛𝑠𝑛 ∈ (1...𝑠)))
6258, 61sylbird 259 . . . . . . . . . . . . . . . . . 18 ((𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ) → (¬ 𝑠 < 𝑛𝑛 ∈ (1...𝑠)))
63 fveq2 6756 . . . . . . . . . . . . . . . . . . . . 21 (𝑏 = 𝑛 → (𝑝𝑏) = (𝑝𝑛))
6463eqeq1d 2740 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = 𝑛 → ((𝑝𝑏) = 0 ↔ (𝑝𝑛) = 0))
6564rspcev 3552 . . . . . . . . . . . . . . . . . . 19 ((𝑛 ∈ (1...𝑠) ∧ (𝑝𝑛) = 0) → ∃𝑏 ∈ (1...𝑠)(𝑝𝑏) = 0)
6665expcom 413 . . . . . . . . . . . . . . . . . 18 ((𝑝𝑛) = 0 → (𝑛 ∈ (1...𝑠) → ∃𝑏 ∈ (1...𝑠)(𝑝𝑏) = 0))
6762, 66sylan9 507 . . . . . . . . . . . . . . . . 17 (((𝑛 ∈ ℕ ∧ 𝑠 ∈ ℕ) ∧ (𝑝𝑛) = 0) → (¬ 𝑠 < 𝑛 → ∃𝑏 ∈ (1...𝑠)(𝑝𝑏) = 0))
6867an32s 648 . . . . . . . . . . . . . . . 16 (((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) ∧ 𝑠 ∈ ℕ) → (¬ 𝑠 < 𝑛 → ∃𝑏 ∈ (1...𝑠)(𝑝𝑏) = 0))
69 nne 2946 . . . . . . . . . . . . . . . . . 18 (¬ (𝑝𝑏) ≠ 0 ↔ (𝑝𝑏) = 0)
7069rexbii 3177 . . . . . . . . . . . . . . . . 17 (∃𝑏 ∈ (1...𝑠) ¬ (𝑝𝑏) ≠ 0 ↔ ∃𝑏 ∈ (1...𝑠)(𝑝𝑏) = 0)
71 rexnal 3165 . . . . . . . . . . . . . . . . 17 (∃𝑏 ∈ (1...𝑠) ¬ (𝑝𝑏) ≠ 0 ↔ ¬ ∀𝑏 ∈ (1...𝑠)(𝑝𝑏) ≠ 0)
7270, 71bitr3i 276 . . . . . . . . . . . . . . . 16 (∃𝑏 ∈ (1...𝑠)(𝑝𝑏) = 0 ↔ ¬ ∀𝑏 ∈ (1...𝑠)(𝑝𝑏) ≠ 0)
7368, 72syl6ib 250 . . . . . . . . . . . . . . 15 (((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) ∧ 𝑠 ∈ ℕ) → (¬ 𝑠 < 𝑛 → ¬ ∀𝑏 ∈ (1...𝑠)(𝑝𝑏) ≠ 0))
7473con4d 115 . . . . . . . . . . . . . 14 (((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) ∧ 𝑠 ∈ ℕ) → (∀𝑏 ∈ (1...𝑠)(𝑝𝑏) ≠ 0 → 𝑠 < 𝑛))
7554, 74sylan2 592 . . . . . . . . . . . . 13 (((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) ∧ 𝑠 ∈ (1...𝑁)) → (∀𝑏 ∈ (1...𝑠)(𝑝𝑏) ≠ 0 → 𝑠 < 𝑛))
7653, 75syl5 34 . . . . . . . . . . . 12 (((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) ∧ 𝑠 ∈ (1...𝑁)) → (∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → 𝑠 < 𝑛))
7776ralrimiva 3107 . . . . . . . . . . 11 ((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) → ∀𝑠 ∈ (1...𝑁)(∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → 𝑠 < 𝑛))
78 ralunb 4121 . . . . . . . . . . . 12 (∀𝑠 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})𝑠 < 𝑛 ↔ (∀𝑠 ∈ {0}𝑠 < 𝑛 ∧ ∀𝑠 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}𝑠 < 𝑛))
79 breq1 5073 . . . . . . . . . . . . . 14 (𝑠 = 0 → (𝑠 < 𝑛 ↔ 0 < 𝑛))
8029, 79ralsn 4614 . . . . . . . . . . . . 13 (∀𝑠 ∈ {0}𝑠 < 𝑛 ↔ 0 < 𝑛)
81 oveq2 7263 . . . . . . . . . . . . . . 15 (𝑎 = 𝑠 → (1...𝑎) = (1...𝑠))
8281raleqdv 3339 . . . . . . . . . . . . . 14 (𝑎 = 𝑠 → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
8382ralrab 3623 . . . . . . . . . . . . 13 (∀𝑠 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}𝑠 < 𝑛 ↔ ∀𝑠 ∈ (1...𝑁)(∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → 𝑠 < 𝑛))
8480, 83anbi12i 626 . . . . . . . . . . . 12 ((∀𝑠 ∈ {0}𝑠 < 𝑛 ∧ ∀𝑠 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}𝑠 < 𝑛) ↔ (0 < 𝑛 ∧ ∀𝑠 ∈ (1...𝑁)(∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → 𝑠 < 𝑛)))
8578, 84bitri 274 . . . . . . . . . . 11 (∀𝑠 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})𝑠 < 𝑛 ↔ (0 < 𝑛 ∧ ∀𝑠 ∈ (1...𝑁)(∀𝑏 ∈ (1...𝑠)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → 𝑠 < 𝑛)))
8651, 77, 85sylanbrc 582 . . . . . . . . . 10 ((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) → ∀𝑠 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})𝑠 < 𝑛)
87 breq1 5073 . . . . . . . . . . 11 (𝑠 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) → (𝑠 < 𝑛 ↔ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < 𝑛))
8887rspcva 3550 . . . . . . . . . 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 586 . . . . . . . . 9 ((𝑛 ∈ ℕ ∧ (𝑝𝑛) = 0) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < 𝑛)
9049, 89sylan 579 . . . . . . . 8 ((𝑛 ∈ (1...𝑁) ∧ (𝑝𝑛) = 0) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < 𝑛)
91903adant2 1129 . . . . . . 7 ((𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 0) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < 𝑛)
9291adantl 481 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 0)) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < 𝑛)
9337zred 12355 . . . . . . . . . . 11 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℝ)
94933ad2ant1 1131 . . . . . . . . . 10 ((𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) → 𝑛 ∈ ℝ)
9594adantl 481 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → 𝑛 ∈ ℝ)
96 simpr1 1192 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → 𝑛 ∈ (1...𝑁))
97 simpll 763 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → 𝜑)
98 simplr 765 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → 𝑘 ∈ ℕ)
99 elfzelz 13185 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ (0...𝑘) → 𝑖 ∈ ℤ)
10099zred 12355 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ (0...𝑘) → 𝑖 ∈ ℝ)
101 nndivre 11944 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖 ∈ ℝ ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ ℝ)
102100, 101sylan 579 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ ℝ)
103 elfzle1 13188 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ (0...𝑘) → 0 ≤ 𝑖)
104100, 103jca 511 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 ∈ (0...𝑘) → (𝑖 ∈ ℝ ∧ 0 ≤ 𝑖))
105 nnrp 12670 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
106105rpregt0d 12707 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ ℕ → (𝑘 ∈ ℝ ∧ 0 < 𝑘))
107 divge0 11774 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑖 ∈ ℝ ∧ 0 ≤ 𝑖) ∧ (𝑘 ∈ ℝ ∧ 0 < 𝑘)) → 0 ≤ (𝑖 / 𝑘))
108104, 106, 107syl2an 595 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝑖 / 𝑘))
109 elfzle2 13189 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑖 ∈ (0...𝑘) → 𝑖𝑘)
110109adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑖𝑘)
111100adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑖 ∈ ℝ)
112 1red 10907 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 1 ∈ ℝ)
113105adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ+)
114111, 112, 113ledivmuld 12754 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑖 / 𝑘) ≤ 1 ↔ 𝑖 ≤ (𝑘 · 1)))
115 nncn 11911 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
116115mulid1d 10923 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 ∈ ℕ → (𝑘 · 1) = 𝑘)
117116breq2d 5082 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ ℕ → (𝑖 ≤ (𝑘 · 1) ↔ 𝑖𝑘))
118117adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 ≤ (𝑘 · 1) ↔ 𝑖𝑘))
119114, 118bitrd 278 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → ((𝑖 / 𝑘) ≤ 1 ↔ 𝑖𝑘))
120110, 119mpbird 256 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ≤ 1)
121 elicc01 13127 . . . . . . . . . . . . . . . . . . . . 21 ((𝑖 / 𝑘) ∈ (0[,]1) ↔ ((𝑖 / 𝑘) ∈ ℝ ∧ 0 ≤ (𝑖 / 𝑘) ∧ (𝑖 / 𝑘) ≤ 1))
122102, 108, 120, 121syl3anbrc 1341 . . . . . . . . . . . . . . . . . . . 20 ((𝑖 ∈ (0...𝑘) ∧ 𝑘 ∈ ℕ) → (𝑖 / 𝑘) ∈ (0[,]1))
123122ancoms 458 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑘)) → (𝑖 / 𝑘) ∈ (0[,]1))
124 elsni 4575 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ {𝑘} → 𝑗 = 𝑘)
125124oveq2d 7271 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ {𝑘} → (𝑖 / 𝑗) = (𝑖 / 𝑘))
126125eleq1d 2823 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ {𝑘} → ((𝑖 / 𝑗) ∈ (0[,]1) ↔ (𝑖 / 𝑘) ∈ (0[,]1)))
127123, 126syl5ibrcom 246 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ ∧ 𝑖 ∈ (0...𝑘)) → (𝑗 ∈ {𝑘} → (𝑖 / 𝑗) ∈ (0[,]1)))
128127impr 454 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ ∧ (𝑖 ∈ (0...𝑘) ∧ 𝑗 ∈ {𝑘})) → (𝑖 / 𝑗) ∈ (0[,]1))
12998, 128sylan 579 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) ∧ (𝑖 ∈ (0...𝑘) ∧ 𝑗 ∈ {𝑘})) → (𝑖 / 𝑗) ∈ (0[,]1))
130 simprr 769 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → 𝑝:(1...𝑁)⟶(0...𝑘))
131 vex 3426 . . . . . . . . . . . . . . . . . 18 𝑘 ∈ V
132131fconst 6644 . . . . . . . . . . . . . . . . 17 ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘}
133132a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → ((1...𝑁) × {𝑘}):(1...𝑁)⟶{𝑘})
134 fzfid 13621 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → (1...𝑁) ∈ Fin)
135 inidm 4149 . . . . . . . . . . . . . . . 16 ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
136129, 130, 133, 134, 134, 135off 7529 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → (𝑝f / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
137 poimir.i . . . . . . . . . . . . . . . . 17 𝐼 = ((0[,]1) ↑m (1...𝑁))
138137eleq2i 2830 . . . . . . . . . . . . . . . 16 ((𝑝f / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ (𝑝f / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑m (1...𝑁)))
139 ovex 7288 . . . . . . . . . . . . . . . . 17 (0[,]1) ∈ V
140 ovex 7288 . . . . . . . . . . . . . . . . 17 (1...𝑁) ∈ V
141139, 140elmap 8617 . . . . . . . . . . . . . . . 16 ((𝑝f / ((1...𝑁) × {𝑘})) ∈ ((0[,]1) ↑m (1...𝑁)) ↔ (𝑝f / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
142138, 141bitri 274 . . . . . . . . . . . . . . 15 ((𝑝f / ((1...𝑁) × {𝑘})) ∈ 𝐼 ↔ (𝑝f / ((1...𝑁) × {𝑘})):(1...𝑁)⟶(0[,]1))
143136, 142sylibr 233 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘))) → (𝑝f / ((1...𝑁) × {𝑘})) ∈ 𝐼)
1441433adantr3 1169 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → (𝑝f / ((1...𝑁) × {𝑘})) ∈ 𝐼)
145 3anass 1093 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) ↔ (𝑛 ∈ (1...𝑁) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)))
146 ancom 460 . . . . . . . . . . . . . . . 16 ((𝑛 ∈ (1...𝑁) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) ↔ ((𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) ∧ 𝑛 ∈ (1...𝑁)))
147145, 146bitri 274 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) ↔ ((𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) ∧ 𝑛 ∈ (1...𝑁)))
148 ffn 6584 . . . . . . . . . . . . . . . . . 18 (𝑝:(1...𝑁)⟶(0...𝑘) → 𝑝 Fn (1...𝑁))
149148ad2antrl 724 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → 𝑝 Fn (1...𝑁))
150 fnconstg 6646 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ V → ((1...𝑁) × {𝑘}) Fn (1...𝑁))
151131, 150mp1i 13 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ((1...𝑁) × {𝑘}) Fn (1...𝑁))
152 fzfid 13621 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → (1...𝑁) ∈ Fin)
153 simplrr 774 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) ∧ 𝑛 ∈ (1...𝑁)) → (𝑝𝑛) = 𝑘)
154131fvconst2 7061 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {𝑘})‘𝑛) = 𝑘)
155154adantl 481 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) ∧ 𝑛 ∈ (1...𝑁)) → (((1...𝑁) × {𝑘})‘𝑛) = 𝑘)
156149, 151, 152, 152, 135, 153, 155ofval 7522 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘 ∈ ℕ) ∧ (𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = (𝑘 / 𝑘))
157156anasss 466 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ) ∧ ((𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) ∧ 𝑛 ∈ (1...𝑁))) → ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = (𝑘 / 𝑘))
158147, 157sylan2b 593 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = (𝑘 / 𝑘))
159 nnne0 11937 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ → 𝑘 ≠ 0)
160115, 159dividd 11679 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ → (𝑘 / 𝑘) = 1)
161160ad2antlr 723 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → (𝑘 / 𝑘) = 1)
162158, 161eqtrd 2778 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = 1)
163 ovex 7288 . . . . . . . . . . . . . 14 (𝑝f / ((1...𝑁) × {𝑘})) ∈ V
164 eleq1 2826 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → (𝑧𝐼 ↔ (𝑝f / ((1...𝑁) × {𝑘})) ∈ 𝐼))
165 fveq1 6755 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → (𝑧𝑛) = ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛))
166165eqeq1d 2740 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → ((𝑧𝑛) = 1 ↔ ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = 1))
167164, 1663anbi23d 1437 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → ((𝑛 ∈ (1...𝑁) ∧ 𝑧𝐼 ∧ (𝑧𝑛) = 1) ↔ (𝑛 ∈ (1...𝑁) ∧ (𝑝f / ((1...𝑁) × {𝑘})) ∈ 𝐼 ∧ ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = 1)))
168167anbi2d 628 . . . . . . . . . . . . . . 15 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧𝐼 ∧ (𝑧𝑛) = 1)) ↔ (𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ (𝑝f / ((1...𝑁) × {𝑘})) ∈ 𝐼 ∧ ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = 1))))
169 fveq2 6756 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → (𝐹𝑧) = (𝐹‘(𝑝f / ((1...𝑁) × {𝑘}))))
170169fveq1d 6758 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → ((𝐹𝑧)‘𝑛) = ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛))
171170breq2d 5082 . . . . . . . . . . . . . . 15 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → (0 ≤ ((𝐹𝑧)‘𝑛) ↔ 0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛)))
172168, 171imbi12d 344 . . . . . . . . . . . . . 14 (𝑧 = (𝑝f / ((1...𝑁) × {𝑘})) → (((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧𝐼 ∧ (𝑧𝑛) = 1)) → 0 ≤ ((𝐹𝑧)‘𝑛)) ↔ ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ (𝑝f / ((1...𝑁) × {𝑘})) ∈ 𝐼 ∧ ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = 1)) → 0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛))))
173 poimir.3 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑧𝐼 ∧ (𝑧𝑛) = 1)) → 0 ≤ ((𝐹𝑧)‘𝑛))
174163, 172, 173vtocl 3488 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑛 ∈ (1...𝑁) ∧ (𝑝f / ((1...𝑁) × {𝑘})) ∈ 𝐼 ∧ ((𝑝f / ((1...𝑁) × {𝑘}))‘𝑛) = 1)) → 0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛))
17597, 96, 144, 162, 174syl13anc 1370 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → 0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛))
176 simpr 484 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
177 simp3 1136 . . . . . . . . . . . . 13 ((𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘) → (𝑝𝑛) = 𝑘)
178 neeq1 3005 . . . . . . . . . . . . . . 15 ((𝑝𝑛) = 𝑘 → ((𝑝𝑛) ≠ 0 ↔ 𝑘 ≠ 0))
179159, 178syl5ibrcom 246 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → ((𝑝𝑛) = 𝑘 → (𝑝𝑛) ≠ 0))
180179imp 406 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ ∧ (𝑝𝑛) = 𝑘) → (𝑝𝑛) ≠ 0)
181176, 177, 180syl2an 595 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → (𝑝𝑛) ≠ 0)
182 vex 3426 . . . . . . . . . . . . 13 𝑛 ∈ V
183 fveq2 6756 . . . . . . . . . . . . . . 15 (𝑏 = 𝑛 → ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) = ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛))
184183breq2d 5082 . . . . . . . . . . . . . 14 (𝑏 = 𝑛 → (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ↔ 0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛)))
18563neeq1d 3002 . . . . . . . . . . . . . 14 (𝑏 = 𝑛 → ((𝑝𝑏) ≠ 0 ↔ (𝑝𝑛) ≠ 0))
186184, 185anbi12d 630 . . . . . . . . . . . . 13 (𝑏 = 𝑛 → ((0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛) ∧ (𝑝𝑛) ≠ 0)))
187182, 186ralsn 4614 . . . . . . . . . . . 12 (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑛) ∧ (𝑝𝑛) ≠ 0))
188175, 181, 187sylanbrc 582 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))
18937zcnd 12356 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ)
190 1cnd 10901 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...𝑁) → 1 ∈ ℂ)
191189, 190subeq0ad 11272 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) = 0 ↔ 𝑛 = 1))
192191biimpcd 248 . . . . . . . . . . . . . . . . 17 ((𝑛 − 1) = 0 → (𝑛 ∈ (1...𝑁) → 𝑛 = 1))
193 1z 12280 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℤ
194 fzsn 13227 . . . . . . . . . . . . . . . . . . . . 21 (1 ∈ ℤ → (1...1) = {1})
195193, 194ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (1...1) = {1}
196 oveq2 7263 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 1 → (1...𝑛) = (1...1))
197 sneq 4568 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 1 → {𝑛} = {1})
198195, 196, 1973eqtr4a 2805 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 1 → (1...𝑛) = {𝑛})
199198raleqdv 3339 . . . . . . . . . . . . . . . . . 18 (𝑛 = 1 → (∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
200199biimprd 247 . . . . . . . . . . . . . . . . 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 4122 . . . . . . . . . . . . . . . . . . . 20 ((∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)) → ∀𝑏 ∈ ((1...(𝑛 − 1)) ∪ {𝑛})(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))
203 npcan1 11330 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ℂ → ((𝑛 − 1) + 1) = 𝑛)
204189, 203syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) + 1) = 𝑛)
205 elfzuz 13181 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ (ℤ‘1))
206204, 205eqeltrd 2839 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) + 1) ∈ (ℤ‘1))
207 peano2zm 12293 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ℤ → (𝑛 − 1) ∈ ℤ)
208 uzid 12526 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 − 1) ∈ ℤ → (𝑛 − 1) ∈ (ℤ‘(𝑛 − 1)))
209 peano2uz 12570 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑛 − 1) ∈ (ℤ‘(𝑛 − 1)) → ((𝑛 − 1) + 1) ∈ (ℤ‘(𝑛 − 1)))
21037, 207, 208, 2094syl 19 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...𝑁) → ((𝑛 − 1) + 1) ∈ (ℤ‘(𝑛 − 1)))
211204, 210eqeltrrd 2840 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (1...𝑁) → 𝑛 ∈ (ℤ‘(𝑛 − 1)))
212 fzsplit2 13210 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑛 − 1) + 1) ∈ (ℤ‘1) ∧ 𝑛 ∈ (ℤ‘(𝑛 − 1))) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)))
213206, 211, 212syl2anc 583 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (1...𝑁) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)))
214204oveq1d 7270 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...𝑁) → (((𝑛 − 1) + 1)...𝑛) = (𝑛...𝑛))
215 fzsn 13227 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 ∈ ℤ → (𝑛...𝑛) = {𝑛})
21637, 215syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 ∈ (1...𝑁) → (𝑛...𝑛) = {𝑛})
217214, 216eqtrd 2778 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 ∈ (1...𝑁) → (((𝑛 − 1) + 1)...𝑛) = {𝑛})
218217uneq2d 4093 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (1...𝑁) → ((1...(𝑛 − 1)) ∪ (((𝑛 − 1) + 1)...𝑛)) = ((1...(𝑛 − 1)) ∪ {𝑛}))
219213, 218eqtrd 2778 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 ∈ (1...𝑁) → (1...𝑛) = ((1...(𝑛 − 1)) ∪ {𝑛}))
220219raleqdv 3339 . . . . . . . . . . . . . . . . . . . 20 (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ ∀𝑏 ∈ ((1...(𝑛 − 1)) ∪ {𝑛})(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
221202, 220syl5ibr 245 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ (1...𝑁) → ((∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
222221expd 415 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
223222com12 32 . . . . . . . . . . . . . . . . 17 (∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
224223adantl 481 . . . . . . . . . . . . . . . 16 (((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)) → (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
225201, 224jaoi 853 . . . . . . . . . . . . . . 15 (((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))) → (𝑛 ∈ (1...𝑁) → (∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) → ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
226225imdistand 570 . . . . . . . . . . . . . 14 (((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))) → ((𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)) → (𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
227226com12 32 . . . . . . . . . . . . 13 ((𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)) → (((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))) → (𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
228 elun 4079 . . . . . . . . . . . . . 14 ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ↔ ((𝑛 − 1) ∈ {0} ∨ (𝑛 − 1) ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}))
229 ovex 7288 . . . . . . . . . . . . . . . 16 (𝑛 − 1) ∈ V
230229elsn 4573 . . . . . . . . . . . . . . 15 ((𝑛 − 1) ∈ {0} ↔ (𝑛 − 1) = 0)
231 oveq2 7263 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑛 − 1) → (1...𝑎) = (1...(𝑛 − 1)))
232231raleqdv 3339 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑛 − 1) → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
233232elrab 3617 . . . . . . . . . . . . . . 15 ((𝑛 − 1) ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ↔ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
234230, 233orbi12i 911 . . . . . . . . . . . . . 14 (((𝑛 − 1) ∈ {0} ∨ (𝑛 − 1) ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ↔ ((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
235228, 234bitri 274 . . . . . . . . . . . . 13 ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ↔ ((𝑛 − 1) = 0 ∨ ((𝑛 − 1) ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...(𝑛 − 1))(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0))))
236 oveq2 7263 . . . . . . . . . . . . . . 15 (𝑎 = 𝑛 → (1...𝑎) = (1...𝑛))
237236raleqdv 3339 . . . . . . . . . . . . . 14 (𝑎 = 𝑛 → (∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0) ↔ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
238237elrab 3617 . . . . . . . . . . . . 13 (𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)} ↔ (𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ (1...𝑛)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)))
239227, 235, 2383imtr4g 295 . . . . . . . . . . . 12 ((𝑛 ∈ (1...𝑁) ∧ ∀𝑏 ∈ {𝑛} (0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)) → ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → 𝑛 ∈ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}))
240 elun2 4107 . . . . . . . . . . . 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 583 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → ((𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → 𝑛 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})))
243 fimaxre2 11850 . . . . . . . . . . . . 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 688 . . . . . . . . . . . 12 𝑖 ∈ ℝ ∀𝑗 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})𝑗𝑖
24542, 33, 2443pm3.2i 1337 . . . . . . . . . . 11 (({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ⊆ ℝ ∧ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) ≠ ∅ ∧ ∃𝑖 ∈ ℝ ∀𝑗 ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)})𝑗𝑖)
246245suprubii 11880 . . . . . . . . . 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 11747 . . . . . . . . . 10 (𝑛 ∈ ℝ → (𝑛 − 1) < 𝑛)
249 peano2rem 11218 . . . . . . . . . . 11 (𝑛 ∈ ℝ → (𝑛 − 1) ∈ ℝ)
25042, 45sselii 3914 . . . . . . . . . . . 12 sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ∈ ℝ
251 ltletr 10997 . . . . . . . . . . . 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 1448 . . . . . . . . . . 11 (((𝑛 − 1) ∈ ℝ ∧ 𝑛 ∈ ℝ) → (((𝑛 − 1) < 𝑛𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )) → (𝑛 − 1) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )))
253249, 252mpancom 684 . . . . . . . . . 10 (𝑛 ∈ ℝ → (((𝑛 − 1) < 𝑛𝑛 ≤ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )) → (𝑛 − 1) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )))
254248, 253mpand 691 . . . . . . . . 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 11014 . . . . . . . . . 10 ¬ sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < )
257 breq1 5073 . . . . . . . . . 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 325 . . . . . . . . 9 (sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) = (𝑛 − 1) → ¬ (𝑛 − 1) < sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ))
259258necon2ai 2972 . . . . . . . 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 2826 . . . . . . . . 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 232 . . . . . . . 8 (sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) = (𝑛 − 1) → (𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}))
263262necon3bi 2969 . . . . . . 7 (¬ (𝑛 − 1) ∈ ({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ≠ (𝑛 − 1))
264260, 263pm2.61d1 180 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ (𝑛 ∈ (1...𝑁) ∧ 𝑝:(1...𝑁)⟶(0...𝑘) ∧ (𝑝𝑛) = 𝑘)) → sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(𝑝f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (𝑝𝑏) ≠ 0)}), ℝ, < ) ≠ (𝑛 − 1))
2652, 12, 48, 92, 264, 176poimirlem28 35732 . . . . 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 12169 . . . . . . . . . . . 12 0 ∈ V
267 fzo0ssnn0 13396 . . . . . . . . . . . 12 (0..^𝑘) ⊆ ℕ0
268 mapss 8635 . . . . . . . . . . . 12 ((ℕ0 ∈ V ∧ (0..^𝑘) ⊆ ℕ0) → ((0..^𝑘) ↑m (1...𝑁)) ⊆ (ℕ0m (1...𝑁)))
269266, 267, 268mp2an 688 . . . . . . . . . . 11 ((0..^𝑘) ↑m (1...𝑁)) ⊆ (ℕ0m (1...𝑁))
270 xpss1 5599 . . . . . . . . . . 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 3913 . . . . . . . . 9 (𝑠 ∈ (((0..^𝑘) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → 𝑠 ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
273 xp1st 7836 . . . . . . . . . 10 (𝑠 ∈ (((0..^𝑘) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (1st𝑠) ∈ ((0..^𝑘) ↑m (1...𝑁)))
274 elmapi 8595 . . . . . . . . . 10 ((1st𝑠) ∈ ((0..^𝑘) ↑m (1...𝑁)) → (1st𝑠):(1...𝑁)⟶(0..^𝑘))
275 frn 6591 . . . . . . . . . 10 ((1st𝑠):(1...𝑁)⟶(0..^𝑘) → ran (1st𝑠) ⊆ (0..^𝑘))
276273, 274, 2753syl 18 . . . . . . . . 9 (𝑠 ∈ (((0..^𝑘) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → ran (1st𝑠) ⊆ (0..^𝑘))
277272, 276jca 511 . . . . . . . 8 (𝑠 ∈ (((0..^𝑘) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) → (𝑠 ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ran (1st𝑠) ⊆ (0..^𝑘)))
278277anim1i 614 . . . . . . 7 ((𝑠 ∈ (((0..^𝑘) ↑m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) → ((𝑠 ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ran (1st𝑠) ⊆ (0..^𝑘)) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))
279 anass 468 . . . . . . 7 (((𝑠 ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ran (1st𝑠) ⊆ (0..^𝑘)) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) ↔ (𝑠 ∈ ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ (ran (1st𝑠) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))))
280278, 279sylib 217 . . . . . 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 3171 . . . . 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 3107 . . 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 11909 . . . 4 ℕ ∈ V
285140, 266ixpconst 8653 . . . . . . 7 X𝑛 ∈ (1...𝑁)ℕ0 = (ℕ0m (1...𝑁))
286 omelon 9334 . . . . . . . . . 10 ω ∈ On
287 nn0ennn 13627 . . . . . . . . . . 11 0 ≈ ℕ
288 nnenom 13628 . . . . . . . . . . 11 ℕ ≈ ω
289287, 288entr2i 8750 . . . . . . . . . 10 ω ≈ ℕ0
290 isnumi 9635 . . . . . . . . . 10 ((ω ∈ On ∧ ω ≈ ℕ0) → ℕ0 ∈ dom card)
291286, 289, 290mp2an 688 . . . . . . . . 9 0 ∈ dom card
292291rgenw 3075 . . . . . . . 8 𝑛 ∈ (1...𝑁)ℕ0 ∈ dom card
293 finixpnum 35689 . . . . . . . 8 (((1...𝑁) ∈ Fin ∧ ∀𝑛 ∈ (1...𝑁)ℕ0 ∈ dom card) → X𝑛 ∈ (1...𝑁)ℕ0 ∈ dom card)
29424, 292, 293mp2an 688 . . . . . . 7 X𝑛 ∈ (1...𝑁)ℕ0 ∈ dom card
295285, 294eqeltrri 2836 . . . . . 6 (ℕ0m (1...𝑁)) ∈ dom card
296140, 140mapval 8585 . . . . . . . . 9 ((1...𝑁) ↑m (1...𝑁)) = {𝑓𝑓:(1...𝑁)⟶(1...𝑁)}
297 mapfi 9045 . . . . . . . . . 10 (((1...𝑁) ∈ Fin ∧ (1...𝑁) ∈ Fin) → ((1...𝑁) ↑m (1...𝑁)) ∈ Fin)
29824, 24, 297mp2an 688 . . . . . . . . 9 ((1...𝑁) ↑m (1...𝑁)) ∈ Fin
299296, 298eqeltrri 2836 . . . . . . . 8 {𝑓𝑓:(1...𝑁)⟶(1...𝑁)} ∈ Fin
300 f1of 6700 . . . . . . . . 9 (𝑓:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑓:(1...𝑁)⟶(1...𝑁))
301300ss2abi 3996 . . . . . . . 8 {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ⊆ {𝑓𝑓:(1...𝑁)⟶(1...𝑁)}
302 ssfi 8918 . . . . . . . 8 (({𝑓𝑓:(1...𝑁)⟶(1...𝑁)} ∈ Fin ∧ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ⊆ {𝑓𝑓:(1...𝑁)⟶(1...𝑁)}) → {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ∈ Fin)
303299, 301, 302mp2an 688 . . . . . . 7 {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ∈ Fin
304 finnum 9637 . . . . . . 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 9640 . . . . . 6 (((ℕ0m (1...𝑁)) ∈ dom card ∧ {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)} ∈ dom card) → ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∈ dom card)
307295, 305, 306mp2an 688 . . . . 5 ((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∈ dom card
308 ssrab2 4009 . . . . . . . 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 3075 . . . . . . 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 4939 . . . . . . 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 11914 . . . . . . 7 1 ∈ ℕ
313 ne0i 4265 . . . . . . 7 (1 ∈ ℕ → ℕ ≠ ∅)
314 iunconst 4930 . . . . . . 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 3953 . . . . 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 9726 . . . . 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 688 . . . 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 6756 . . . . . . . 8 (𝑠 = (𝑔𝑘) → (1st𝑠) = (1st ‘(𝑔𝑘)))
320319rneqd 5836 . . . . . . 7 (𝑠 = (𝑔𝑘) → ran (1st𝑠) = ran (1st ‘(𝑔𝑘)))
321320sseq1d 3948 . . . . . 6 (𝑠 = (𝑔𝑘) → (ran (1st𝑠) ⊆ (0..^𝑘) ↔ ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘)))
322 fveq2 6756 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = (𝑔𝑘) → (2nd𝑠) = (2nd ‘(𝑔𝑘)))
323322imaeq1d 5957 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = (𝑔𝑘) → ((2nd𝑠) “ (1...𝑗)) = ((2nd ‘(𝑔𝑘)) “ (1...𝑗)))
324323xpeq1d 5609 . . . . . . . . . . . . . . . . . . 19 (𝑠 = (𝑔𝑘) → (((2nd𝑠) “ (1...𝑗)) × {1}) = (((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}))
325322imaeq1d 5957 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = (𝑔𝑘) → ((2nd𝑠) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)))
326325xpeq1d 5609 . . . . . . . . . . . . . . . . . . 19 (𝑠 = (𝑔𝑘) → (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))
327324, 326uneq12d 4094 . . . . . . . . . . . . . . . . . 18 (𝑠 = (𝑔𝑘) → ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))
328319, 327oveq12d 7273 . . . . . . . . . . . . . . . . 17 (𝑠 = (𝑔𝑘) → ((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))))
329328fvoveq1d 7277 . . . . . . . . . . . . . . . 16 (𝑠 = (𝑔𝑘) → (𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))) = (𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))))
330329fveq1d 6758 . . . . . . . . . . . . . . 15 (𝑠 = (𝑔𝑘) → ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) = ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏))
331330breq2d 5082 . . . . . . . . . . . . . 14 (𝑠 = (𝑔𝑘) → (0 ≤ ((𝐹‘(((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ↔ 0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏)))
332328fveq1d 6758 . . . . . . . . . . . . . . 15 (𝑠 = (𝑔𝑘) → (((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) = (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏))
333332neeq1d 3002 . . . . . . . . . . . . . 14 (𝑠 = (𝑔𝑘) → ((((1st𝑠) ∘f + ((((2nd𝑠) “ (1...𝑗)) × {1}) ∪ (((2nd𝑠) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0 ↔ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0))
334331, 333anbi12d 630 . . . . . . . . . . . . 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 3120 . . . . . . . . . . . 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 3404 . . . . . . . . . . 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 4093 . . . . . . . . . 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 9135 . . . . . . . . 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 2749 . . . . . . . 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 3225 . . . . . . 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 3120 . . . . . 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 630 . . . . 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 10166 . . . 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 1449 . . 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 722 . . . 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 722 . . . 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 2738 . . . 4 ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑛) = ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑛)
351 simplr 765 . . . 4 (((𝜑𝑔:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) → 𝑔:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}))
352 simpl 482 . . . . . . 7 ((ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) → ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘))
353352ralimi 3086 . . . . . 6 (∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) → ∀𝑘 ∈ ℕ ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘))
354353adantl 481 . . . . 5 (((𝜑𝑔:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) → ∀𝑘 ∈ ℕ ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘))
355 2fveq3 6761 . . . . . . . 8 (𝑘 = 𝑝 → (1st ‘(𝑔𝑘)) = (1st ‘(𝑔𝑝)))
356355rneqd 5836 . . . . . . 7 (𝑘 = 𝑝 → ran (1st ‘(𝑔𝑘)) = ran (1st ‘(𝑔𝑝)))
357 oveq2 7263 . . . . . . 7 (𝑘 = 𝑝 → (0..^𝑘) = (0..^𝑝))
358356, 357sseq12d 3950 . . . . . 6 (𝑘 = 𝑝 → (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ↔ ran (1st ‘(𝑔𝑝)) ⊆ (0..^𝑝)))
359358rspccva 3551 . . . . 5 ((∀𝑘 ∈ ℕ ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ 𝑝 ∈ ℕ) → ran (1st ‘(𝑔𝑝)) ⊆ (0..^𝑝))
360354, 359sylan 579 . . . 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 763 . . . . . 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 579 . . . . 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 2738 . . . . 5 ((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) = ((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))
365 simpr 484 . . . . . . . 8 ((ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) → ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))
366365ralimi 3086 . . . . . . 7 (∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )) → ∀𝑘 ∈ ℕ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))
367366adantl 481 . . . . . 6 (((𝜑𝑔:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) → ∀𝑘 ∈ ℕ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))
368 2fveq3 6761 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 𝑝 → (2nd ‘(𝑔𝑘)) = (2nd ‘(𝑔𝑝)))
369368imaeq1d 5957 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑝 → ((2nd ‘(𝑔𝑘)) “ (1...𝑗)) = ((2nd ‘(𝑔𝑝)) “ (1...𝑗)))
370369xpeq1d 5609 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑝 → (((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) = (((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}))
371368imaeq1d 5957 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑝 → ((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)))
372371xpeq1d 5609 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑝 → (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))
373370, 372uneq12d 4094 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑝 → ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))
374355, 373oveq12d 7273 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑝 → ((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))))
375 sneq 4568 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑝 → {𝑘} = {𝑝})
376375xpeq2d 5610 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑝 → ((1...𝑁) × {𝑘}) = ((1...𝑁) × {𝑝}))
377374, 376oveq12d 7273 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑝 → (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})) = (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))
378377fveq2d 6760 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑝 → (𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘}))) = (𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝}))))
379378fveq1d 6758 . . . . . . . . . . . . . . 15 (𝑘 = 𝑝 → ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) = ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏))
380379breq2d 5082 . . . . . . . . . . . . . 14 (𝑘 = 𝑝 → (0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ↔ 0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏)))
381374fveq1d 6758 . . . . . . . . . . . . . . 15 (𝑘 = 𝑝 → (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) = (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏))
382381neeq1d 3002 . . . . . . . . . . . . . 14 (𝑘 = 𝑝 → ((((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0 ↔ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0))
383380, 382anbi12d 630 . . . . . . . . . . . . 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 3120 . . . . . . . . . . . 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 3404 . . . . . . . . . . 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 4093 . . . . . . . . . 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 9135 . . . . . . . . 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 2749 . . . . . . . 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 3225 . . . . . . 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 2742 . . . . . . . . 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 3225 . . . . . . . 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 7263 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑚 → (1...𝑗) = (1...𝑚))
393392imaeq2d 5958 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑚 → ((2nd ‘(𝑔𝑝)) “ (1...𝑗)) = ((2nd ‘(𝑔𝑝)) “ (1...𝑚)))
394393xpeq1d 5609 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑚 → (((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) = (((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}))
395 oveq1 7262 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗 = 𝑚 → (𝑗 + 1) = (𝑚 + 1))
396395oveq1d 7270 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = 𝑚 → ((𝑗 + 1)...𝑁) = ((𝑚 + 1)...𝑁))
397396imaeq2d 5958 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 𝑚 → ((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) = ((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)))
398397xpeq1d 5609 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝑚 → (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}) = (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))
399394, 398uneq12d 4094 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑚 → ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})) = ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))
400399oveq2d 7271 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑚 → ((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) = ((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))))
401400fvoveq1d 7277 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝑚 → (𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝}))) = (𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝}))))
402401fveq1d 6758 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑚 → ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) = ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏))
403402breq2d 5082 . . . . . . . . . . . . . . 15 (𝑗 = 𝑚 → (0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ↔ 0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏)))
404400fveq1d 6758 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑚 → (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) = (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏))
405404neeq1d 3002 . . . . . . . . . . . . . . 15 (𝑗 = 𝑚 → ((((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0 ↔ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0))
406403, 405anbi12d 630 . . . . . . . . . . . . . 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 3120 . . . . . . . . . . . . 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 3404 . . . . . . . . . . . 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 4093 . . . . . . . . . . 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 9135 . . . . . . . . . 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 2749 . . . . . . . . 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 3373 . . . . . . . 8 (∃𝑗 ∈ (0...𝑁)𝑞 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) ↔ ∃𝑚 ∈ (0...𝑁)𝑞 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))
413391, 412bitrdi 286 . . . . . . 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 3562 . . . . . 6 ((𝑝 ∈ ℕ ∧ 𝑞 ∈ (0...𝑁)) → (∀𝑘 ∈ ℕ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ) → ∃𝑚 ∈ (0...𝑁)𝑞 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))
415367, 414mpan9 506 . . . . 5 ((((𝜑𝑔:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) ∧ (𝑝 ∈ ℕ ∧ 𝑞 ∈ (0...𝑁))) → ∃𝑚 ∈ (0...𝑁)𝑞 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑝})))‘𝑏) ∧ (((1st ‘(𝑔𝑝)) ∘f + ((((2nd ‘(𝑔𝑝)) “ (1...𝑚)) × {1}) ∪ (((2nd ‘(𝑔𝑝)) “ ((𝑚 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))
416346, 137, 347, 349, 363, 364, 351, 360, 415poimirlem31 35735 . . . 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 35734 . . 3 (((𝜑𝑔:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)})) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < ))) → ∃𝑐𝐼𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
418417anasss 466 . 2 ((𝜑 ∧ (𝑔:ℕ⟶((ℕ0m (1...𝑁)) × {𝑓𝑓:(1...𝑁)–1-1-onto→(1...𝑁)}) ∧ ∀𝑘 ∈ ℕ (ran (1st ‘(𝑔𝑘)) ⊆ (0..^𝑘) ∧ ∀𝑖 ∈ (0...𝑁)∃𝑗 ∈ (0...𝑁)𝑖 = sup(({0} ∪ {𝑎 ∈ (1...𝑁) ∣ ∀𝑏 ∈ (1...𝑎)(0 ≤ ((𝐹‘(((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0}))) ∘f / ((1...𝑁) × {𝑘})))‘𝑏) ∧ (((1st ‘(𝑔𝑘)) ∘f + ((((2nd ‘(𝑔𝑘)) “ (1...𝑗)) × {1}) ∪ (((2nd ‘(𝑔𝑘)) “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑏) ≠ 0)}), ℝ, < )))) → ∃𝑐𝐼𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
419345, 418exlimddv 1939 1 (𝜑 → ∃𝑐𝐼𝑛 ∈ (1...𝑁)∀𝑣 ∈ (𝑅t 𝐼)(𝑐𝑣 → ∀𝑟 ∈ { ≤ , ≤ }∃𝑧𝑣 0𝑟((𝐹𝑧)‘𝑛)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  wo 843  w3a 1085   = wceq 1539  wex 1783  wcel 2108  {cab 2715  wne 2942  wral 3063  wrex 3064  {crab 3067  Vcvv 3422  cun 3881  wss 3883  c0 4253  {csn 4558  {cpr 4560   ciun 4921   class class class wbr 5070   Or wor 5493   × cxp 5578  ccnv 5579  dom cdm 5580  ran crn 5581  cima 5583  Oncon0 6251   Fn wfn 6413  wf 6414  1-1-ontowf1o 6417  cfv 6418  (class class class)co 7255  f cof 7509  ωcom 7687  1st c1st 7802  2nd c2nd 7803  m cmap 8573  Xcixp 8643  cen 8688  Fincfn 8691  supcsup 9129  cardccrd 9624  cc 10800  cr 10801  0cc0 10802  1c1 10803   + caddc 10805   · cmul 10807   < clt 10940  cle 10941  cmin 11135   / cdiv 11562  cn 11903  0cn0 12163  cz 12249  cuz 12511  +crp 12659  (,)cioo 13008  [,]cicc 13011  ...cfz 13168  ..^cfzo 13311  t crest 17048  topGenctg 17065  tcpt 17066   Cn ccn 22283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-inf2 9329  ax-cnex 10858  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879  ax-pre-sup 10880
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-int 4877  df-iun 4923  df-iin 4924  df-disj 5036  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-se 5536  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-isom 6427  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-of 7511  df-om 7688  df-1st 7804  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-1o 8267  df-oadd 8271  df-omul 8272  df-er 8456  df-map 8575  df-pm 8576  df-ixp 8644  df-en 8692  df-dom 8693  df-sdom 8694  df-fin 8695  df-fi 9100  df-sup 9131  df-inf 9132  df-oi 9199  df-dju 9590  df-card 9628  df-acn 9631  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-div 11563  df-nn 11904  df-2 11966  df-3 11967  df-n0 12164  df-xnn0 12236  df-z 12250  df-uz 12512  df-q 12618  df-rp 12660  df-xneg 12777  df-xadd 12778  df-xmul 12779  df-ioo 13012  df-icc 13015  df-fz 13169  df-fzo 13312  df-fl 13440  df-seq 13650  df-exp 13711  df-fac 13916  df-bc 13945  df-hash 13973  df-cj 14738  df-re 14739  df-im 14740  df-sqrt 14874  df-abs 14875  df-clim 15125  df-sum 15326  df-dvds 15892  df-rest 17050  df-topgen 17071  df-pt 17072  df-psmet 20502  df-xmet 20503  df-met 20504  df-bl 20505  df-mopn 20506  df-top 21951  df-topon 21968  df-bases 22004  df-cld 22078  df-ntr 22079  df-cls 22080  df-lp 22195  df-cn 22286  df-cnp 22287  df-t1 22373  df-haus 22374  df-cmp 22446  df-tx 22621  df-hmeo 22814  df-hmph 22815  df-ii 23946
This theorem is referenced by:  poimir  35737
  Copyright terms: Public domain W3C validator