MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imasdsf1olem Structured version   Visualization version   GIF version

Theorem imasdsf1olem 22397
Description: Lemma for imasdsf1o 22398. (Contributed by Mario Carneiro, 21-Aug-2015.) (Proof shortened by AV, 6-Oct-2020.)
Hypotheses
Ref Expression
imasdsf1o.u (𝜑𝑈 = (𝐹s 𝑅))
imasdsf1o.v (𝜑𝑉 = (Base‘𝑅))
imasdsf1o.f (𝜑𝐹:𝑉1-1-onto𝐵)
imasdsf1o.r (𝜑𝑅𝑍)
imasdsf1o.e 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉))
imasdsf1o.d 𝐷 = (dist‘𝑈)
imasdsf1o.m (𝜑𝐸 ∈ (∞Met‘𝑉))
imasdsf1o.x (𝜑𝑋𝑉)
imasdsf1o.y (𝜑𝑌𝑉)
imasdsf1o.w 𝑊 = (ℝ*𝑠s (ℝ* ∖ {-∞}))
imasdsf1o.s 𝑆 = { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))}
imasdsf1o.t 𝑇 = 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔)))
Assertion
Ref Expression
imasdsf1olem (𝜑 → ((𝐹𝑋)𝐷(𝐹𝑌)) = (𝑋𝐸𝑌))
Distinct variable groups:   𝑔,,𝑖,𝑛,𝐹   𝜑,𝑔,,𝑖,𝑛   𝑔,𝑉,,𝑖,𝑛   𝑔,𝐸,𝑖,𝑛   𝑅,𝑔,,𝑖,𝑛   𝑆,𝑔   𝑔,𝑋,,𝑖,𝑛   𝑔,𝑌,,𝑖,𝑛
Allowed substitution hints:   𝐵(𝑔,,𝑖,𝑛)   𝐷(𝑔,,𝑖,𝑛)   𝑆(,𝑖,𝑛)   𝑇(𝑔,,𝑖,𝑛)   𝑈(𝑔,,𝑖,𝑛)   𝐸()   𝑊(𝑔,,𝑖,𝑛)   𝑍(𝑔,,𝑖,𝑛)

Proof of Theorem imasdsf1olem
Dummy variables 𝑓 𝑗 𝑚 𝑝 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 imasdsf1o.u . . . 4 (𝜑𝑈 = (𝐹s 𝑅))
2 imasdsf1o.v . . . 4 (𝜑𝑉 = (Base‘𝑅))
3 imasdsf1o.f . . . . 5 (𝜑𝐹:𝑉1-1-onto𝐵)
4 f1ofo 6285 . . . . 5 (𝐹:𝑉1-1-onto𝐵𝐹:𝑉onto𝐵)
53, 4syl 17 . . . 4 (𝜑𝐹:𝑉onto𝐵)
6 imasdsf1o.r . . . 4 (𝜑𝑅𝑍)
7 eqid 2770 . . . 4 (dist‘𝑅) = (dist‘𝑅)
8 imasdsf1o.d . . . 4 𝐷 = (dist‘𝑈)
9 f1of 6278 . . . . . 6 (𝐹:𝑉1-1-onto𝐵𝐹:𝑉𝐵)
103, 9syl 17 . . . . 5 (𝜑𝐹:𝑉𝐵)
11 imasdsf1o.x . . . . 5 (𝜑𝑋𝑉)
1210, 11ffvelrnd 6503 . . . 4 (𝜑 → (𝐹𝑋) ∈ 𝐵)
13 imasdsf1o.y . . . . 5 (𝜑𝑌𝑉)
1410, 13ffvelrnd 6503 . . . 4 (𝜑 → (𝐹𝑌) ∈ 𝐵)
15 imasdsf1o.s . . . 4 𝑆 = { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))}
16 imasdsf1o.e . . . 4 𝐸 = ((dist‘𝑅) ↾ (𝑉 × 𝑉))
171, 2, 5, 6, 7, 8, 12, 14, 15, 16imasdsval2 16383 . . 3 (𝜑 → ((𝐹𝑋)𝐷(𝐹𝑌)) = inf( 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))), ℝ*, < ))
18 imasdsf1o.t . . . 4 𝑇 = 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔)))
1918infeq1i 8539 . . 3 inf(𝑇, ℝ*, < ) = inf( 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))), ℝ*, < )
2017, 19syl6eqr 2822 . 2 (𝜑 → ((𝐹𝑋)𝐷(𝐹𝑌)) = inf(𝑇, ℝ*, < ))
21 xrsbas 19976 . . . . . . . . . . . 12 * = (Base‘ℝ*𝑠)
22 xrsadd 19977 . . . . . . . . . . . 12 +𝑒 = (+g‘ℝ*𝑠)
23 imasdsf1o.w . . . . . . . . . . . 12 𝑊 = (ℝ*𝑠s (ℝ* ∖ {-∞}))
24 xrsex 19975 . . . . . . . . . . . . 13 *𝑠 ∈ V
2524a1i 11 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ℝ*𝑠 ∈ V)
26 fzfid 12979 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (1...𝑛) ∈ Fin)
27 difss 3886 . . . . . . . . . . . . 13 (ℝ* ∖ {-∞}) ⊆ ℝ*
2827a1i 11 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (ℝ* ∖ {-∞}) ⊆ ℝ*)
29 imasdsf1o.m . . . . . . . . . . . . . . . 16 (𝜑𝐸 ∈ (∞Met‘𝑉))
30 xmetf 22353 . . . . . . . . . . . . . . . 16 (𝐸 ∈ (∞Met‘𝑉) → 𝐸:(𝑉 × 𝑉)⟶ℝ*)
31 ffn 6185 . . . . . . . . . . . . . . . 16 (𝐸:(𝑉 × 𝑉)⟶ℝ*𝐸 Fn (𝑉 × 𝑉))
3229, 30, 313syl 18 . . . . . . . . . . . . . . 15 (𝜑𝐸 Fn (𝑉 × 𝑉))
33 xmetcl 22355 . . . . . . . . . . . . . . . . . . 19 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓𝑉𝑔𝑉) → (𝑓𝐸𝑔) ∈ ℝ*)
34 xmetge0 22368 . . . . . . . . . . . . . . . . . . . 20 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓𝑉𝑔𝑉) → 0 ≤ (𝑓𝐸𝑔))
35 ge0nemnf 12208 . . . . . . . . . . . . . . . . . . . 20 (((𝑓𝐸𝑔) ∈ ℝ* ∧ 0 ≤ (𝑓𝐸𝑔)) → (𝑓𝐸𝑔) ≠ -∞)
3633, 34, 35syl2anc 565 . . . . . . . . . . . . . . . . . . 19 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓𝑉𝑔𝑉) → (𝑓𝐸𝑔) ≠ -∞)
37 eldifsn 4451 . . . . . . . . . . . . . . . . . . 19 ((𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}) ↔ ((𝑓𝐸𝑔) ∈ ℝ* ∧ (𝑓𝐸𝑔) ≠ -∞))
3833, 36, 37sylanbrc 564 . . . . . . . . . . . . . . . . . 18 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓𝑉𝑔𝑉) → (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
39383expb 1112 . . . . . . . . . . . . . . . . 17 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑓𝑉𝑔𝑉)) → (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
4029, 39sylan 561 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑓𝑉𝑔𝑉)) → (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
4140ralrimivva 3119 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑓𝑉𝑔𝑉 (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
42 ffnov 6910 . . . . . . . . . . . . . . 15 (𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}) ↔ (𝐸 Fn (𝑉 × 𝑉) ∧ ∀𝑓𝑉𝑔𝑉 (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞})))
4332, 41, 42sylanbrc 564 . . . . . . . . . . . . . 14 (𝜑𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
4443ad2antrr 697 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
45 ssrab2 3834 . . . . . . . . . . . . . . . . 17 { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} ⊆ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛))
4615, 45eqsstri 3782 . . . . . . . . . . . . . . . 16 𝑆 ⊆ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛))
4746a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → 𝑆 ⊆ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)))
4847sselda 3750 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)))
49 elmapi 8030 . . . . . . . . . . . . . 14 (𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
5048, 49syl 17 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
51 fco 6198 . . . . . . . . . . . . 13 ((𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}) ∧ 𝑔:(1...𝑛)⟶(𝑉 × 𝑉)) → (𝐸𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}))
5244, 50, 51syl2anc 565 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐸𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}))
53 0re 10241 . . . . . . . . . . . . 13 0 ∈ ℝ
54 rexr 10286 . . . . . . . . . . . . . 14 (0 ∈ ℝ → 0 ∈ ℝ*)
55 renemnf 10289 . . . . . . . . . . . . . 14 (0 ∈ ℝ → 0 ≠ -∞)
56 eldifsn 4451 . . . . . . . . . . . . . 14 (0 ∈ (ℝ* ∖ {-∞}) ↔ (0 ∈ ℝ* ∧ 0 ≠ -∞))
5754, 55, 56sylanbrc 564 . . . . . . . . . . . . 13 (0 ∈ ℝ → 0 ∈ (ℝ* ∖ {-∞}))
5853, 57mp1i 13 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 0 ∈ (ℝ* ∖ {-∞}))
59 xaddid2 12277 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ* → (0 +𝑒 𝑥) = 𝑥)
60 xaddid1 12276 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ* → (𝑥 +𝑒 0) = 𝑥)
6159, 60jca 495 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ* → ((0 +𝑒 𝑥) = 𝑥 ∧ (𝑥 +𝑒 0) = 𝑥))
6261adantl 467 . . . . . . . . . . . 12 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ 𝑥 ∈ ℝ*) → ((0 +𝑒 𝑥) = 𝑥 ∧ (𝑥 +𝑒 0) = 𝑥))
6321, 22, 23, 25, 26, 28, 52, 58, 62gsumress 17483 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (ℝ*𝑠 Σg (𝐸𝑔)) = (𝑊 Σg (𝐸𝑔)))
6423, 21ressbas2 16137 . . . . . . . . . . . . 13 ((ℝ* ∖ {-∞}) ⊆ ℝ* → (ℝ* ∖ {-∞}) = (Base‘𝑊))
6527, 64ax-mp 5 . . . . . . . . . . . 12 (ℝ* ∖ {-∞}) = (Base‘𝑊)
6623xrs10 19999 . . . . . . . . . . . 12 0 = (0g𝑊)
6723xrs1cmn 20000 . . . . . . . . . . . . 13 𝑊 ∈ CMnd
6867a1i 11 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑊 ∈ CMnd)
69 c0ex 10235 . . . . . . . . . . . . . 14 0 ∈ V
7069a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 0 ∈ V)
7152, 26, 70fdmfifsupp 8440 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐸𝑔) finSupp 0)
7265, 66, 68, 26, 52, 71gsumcl 18522 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑊 Σg (𝐸𝑔)) ∈ (ℝ* ∖ {-∞}))
7363, 72eqeltrd 2849 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (ℝ*𝑠 Σg (𝐸𝑔)) ∈ (ℝ* ∖ {-∞}))
7473eldifad 3733 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (ℝ*𝑠 Σg (𝐸𝑔)) ∈ ℝ*)
75 eqid 2770 . . . . . . . . 9 (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) = (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔)))
7674, 75fmptd 6527 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))):𝑆⟶ℝ*)
77 frn 6193 . . . . . . . 8 ((𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))):𝑆⟶ℝ* → ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ⊆ ℝ*)
7876, 77syl 17 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ⊆ ℝ*)
7978ralrimiva 3114 . . . . . 6 (𝜑 → ∀𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ⊆ ℝ*)
80 iunss 4693 . . . . . 6 ( 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ⊆ ℝ* ↔ ∀𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ⊆ ℝ*)
8179, 80sylibr 224 . . . . 5 (𝜑 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ⊆ ℝ*)
8218, 81syl5eqss 3796 . . . 4 (𝜑𝑇 ⊆ ℝ*)
83 infxrcl 12367 . . . 4 (𝑇 ⊆ ℝ* → inf(𝑇, ℝ*, < ) ∈ ℝ*)
8482, 83syl 17 . . 3 (𝜑 → inf(𝑇, ℝ*, < ) ∈ ℝ*)
85 xmetcl 22355 . . . 4 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋𝑉𝑌𝑉) → (𝑋𝐸𝑌) ∈ ℝ*)
8629, 11, 13, 85syl3anc 1475 . . 3 (𝜑 → (𝑋𝐸𝑌) ∈ ℝ*)
87 1nn 11232 . . . . . . 7 1 ∈ ℕ
88 1ex 10236 . . . . . . . . . . . 12 1 ∈ V
89 opex 5060 . . . . . . . . . . . 12 𝑋, 𝑌⟩ ∈ V
9088, 89f1osn 6317 . . . . . . . . . . 11 {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}–1-1-onto→{⟨𝑋, 𝑌⟩}
91 f1of 6278 . . . . . . . . . . 11 ({⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}–1-1-onto→{⟨𝑋, 𝑌⟩} → {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶{⟨𝑋, 𝑌⟩})
9290, 91ax-mp 5 . . . . . . . . . 10 {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶{⟨𝑋, 𝑌⟩}
93 opelxpi 5288 . . . . . . . . . . . 12 ((𝑋𝑉𝑌𝑉) → ⟨𝑋, 𝑌⟩ ∈ (𝑉 × 𝑉))
9411, 13, 93syl2anc 565 . . . . . . . . . . 11 (𝜑 → ⟨𝑋, 𝑌⟩ ∈ (𝑉 × 𝑉))
9594snssd 4473 . . . . . . . . . 10 (𝜑 → {⟨𝑋, 𝑌⟩} ⊆ (𝑉 × 𝑉))
96 fss 6196 . . . . . . . . . 10 (({⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶{⟨𝑋, 𝑌⟩} ∧ {⟨𝑋, 𝑌⟩} ⊆ (𝑉 × 𝑉)) → {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉))
9792, 95, 96sylancr 567 . . . . . . . . 9 (𝜑 → {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉))
9829elfvexd 6363 . . . . . . . . . . 11 (𝜑𝑉 ∈ V)
99 xpexg 7106 . . . . . . . . . . 11 ((𝑉 ∈ V ∧ 𝑉 ∈ V) → (𝑉 × 𝑉) ∈ V)
10098, 98, 99syl2anc 565 . . . . . . . . . 10 (𝜑 → (𝑉 × 𝑉) ∈ V)
101 snex 5036 . . . . . . . . . 10 {1} ∈ V
102 elmapg 8021 . . . . . . . . . 10 (((𝑉 × 𝑉) ∈ V ∧ {1} ∈ V) → ({⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑𝑚 {1}) ↔ {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉)))
103100, 101, 102sylancl 566 . . . . . . . . 9 (𝜑 → ({⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑𝑚 {1}) ↔ {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉)))
10497, 103mpbird 247 . . . . . . . 8 (𝜑 → {⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑𝑚 {1}))
105 op1stg 7326 . . . . . . . . . . 11 ((𝑋𝑉𝑌𝑉) → (1st ‘⟨𝑋, 𝑌⟩) = 𝑋)
10611, 13, 105syl2anc 565 . . . . . . . . . 10 (𝜑 → (1st ‘⟨𝑋, 𝑌⟩) = 𝑋)
107106fveq2d 6336 . . . . . . . . 9 (𝜑 → (𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑋))
108 op2ndg 7327 . . . . . . . . . . 11 ((𝑋𝑉𝑌𝑉) → (2nd ‘⟨𝑋, 𝑌⟩) = 𝑌)
10911, 13, 108syl2anc 565 . . . . . . . . . 10 (𝜑 → (2nd ‘⟨𝑋, 𝑌⟩) = 𝑌)
110109fveq2d 6336 . . . . . . . . 9 (𝜑 → (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑌))
111107, 110jca 495 . . . . . . . 8 (𝜑 → ((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑌)))
11224a1i 11 . . . . . . . . . 10 (𝜑 → ℝ*𝑠 ∈ V)
113 snfi 8193 . . . . . . . . . . 11 {1} ∈ Fin
114113a1i 11 . . . . . . . . . 10 (𝜑 → {1} ∈ Fin)
11527a1i 11 . . . . . . . . . 10 (𝜑 → (ℝ* ∖ {-∞}) ⊆ ℝ*)
116 xmetge0 22368 . . . . . . . . . . . . . . 15 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋𝑉𝑌𝑉) → 0 ≤ (𝑋𝐸𝑌))
11729, 11, 13, 116syl3anc 1475 . . . . . . . . . . . . . 14 (𝜑 → 0 ≤ (𝑋𝐸𝑌))
118 ge0nemnf 12208 . . . . . . . . . . . . . 14 (((𝑋𝐸𝑌) ∈ ℝ* ∧ 0 ≤ (𝑋𝐸𝑌)) → (𝑋𝐸𝑌) ≠ -∞)
11986, 117, 118syl2anc 565 . . . . . . . . . . . . 13 (𝜑 → (𝑋𝐸𝑌) ≠ -∞)
120 eldifsn 4451 . . . . . . . . . . . . 13 ((𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞}) ↔ ((𝑋𝐸𝑌) ∈ ℝ* ∧ (𝑋𝐸𝑌) ≠ -∞))
12186, 119, 120sylanbrc 564 . . . . . . . . . . . 12 (𝜑 → (𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞}))
122 fconst6g 6234 . . . . . . . . . . . 12 ((𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞}) → ({1} × {(𝑋𝐸𝑌)}):{1}⟶(ℝ* ∖ {-∞}))
123121, 122syl 17 . . . . . . . . . . 11 (𝜑 → ({1} × {(𝑋𝐸𝑌)}):{1}⟶(ℝ* ∖ {-∞}))
124 fcoconst 6543 . . . . . . . . . . . . . 14 ((𝐸 Fn (𝑉 × 𝑉) ∧ ⟨𝑋, 𝑌⟩ ∈ (𝑉 × 𝑉)) → (𝐸 ∘ ({1} × {⟨𝑋, 𝑌⟩})) = ({1} × {(𝐸‘⟨𝑋, 𝑌⟩)}))
12532, 94, 124syl2anc 565 . . . . . . . . . . . . 13 (𝜑 → (𝐸 ∘ ({1} × {⟨𝑋, 𝑌⟩})) = ({1} × {(𝐸‘⟨𝑋, 𝑌⟩)}))
12688, 89xpsn 6549 . . . . . . . . . . . . . 14 ({1} × {⟨𝑋, 𝑌⟩}) = {⟨1, ⟨𝑋, 𝑌⟩⟩}
127126coeq2i 5421 . . . . . . . . . . . . 13 (𝐸 ∘ ({1} × {⟨𝑋, 𝑌⟩})) = (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})
128 df-ov 6795 . . . . . . . . . . . . . . . 16 (𝑋𝐸𝑌) = (𝐸‘⟨𝑋, 𝑌⟩)
129128eqcomi 2779 . . . . . . . . . . . . . . 15 (𝐸‘⟨𝑋, 𝑌⟩) = (𝑋𝐸𝑌)
130129sneqi 4325 . . . . . . . . . . . . . 14 {(𝐸‘⟨𝑋, 𝑌⟩)} = {(𝑋𝐸𝑌)}
131130xpeq2i 5276 . . . . . . . . . . . . 13 ({1} × {(𝐸‘⟨𝑋, 𝑌⟩)}) = ({1} × {(𝑋𝐸𝑌)})
132125, 127, 1313eqtr3g 2827 . . . . . . . . . . . 12 (𝜑 → (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}) = ({1} × {(𝑋𝐸𝑌)}))
133132feq1d 6170 . . . . . . . . . . 11 (𝜑 → ((𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}):{1}⟶(ℝ* ∖ {-∞}) ↔ ({1} × {(𝑋𝐸𝑌)}):{1}⟶(ℝ* ∖ {-∞})))
134123, 133mpbird 247 . . . . . . . . . 10 (𝜑 → (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}):{1}⟶(ℝ* ∖ {-∞}))
13553, 57mp1i 13 . . . . . . . . . 10 (𝜑 → 0 ∈ (ℝ* ∖ {-∞}))
13661adantl 467 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ*) → ((0 +𝑒 𝑥) = 𝑥 ∧ (𝑥 +𝑒 0) = 𝑥))
13721, 22, 23, 112, 114, 115, 134, 135, 136gsumress 17483 . . . . . . . . 9 (𝜑 → (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})) = (𝑊 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))
138 fconstmpt 5303 . . . . . . . . . . 11 ({1} × {(𝑋𝐸𝑌)}) = (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))
139132, 138syl6eq 2820 . . . . . . . . . 10 (𝜑 → (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}) = (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌)))
140139oveq2d 6808 . . . . . . . . 9 (𝜑 → (𝑊 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})) = (𝑊 Σg (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))))
141 cmnmnd 18414 . . . . . . . . . . 11 (𝑊 ∈ CMnd → 𝑊 ∈ Mnd)
14267, 141mp1i 13 . . . . . . . . . 10 (𝜑𝑊 ∈ Mnd)
14387a1i 11 . . . . . . . . . 10 (𝜑 → 1 ∈ ℕ)
144 eqidd 2771 . . . . . . . . . . 11 (𝑗 = 1 → (𝑋𝐸𝑌) = (𝑋𝐸𝑌))
14565, 144gsumsn 18560 . . . . . . . . . 10 ((𝑊 ∈ Mnd ∧ 1 ∈ ℕ ∧ (𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞})) → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))) = (𝑋𝐸𝑌))
146142, 143, 121, 145syl3anc 1475 . . . . . . . . 9 (𝜑 → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))) = (𝑋𝐸𝑌))
147137, 140, 1463eqtrrd 2809 . . . . . . . 8 (𝜑 → (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))
148 fveq1 6331 . . . . . . . . . . . . . . 15 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝑔‘1) = ({⟨1, ⟨𝑋, 𝑌⟩⟩}‘1))
14988, 89fvsn 6589 . . . . . . . . . . . . . . 15 ({⟨1, ⟨𝑋, 𝑌⟩⟩}‘1) = ⟨𝑋, 𝑌
150148, 149syl6eq 2820 . . . . . . . . . . . . . 14 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝑔‘1) = ⟨𝑋, 𝑌⟩)
151150fveq2d 6336 . . . . . . . . . . . . 13 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (1st ‘(𝑔‘1)) = (1st ‘⟨𝑋, 𝑌⟩))
152151fveq2d 6336 . . . . . . . . . . . 12 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘(1st ‘⟨𝑋, 𝑌⟩)))
153152eqeq1d 2772 . . . . . . . . . . 11 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ↔ (𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑋)))
154150fveq2d 6336 . . . . . . . . . . . . 13 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (2nd ‘(𝑔‘1)) = (2nd ‘⟨𝑋, 𝑌⟩))
155154fveq2d 6336 . . . . . . . . . . . 12 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)))
156155eqeq1d 2772 . . . . . . . . . . 11 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌) ↔ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑌)))
157153, 156anbi12d 608 . . . . . . . . . 10 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ↔ ((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑌))))
158 coeq2 5419 . . . . . . . . . . . 12 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝐸𝑔) = (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}))
159158oveq2d 6808 . . . . . . . . . . 11 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (ℝ*𝑠 Σg (𝐸𝑔)) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))
160159eqeq2d 2780 . . . . . . . . . 10 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)) ↔ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}))))
161157, 160anbi12d 608 . . . . . . . . 9 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))) ↔ (((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))))
162161rspcev 3458 . . . . . . . 8 (({⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑𝑚 {1}) ∧ (((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))) → ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))))
163104, 111, 147, 162syl12anc 1473 . . . . . . 7 (𝜑 → ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))))
164 ovex 6822 . . . . . . . . . 10 (𝑋𝐸𝑌) ∈ V
16575elrnmpt 5510 . . . . . . . . . 10 ((𝑋𝐸𝑌) ∈ V → ((𝑋𝐸𝑌) ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑔𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))))
166164, 165ax-mp 5 . . . . . . . . 9 ((𝑋𝐸𝑌) ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑔𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))
16715rexeqi 3291 . . . . . . . . . . 11 (∃𝑔𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)) ↔ ∃𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))
168 fveq1 6331 . . . . . . . . . . . . . . . 16 ( = 𝑔 → (‘1) = (𝑔‘1))
169168fveq2d 6336 . . . . . . . . . . . . . . 15 ( = 𝑔 → (1st ‘(‘1)) = (1st ‘(𝑔‘1)))
170169fveq2d 6336 . . . . . . . . . . . . . 14 ( = 𝑔 → (𝐹‘(1st ‘(‘1))) = (𝐹‘(1st ‘(𝑔‘1))))
171170eqeq1d 2772 . . . . . . . . . . . . 13 ( = 𝑔 → ((𝐹‘(1st ‘(‘1))) = (𝐹𝑋) ↔ (𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋)))
172 fveq1 6331 . . . . . . . . . . . . . . . 16 ( = 𝑔 → (𝑛) = (𝑔𝑛))
173172fveq2d 6336 . . . . . . . . . . . . . . 15 ( = 𝑔 → (2nd ‘(𝑛)) = (2nd ‘(𝑔𝑛)))
174173fveq2d 6336 . . . . . . . . . . . . . 14 ( = 𝑔 → (𝐹‘(2nd ‘(𝑛))) = (𝐹‘(2nd ‘(𝑔𝑛))))
175174eqeq1d 2772 . . . . . . . . . . . . 13 ( = 𝑔 → ((𝐹‘(2nd ‘(𝑛))) = (𝐹𝑌) ↔ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌)))
176 fveq1 6331 . . . . . . . . . . . . . . . . 17 ( = 𝑔 → (𝑖) = (𝑔𝑖))
177176fveq2d 6336 . . . . . . . . . . . . . . . 16 ( = 𝑔 → (2nd ‘(𝑖)) = (2nd ‘(𝑔𝑖)))
178177fveq2d 6336 . . . . . . . . . . . . . . 15 ( = 𝑔 → (𝐹‘(2nd ‘(𝑖))) = (𝐹‘(2nd ‘(𝑔𝑖))))
179 fveq1 6331 . . . . . . . . . . . . . . . . 17 ( = 𝑔 → (‘(𝑖 + 1)) = (𝑔‘(𝑖 + 1)))
180179fveq2d 6336 . . . . . . . . . . . . . . . 16 ( = 𝑔 → (1st ‘(‘(𝑖 + 1))) = (1st ‘(𝑔‘(𝑖 + 1))))
181180fveq2d 6336 . . . . . . . . . . . . . . 15 ( = 𝑔 → (𝐹‘(1st ‘(‘(𝑖 + 1)))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
182178, 181eqeq12d 2785 . . . . . . . . . . . . . 14 ( = 𝑔 → ((𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))) ↔ (𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
183182ralbidv 3134 . . . . . . . . . . . . 13 ( = 𝑔 → (∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))) ↔ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
184171, 175, 1833anbi123d 1546 . . . . . . . . . . . 12 ( = 𝑔 → (((𝐹‘(1st ‘(‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1))))) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))))
185184rexrab 3520 . . . . . . . . . . 11 (∃𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛))(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))))
186167, 185bitri 264 . . . . . . . . . 10 (∃𝑔𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛))(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))))
187 oveq2 6800 . . . . . . . . . . . . 13 (𝑛 = 1 → (1...𝑛) = (1...1))
188 1z 11608 . . . . . . . . . . . . . 14 1 ∈ ℤ
189 fzsn 12589 . . . . . . . . . . . . . 14 (1 ∈ ℤ → (1...1) = {1})
190188, 189ax-mp 5 . . . . . . . . . . . . 13 (1...1) = {1}
191187, 190syl6eq 2820 . . . . . . . . . . . 12 (𝑛 = 1 → (1...𝑛) = {1})
192191oveq2d 6808 . . . . . . . . . . 11 (𝑛 = 1 → ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) = ((𝑉 × 𝑉) ↑𝑚 {1}))
193 df-3an 1072 . . . . . . . . . . . . 13 (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ↔ (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌)) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
194 ral0 4215 . . . . . . . . . . . . . . . 16 𝑖 ∈ ∅ (𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))
195 oveq1 6799 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 1 → (𝑛 − 1) = (1 − 1))
196 1m1e0 11290 . . . . . . . . . . . . . . . . . . . 20 (1 − 1) = 0
197195, 196syl6eq 2820 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 1 → (𝑛 − 1) = 0)
198197oveq2d 6808 . . . . . . . . . . . . . . . . . 18 (𝑛 = 1 → (1...(𝑛 − 1)) = (1...0))
199 fz10 12568 . . . . . . . . . . . . . . . . . 18 (1...0) = ∅
200198, 199syl6eq 2820 . . . . . . . . . . . . . . . . 17 (𝑛 = 1 → (1...(𝑛 − 1)) = ∅)
201200raleqdv 3292 . . . . . . . . . . . . . . . 16 (𝑛 = 1 → (∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))) ↔ ∀𝑖 ∈ ∅ (𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
202194, 201mpbiri 248 . . . . . . . . . . . . . . 15 (𝑛 = 1 → ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
203202biantrud 515 . . . . . . . . . . . . . 14 (𝑛 = 1 → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌)) ↔ (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌)) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))))
204 fveq2 6332 . . . . . . . . . . . . . . . . . 18 (𝑛 = 1 → (𝑔𝑛) = (𝑔‘1))
205204fveq2d 6336 . . . . . . . . . . . . . . . . 17 (𝑛 = 1 → (2nd ‘(𝑔𝑛)) = (2nd ‘(𝑔‘1)))
206205fveq2d 6336 . . . . . . . . . . . . . . . 16 (𝑛 = 1 → (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹‘(2nd ‘(𝑔‘1))))
207206eqeq1d 2772 . . . . . . . . . . . . . . 15 (𝑛 = 1 → ((𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ↔ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)))
208207anbi2d 606 . . . . . . . . . . . . . 14 (𝑛 = 1 → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌)) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌))))
209203, 208bitr3d 270 . . . . . . . . . . . . 13 (𝑛 = 1 → ((((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌)) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌))))
210193, 209syl5bb 272 . . . . . . . . . . . 12 (𝑛 = 1 → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌))))
211210anbi1d 607 . . . . . . . . . . 11 (𝑛 = 1 → ((((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))) ↔ (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))))
212192, 211rexeqbidv 3301 . . . . . . . . . 10 (𝑛 = 1 → (∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛))(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))))
213186, 212syl5bb 272 . . . . . . . . 9 (𝑛 = 1 → (∃𝑔𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))))
214166, 213syl5bb 272 . . . . . . . 8 (𝑛 = 1 → ((𝑋𝐸𝑌) ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))))
215214rspcev 3458 . . . . . . 7 ((1 ∈ ℕ ∧ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))) → ∃𝑛 ∈ ℕ (𝑋𝐸𝑌) ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
21687, 163, 215sylancr 567 . . . . . 6 (𝜑 → ∃𝑛 ∈ ℕ (𝑋𝐸𝑌) ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
217 eliun 4656 . . . . . 6 ((𝑋𝐸𝑌) ∈ 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑛 ∈ ℕ (𝑋𝐸𝑌) ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
218216, 217sylibr 224 . . . . 5 (𝜑 → (𝑋𝐸𝑌) ∈ 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
219218, 18syl6eleqr 2860 . . . 4 (𝜑 → (𝑋𝐸𝑌) ∈ 𝑇)
220 infxrlb 12368 . . . 4 ((𝑇 ⊆ ℝ* ∧ (𝑋𝐸𝑌) ∈ 𝑇) → inf(𝑇, ℝ*, < ) ≤ (𝑋𝐸𝑌))
22182, 219, 220syl2anc 565 . . 3 (𝜑 → inf(𝑇, ℝ*, < ) ≤ (𝑋𝐸𝑌))
22218eleq2i 2841 . . . . . . 7 (𝑝𝑇𝑝 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
223 eliun 4656 . . . . . . 7 (𝑝 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑛 ∈ ℕ 𝑝 ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
224222, 223bitri 264 . . . . . 6 (𝑝𝑇 ↔ ∃𝑛 ∈ ℕ 𝑝 ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
225 vex 3352 . . . . . . . . 9 𝑝 ∈ V
22675elrnmpt 5510 . . . . . . . . 9 (𝑝 ∈ V → (𝑝 ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑔𝑆 𝑝 = (ℝ*𝑠 Σg (𝐸𝑔))))
227225, 226ax-mp 5 . . . . . . . 8 (𝑝 ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑔𝑆 𝑝 = (ℝ*𝑠 Σg (𝐸𝑔)))
228184, 15elrab2 3516 . . . . . . . . . . . . . . . . 17 (𝑔𝑆 ↔ (𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∧ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))))
229228simprbi 478 . . . . . . . . . . . . . . . 16 (𝑔𝑆 → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
230229adantl 467 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
231230simp2d 1136 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌))
2323ad2antrr 697 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝐹:𝑉1-1-onto𝐵)
233 f1of1 6277 . . . . . . . . . . . . . . . 16 (𝐹:𝑉1-1-onto𝐵𝐹:𝑉1-1𝐵)
234232, 233syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝐹:𝑉1-1𝐵)
235 simplr 744 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑛 ∈ ℕ)
236 elfz1end 12577 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ ↔ 𝑛 ∈ (1...𝑛))
237235, 236sylib 208 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑛 ∈ (1...𝑛))
23850, 237ffvelrnd 6503 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑔𝑛) ∈ (𝑉 × 𝑉))
239 xp2nd 7347 . . . . . . . . . . . . . . . 16 ((𝑔𝑛) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔𝑛)) ∈ 𝑉)
240238, 239syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (2nd ‘(𝑔𝑛)) ∈ 𝑉)
24113ad2antrr 697 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑌𝑉)
242 f1fveq 6661 . . . . . . . . . . . . . . 15 ((𝐹:𝑉1-1𝐵 ∧ ((2nd ‘(𝑔𝑛)) ∈ 𝑉𝑌𝑉)) → ((𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ↔ (2nd ‘(𝑔𝑛)) = 𝑌))
243234, 240, 241, 242syl12anc 1473 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ↔ (2nd ‘(𝑔𝑛)) = 𝑌))
244231, 243mpbid 222 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (2nd ‘(𝑔𝑛)) = 𝑌)
245244oveq2d 6808 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸(2nd ‘(𝑔𝑛))) = (𝑋𝐸𝑌))
246 eleq1 2837 . . . . . . . . . . . . . . . . 17 (𝑚 = 1 → (𝑚 ∈ (1...𝑛) ↔ 1 ∈ (1...𝑛)))
247 fveq2 6332 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 1 → (𝑔𝑚) = (𝑔‘1))
248247fveq2d 6336 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 1 → (2nd ‘(𝑔𝑚)) = (2nd ‘(𝑔‘1)))
249248oveq2d 6808 . . . . . . . . . . . . . . . . . 18 (𝑚 = 1 → (𝑋𝐸(2nd ‘(𝑔𝑚))) = (𝑋𝐸(2nd ‘(𝑔‘1))))
250 oveq2 6800 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 1 → (1...𝑚) = (1...1))
251250, 190syl6eq 2820 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 1 → (1...𝑚) = {1})
252251reseq2d 5534 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 1 → ((𝐸𝑔) ↾ (1...𝑚)) = ((𝐸𝑔) ↾ {1}))
253252oveq2d 6808 . . . . . . . . . . . . . . . . . 18 (𝑚 = 1 → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸𝑔) ↾ {1})))
254249, 253breq12d 4797 . . . . . . . . . . . . . . . . 17 (𝑚 = 1 → ((𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ {1}))))
255246, 254imbi12d 333 . . . . . . . . . . . . . . . 16 (𝑚 = 1 → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚)))) ↔ (1 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ {1})))))
256255imbi2d 329 . . . . . . . . . . . . . . 15 (𝑚 = 1 → ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))))) ↔ (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (1 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ {1}))))))
257 eleq1 2837 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑥 → (𝑚 ∈ (1...𝑛) ↔ 𝑥 ∈ (1...𝑛)))
258 fveq2 6332 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑥 → (𝑔𝑚) = (𝑔𝑥))
259258fveq2d 6336 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑥 → (2nd ‘(𝑔𝑚)) = (2nd ‘(𝑔𝑥)))
260259oveq2d 6808 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑥 → (𝑋𝐸(2nd ‘(𝑔𝑚))) = (𝑋𝐸(2nd ‘(𝑔𝑥))))
261 oveq2 6800 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑥 → (1...𝑚) = (1...𝑥))
262261reseq2d 5534 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑥 → ((𝐸𝑔) ↾ (1...𝑚)) = ((𝐸𝑔) ↾ (1...𝑥)))
263262oveq2d 6808 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑥 → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))))
264260, 263breq12d 4797 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑥 → ((𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥)))))
265257, 264imbi12d 333 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑥 → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚)))) ↔ (𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))))))
266265imbi2d 329 . . . . . . . . . . . . . . 15 (𝑚 = 𝑥 → ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))))) ↔ (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥)))))))
267 eleq1 2837 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝑥 + 1) → (𝑚 ∈ (1...𝑛) ↔ (𝑥 + 1) ∈ (1...𝑛)))
268 fveq2 6332 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = (𝑥 + 1) → (𝑔𝑚) = (𝑔‘(𝑥 + 1)))
269268fveq2d 6336 . . . . . . . . . . . . . . . . . . 19 (𝑚 = (𝑥 + 1) → (2nd ‘(𝑔𝑚)) = (2nd ‘(𝑔‘(𝑥 + 1))))
270269oveq2d 6808 . . . . . . . . . . . . . . . . . 18 (𝑚 = (𝑥 + 1) → (𝑋𝐸(2nd ‘(𝑔𝑚))) = (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))))
271 oveq2 6800 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = (𝑥 + 1) → (1...𝑚) = (1...(𝑥 + 1)))
272271reseq2d 5534 . . . . . . . . . . . . . . . . . . 19 (𝑚 = (𝑥 + 1) → ((𝐸𝑔) ↾ (1...𝑚)) = ((𝐸𝑔) ↾ (1...(𝑥 + 1))))
273272oveq2d 6808 . . . . . . . . . . . . . . . . . 18 (𝑚 = (𝑥 + 1) → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))))
274270, 273breq12d 4797 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝑥 + 1) → ((𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1))))))
275267, 274imbi12d 333 . . . . . . . . . . . . . . . 16 (𝑚 = (𝑥 + 1) → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚)))) ↔ ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))))))
276275imbi2d 329 . . . . . . . . . . . . . . 15 (𝑚 = (𝑥 + 1) → ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))))) ↔ (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1))))))))
277 eleq1 2837 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑛 → (𝑚 ∈ (1...𝑛) ↔ 𝑛 ∈ (1...𝑛)))
278 fveq2 6332 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑛 → (𝑔𝑚) = (𝑔𝑛))
279278fveq2d 6336 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑛 → (2nd ‘(𝑔𝑚)) = (2nd ‘(𝑔𝑛)))
280279oveq2d 6808 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑛 → (𝑋𝐸(2nd ‘(𝑔𝑚))) = (𝑋𝐸(2nd ‘(𝑔𝑛))))
281 oveq2 6800 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛))
282281reseq2d 5534 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑛 → ((𝐸𝑔) ↾ (1...𝑚)) = ((𝐸𝑔) ↾ (1...𝑛)))
283282oveq2d 6808 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑛 → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))))
284280, 283breq12d 4797 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑛 → ((𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔𝑛))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛)))))
285277, 284imbi12d 333 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑛 → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚)))) ↔ (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑛))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))))))
286285imbi2d 329 . . . . . . . . . . . . . . 15 (𝑚 = 𝑛 → ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))))) ↔ (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑛))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛)))))))
28729ad2antrr 697 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝐸 ∈ (∞Met‘𝑉))
28811ad2antrr 697 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑋𝑉)
289 nnuz 11924 . . . . . . . . . . . . . . . . . . . . . . 23 ℕ = (ℤ‘1)
290235, 289syl6eleq 2859 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑛 ∈ (ℤ‘1))
291 eluzfz1 12554 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (ℤ‘1) → 1 ∈ (1...𝑛))
292290, 291syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 1 ∈ (1...𝑛))
29350, 292ffvelrnd 6503 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑔‘1) ∈ (𝑉 × 𝑉))
294 xp2nd 7347 . . . . . . . . . . . . . . . . . . . 20 ((𝑔‘1) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔‘1)) ∈ 𝑉)
295293, 294syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (2nd ‘(𝑔‘1)) ∈ 𝑉)
296 xmetcl 22355 . . . . . . . . . . . . . . . . . . 19 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋𝑉 ∧ (2nd ‘(𝑔‘1)) ∈ 𝑉) → (𝑋𝐸(2nd ‘(𝑔‘1))) ∈ ℝ*)
297287, 288, 295, 296syl3anc 1475 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) ∈ ℝ*)
298 xrleid 12187 . . . . . . . . . . . . . . . . . 18 ((𝑋𝐸(2nd ‘(𝑔‘1))) ∈ ℝ* → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑋𝐸(2nd ‘(𝑔‘1))))
299297, 298syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑋𝐸(2nd ‘(𝑔‘1))))
300142ad2antrr 697 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑊 ∈ Mnd)
30187a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 1 ∈ ℕ)
30244, 293ffvelrnd 6503 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐸‘(𝑔‘1)) ∈ (ℝ* ∖ {-∞}))
303 fveq2 6332 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 1 → (𝑔𝑗) = (𝑔‘1))
304303fveq2d 6336 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 1 → (𝐸‘(𝑔𝑗)) = (𝐸‘(𝑔‘1)))
30565, 304gsumsn 18560 . . . . . . . . . . . . . . . . . . 19 ((𝑊 ∈ Mnd ∧ 1 ∈ ℕ ∧ (𝐸‘(𝑔‘1)) ∈ (ℝ* ∖ {-∞})) → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝐸‘(𝑔𝑗)))) = (𝐸‘(𝑔‘1)))
306300, 301, 302, 305syl3anc 1475 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝐸‘(𝑔𝑗)))) = (𝐸‘(𝑔‘1)))
307287, 30syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝐸:(𝑉 × 𝑉)⟶ℝ*)
308 fcompt 6542 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐸:(𝑉 × 𝑉)⟶ℝ*𝑔:(1...𝑛)⟶(𝑉 × 𝑉)) → (𝐸𝑔) = (𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))))
309307, 50, 308syl2anc 565 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐸𝑔) = (𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))))
310309reseq1d 5533 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝐸𝑔) ↾ {1}) = ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))) ↾ {1}))
311292snssd 4473 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → {1} ⊆ (1...𝑛))
312311resmptd 5593 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))) ↾ {1}) = (𝑗 ∈ {1} ↦ (𝐸‘(𝑔𝑗))))
313310, 312eqtrd 2804 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝐸𝑔) ↾ {1}) = (𝑗 ∈ {1} ↦ (𝐸‘(𝑔𝑗))))
314313oveq2d 6808 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑊 Σg ((𝐸𝑔) ↾ {1})) = (𝑊 Σg (𝑗 ∈ {1} ↦ (𝐸‘(𝑔𝑗)))))
315 df-ov 6795 . . . . . . . . . . . . . . . . . . 19 (𝑋𝐸(2nd ‘(𝑔‘1))) = (𝐸‘⟨𝑋, (2nd ‘(𝑔‘1))⟩)
316 1st2nd2 7353 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔‘1) ∈ (𝑉 × 𝑉) → (𝑔‘1) = ⟨(1st ‘(𝑔‘1)), (2nd ‘(𝑔‘1))⟩)
317293, 316syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑔‘1) = ⟨(1st ‘(𝑔‘1)), (2nd ‘(𝑔‘1))⟩)
318230simp1d 1135 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋))
319 xp1st 7346 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔‘1) ∈ (𝑉 × 𝑉) → (1st ‘(𝑔‘1)) ∈ 𝑉)
320293, 319syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (1st ‘(𝑔‘1)) ∈ 𝑉)
321 f1fveq 6661 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹:𝑉1-1𝐵 ∧ ((1st ‘(𝑔‘1)) ∈ 𝑉𝑋𝑉)) → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ↔ (1st ‘(𝑔‘1)) = 𝑋))
322234, 320, 288, 321syl12anc 1473 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ↔ (1st ‘(𝑔‘1)) = 𝑋))
323318, 322mpbid 222 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (1st ‘(𝑔‘1)) = 𝑋)
324323opeq1d 4543 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ⟨(1st ‘(𝑔‘1)), (2nd ‘(𝑔‘1))⟩ = ⟨𝑋, (2nd ‘(𝑔‘1))⟩)
325317, 324eqtr2d 2805 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ⟨𝑋, (2nd ‘(𝑔‘1))⟩ = (𝑔‘1))
326325fveq2d 6336 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐸‘⟨𝑋, (2nd ‘(𝑔‘1))⟩) = (𝐸‘(𝑔‘1)))
327315, 326syl5eq 2816 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) = (𝐸‘(𝑔‘1)))
328306, 314, 3273eqtr4d 2814 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑊 Σg ((𝐸𝑔) ↾ {1})) = (𝑋𝐸(2nd ‘(𝑔‘1))))
329299, 328breqtrrd 4812 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ {1})))
330329a1d 25 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (1 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ {1}))))
331 simprl 746 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ ℕ)
332331, 289syl6eleq 2859 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ (ℤ‘1))
333 simprr 748 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑥 + 1) ∈ (1...𝑛))
334 peano2fzr 12560 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ (ℤ‘1) ∧ (𝑥 + 1) ∈ (1...𝑛)) → 𝑥 ∈ (1...𝑛))
335332, 333, 334syl2anc 565 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ (1...𝑛))
336335expr 444 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ 𝑥 ∈ ℕ) → ((𝑥 + 1) ∈ (1...𝑛) → 𝑥 ∈ (1...𝑛)))
337336imim1d 82 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ 𝑥 ∈ ℕ) → ((𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥)))) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))))))
338287adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐸 ∈ (∞Met‘𝑉))
339288adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑋𝑉)
34050adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
341340, 335ffvelrnd 6503 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔𝑥) ∈ (𝑉 × 𝑉))
342 xp2nd 7347 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔𝑥) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔𝑥)) ∈ 𝑉)
343341, 342syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (2nd ‘(𝑔𝑥)) ∈ 𝑉)
344 xmetcl 22355 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋𝑉 ∧ (2nd ‘(𝑔𝑥)) ∈ 𝑉) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ∈ ℝ*)
345338, 339, 343, 344syl3anc 1475 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ∈ ℝ*)
34667a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑊 ∈ CMnd)
347 fzfid 12979 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...𝑥) ∈ Fin)
34852adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}))
349 fzsuc 12594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ (ℤ‘1) → (1...(𝑥 + 1)) = ((1...𝑥) ∪ {(𝑥 + 1)}))
350332, 349syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...(𝑥 + 1)) = ((1...𝑥) ∪ {(𝑥 + 1)}))
351 elfzuz3 12545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑥 + 1) ∈ (1...𝑛) → 𝑛 ∈ (ℤ‘(𝑥 + 1)))
352351ad2antll 700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑛 ∈ (ℤ‘(𝑥 + 1)))
353 fzss2 12587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 ∈ (ℤ‘(𝑥 + 1)) → (1...(𝑥 + 1)) ⊆ (1...𝑛))
354352, 353syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...(𝑥 + 1)) ⊆ (1...𝑛))
355350, 354eqsstr3d 3787 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((1...𝑥) ∪ {(𝑥 + 1)}) ⊆ (1...𝑛))
356355unssad 3939 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...𝑥) ⊆ (1...𝑛))
357348, 356fssresd 6211 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸𝑔) ↾ (1...𝑥)):(1...𝑥)⟶(ℝ* ∖ {-∞}))
35869a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 0 ∈ V)
359357, 347, 358fdmfifsupp 8440 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸𝑔) ↾ (1...𝑥)) finSupp 0)
36065, 66, 346, 347, 357, 359gsumcl 18522 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) ∈ (ℝ* ∖ {-∞}))
361360eldifad 3733 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) ∈ ℝ*)
362338, 30syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐸:(𝑉 × 𝑉)⟶ℝ*)
363340, 333ffvelrnd 6503 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉))
364362, 363ffvelrnd 6503 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) ∈ ℝ*)
365 xleadd1a 12287 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑋𝐸(2nd ‘(𝑔𝑥))) ∈ ℝ* ∧ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) ∈ ℝ* ∧ (𝐸‘(𝑔‘(𝑥 + 1))) ∈ ℝ*) ∧ (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥)))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
366365ex 397 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑋𝐸(2nd ‘(𝑔𝑥))) ∈ ℝ* ∧ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) ∈ ℝ* ∧ (𝐸‘(𝑔‘(𝑥 + 1))) ∈ ℝ*) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
367345, 361, 364, 366syl3anc 1475 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
368 xp2nd 7347 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
369363, 368syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
370 xmettri 22375 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑋𝑉 ∧ (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉 ∧ (2nd ‘(𝑔𝑥)) ∈ 𝑉)) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 ((2nd ‘(𝑔𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1))))))
371338, 339, 369, 343, 370syl13anc 1477 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 ((2nd ‘(𝑔𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1))))))
372 1st2nd2 7353 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉) → (𝑔‘(𝑥 + 1)) = ⟨(1st ‘(𝑔‘(𝑥 + 1))), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
373363, 372syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘(𝑥 + 1)) = ⟨(1st ‘(𝑔‘(𝑥 + 1))), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
374 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑖 = 𝑥 → (𝑔𝑖) = (𝑔𝑥))
375374fveq2d 6336 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 = 𝑥 → (2nd ‘(𝑔𝑖)) = (2nd ‘(𝑔𝑥)))
376375fveq2d 6336 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑖 = 𝑥 → (𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(2nd ‘(𝑔𝑥))))
377 fvoveq1 6815 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑖 = 𝑥 → (𝑔‘(𝑖 + 1)) = (𝑔‘(𝑥 + 1)))
378377fveq2d 6336 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 = 𝑥 → (1st ‘(𝑔‘(𝑖 + 1))) = (1st ‘(𝑔‘(𝑥 + 1))))
379378fveq2d 6336 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑖 = 𝑥 → (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))))
380376, 379eqeq12d 2785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑖 = 𝑥 → ((𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))) ↔ (𝐹‘(2nd ‘(𝑔𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1))))))
381230simp3d 1137 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
382381adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
383 nnz 11600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑥 ∈ ℕ → 𝑥 ∈ ℤ)
384383ad2antrl 699 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ ℤ)
385 eluzp1m1 11911 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑥 ∈ ℤ ∧ 𝑛 ∈ (ℤ‘(𝑥 + 1))) → (𝑛 − 1) ∈ (ℤ𝑥))
386384, 352, 385syl2anc 565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑛 − 1) ∈ (ℤ𝑥))
387 elfzuzb 12542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 ∈ (1...(𝑛 − 1)) ↔ (𝑥 ∈ (ℤ‘1) ∧ (𝑛 − 1) ∈ (ℤ𝑥)))
388332, 386, 387sylanbrc 564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ (1...(𝑛 − 1)))
389380, 382, 388rspcdva 3464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐹‘(2nd ‘(𝑔𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))))
390234adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐹:𝑉1-1𝐵)
391 xp1st 7346 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉) → (1st ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
392363, 391syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1st ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
393 f1fveq 6661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐹:𝑉1-1𝐵 ∧ ((2nd ‘(𝑔𝑥)) ∈ 𝑉 ∧ (1st ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)) → ((𝐹‘(2nd ‘(𝑔𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))) ↔ (2nd ‘(𝑔𝑥)) = (1st ‘(𝑔‘(𝑥 + 1)))))
394390, 343, 392, 393syl12anc 1473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐹‘(2nd ‘(𝑔𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))) ↔ (2nd ‘(𝑔𝑥)) = (1st ‘(𝑔‘(𝑥 + 1)))))
395389, 394mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (2nd ‘(𝑔𝑥)) = (1st ‘(𝑔‘(𝑥 + 1))))
396395opeq1d 4543 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ⟨(2nd ‘(𝑔𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩ = ⟨(1st ‘(𝑔‘(𝑥 + 1))), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
397373, 396eqtr4d 2807 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘(𝑥 + 1)) = ⟨(2nd ‘(𝑔𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
398397fveq2d 6336 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) = (𝐸‘⟨(2nd ‘(𝑔𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩))
399 df-ov 6795 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2nd ‘(𝑔𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) = (𝐸‘⟨(2nd ‘(𝑔𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
400398, 399syl6eqr 2822 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) = ((2nd ‘(𝑔𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1)))))
401400oveq2d 6808 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) = ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 ((2nd ‘(𝑔𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1))))))
402371, 401breqtrrd 4812 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
403 xmetcl 22355 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋𝑉 ∧ (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
404338, 339, 369, 403syl3anc 1475 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
405345, 364xaddcld 12335 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
406361, 364xaddcld 12335 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
407 xrletr 12193 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ∈ ℝ* ∧ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ* ∧ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*) → (((𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∧ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
408404, 405, 406, 407syl3anc 1475 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (((𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∧ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
409402, 408mpand 667 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
410367, 409syld 47 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
411 xrex 12031 . . . . . . . . . . . . . . . . . . . . . . . . . 26 * ∈ V
412411, 27ssexi 4934 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ℝ* ∖ {-∞}) ∈ V
41323, 22ressplusg 16200 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((ℝ* ∖ {-∞}) ∈ V → +𝑒 = (+g𝑊))
414412, 413ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 +𝑒 = (+g𝑊)
41544ad2antrr 697 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...𝑥)) → 𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
416 fzelp1 12599 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 ∈ (1...𝑥) → 𝑗 ∈ (1...(𝑥 + 1)))
41750ad2antrr 697 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...(𝑥 + 1))) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
418354sselda 3750 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...(𝑥 + 1))) → 𝑗 ∈ (1...𝑛))
419417, 418ffvelrnd 6503 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...(𝑥 + 1))) → (𝑔𝑗) ∈ (𝑉 × 𝑉))
420416, 419sylan2 572 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...𝑥)) → (𝑔𝑗) ∈ (𝑉 × 𝑉))
421415, 420ffvelrnd 6503 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...𝑥)) → (𝐸‘(𝑔𝑗)) ∈ (ℝ* ∖ {-∞}))
422 fzp1disj 12605 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((1...𝑥) ∩ {(𝑥 + 1)}) = ∅
423422a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((1...𝑥) ∩ {(𝑥 + 1)}) = ∅)
424 disjsn 4381 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((1...𝑥) ∩ {(𝑥 + 1)}) = ∅ ↔ ¬ (𝑥 + 1) ∈ (1...𝑥))
425423, 424sylib 208 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ¬ (𝑥 + 1) ∈ (1...𝑥))
42644adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
427426, 363ffvelrnd 6503 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) ∈ (ℝ* ∖ {-∞}))
428 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = (𝑥 + 1) → (𝑔𝑗) = (𝑔‘(𝑥 + 1)))
429428fveq2d 6336 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = (𝑥 + 1) → (𝐸‘(𝑔𝑗)) = (𝐸‘(𝑔‘(𝑥 + 1))))
43065, 414, 346, 347, 421, 333, 425, 427, 429gsumunsn 18565 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔𝑗)))) = ((𝑊 Σg (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔𝑗)))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
431309adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸𝑔) = (𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))))
432431, 350reseq12d 5535 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸𝑔) ↾ (1...(𝑥 + 1))) = ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))) ↾ ((1...𝑥) ∪ {(𝑥 + 1)})))
433355resmptd 5593 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))) ↾ ((1...𝑥) ∪ {(𝑥 + 1)})) = (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔𝑗))))
434432, 433eqtrd 2804 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸𝑔) ↾ (1...(𝑥 + 1))) = (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔𝑗))))
435434oveq2d 6808 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))) = (𝑊 Σg (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔𝑗)))))
436431reseq1d 5533 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸𝑔) ↾ (1...𝑥)) = ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))) ↾ (1...𝑥)))
437356resmptd 5593 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))) ↾ (1...𝑥)) = (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔𝑗))))
438436, 437eqtrd 2804 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸𝑔) ↾ (1...𝑥)) = (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔𝑗))))
439438oveq2d 6808 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) = (𝑊 Σg (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔𝑗)))))
440439oveq1d 6807 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) = ((𝑊 Σg (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔𝑗)))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
441430, 435, 4403eqtr4d 2814 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))) = ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
442441breq2d 4796 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))) ↔ (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
443410, 442sylibrd 249 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1))))))
444443expr 444 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ 𝑥 ∈ ℕ) → ((𝑥 + 1) ∈ (1...𝑛) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))))))
445444a2d 29 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ 𝑥 ∈ ℕ) → (((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥)))) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))))))
446337, 445syld 47 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ 𝑥 ∈ ℕ) → ((𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥)))) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))))))
447446expcom 398 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℕ → (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥)))) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1))))))))
448447a2d 29 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℕ → ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))))) → (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1))))))))
449256, 266, 276, 286, 330, 448nnind 11239 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑛))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))))))
450235, 449mpcom 38 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑛))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛)))))
451237, 450mpd 15 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸(2nd ‘(𝑔𝑛))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))))
452245, 451eqbrtrrd 4808 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸𝑌) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))))
453 ffn 6185 . . . . . . . . . . . . . 14 ((𝐸𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}) → (𝐸𝑔) Fn (1...𝑛))
454 fnresdm 6140 . . . . . . . . . . . . . 14 ((𝐸𝑔) Fn (1...𝑛) → ((𝐸𝑔) ↾ (1...𝑛)) = (𝐸𝑔))
45552, 453, 4543syl 18 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝐸𝑔) ↾ (1...𝑛)) = (𝐸𝑔))
456455oveq2d 6808 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))) = (𝑊 Σg (𝐸𝑔)))
45763, 456eqtr4d 2807 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (ℝ*𝑠 Σg (𝐸𝑔)) = (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))))
458452, 457breqtrrd 4812 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸𝑌) ≤ (ℝ*𝑠 Σg (𝐸𝑔)))
459 breq2 4788 . . . . . . . . . 10 (𝑝 = (ℝ*𝑠 Σg (𝐸𝑔)) → ((𝑋𝐸𝑌) ≤ 𝑝 ↔ (𝑋𝐸𝑌) ≤ (ℝ*𝑠 Σg (𝐸𝑔))))
460458, 459syl5ibrcom 237 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑝 = (ℝ*𝑠 Σg (𝐸𝑔)) → (𝑋𝐸𝑌) ≤ 𝑝))
461460rexlimdva 3178 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (∃𝑔𝑆 𝑝 = (ℝ*𝑠 Σg (𝐸𝑔)) → (𝑋𝐸𝑌) ≤ 𝑝))
462227, 461syl5bi 232 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝑝 ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) → (𝑋𝐸𝑌) ≤ 𝑝))
463462rexlimdva 3178 . . . . . 6 (𝜑 → (∃𝑛 ∈ ℕ 𝑝 ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) → (𝑋𝐸𝑌) ≤ 𝑝))
464224, 463syl5bi 232 . . . . 5 (𝜑 → (𝑝𝑇 → (𝑋𝐸𝑌) ≤ 𝑝))
465464ralrimiv 3113 . . . 4 (𝜑 → ∀𝑝𝑇 (𝑋𝐸𝑌) ≤ 𝑝)
466 infxrgelb 12369 . . . . 5 ((𝑇 ⊆ ℝ* ∧ (𝑋𝐸𝑌) ∈ ℝ*) → ((𝑋𝐸𝑌) ≤ inf(𝑇, ℝ*, < ) ↔ ∀𝑝𝑇 (𝑋𝐸𝑌) ≤ 𝑝))
46782, 86, 466syl2anc 565 . . . 4 (𝜑 → ((𝑋𝐸𝑌) ≤ inf(𝑇, ℝ*, < ) ↔ ∀𝑝𝑇 (𝑋𝐸𝑌) ≤ 𝑝))
468465, 467mpbird 247 . . 3 (𝜑 → (𝑋𝐸𝑌) ≤ inf(𝑇, ℝ*, < ))
46984, 86, 221, 468xrletrid 12190 . 2 (𝜑 → inf(𝑇, ℝ*, < ) = (𝑋𝐸𝑌))
47020, 469eqtrd 2804 1 (𝜑 → ((𝐹𝑋)𝐷(𝐹𝑌)) = (𝑋𝐸𝑌))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  w3a 1070   = wceq 1630  wcel 2144  wne 2942  wral 3060  wrex 3061  {crab 3064  Vcvv 3349  cdif 3718  cun 3719  cin 3720  wss 3721  c0 4061  {csn 4314  cop 4320   ciun 4652   class class class wbr 4784  cmpt 4861   × cxp 5247  ran crn 5250  cres 5251  ccom 5253   Fn wfn 6026  wf 6027  1-1wf1 6028  ontowfo 6029  1-1-ontowf1o 6030  cfv 6031  (class class class)co 6792  1st c1st 7312  2nd c2nd 7313  𝑚 cmap 8008  Fincfn 8108  infcinf 8502  cr 10136  0cc0 10137  1c1 10138   + caddc 10140  -∞cmnf 10273  *cxr 10274   < clt 10275  cle 10276  cmin 10467  cn 11221  cz 11578  cuz 11887   +𝑒 cxad 12148  ...cfz 12532  Basecbs 16063  s cress 16064  +gcplusg 16148  distcds 16157   Σg cgsu 16308  *𝑠cxrs 16367  s cimas 16371  Mndcmnd 17501  CMndccmn 18399  ∞Metcxmt 19945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-8 2146  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-rep 4902  ax-sep 4912  ax-nul 4920  ax-pow 4971  ax-pr 5034  ax-un 7095  ax-inf2 8701  ax-cnex 10193  ax-resscn 10194  ax-1cn 10195  ax-icn 10196  ax-addcl 10197  ax-addrcl 10198  ax-mulcl 10199  ax-mulrcl 10200  ax-mulcom 10201  ax-addass 10202  ax-mulass 10203  ax-distr 10204  ax-i2m1 10205  ax-1ne0 10206  ax-1rid 10207  ax-rnegex 10208  ax-rrecex 10209  ax-cnre 10210  ax-pre-lttri 10211  ax-pre-lttrn 10212  ax-pre-ltadd 10213  ax-pre-mulgt0 10214  ax-pre-sup 10215
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1071  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-nel 3046  df-ral 3065  df-rex 3066  df-reu 3067  df-rmo 3068  df-rab 3069  df-v 3351  df-sbc 3586  df-csb 3681  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-pss 3737  df-nul 4062  df-if 4224  df-pw 4297  df-sn 4315  df-pr 4317  df-tp 4319  df-op 4321  df-uni 4573  df-int 4610  df-iun 4654  df-iin 4655  df-br 4785  df-opab 4845  df-mpt 4862  df-tr 4885  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-isom 6040  df-riota 6753  df-ov 6795  df-oprab 6796  df-mpt2 6797  df-of 7043  df-om 7212  df-1st 7314  df-2nd 7315  df-supp 7446  df-wrecs 7558  df-recs 7620  df-rdg 7658  df-1o 7712  df-oadd 7716  df-er 7895  df-map 8010  df-en 8109  df-dom 8110  df-sdom 8111  df-fin 8112  df-fsupp 8431  df-sup 8503  df-inf 8504  df-oi 8570  df-card 8964  df-pnf 10277  df-mnf 10278  df-xr 10279  df-ltxr 10280  df-le 10281  df-sub 10469  df-neg 10470  df-div 10886  df-nn 11222  df-2 11280  df-3 11281  df-4 11282  df-5 11283  df-6 11284  df-7 11285  df-8 11286  df-9 11287  df-n0 11494  df-z 11579  df-dec 11695  df-uz 11888  df-rp 12035  df-xneg 12150  df-xadd 12151  df-xmul 12152  df-fz 12533  df-fzo 12673  df-seq 13008  df-hash 13321  df-struct 16065  df-ndx 16066  df-slot 16067  df-base 16069  df-sets 16070  df-ress 16071  df-plusg 16161  df-mulr 16162  df-sca 16164  df-vsca 16165  df-ip 16166  df-tset 16167  df-ple 16168  df-ds 16171  df-0g 16309  df-gsum 16310  df-xrs 16369  df-imas 16375  df-mre 16453  df-mrc 16454  df-acs 16456  df-mgm 17449  df-sgrp 17491  df-mnd 17502  df-submnd 17543  df-mulg 17748  df-cntz 17956  df-cmn 18401  df-xmet 19953
This theorem is referenced by:  imasdsf1o  22398
  Copyright terms: Public domain W3C validator