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

Theorem imasdsf1olem 21936
Description: Lemma for imasdsf1o 21937. (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 6042 . . . . 5 (𝐹:𝑉1-1-onto𝐵𝐹:𝑉onto𝐵)
53, 4syl 17 . . . 4 (𝜑𝐹:𝑉onto𝐵)
6 imasdsf1o.r . . . 4 (𝜑𝑅𝑍)
7 eqid 2609 . . . 4 (dist‘𝑅) = (dist‘𝑅)
8 imasdsf1o.d . . . 4 𝐷 = (dist‘𝑈)
9 f1of 6035 . . . . . 6 (𝐹:𝑉1-1-onto𝐵𝐹:𝑉𝐵)
103, 9syl 17 . . . . 5 (𝜑𝐹:𝑉𝐵)
11 imasdsf1o.x . . . . 5 (𝜑𝑋𝑉)
1210, 11ffvelrnd 6253 . . . 4 (𝜑 → (𝐹𝑋) ∈ 𝐵)
13 imasdsf1o.y . . . . 5 (𝜑𝑌𝑉)
1410, 13ffvelrnd 6253 . . . 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 15948 . . 3 (𝜑 → ((𝐹𝑋)𝐷(𝐹𝑌)) = inf( 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))), ℝ*, < ))
18 imasdsf1o.t . . . 4 𝑇 = 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔)))
1918infeq1i 8245 . . 3 inf(𝑇, ℝ*, < ) = inf( 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))), ℝ*, < )
2017, 19syl6eqr 2661 . 2 (𝜑 → ((𝐹𝑋)𝐷(𝐹𝑌)) = inf(𝑇, ℝ*, < ))
21 xrsbas 19530 . . . . . . . . . . . 12 * = (Base‘ℝ*𝑠)
22 xrsadd 19531 . . . . . . . . . . . 12 +𝑒 = (+g‘ℝ*𝑠)
23 imasdsf1o.w . . . . . . . . . . . 12 𝑊 = (ℝ*𝑠s (ℝ* ∖ {-∞}))
24 xrsex 19529 . . . . . . . . . . . . 13 *𝑠 ∈ V
2524a1i 11 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ℝ*𝑠 ∈ V)
26 fzfid 12592 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (1...𝑛) ∈ Fin)
27 difss 3698 . . . . . . . . . . . . 13 (ℝ* ∖ {-∞}) ⊆ ℝ*
2827a1i 11 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (ℝ* ∖ {-∞}) ⊆ ℝ*)
29 imasdsf1o.m . . . . . . . . . . . . . . . 16 (𝜑𝐸 ∈ (∞Met‘𝑉))
30 xmetf 21892 . . . . . . . . . . . . . . . 16 (𝐸 ∈ (∞Met‘𝑉) → 𝐸:(𝑉 × 𝑉)⟶ℝ*)
31 ffn 5944 . . . . . . . . . . . . . . . 16 (𝐸:(𝑉 × 𝑉)⟶ℝ*𝐸 Fn (𝑉 × 𝑉))
3229, 30, 313syl 18 . . . . . . . . . . . . . . 15 (𝜑𝐸 Fn (𝑉 × 𝑉))
33 xmetcl 21894 . . . . . . . . . . . . . . . . . . 19 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓𝑉𝑔𝑉) → (𝑓𝐸𝑔) ∈ ℝ*)
34 xmetge0 21907 . . . . . . . . . . . . . . . . . . . 20 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓𝑉𝑔𝑉) → 0 ≤ (𝑓𝐸𝑔))
35 ge0nemnf 11840 . . . . . . . . . . . . . . . . . . . 20 (((𝑓𝐸𝑔) ∈ ℝ* ∧ 0 ≤ (𝑓𝐸𝑔)) → (𝑓𝐸𝑔) ≠ -∞)
3633, 34, 35syl2anc 690 . . . . . . . . . . . . . . . . . . 19 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓𝑉𝑔𝑉) → (𝑓𝐸𝑔) ≠ -∞)
37 eldifsn 4259 . . . . . . . . . . . . . . . . . . 19 ((𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}) ↔ ((𝑓𝐸𝑔) ∈ ℝ* ∧ (𝑓𝐸𝑔) ≠ -∞))
3833, 36, 37sylanbrc 694 . . . . . . . . . . . . . . . . . 18 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑓𝑉𝑔𝑉) → (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
39383expb 1257 . . . . . . . . . . . . . . . . 17 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑓𝑉𝑔𝑉)) → (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
4029, 39sylan 486 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑓𝑉𝑔𝑉)) → (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
4140ralrimivva 2953 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑓𝑉𝑔𝑉 (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞}))
42 ffnov 6640 . . . . . . . . . . . . . . 15 (𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}) ↔ (𝐸 Fn (𝑉 × 𝑉) ∧ ∀𝑓𝑉𝑔𝑉 (𝑓𝐸𝑔) ∈ (ℝ* ∖ {-∞})))
4332, 41, 42sylanbrc 694 . . . . . . . . . . . . . 14 (𝜑𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
4443ad2antrr 757 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
45 ssrab2 3649 . . . . . . . . . . . . . . . . 17 { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} ⊆ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛))
4615, 45eqsstri 3597 . . . . . . . . . . . . . . . 16 𝑆 ⊆ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛))
4746a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → 𝑆 ⊆ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)))
4847sselda 3567 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)))
49 elmapi 7743 . . . . . . . . . . . . . 14 (𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
5048, 49syl 17 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
51 fco 5957 . . . . . . . . . . . . 13 ((𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}) ∧ 𝑔:(1...𝑛)⟶(𝑉 × 𝑉)) → (𝐸𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}))
5244, 50, 51syl2anc 690 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐸𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}))
53 0re 9897 . . . . . . . . . . . . 13 0 ∈ ℝ
54 rexr 9942 . . . . . . . . . . . . . 14 (0 ∈ ℝ → 0 ∈ ℝ*)
55 renemnf 9945 . . . . . . . . . . . . . 14 (0 ∈ ℝ → 0 ≠ -∞)
56 eldifsn 4259 . . . . . . . . . . . . . 14 (0 ∈ (ℝ* ∖ {-∞}) ↔ (0 ∈ ℝ* ∧ 0 ≠ -∞))
5754, 55, 56sylanbrc 694 . . . . . . . . . . . . 13 (0 ∈ ℝ → 0 ∈ (ℝ* ∖ {-∞}))
5853, 57mp1i 13 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 0 ∈ (ℝ* ∖ {-∞}))
59 xaddid2 11908 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ* → (0 +𝑒 𝑥) = 𝑥)
60 xaddid1 11907 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ* → (𝑥 +𝑒 0) = 𝑥)
6159, 60jca 552 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ* → ((0 +𝑒 𝑥) = 𝑥 ∧ (𝑥 +𝑒 0) = 𝑥))
6261adantl 480 . . . . . . . . . . . 12 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ 𝑥 ∈ ℝ*) → ((0 +𝑒 𝑥) = 𝑥 ∧ (𝑥 +𝑒 0) = 𝑥))
6321, 22, 23, 25, 26, 28, 52, 58, 62gsumress 17048 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (ℝ*𝑠 Σg (𝐸𝑔)) = (𝑊 Σg (𝐸𝑔)))
6423, 21ressbas2 15707 . . . . . . . . . . . . 13 ((ℝ* ∖ {-∞}) ⊆ ℝ* → (ℝ* ∖ {-∞}) = (Base‘𝑊))
6527, 64ax-mp 5 . . . . . . . . . . . 12 (ℝ* ∖ {-∞}) = (Base‘𝑊)
6623xrs10 19553 . . . . . . . . . . . 12 0 = (0g𝑊)
6723xrs1cmn 19554 . . . . . . . . . . . . 13 𝑊 ∈ CMnd
6867a1i 11 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑊 ∈ CMnd)
69 c0ex 9891 . . . . . . . . . . . . . 14 0 ∈ V
7069a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 0 ∈ V)
7152, 26, 70fdmfifsupp 8146 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐸𝑔) finSupp 0)
7265, 66, 68, 26, 52, 71gsumcl 18088 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑊 Σg (𝐸𝑔)) ∈ (ℝ* ∖ {-∞}))
7363, 72eqeltrd 2687 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (ℝ*𝑠 Σg (𝐸𝑔)) ∈ (ℝ* ∖ {-∞}))
7473eldifad 3551 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (ℝ*𝑠 Σg (𝐸𝑔)) ∈ ℝ*)
75 eqid 2609 . . . . . . . . 9 (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) = (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔)))
7674, 75fmptd 6277 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))):𝑆⟶ℝ*)
77 frn 5952 . . . . . . . 8 ((𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))):𝑆⟶ℝ* → ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ⊆ ℝ*)
7876, 77syl 17 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ⊆ ℝ*)
7978ralrimiva 2948 . . . . . 6 (𝜑 → ∀𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ⊆ ℝ*)
80 iunss 4491 . . . . . 6 ( 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ⊆ ℝ* ↔ ∀𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ⊆ ℝ*)
8179, 80sylibr 222 . . . . 5 (𝜑 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ⊆ ℝ*)
8218, 81syl5eqss 3611 . . . 4 (𝜑𝑇 ⊆ ℝ*)
83 infxrcl 11994 . . . 4 (𝑇 ⊆ ℝ* → inf(𝑇, ℝ*, < ) ∈ ℝ*)
8482, 83syl 17 . . 3 (𝜑 → inf(𝑇, ℝ*, < ) ∈ ℝ*)
85 xmetcl 21894 . . . 4 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋𝑉𝑌𝑉) → (𝑋𝐸𝑌) ∈ ℝ*)
8629, 11, 13, 85syl3anc 1317 . . 3 (𝜑 → (𝑋𝐸𝑌) ∈ ℝ*)
87 1nn 10881 . . . . . . 7 1 ∈ ℕ
88 1ex 9892 . . . . . . . . . . . 12 1 ∈ V
89 opex 4853 . . . . . . . . . . . 12 𝑋, 𝑌⟩ ∈ V
9088, 89f1osn 6073 . . . . . . . . . . 11 {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}–1-1-onto→{⟨𝑋, 𝑌⟩}
91 f1of 6035 . . . . . . . . . . 11 ({⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}–1-1-onto→{⟨𝑋, 𝑌⟩} → {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶{⟨𝑋, 𝑌⟩})
9290, 91ax-mp 5 . . . . . . . . . 10 {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶{⟨𝑋, 𝑌⟩}
93 opelxpi 5062 . . . . . . . . . . . 12 ((𝑋𝑉𝑌𝑉) → ⟨𝑋, 𝑌⟩ ∈ (𝑉 × 𝑉))
9411, 13, 93syl2anc 690 . . . . . . . . . . 11 (𝜑 → ⟨𝑋, 𝑌⟩ ∈ (𝑉 × 𝑉))
9594snssd 4280 . . . . . . . . . 10 (𝜑 → {⟨𝑋, 𝑌⟩} ⊆ (𝑉 × 𝑉))
96 fss 5955 . . . . . . . . . 10 (({⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶{⟨𝑋, 𝑌⟩} ∧ {⟨𝑋, 𝑌⟩} ⊆ (𝑉 × 𝑉)) → {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉))
9792, 95, 96sylancr 693 . . . . . . . . 9 (𝜑 → {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉))
9829elfvexd 6117 . . . . . . . . . . 11 (𝜑𝑉 ∈ V)
99 xpexg 6836 . . . . . . . . . . 11 ((𝑉 ∈ V ∧ 𝑉 ∈ V) → (𝑉 × 𝑉) ∈ V)
10098, 98, 99syl2anc 690 . . . . . . . . . 10 (𝜑 → (𝑉 × 𝑉) ∈ V)
101 snex 4830 . . . . . . . . . 10 {1} ∈ V
102 elmapg 7735 . . . . . . . . . 10 (((𝑉 × 𝑉) ∈ V ∧ {1} ∈ V) → ({⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑𝑚 {1}) ↔ {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉)))
103100, 101, 102sylancl 692 . . . . . . . . 9 (𝜑 → ({⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑𝑚 {1}) ↔ {⟨1, ⟨𝑋, 𝑌⟩⟩}:{1}⟶(𝑉 × 𝑉)))
10497, 103mpbird 245 . . . . . . . 8 (𝜑 → {⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑𝑚 {1}))
105 op1stg 7049 . . . . . . . . . . 11 ((𝑋𝑉𝑌𝑉) → (1st ‘⟨𝑋, 𝑌⟩) = 𝑋)
10611, 13, 105syl2anc 690 . . . . . . . . . 10 (𝜑 → (1st ‘⟨𝑋, 𝑌⟩) = 𝑋)
107106fveq2d 6092 . . . . . . . . 9 (𝜑 → (𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑋))
108 op2ndg 7050 . . . . . . . . . . 11 ((𝑋𝑉𝑌𝑉) → (2nd ‘⟨𝑋, 𝑌⟩) = 𝑌)
10911, 13, 108syl2anc 690 . . . . . . . . . 10 (𝜑 → (2nd ‘⟨𝑋, 𝑌⟩) = 𝑌)
110109fveq2d 6092 . . . . . . . . 9 (𝜑 → (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑌))
111107, 110jca 552 . . . . . . . 8 (𝜑 → ((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑌)))
11224a1i 11 . . . . . . . . . 10 (𝜑 → ℝ*𝑠 ∈ V)
113 snfi 7901 . . . . . . . . . . 11 {1} ∈ Fin
114113a1i 11 . . . . . . . . . 10 (𝜑 → {1} ∈ Fin)
11527a1i 11 . . . . . . . . . 10 (𝜑 → (ℝ* ∖ {-∞}) ⊆ ℝ*)
116 xmetge0 21907 . . . . . . . . . . . . . . 15 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋𝑉𝑌𝑉) → 0 ≤ (𝑋𝐸𝑌))
11729, 11, 13, 116syl3anc 1317 . . . . . . . . . . . . . 14 (𝜑 → 0 ≤ (𝑋𝐸𝑌))
118 ge0nemnf 11840 . . . . . . . . . . . . . 14 (((𝑋𝐸𝑌) ∈ ℝ* ∧ 0 ≤ (𝑋𝐸𝑌)) → (𝑋𝐸𝑌) ≠ -∞)
11986, 117, 118syl2anc 690 . . . . . . . . . . . . 13 (𝜑 → (𝑋𝐸𝑌) ≠ -∞)
120 eldifsn 4259 . . . . . . . . . . . . 13 ((𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞}) ↔ ((𝑋𝐸𝑌) ∈ ℝ* ∧ (𝑋𝐸𝑌) ≠ -∞))
12186, 119, 120sylanbrc 694 . . . . . . . . . . . 12 (𝜑 → (𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞}))
122 fconst6g 5992 . . . . . . . . . . . 12 ((𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞}) → ({1} × {(𝑋𝐸𝑌)}):{1}⟶(ℝ* ∖ {-∞}))
123121, 122syl 17 . . . . . . . . . . 11 (𝜑 → ({1} × {(𝑋𝐸𝑌)}):{1}⟶(ℝ* ∖ {-∞}))
124 fcoconst 6292 . . . . . . . . . . . . . 14 ((𝐸 Fn (𝑉 × 𝑉) ∧ ⟨𝑋, 𝑌⟩ ∈ (𝑉 × 𝑉)) → (𝐸 ∘ ({1} × {⟨𝑋, 𝑌⟩})) = ({1} × {(𝐸‘⟨𝑋, 𝑌⟩)}))
12532, 94, 124syl2anc 690 . . . . . . . . . . . . 13 (𝜑 → (𝐸 ∘ ({1} × {⟨𝑋, 𝑌⟩})) = ({1} × {(𝐸‘⟨𝑋, 𝑌⟩)}))
12688, 89xpsn 6298 . . . . . . . . . . . . . 14 ({1} × {⟨𝑋, 𝑌⟩}) = {⟨1, ⟨𝑋, 𝑌⟩⟩}
127126coeq2i 5192 . . . . . . . . . . . . 13 (𝐸 ∘ ({1} × {⟨𝑋, 𝑌⟩})) = (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})
128 df-ov 6530 . . . . . . . . . . . . . . . 16 (𝑋𝐸𝑌) = (𝐸‘⟨𝑋, 𝑌⟩)
129128eqcomi 2618 . . . . . . . . . . . . . . 15 (𝐸‘⟨𝑋, 𝑌⟩) = (𝑋𝐸𝑌)
130129sneqi 4135 . . . . . . . . . . . . . 14 {(𝐸‘⟨𝑋, 𝑌⟩)} = {(𝑋𝐸𝑌)}
131130xpeq2i 5050 . . . . . . . . . . . . 13 ({1} × {(𝐸‘⟨𝑋, 𝑌⟩)}) = ({1} × {(𝑋𝐸𝑌)})
132125, 127, 1313eqtr3g 2666 . . . . . . . . . . . 12 (𝜑 → (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}) = ({1} × {(𝑋𝐸𝑌)}))
133132feq1d 5929 . . . . . . . . . . 11 (𝜑 → ((𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}):{1}⟶(ℝ* ∖ {-∞}) ↔ ({1} × {(𝑋𝐸𝑌)}):{1}⟶(ℝ* ∖ {-∞})))
134123, 133mpbird 245 . . . . . . . . . 10 (𝜑 → (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}):{1}⟶(ℝ* ∖ {-∞}))
13553, 57mp1i 13 . . . . . . . . . 10 (𝜑 → 0 ∈ (ℝ* ∖ {-∞}))
13661adantl 480 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ*) → ((0 +𝑒 𝑥) = 𝑥 ∧ (𝑥 +𝑒 0) = 𝑥))
13721, 22, 23, 112, 114, 115, 134, 135, 136gsumress 17048 . . . . . . . . 9 (𝜑 → (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})) = (𝑊 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))
138 fconstmpt 5075 . . . . . . . . . . 11 ({1} × {(𝑋𝐸𝑌)}) = (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))
139132, 138syl6eq 2659 . . . . . . . . . 10 (𝜑 → (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}) = (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌)))
140139oveq2d 6543 . . . . . . . . 9 (𝜑 → (𝑊 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})) = (𝑊 Σg (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))))
141 cmnmnd 17980 . . . . . . . . . . 11 (𝑊 ∈ CMnd → 𝑊 ∈ Mnd)
14267, 141mp1i 13 . . . . . . . . . 10 (𝜑𝑊 ∈ Mnd)
14387a1i 11 . . . . . . . . . 10 (𝜑 → 1 ∈ ℕ)
144 eqidd 2610 . . . . . . . . . . 11 (𝑗 = 1 → (𝑋𝐸𝑌) = (𝑋𝐸𝑌))
14565, 144gsumsn 18126 . . . . . . . . . 10 ((𝑊 ∈ Mnd ∧ 1 ∈ ℕ ∧ (𝑋𝐸𝑌) ∈ (ℝ* ∖ {-∞})) → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))) = (𝑋𝐸𝑌))
146142, 143, 121, 145syl3anc 1317 . . . . . . . . 9 (𝜑 → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝑋𝐸𝑌))) = (𝑋𝐸𝑌))
147137, 140, 1463eqtrrd 2648 . . . . . . . 8 (𝜑 → (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))
148 fveq1 6087 . . . . . . . . . . . . . . 15 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝑔‘1) = ({⟨1, ⟨𝑋, 𝑌⟩⟩}‘1))
14988, 89fvsn 6329 . . . . . . . . . . . . . . 15 ({⟨1, ⟨𝑋, 𝑌⟩⟩}‘1) = ⟨𝑋, 𝑌
150148, 149syl6eq 2659 . . . . . . . . . . . . . 14 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝑔‘1) = ⟨𝑋, 𝑌⟩)
151150fveq2d 6092 . . . . . . . . . . . . 13 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (1st ‘(𝑔‘1)) = (1st ‘⟨𝑋, 𝑌⟩))
152151fveq2d 6092 . . . . . . . . . . . 12 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝐹‘(1st ‘(𝑔‘1))) = (𝐹‘(1st ‘⟨𝑋, 𝑌⟩)))
153152eqeq1d 2611 . . . . . . . . . . 11 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ↔ (𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑋)))
154150fveq2d 6092 . . . . . . . . . . . . 13 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (2nd ‘(𝑔‘1)) = (2nd ‘⟨𝑋, 𝑌⟩))
155154fveq2d 6092 . . . . . . . . . . . 12 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)))
156155eqeq1d 2611 . . . . . . . . . . 11 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌) ↔ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑌)))
157153, 156anbi12d 742 . . . . . . . . . 10 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ↔ ((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑌))))
158 coeq2 5190 . . . . . . . . . . . 12 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (𝐸𝑔) = (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}))
159158oveq2d 6543 . . . . . . . . . . 11 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → (ℝ*𝑠 Σg (𝐸𝑔)) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))
160159eqeq2d 2619 . . . . . . . . . 10 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)) ↔ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩}))))
161157, 160anbi12d 742 . . . . . . . . 9 (𝑔 = {⟨1, ⟨𝑋, 𝑌⟩⟩} → ((((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))) ↔ (((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))))
162161rspcev 3281 . . . . . . . 8 (({⟨1, ⟨𝑋, 𝑌⟩⟩} ∈ ((𝑉 × 𝑉) ↑𝑚 {1}) ∧ (((𝐹‘(1st ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘⟨𝑋, 𝑌⟩)) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸 ∘ {⟨1, ⟨𝑋, 𝑌⟩⟩})))) → ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))))
163104, 111, 147, 162syl12anc 1315 . . . . . . 7 (𝜑 → ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))))
164 ovex 6555 . . . . . . . . . 10 (𝑋𝐸𝑌) ∈ V
16575elrnmpt 5280 . . . . . . . . . 10 ((𝑋𝐸𝑌) ∈ V → ((𝑋𝐸𝑌) ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑔𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))))
166164, 165ax-mp 5 . . . . . . . . 9 ((𝑋𝐸𝑌) ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑔𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))
16715rexeqi 3119 . . . . . . . . . . 11 (∃𝑔𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)) ↔ ∃𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))
168 fveq1 6087 . . . . . . . . . . . . . . . 16 ( = 𝑔 → (‘1) = (𝑔‘1))
169168fveq2d 6092 . . . . . . . . . . . . . . 15 ( = 𝑔 → (1st ‘(‘1)) = (1st ‘(𝑔‘1)))
170169fveq2d 6092 . . . . . . . . . . . . . 14 ( = 𝑔 → (𝐹‘(1st ‘(‘1))) = (𝐹‘(1st ‘(𝑔‘1))))
171170eqeq1d 2611 . . . . . . . . . . . . 13 ( = 𝑔 → ((𝐹‘(1st ‘(‘1))) = (𝐹𝑋) ↔ (𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋)))
172 fveq1 6087 . . . . . . . . . . . . . . . 16 ( = 𝑔 → (𝑛) = (𝑔𝑛))
173172fveq2d 6092 . . . . . . . . . . . . . . 15 ( = 𝑔 → (2nd ‘(𝑛)) = (2nd ‘(𝑔𝑛)))
174173fveq2d 6092 . . . . . . . . . . . . . 14 ( = 𝑔 → (𝐹‘(2nd ‘(𝑛))) = (𝐹‘(2nd ‘(𝑔𝑛))))
175174eqeq1d 2611 . . . . . . . . . . . . 13 ( = 𝑔 → ((𝐹‘(2nd ‘(𝑛))) = (𝐹𝑌) ↔ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌)))
176 fveq1 6087 . . . . . . . . . . . . . . . . 17 ( = 𝑔 → (𝑖) = (𝑔𝑖))
177176fveq2d 6092 . . . . . . . . . . . . . . . 16 ( = 𝑔 → (2nd ‘(𝑖)) = (2nd ‘(𝑔𝑖)))
178177fveq2d 6092 . . . . . . . . . . . . . . 15 ( = 𝑔 → (𝐹‘(2nd ‘(𝑖))) = (𝐹‘(2nd ‘(𝑔𝑖))))
179 fveq1 6087 . . . . . . . . . . . . . . . . 17 ( = 𝑔 → (‘(𝑖 + 1)) = (𝑔‘(𝑖 + 1)))
180179fveq2d 6092 . . . . . . . . . . . . . . . 16 ( = 𝑔 → (1st ‘(‘(𝑖 + 1))) = (1st ‘(𝑔‘(𝑖 + 1))))
181180fveq2d 6092 . . . . . . . . . . . . . . 15 ( = 𝑔 → (𝐹‘(1st ‘(‘(𝑖 + 1)))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
182178, 181eqeq12d 2624 . . . . . . . . . . . . . 14 ( = 𝑔 → ((𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))) ↔ (𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
183182ralbidv 2968 . . . . . . . . . . . . 13 ( = 𝑔 → (∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))) ↔ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
184171, 175, 1833anbi123d 1390 . . . . . . . . . . . 12 ( = 𝑔 → (((𝐹‘(1st ‘(‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1))))) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))))
185184rexrab 3336 . . . . . . . . . . 11 (∃𝑔 ∈ { ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∣ ((𝐹‘(1st ‘(‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑖))) = (𝐹‘(1st ‘(‘(𝑖 + 1)))))} (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛))(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))))
186167, 185bitri 262 . . . . . . . . . 10 (∃𝑔𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛))(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))))
187 oveq2 6535 . . . . . . . . . . . . 13 (𝑛 = 1 → (1...𝑛) = (1...1))
188 1z 11243 . . . . . . . . . . . . . 14 1 ∈ ℤ
189 fzsn 12212 . . . . . . . . . . . . . 14 (1 ∈ ℤ → (1...1) = {1})
190188, 189ax-mp 5 . . . . . . . . . . . . 13 (1...1) = {1}
191187, 190syl6eq 2659 . . . . . . . . . . . 12 (𝑛 = 1 → (1...𝑛) = {1})
192191oveq2d 6543 . . . . . . . . . . 11 (𝑛 = 1 → ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) = ((𝑉 × 𝑉) ↑𝑚 {1}))
193 df-3an 1032 . . . . . . . . . . . . 13 (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ↔ (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌)) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
194 ral0 4027 . . . . . . . . . . . . . . . 16 𝑖 ∈ ∅ (𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))
195 oveq1 6534 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 1 → (𝑛 − 1) = (1 − 1))
196 1m1e0 10939 . . . . . . . . . . . . . . . . . . . 20 (1 − 1) = 0
197195, 196syl6eq 2659 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 1 → (𝑛 − 1) = 0)
198197oveq2d 6543 . . . . . . . . . . . . . . . . . 18 (𝑛 = 1 → (1...(𝑛 − 1)) = (1...0))
199 fz10 12191 . . . . . . . . . . . . . . . . . 18 (1...0) = ∅
200198, 199syl6eq 2659 . . . . . . . . . . . . . . . . 17 (𝑛 = 1 → (1...(𝑛 − 1)) = ∅)
201200raleqdv 3120 . . . . . . . . . . . . . . . 16 (𝑛 = 1 → (∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))) ↔ ∀𝑖 ∈ ∅ (𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
202194, 201mpbiri 246 . . . . . . . . . . . . . . 15 (𝑛 = 1 → ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
203202biantrud 526 . . . . . . . . . . . . . 14 (𝑛 = 1 → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌)) ↔ (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌)) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))))
204 fveq2 6088 . . . . . . . . . . . . . . . . . 18 (𝑛 = 1 → (𝑔𝑛) = (𝑔‘1))
205204fveq2d 6092 . . . . . . . . . . . . . . . . 17 (𝑛 = 1 → (2nd ‘(𝑔𝑛)) = (2nd ‘(𝑔‘1)))
206205fveq2d 6092 . . . . . . . . . . . . . . . 16 (𝑛 = 1 → (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹‘(2nd ‘(𝑔‘1))))
207206eqeq1d 2611 . . . . . . . . . . . . . . 15 (𝑛 = 1 → ((𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ↔ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)))
208207anbi2d 735 . . . . . . . . . . . . . 14 (𝑛 = 1 → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌)) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌))))
209203, 208bitr3d 268 . . . . . . . . . . . . 13 (𝑛 = 1 → ((((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌)) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌))))
210193, 209syl5bb 270 . . . . . . . . . . . 12 (𝑛 = 1 → (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ↔ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌))))
211210anbi1d 736 . . . . . . . . . . 11 (𝑛 = 1 → ((((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))) ↔ (((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))))
212192, 211rexeqbidv 3129 . . . . . . . . . 10 (𝑛 = 1 → (∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛))(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))))
213186, 212syl5bb 270 . . . . . . . . 9 (𝑛 = 1 → (∃𝑔𝑆 (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))))
214166, 213syl5bb 270 . . . . . . . 8 (𝑛 = 1 → ((𝑋𝐸𝑌) ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))))
215214rspcev 3281 . . . . . . 7 ((1 ∈ ℕ ∧ ∃𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 {1})(((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔‘1))) = (𝐹𝑌)) ∧ (𝑋𝐸𝑌) = (ℝ*𝑠 Σg (𝐸𝑔)))) → ∃𝑛 ∈ ℕ (𝑋𝐸𝑌) ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
21687, 163, 215sylancr 693 . . . . . 6 (𝜑 → ∃𝑛 ∈ ℕ (𝑋𝐸𝑌) ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
217 eliun 4454 . . . . . 6 ((𝑋𝐸𝑌) ∈ 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑛 ∈ ℕ (𝑋𝐸𝑌) ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
218216, 217sylibr 222 . . . . 5 (𝜑 → (𝑋𝐸𝑌) ∈ 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
219218, 18syl6eleqr 2698 . . . 4 (𝜑 → (𝑋𝐸𝑌) ∈ 𝑇)
220 infxrlb 11995 . . . 4 ((𝑇 ⊆ ℝ* ∧ (𝑋𝐸𝑌) ∈ 𝑇) → inf(𝑇, ℝ*, < ) ≤ (𝑋𝐸𝑌))
22182, 219, 220syl2anc 690 . . 3 (𝜑 → inf(𝑇, ℝ*, < ) ≤ (𝑋𝐸𝑌))
22218eleq2i 2679 . . . . . . 7 (𝑝𝑇𝑝 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
223 eliun 4454 . . . . . . 7 (𝑝 𝑛 ∈ ℕ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑛 ∈ ℕ 𝑝 ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
224222, 223bitri 262 . . . . . 6 (𝑝𝑇 ↔ ∃𝑛 ∈ ℕ 𝑝 ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))))
225 vex 3175 . . . . . . . . 9 𝑝 ∈ V
22675elrnmpt 5280 . . . . . . . . 9 (𝑝 ∈ V → (𝑝 ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑔𝑆 𝑝 = (ℝ*𝑠 Σg (𝐸𝑔))))
227225, 226ax-mp 5 . . . . . . . 8 (𝑝 ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) ↔ ∃𝑔𝑆 𝑝 = (ℝ*𝑠 Σg (𝐸𝑔)))
228184, 15elrab2 3332 . . . . . . . . . . . . . . . . 17 (𝑔𝑆 ↔ (𝑔 ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑛)) ∧ ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))))
229228simprbi 478 . . . . . . . . . . . . . . . 16 (𝑔𝑆 → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
230229adantl 480 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ∧ (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1))))))
231230simp2d 1066 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌))
2323ad2antrr 757 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝐹:𝑉1-1-onto𝐵)
233 f1of1 6034 . . . . . . . . . . . . . . . 16 (𝐹:𝑉1-1-onto𝐵𝐹:𝑉1-1𝐵)
234232, 233syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝐹:𝑉1-1𝐵)
235 simplr 787 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑛 ∈ ℕ)
236 elfz1end 12200 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ ↔ 𝑛 ∈ (1...𝑛))
237235, 236sylib 206 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑛 ∈ (1...𝑛))
23850, 237ffvelrnd 6253 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑔𝑛) ∈ (𝑉 × 𝑉))
239 xp2nd 7068 . . . . . . . . . . . . . . . 16 ((𝑔𝑛) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔𝑛)) ∈ 𝑉)
240238, 239syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (2nd ‘(𝑔𝑛)) ∈ 𝑉)
24113ad2antrr 757 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑌𝑉)
242 f1fveq 6398 . . . . . . . . . . . . . . 15 ((𝐹:𝑉1-1𝐵 ∧ ((2nd ‘(𝑔𝑛)) ∈ 𝑉𝑌𝑉)) → ((𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ↔ (2nd ‘(𝑔𝑛)) = 𝑌))
243234, 240, 241, 242syl12anc 1315 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝐹‘(2nd ‘(𝑔𝑛))) = (𝐹𝑌) ↔ (2nd ‘(𝑔𝑛)) = 𝑌))
244231, 243mpbid 220 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (2nd ‘(𝑔𝑛)) = 𝑌)
245244oveq2d 6543 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸(2nd ‘(𝑔𝑛))) = (𝑋𝐸𝑌))
246 eleq1 2675 . . . . . . . . . . . . . . . . 17 (𝑚 = 1 → (𝑚 ∈ (1...𝑛) ↔ 1 ∈ (1...𝑛)))
247 fveq2 6088 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 1 → (𝑔𝑚) = (𝑔‘1))
248247fveq2d 6092 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 1 → (2nd ‘(𝑔𝑚)) = (2nd ‘(𝑔‘1)))
249248oveq2d 6543 . . . . . . . . . . . . . . . . . 18 (𝑚 = 1 → (𝑋𝐸(2nd ‘(𝑔𝑚))) = (𝑋𝐸(2nd ‘(𝑔‘1))))
250 oveq2 6535 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 1 → (1...𝑚) = (1...1))
251250, 190syl6eq 2659 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 1 → (1...𝑚) = {1})
252251reseq2d 5304 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 1 → ((𝐸𝑔) ↾ (1...𝑚)) = ((𝐸𝑔) ↾ {1}))
253252oveq2d 6543 . . . . . . . . . . . . . . . . . 18 (𝑚 = 1 → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸𝑔) ↾ {1})))
254249, 253breq12d 4590 . . . . . . . . . . . . . . . . 17 (𝑚 = 1 → ((𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ {1}))))
255246, 254imbi12d 332 . . . . . . . . . . . . . . . 16 (𝑚 = 1 → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚)))) ↔ (1 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ {1})))))
256255imbi2d 328 . . . . . . . . . . . . . . 15 (𝑚 = 1 → ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))))) ↔ (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (1 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ {1}))))))
257 eleq1 2675 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑥 → (𝑚 ∈ (1...𝑛) ↔ 𝑥 ∈ (1...𝑛)))
258 fveq2 6088 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑥 → (𝑔𝑚) = (𝑔𝑥))
259258fveq2d 6092 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑥 → (2nd ‘(𝑔𝑚)) = (2nd ‘(𝑔𝑥)))
260259oveq2d 6543 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑥 → (𝑋𝐸(2nd ‘(𝑔𝑚))) = (𝑋𝐸(2nd ‘(𝑔𝑥))))
261 oveq2 6535 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑥 → (1...𝑚) = (1...𝑥))
262261reseq2d 5304 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑥 → ((𝐸𝑔) ↾ (1...𝑚)) = ((𝐸𝑔) ↾ (1...𝑥)))
263262oveq2d 6543 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑥 → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))))
264260, 263breq12d 4590 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑥 → ((𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥)))))
265257, 264imbi12d 332 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑥 → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚)))) ↔ (𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))))))
266265imbi2d 328 . . . . . . . . . . . . . . 15 (𝑚 = 𝑥 → ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))))) ↔ (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥)))))))
267 eleq1 2675 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝑥 + 1) → (𝑚 ∈ (1...𝑛) ↔ (𝑥 + 1) ∈ (1...𝑛)))
268 fveq2 6088 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = (𝑥 + 1) → (𝑔𝑚) = (𝑔‘(𝑥 + 1)))
269268fveq2d 6092 . . . . . . . . . . . . . . . . . . 19 (𝑚 = (𝑥 + 1) → (2nd ‘(𝑔𝑚)) = (2nd ‘(𝑔‘(𝑥 + 1))))
270269oveq2d 6543 . . . . . . . . . . . . . . . . . 18 (𝑚 = (𝑥 + 1) → (𝑋𝐸(2nd ‘(𝑔𝑚))) = (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))))
271 oveq2 6535 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = (𝑥 + 1) → (1...𝑚) = (1...(𝑥 + 1)))
272271reseq2d 5304 . . . . . . . . . . . . . . . . . . 19 (𝑚 = (𝑥 + 1) → ((𝐸𝑔) ↾ (1...𝑚)) = ((𝐸𝑔) ↾ (1...(𝑥 + 1))))
273272oveq2d 6543 . . . . . . . . . . . . . . . . . 18 (𝑚 = (𝑥 + 1) → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))))
274270, 273breq12d 4590 . . . . . . . . . . . . . . . . 17 (𝑚 = (𝑥 + 1) → ((𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1))))))
275267, 274imbi12d 332 . . . . . . . . . . . . . . . 16 (𝑚 = (𝑥 + 1) → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚)))) ↔ ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))))))
276275imbi2d 328 . . . . . . . . . . . . . . 15 (𝑚 = (𝑥 + 1) → ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))))) ↔ (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1))))))))
277 eleq1 2675 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑛 → (𝑚 ∈ (1...𝑛) ↔ 𝑛 ∈ (1...𝑛)))
278 fveq2 6088 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑛 → (𝑔𝑚) = (𝑔𝑛))
279278fveq2d 6092 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑛 → (2nd ‘(𝑔𝑚)) = (2nd ‘(𝑔𝑛)))
280279oveq2d 6543 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑛 → (𝑋𝐸(2nd ‘(𝑔𝑚))) = (𝑋𝐸(2nd ‘(𝑔𝑛))))
281 oveq2 6535 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑛 → (1...𝑚) = (1...𝑛))
282281reseq2d 5304 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑛 → ((𝐸𝑔) ↾ (1...𝑚)) = ((𝐸𝑔) ↾ (1...𝑛)))
283282oveq2d 6543 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑛 → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) = (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))))
284280, 283breq12d 4590 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑛 → ((𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))) ↔ (𝑋𝐸(2nd ‘(𝑔𝑛))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛)))))
285277, 284imbi12d 332 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑛 → ((𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚)))) ↔ (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑛))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))))))
286285imbi2d 328 . . . . . . . . . . . . . . 15 (𝑚 = 𝑛 → ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑚 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑚))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑚))))) ↔ (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑛))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛)))))))
28729ad2antrr 757 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝐸 ∈ (∞Met‘𝑉))
28811ad2antrr 757 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑋𝑉)
289 nnuz 11558 . . . . . . . . . . . . . . . . . . . . . . 23 ℕ = (ℤ‘1)
290235, 289syl6eleq 2697 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑛 ∈ (ℤ‘1))
291 eluzfz1 12177 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 ∈ (ℤ‘1) → 1 ∈ (1...𝑛))
292290, 291syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 1 ∈ (1...𝑛))
29350, 292ffvelrnd 6253 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑔‘1) ∈ (𝑉 × 𝑉))
294 xp2nd 7068 . . . . . . . . . . . . . . . . . . . 20 ((𝑔‘1) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔‘1)) ∈ 𝑉)
295293, 294syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (2nd ‘(𝑔‘1)) ∈ 𝑉)
296 xmetcl 21894 . . . . . . . . . . . . . . . . . . 19 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋𝑉 ∧ (2nd ‘(𝑔‘1)) ∈ 𝑉) → (𝑋𝐸(2nd ‘(𝑔‘1))) ∈ ℝ*)
297287, 288, 295, 296syl3anc 1317 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) ∈ ℝ*)
298 xrleid 11821 . . . . . . . . . . . . . . . . . 18 ((𝑋𝐸(2nd ‘(𝑔‘1))) ∈ ℝ* → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑋𝐸(2nd ‘(𝑔‘1))))
299297, 298syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑋𝐸(2nd ‘(𝑔‘1))))
300142ad2antrr 757 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝑊 ∈ Mnd)
30187a1i 11 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 1 ∈ ℕ)
30244, 293ffvelrnd 6253 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐸‘(𝑔‘1)) ∈ (ℝ* ∖ {-∞}))
303 fveq2 6088 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 = 1 → (𝑔𝑗) = (𝑔‘1))
304303fveq2d 6092 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 1 → (𝐸‘(𝑔𝑗)) = (𝐸‘(𝑔‘1)))
30565, 304gsumsn 18126 . . . . . . . . . . . . . . . . . . 19 ((𝑊 ∈ Mnd ∧ 1 ∈ ℕ ∧ (𝐸‘(𝑔‘1)) ∈ (ℝ* ∖ {-∞})) → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝐸‘(𝑔𝑗)))) = (𝐸‘(𝑔‘1)))
306300, 301, 302, 305syl3anc 1317 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑊 Σg (𝑗 ∈ {1} ↦ (𝐸‘(𝑔𝑗)))) = (𝐸‘(𝑔‘1)))
307287, 30syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → 𝐸:(𝑉 × 𝑉)⟶ℝ*)
308 fcompt 6291 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐸:(𝑉 × 𝑉)⟶ℝ*𝑔:(1...𝑛)⟶(𝑉 × 𝑉)) → (𝐸𝑔) = (𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))))
309307, 50, 308syl2anc 690 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐸𝑔) = (𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))))
310309reseq1d 5303 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝐸𝑔) ↾ {1}) = ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))) ↾ {1}))
311292snssd 4280 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → {1} ⊆ (1...𝑛))
312311resmptd 5358 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))) ↾ {1}) = (𝑗 ∈ {1} ↦ (𝐸‘(𝑔𝑗))))
313310, 312eqtrd 2643 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝐸𝑔) ↾ {1}) = (𝑗 ∈ {1} ↦ (𝐸‘(𝑔𝑗))))
314313oveq2d 6543 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑊 Σg ((𝐸𝑔) ↾ {1})) = (𝑊 Σg (𝑗 ∈ {1} ↦ (𝐸‘(𝑔𝑗)))))
315 df-ov 6530 . . . . . . . . . . . . . . . . . . 19 (𝑋𝐸(2nd ‘(𝑔‘1))) = (𝐸‘⟨𝑋, (2nd ‘(𝑔‘1))⟩)
316 1st2nd2 7074 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔‘1) ∈ (𝑉 × 𝑉) → (𝑔‘1) = ⟨(1st ‘(𝑔‘1)), (2nd ‘(𝑔‘1))⟩)
317293, 316syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑔‘1) = ⟨(1st ‘(𝑔‘1)), (2nd ‘(𝑔‘1))⟩)
318230simp1d 1065 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋))
319 xp1st 7067 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔‘1) ∈ (𝑉 × 𝑉) → (1st ‘(𝑔‘1)) ∈ 𝑉)
320293, 319syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (1st ‘(𝑔‘1)) ∈ 𝑉)
321 f1fveq 6398 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹:𝑉1-1𝐵 ∧ ((1st ‘(𝑔‘1)) ∈ 𝑉𝑋𝑉)) → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ↔ (1st ‘(𝑔‘1)) = 𝑋))
322234, 320, 288, 321syl12anc 1315 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝐹‘(1st ‘(𝑔‘1))) = (𝐹𝑋) ↔ (1st ‘(𝑔‘1)) = 𝑋))
323318, 322mpbid 220 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (1st ‘(𝑔‘1)) = 𝑋)
324323opeq1d 4340 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ⟨(1st ‘(𝑔‘1)), (2nd ‘(𝑔‘1))⟩ = ⟨𝑋, (2nd ‘(𝑔‘1))⟩)
325317, 324eqtr2d 2644 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ⟨𝑋, (2nd ‘(𝑔‘1))⟩ = (𝑔‘1))
326325fveq2d 6092 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝐸‘⟨𝑋, (2nd ‘(𝑔‘1))⟩) = (𝐸‘(𝑔‘1)))
327315, 326syl5eq 2655 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) = (𝐸‘(𝑔‘1)))
328306, 314, 3273eqtr4d 2653 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑊 Σg ((𝐸𝑔) ↾ {1})) = (𝑋𝐸(2nd ‘(𝑔‘1))))
329299, 328breqtrrd 4605 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ {1})))
330329a1d 25 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (1 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘1))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ {1}))))
331 simprl 789 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ ℕ)
332331, 289syl6eleq 2697 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ (ℤ‘1))
333 simprr 791 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑥 + 1) ∈ (1...𝑛))
334 peano2fzr 12183 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ (ℤ‘1) ∧ (𝑥 + 1) ∈ (1...𝑛)) → 𝑥 ∈ (1...𝑛))
335332, 333, 334syl2anc 690 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ (1...𝑛))
336335expr 640 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ 𝑥 ∈ ℕ) → ((𝑥 + 1) ∈ (1...𝑛) → 𝑥 ∈ (1...𝑛)))
337336imim1d 79 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ 𝑥 ∈ ℕ) → ((𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥)))) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))))))
338287adantr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐸 ∈ (∞Met‘𝑉))
339288adantr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑋𝑉)
34050adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
341340, 335ffvelrnd 6253 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔𝑥) ∈ (𝑉 × 𝑉))
342 xp2nd 7068 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑔𝑥) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔𝑥)) ∈ 𝑉)
343341, 342syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (2nd ‘(𝑔𝑥)) ∈ 𝑉)
344 xmetcl 21894 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋𝑉 ∧ (2nd ‘(𝑔𝑥)) ∈ 𝑉) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ∈ ℝ*)
345338, 339, 343, 344syl3anc 1317 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ∈ ℝ*)
34667a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑊 ∈ CMnd)
347 fzfid 12592 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...𝑥) ∈ Fin)
34852adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}))
349 fzsuc 12216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 ∈ (ℤ‘1) → (1...(𝑥 + 1)) = ((1...𝑥) ∪ {(𝑥 + 1)}))
350332, 349syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...(𝑥 + 1)) = ((1...𝑥) ∪ {(𝑥 + 1)}))
351 elfzuz3 12168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑥 + 1) ∈ (1...𝑛) → 𝑛 ∈ (ℤ‘(𝑥 + 1)))
352351ad2antll 760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑛 ∈ (ℤ‘(𝑥 + 1)))
353 fzss2 12210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 ∈ (ℤ‘(𝑥 + 1)) → (1...(𝑥 + 1)) ⊆ (1...𝑛))
354352, 353syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...(𝑥 + 1)) ⊆ (1...𝑛))
355350, 354eqsstr3d 3602 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((1...𝑥) ∪ {(𝑥 + 1)}) ⊆ (1...𝑛))
356355unssad 3751 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1...𝑥) ⊆ (1...𝑛))
357348, 356fssresd 5969 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸𝑔) ↾ (1...𝑥)):(1...𝑥)⟶(ℝ* ∖ {-∞}))
35869a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 0 ∈ V)
359357, 347, 358fdmfifsupp 8146 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸𝑔) ↾ (1...𝑥)) finSupp 0)
36065, 66, 346, 347, 357, 359gsumcl 18088 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) ∈ (ℝ* ∖ {-∞}))
361360eldifad 3551 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) ∈ ℝ*)
362338, 30syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐸:(𝑉 × 𝑉)⟶ℝ*)
363340, 333ffvelrnd 6253 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉))
364362, 363ffvelrnd 6253 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) ∈ ℝ*)
365 xleadd1a 11915 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑋𝐸(2nd ‘(𝑔𝑥))) ∈ ℝ* ∧ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) ∈ ℝ* ∧ (𝐸‘(𝑔‘(𝑥 + 1))) ∈ ℝ*) ∧ (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥)))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
366365ex 448 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑋𝐸(2nd ‘(𝑔𝑥))) ∈ ℝ* ∧ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) ∈ ℝ* ∧ (𝐸‘(𝑔‘(𝑥 + 1))) ∈ ℝ*) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
367345, 361, 364, 366syl3anc 1317 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
368 xp2nd 7068 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉) → (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
369363, 368syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
370 xmettri 21914 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐸 ∈ (∞Met‘𝑉) ∧ (𝑋𝑉 ∧ (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉 ∧ (2nd ‘(𝑔𝑥)) ∈ 𝑉)) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 ((2nd ‘(𝑔𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1))))))
371338, 339, 369, 343, 370syl13anc 1319 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 ((2nd ‘(𝑔𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1))))))
372 1st2nd2 7074 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉) → (𝑔‘(𝑥 + 1)) = ⟨(1st ‘(𝑔‘(𝑥 + 1))), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
373363, 372syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘(𝑥 + 1)) = ⟨(1st ‘(𝑔‘(𝑥 + 1))), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
374 nnz 11235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑥 ∈ ℕ → 𝑥 ∈ ℤ)
375374ad2antrl 759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ ℤ)
376 eluzp1m1 11546 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑥 ∈ ℤ ∧ 𝑛 ∈ (ℤ‘(𝑥 + 1))) → (𝑛 − 1) ∈ (ℤ𝑥))
377375, 352, 376syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑛 − 1) ∈ (ℤ𝑥))
378 elfzuzb 12165 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑥 ∈ (1...(𝑛 − 1)) ↔ (𝑥 ∈ (ℤ‘1) ∧ (𝑛 − 1) ∈ (ℤ𝑥)))
379332, 377, 378sylanbrc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝑥 ∈ (1...(𝑛 − 1)))
380230simp3d 1067 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
381380adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))))
382 fveq2 6088 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑖 = 𝑥 → (𝑔𝑖) = (𝑔𝑥))
383382fveq2d 6092 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑖 = 𝑥 → (2nd ‘(𝑔𝑖)) = (2nd ‘(𝑔𝑥)))
384383fveq2d 6092 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 = 𝑥 → (𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(2nd ‘(𝑔𝑥))))
385 oveq1 6534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑖 = 𝑥 → (𝑖 + 1) = (𝑥 + 1))
386385fveq2d 6092 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑖 = 𝑥 → (𝑔‘(𝑖 + 1)) = (𝑔‘(𝑥 + 1)))
387386fveq2d 6092 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑖 = 𝑥 → (1st ‘(𝑔‘(𝑖 + 1))) = (1st ‘(𝑔‘(𝑥 + 1))))
388387fveq2d 6092 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑖 = 𝑥 → (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))))
389384, 388eqeq12d 2624 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑖 = 𝑥 → ((𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))) ↔ (𝐹‘(2nd ‘(𝑔𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1))))))
390389rspcv 3277 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑥 ∈ (1...(𝑛 − 1)) → (∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(𝑔𝑖))) = (𝐹‘(1st ‘(𝑔‘(𝑖 + 1)))) → (𝐹‘(2nd ‘(𝑔𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1))))))
391379, 381, 390sylc 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐹‘(2nd ‘(𝑔𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))))
392234adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐹:𝑉1-1𝐵)
393 xp1st 7067 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑔‘(𝑥 + 1)) ∈ (𝑉 × 𝑉) → (1st ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
394363, 393syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (1st ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)
395 f1fveq 6398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐹:𝑉1-1𝐵 ∧ ((2nd ‘(𝑔𝑥)) ∈ 𝑉 ∧ (1st ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉)) → ((𝐹‘(2nd ‘(𝑔𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))) ↔ (2nd ‘(𝑔𝑥)) = (1st ‘(𝑔‘(𝑥 + 1)))))
396392, 343, 394, 395syl12anc 1315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐹‘(2nd ‘(𝑔𝑥))) = (𝐹‘(1st ‘(𝑔‘(𝑥 + 1)))) ↔ (2nd ‘(𝑔𝑥)) = (1st ‘(𝑔‘(𝑥 + 1)))))
397391, 396mpbid 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (2nd ‘(𝑔𝑥)) = (1st ‘(𝑔‘(𝑥 + 1))))
398397opeq1d 4340 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ⟨(2nd ‘(𝑔𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩ = ⟨(1st ‘(𝑔‘(𝑥 + 1))), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
399373, 398eqtr4d 2646 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑔‘(𝑥 + 1)) = ⟨(2nd ‘(𝑔𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
400399fveq2d 6092 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) = (𝐸‘⟨(2nd ‘(𝑔𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩))
401 df-ov 6530 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((2nd ‘(𝑔𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) = (𝐸‘⟨(2nd ‘(𝑔𝑥)), (2nd ‘(𝑔‘(𝑥 + 1)))⟩)
402400, 401syl6eqr 2661 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) = ((2nd ‘(𝑔𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1)))))
403402oveq2d 6543 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) = ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 ((2nd ‘(𝑔𝑥))𝐸(2nd ‘(𝑔‘(𝑥 + 1))))))
404371, 403breqtrrd 4605 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
405 xmetcl 21894 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐸 ∈ (∞Met‘𝑉) ∧ 𝑋𝑉 ∧ (2nd ‘(𝑔‘(𝑥 + 1))) ∈ 𝑉) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
406338, 339, 369, 405syl3anc 1317 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
407345, 364xaddcld 11963 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
408361, 364xaddcld 11963 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*)
409 xrletr 11827 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ∈ ℝ* ∧ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ* ∧ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∈ ℝ*) → (((𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∧ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
410406, 407, 408, 409syl3anc 1317 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (((𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ∧ ((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
411404, 410mpand 706 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (((𝑋𝐸(2nd ‘(𝑔𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
412367, 411syld 45 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
413 xrex 11664 . . . . . . . . . . . . . . . . . . . . . . . . . 26 * ∈ V
414413, 27ssexi 4726 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ℝ* ∖ {-∞}) ∈ V
41523, 22ressplusg 15767 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((ℝ* ∖ {-∞}) ∈ V → +𝑒 = (+g𝑊))
416414, 415ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24 +𝑒 = (+g𝑊)
41744ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...𝑥)) → 𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
418 fzelp1 12221 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑗 ∈ (1...𝑥) → 𝑗 ∈ (1...(𝑥 + 1)))
41950ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...(𝑥 + 1))) → 𝑔:(1...𝑛)⟶(𝑉 × 𝑉))
420354sselda 3567 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...(𝑥 + 1))) → 𝑗 ∈ (1...𝑛))
421419, 420ffvelrnd 6253 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...(𝑥 + 1))) → (𝑔𝑗) ∈ (𝑉 × 𝑉))
422418, 421sylan2 489 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...𝑥)) → (𝑔𝑗) ∈ (𝑉 × 𝑉))
423417, 422ffvelrnd 6253 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) ∧ 𝑗 ∈ (1...𝑥)) → (𝐸‘(𝑔𝑗)) ∈ (ℝ* ∖ {-∞}))
424 fzp1disj 12227 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((1...𝑥) ∩ {(𝑥 + 1)}) = ∅
425424a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((1...𝑥) ∩ {(𝑥 + 1)}) = ∅)
426 disjsn 4191 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((1...𝑥) ∩ {(𝑥 + 1)}) = ∅ ↔ ¬ (𝑥 + 1) ∈ (1...𝑥))
427425, 426sylib 206 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ¬ (𝑥 + 1) ∈ (1...𝑥))
42844adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → 𝐸:(𝑉 × 𝑉)⟶(ℝ* ∖ {-∞}))
429428, 363ffvelrnd 6253 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸‘(𝑔‘(𝑥 + 1))) ∈ (ℝ* ∖ {-∞}))
430 fveq2 6088 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑗 = (𝑥 + 1) → (𝑔𝑗) = (𝑔‘(𝑥 + 1)))
431430fveq2d 6092 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑗 = (𝑥 + 1) → (𝐸‘(𝑔𝑗)) = (𝐸‘(𝑔‘(𝑥 + 1))))
43265, 416, 346, 347, 423, 333, 427, 429, 431gsumunsn 18131 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔𝑗)))) = ((𝑊 Σg (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔𝑗)))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
433309adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝐸𝑔) = (𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))))
434433, 350reseq12d 5305 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸𝑔) ↾ (1...(𝑥 + 1))) = ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))) ↾ ((1...𝑥) ∪ {(𝑥 + 1)})))
435355resmptd 5358 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))) ↾ ((1...𝑥) ∪ {(𝑥 + 1)})) = (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔𝑗))))
436434, 435eqtrd 2643 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸𝑔) ↾ (1...(𝑥 + 1))) = (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔𝑗))))
437436oveq2d 6543 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))) = (𝑊 Σg (𝑗 ∈ ((1...𝑥) ∪ {(𝑥 + 1)}) ↦ (𝐸‘(𝑔𝑗)))))
438433reseq1d 5303 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸𝑔) ↾ (1...𝑥)) = ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))) ↾ (1...𝑥)))
439356resmptd 5358 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑗 ∈ (1...𝑛) ↦ (𝐸‘(𝑔𝑗))) ↾ (1...𝑥)) = (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔𝑗))))
440438, 439eqtrd 2643 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝐸𝑔) ↾ (1...𝑥)) = (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔𝑗))))
441440oveq2d 6543 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) = (𝑊 Σg (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔𝑗)))))
442441oveq1d 6542 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))) = ((𝑊 Σg (𝑗 ∈ (1...𝑥) ↦ (𝐸‘(𝑔𝑗)))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
443432, 437, 4423eqtr4d 2653 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))) = ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1)))))
444443breq2d 4589 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))) ↔ (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ ((𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) +𝑒 (𝐸‘(𝑔‘(𝑥 + 1))))))
445412, 444sylibrd 247 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ (𝑥 ∈ ℕ ∧ (𝑥 + 1) ∈ (1...𝑛))) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1))))))
446445expr 640 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ 𝑥 ∈ ℕ) → ((𝑥 + 1) ∈ (1...𝑛) → ((𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))))))
447446a2d 29 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ 𝑥 ∈ ℕ) → (((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥)))) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))))))
448337, 447syld 45 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) ∧ 𝑥 ∈ ℕ) → ((𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥)))) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1)))))))
449448expcom 449 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℕ → (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥)))) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1))))))))
450449a2d 29 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℕ → ((((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑥 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑥))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑥))))) → (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝑥 + 1) ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔‘(𝑥 + 1)))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...(𝑥 + 1))))))))
451256, 266, 276, 286, 330, 450nnind 10888 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ → (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑛))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))))))
452235, 451mpcom 37 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑛 ∈ (1...𝑛) → (𝑋𝐸(2nd ‘(𝑔𝑛))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛)))))
453237, 452mpd 15 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸(2nd ‘(𝑔𝑛))) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))))
454245, 453eqbrtrrd 4601 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸𝑌) ≤ (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))))
455 ffn 5944 . . . . . . . . . . . . . 14 ((𝐸𝑔):(1...𝑛)⟶(ℝ* ∖ {-∞}) → (𝐸𝑔) Fn (1...𝑛))
456 fnresdm 5900 . . . . . . . . . . . . . 14 ((𝐸𝑔) Fn (1...𝑛) → ((𝐸𝑔) ↾ (1...𝑛)) = (𝐸𝑔))
45752, 455, 4563syl 18 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → ((𝐸𝑔) ↾ (1...𝑛)) = (𝐸𝑔))
458457oveq2d 6543 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))) = (𝑊 Σg (𝐸𝑔)))
45963, 458eqtr4d 2646 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (ℝ*𝑠 Σg (𝐸𝑔)) = (𝑊 Σg ((𝐸𝑔) ↾ (1...𝑛))))
460454, 459breqtrrd 4605 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑋𝐸𝑌) ≤ (ℝ*𝑠 Σg (𝐸𝑔)))
461 breq2 4581 . . . . . . . . . 10 (𝑝 = (ℝ*𝑠 Σg (𝐸𝑔)) → ((𝑋𝐸𝑌) ≤ 𝑝 ↔ (𝑋𝐸𝑌) ≤ (ℝ*𝑠 Σg (𝐸𝑔))))
462460, 461syl5ibrcom 235 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑔𝑆) → (𝑝 = (ℝ*𝑠 Σg (𝐸𝑔)) → (𝑋𝐸𝑌) ≤ 𝑝))
463462rexlimdva 3012 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (∃𝑔𝑆 𝑝 = (ℝ*𝑠 Σg (𝐸𝑔)) → (𝑋𝐸𝑌) ≤ 𝑝))
464227, 463syl5bi 230 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → (𝑝 ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) → (𝑋𝐸𝑌) ≤ 𝑝))
465464rexlimdva 3012 . . . . . 6 (𝜑 → (∃𝑛 ∈ ℕ 𝑝 ∈ ran (𝑔𝑆 ↦ (ℝ*𝑠 Σg (𝐸𝑔))) → (𝑋𝐸𝑌) ≤ 𝑝))
466224, 465syl5bi 230 . . . . 5 (𝜑 → (𝑝𝑇 → (𝑋𝐸𝑌) ≤ 𝑝))
467466ralrimiv 2947 . . . 4 (𝜑 → ∀𝑝𝑇 (𝑋𝐸𝑌) ≤ 𝑝)
468 infxrgelb 11996 . . . . 5 ((𝑇 ⊆ ℝ* ∧ (𝑋𝐸𝑌) ∈ ℝ*) → ((𝑋𝐸𝑌) ≤ inf(𝑇, ℝ*, < ) ↔ ∀𝑝𝑇 (𝑋𝐸𝑌) ≤ 𝑝))
46982, 86, 468syl2anc 690 . . . 4 (𝜑 → ((𝑋𝐸𝑌) ≤ inf(𝑇, ℝ*, < ) ↔ ∀𝑝𝑇 (𝑋𝐸𝑌) ≤ 𝑝))
470467, 469mpbird 245 . . 3 (𝜑 → (𝑋𝐸𝑌) ≤ inf(𝑇, ℝ*, < ))
47184, 86, 221, 470xrletrid 11824 . 2 (𝜑 → inf(𝑇, ℝ*, < ) = (𝑋𝐸𝑌))
47220, 471eqtrd 2643 1 (𝜑 → ((𝐹𝑋)𝐷(𝐹𝑌)) = (𝑋𝐸𝑌))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1976  wne 2779  wral 2895  wrex 2896  {crab 2899  Vcvv 3172  cdif 3536  cun 3537  cin 3538  wss 3539  c0 3873  {csn 4124  cop 4130   ciun 4449   class class class wbr 4577  cmpt 4637   × cxp 5026  ran crn 5029  cres 5030  ccom 5032   Fn wfn 5785  wf 5786  1-1wf1 5787  ontowfo 5788  1-1-ontowf1o 5789  cfv 5790  (class class class)co 6527  1st c1st 7035  2nd c2nd 7036  𝑚 cmap 7722  Fincfn 7819  infcinf 8208  cr 9792  0cc0 9793  1c1 9794   + caddc 9796  -∞cmnf 9929  *cxr 9930   < clt 9931  cle 9932  cmin 10118  cn 10870  cz 11213  cuz 11522   +𝑒 cxad 11779  ...cfz 12155  Basecbs 15644  s cress 15645  +gcplusg 15717  distcds 15726   Σg cgsu 15873  *𝑠cxrs 15932  s cimas 15936  Mndcmnd 17066  CMndccmn 17965  ∞Metcxmt 19501
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-inf2 8399  ax-cnex 9849  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869  ax-pre-mulgt0 9870  ax-pre-sup 9871
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-iin 4452  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-se 4988  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-isom 5799  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-of 6773  df-om 6936  df-1st 7037  df-2nd 7038  df-supp 7161  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-1o 7425  df-oadd 7429  df-er 7607  df-map 7724  df-en 7820  df-dom 7821  df-sdom 7822  df-fin 7823  df-fsupp 8137  df-sup 8209  df-inf 8210  df-oi 8276  df-card 8626  df-pnf 9933  df-mnf 9934  df-xr 9935  df-ltxr 9936  df-le 9937  df-sub 10120  df-neg 10121  df-div 10537  df-nn 10871  df-2 10929  df-3 10930  df-4 10931  df-5 10932  df-6 10933  df-7 10934  df-8 10935  df-9 10936  df-n0 11143  df-z 11214  df-dec 11329  df-uz 11523  df-rp 11668  df-xneg 11781  df-xadd 11782  df-xmul 11783  df-fz 12156  df-fzo 12293  df-seq 12622  df-hash 12938  df-struct 15646  df-ndx 15647  df-slot 15648  df-base 15649  df-sets 15650  df-ress 15651  df-plusg 15730  df-mulr 15731  df-sca 15733  df-vsca 15734  df-ip 15735  df-tset 15736  df-ple 15737  df-ds 15740  df-0g 15874  df-gsum 15875  df-xrs 15934  df-imas 15940  df-mre 16018  df-mrc 16019  df-acs 16021  df-mgm 17014  df-sgrp 17056  df-mnd 17067  df-submnd 17108  df-mulg 17313  df-cntz 17522  df-cmn 17967  df-xmet 19509
This theorem is referenced by:  imasdsf1o  21937
  Copyright terms: Public domain W3C validator