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

Theorem opsrval 19835
Description: The value of the "ordered power series" function. This is the same as mPwSer psrval 19723, but with the addition of a well-order on 𝐼 we can turn a strict order on 𝑅 into a strict order on the power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.)
Hypotheses
Ref Expression
opsrval.s 𝑆 = (𝐼 mPwSer 𝑅)
opsrval.o 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)
opsrval.b 𝐵 = (Base‘𝑆)
opsrval.q < = (lt‘𝑅)
opsrval.c 𝐶 = (𝑇 <bag 𝐼)
opsrval.d 𝐷 = { ∈ (ℕ0𝑚 𝐼) ∣ ( “ ℕ) ∈ Fin}
opsrval.l = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}
opsrval.i (𝜑𝐼𝑉)
opsrval.r (𝜑𝑅𝑊)
opsrval.t (𝜑𝑇 ⊆ (𝐼 × 𝐼))
Assertion
Ref Expression
opsrval (𝜑𝑂 = (𝑆 sSet ⟨(le‘ndx), ⟩))
Distinct variable groups:   𝑤,,𝑥,𝑦,𝑧,𝐼   𝜑,𝑤,𝑥,𝑦,𝑧   𝑤,𝐷,𝑧   𝑤,𝑇,𝑥,𝑦,𝑧   𝑤,𝑅,𝑥,𝑦,𝑧
Allowed substitution hints:   𝜑()   𝐵(𝑥,𝑦,𝑧,𝑤,)   𝐶(𝑥,𝑦,𝑧,𝑤,)   𝐷(𝑥,𝑦,)   𝑅()   𝑆(𝑥,𝑦,𝑧,𝑤,)   < (𝑥,𝑦,𝑧,𝑤,)   𝑇()   (𝑥,𝑦,𝑧,𝑤,)   𝑂(𝑥,𝑦,𝑧,𝑤,)   𝑉(𝑥,𝑦,𝑧,𝑤,)   𝑊(𝑥,𝑦,𝑧,𝑤,)

Proof of Theorem opsrval
Dummy variables 𝑟 𝑖 𝑝 𝑠 𝑑 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opsrval.o . 2 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)
2 opsrval.i . . . . 5 (𝜑𝐼𝑉)
3 elex 3429 . . . . 5 (𝐼𝑉𝐼 ∈ V)
42, 3syl 17 . . . 4 (𝜑𝐼 ∈ V)
5 opsrval.r . . . . 5 (𝜑𝑅𝑊)
6 elex 3429 . . . . 5 (𝑅𝑊𝑅 ∈ V)
75, 6syl 17 . . . 4 (𝜑𝑅 ∈ V)
82, 2xpexd 7221 . . . . 5 (𝜑 → (𝐼 × 𝐼) ∈ V)
9 pwexg 5078 . . . . 5 ((𝐼 × 𝐼) ∈ V → 𝒫 (𝐼 × 𝐼) ∈ V)
10 mptexg 6740 . . . . 5 (𝒫 (𝐼 × 𝐼) ∈ V → (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)) ∈ V)
118, 9, 103syl 18 . . . 4 (𝜑 → (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)) ∈ V)
12 simpl 476 . . . . . . . 8 ((𝑖 = 𝐼𝑠 = 𝑅) → 𝑖 = 𝐼)
1312sqxpeqd 5374 . . . . . . 7 ((𝑖 = 𝐼𝑠 = 𝑅) → (𝑖 × 𝑖) = (𝐼 × 𝐼))
1413pweqd 4383 . . . . . 6 ((𝑖 = 𝐼𝑠 = 𝑅) → 𝒫 (𝑖 × 𝑖) = 𝒫 (𝐼 × 𝐼))
15 ovexd 6939 . . . . . . 7 ((𝑖 = 𝐼𝑠 = 𝑅) → (𝑖 mPwSer 𝑠) ∈ V)
16 id 22 . . . . . . . . . 10 (𝑝 = (𝑖 mPwSer 𝑠) → 𝑝 = (𝑖 mPwSer 𝑠))
17 oveq12 6914 . . . . . . . . . 10 ((𝑖 = 𝐼𝑠 = 𝑅) → (𝑖 mPwSer 𝑠) = (𝐼 mPwSer 𝑅))
1816, 17sylan9eqr 2883 . . . . . . . . 9 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → 𝑝 = (𝐼 mPwSer 𝑅))
19 opsrval.s . . . . . . . . 9 𝑆 = (𝐼 mPwSer 𝑅)
2018, 19syl6eqr 2879 . . . . . . . 8 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → 𝑝 = 𝑆)
2120fveq2d 6437 . . . . . . . . . . . . 13 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (Base‘𝑝) = (Base‘𝑆))
22 opsrval.b . . . . . . . . . . . . 13 𝐵 = (Base‘𝑆)
2321, 22syl6eqr 2879 . . . . . . . . . . . 12 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (Base‘𝑝) = 𝐵)
2423sseq2d 3858 . . . . . . . . . . 11 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → ({𝑥, 𝑦} ⊆ (Base‘𝑝) ↔ {𝑥, 𝑦} ⊆ 𝐵))
25 ovex 6937 . . . . . . . . . . . . . . 15 (ℕ0𝑚 𝑖) ∈ V
2625rabex 5037 . . . . . . . . . . . . . 14 { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} ∈ V
2726a1i 11 . . . . . . . . . . . . 13 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} ∈ V)
2812adantr 474 . . . . . . . . . . . . . . . 16 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → 𝑖 = 𝐼)
2928oveq2d 6921 . . . . . . . . . . . . . . 15 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (ℕ0𝑚 𝑖) = (ℕ0𝑚 𝐼))
30 rabeq 3405 . . . . . . . . . . . . . . 15 ((ℕ0𝑚 𝑖) = (ℕ0𝑚 𝐼) → { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} = { ∈ (ℕ0𝑚 𝐼) ∣ ( “ ℕ) ∈ Fin})
3129, 30syl 17 . . . . . . . . . . . . . 14 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} = { ∈ (ℕ0𝑚 𝐼) ∣ ( “ ℕ) ∈ Fin})
32 opsrval.d . . . . . . . . . . . . . 14 𝐷 = { ∈ (ℕ0𝑚 𝐼) ∣ ( “ ℕ) ∈ Fin}
3331, 32syl6eqr 2879 . . . . . . . . . . . . 13 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} = 𝐷)
34 simpr 479 . . . . . . . . . . . . . 14 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → 𝑑 = 𝐷)
35 simpllr 795 . . . . . . . . . . . . . . . . . 18 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → 𝑠 = 𝑅)
3635fveq2d 6437 . . . . . . . . . . . . . . . . 17 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (lt‘𝑠) = (lt‘𝑅))
37 opsrval.q . . . . . . . . . . . . . . . . 17 < = (lt‘𝑅)
3836, 37syl6eqr 2879 . . . . . . . . . . . . . . . 16 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (lt‘𝑠) = < )
3938breqd 4884 . . . . . . . . . . . . . . 15 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ↔ (𝑥𝑧) < (𝑦𝑧)))
4028adantr 474 . . . . . . . . . . . . . . . . . . 19 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → 𝑖 = 𝐼)
4140oveq2d 6921 . . . . . . . . . . . . . . . . . 18 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (𝑟 <bag 𝑖) = (𝑟 <bag 𝐼))
4241breqd 4884 . . . . . . . . . . . . . . . . 17 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (𝑤(𝑟 <bag 𝑖)𝑧𝑤(𝑟 <bag 𝐼)𝑧))
4342imbi1d 333 . . . . . . . . . . . . . . . 16 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → ((𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤)) ↔ (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))))
4434, 43raleqbidv 3364 . . . . . . . . . . . . . . 15 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤)) ↔ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))))
4539, 44anbi12d 626 . . . . . . . . . . . . . 14 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ↔ ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤)))))
4634, 45rexeqbidv 3365 . . . . . . . . . . . . 13 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (∃𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤)))))
4727, 33, 46sbcied2 3700 . . . . . . . . . . . 12 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → ([{ ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤)))))
4847orbi1d 947 . . . . . . . . . . 11 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (([{ ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦) ↔ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦)))
4924, 48anbi12d 626 . . . . . . . . . 10 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦)) ↔ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))))
5049opabbidv 4939 . . . . . . . . 9 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))} = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))})
5150opeq2d 4630 . . . . . . . 8 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩ = ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)
5220, 51oveq12d 6923 . . . . . . 7 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩) = (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩))
5315, 52csbied 3784 . . . . . 6 ((𝑖 = 𝐼𝑠 = 𝑅) → (𝑖 mPwSer 𝑠) / 𝑝(𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩) = (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩))
5414, 53mpteq12dv 4956 . . . . 5 ((𝑖 = 𝐼𝑠 = 𝑅) → (𝑟 ∈ 𝒫 (𝑖 × 𝑖) ↦ (𝑖 mPwSer 𝑠) / 𝑝(𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)) = (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)))
55 df-opsr 19721 . . . . 5 ordPwSer = (𝑖 ∈ V, 𝑠 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑖 × 𝑖) ↦ (𝑖 mPwSer 𝑠) / 𝑝(𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)))
5654, 55ovmpt2ga 7050 . . . 4 ((𝐼 ∈ V ∧ 𝑅 ∈ V ∧ (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)) ∈ V) → (𝐼 ordPwSer 𝑅) = (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)))
574, 7, 11, 56syl3anc 1496 . . 3 (𝜑 → (𝐼 ordPwSer 𝑅) = (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)))
58 simpr 479 . . . . . . . . . . . . . . . 16 ((𝜑𝑟 = 𝑇) → 𝑟 = 𝑇)
5958oveq1d 6920 . . . . . . . . . . . . . . 15 ((𝜑𝑟 = 𝑇) → (𝑟 <bag 𝐼) = (𝑇 <bag 𝐼))
60 opsrval.c . . . . . . . . . . . . . . 15 𝐶 = (𝑇 <bag 𝐼)
6159, 60syl6eqr 2879 . . . . . . . . . . . . . 14 ((𝜑𝑟 = 𝑇) → (𝑟 <bag 𝐼) = 𝐶)
6261breqd 4884 . . . . . . . . . . . . 13 ((𝜑𝑟 = 𝑇) → (𝑤(𝑟 <bag 𝐼)𝑧𝑤𝐶𝑧))
6362imbi1d 333 . . . . . . . . . . . 12 ((𝜑𝑟 = 𝑇) → ((𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤)) ↔ (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤))))
6463ralbidv 3195 . . . . . . . . . . 11 ((𝜑𝑟 = 𝑇) → (∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤)) ↔ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤))))
6564anbi2d 624 . . . . . . . . . 10 ((𝜑𝑟 = 𝑇) → (((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ↔ ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤)))))
6665rexbidv 3262 . . . . . . . . 9 ((𝜑𝑟 = 𝑇) → (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤)))))
6766orbi1d 947 . . . . . . . 8 ((𝜑𝑟 = 𝑇) → ((∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦) ↔ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦)))
6867anbi2d 624 . . . . . . 7 ((𝜑𝑟 = 𝑇) → (({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦)) ↔ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))))
6968opabbidv 4939 . . . . . 6 ((𝜑𝑟 = 𝑇) → {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))} = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))})
70 opsrval.l . . . . . 6 = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}
7169, 70syl6eqr 2879 . . . . 5 ((𝜑𝑟 = 𝑇) → {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))} = )
7271opeq2d 4630 . . . 4 ((𝜑𝑟 = 𝑇) → ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩ = ⟨(le‘ndx), ⟩)
7372oveq2d 6921 . . 3 ((𝜑𝑟 = 𝑇) → (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩) = (𝑆 sSet ⟨(le‘ndx), ⟩))
74 opsrval.t . . . 4 (𝜑𝑇 ⊆ (𝐼 × 𝐼))
75 elpw2g 5049 . . . . 5 ((𝐼 × 𝐼) ∈ V → (𝑇 ∈ 𝒫 (𝐼 × 𝐼) ↔ 𝑇 ⊆ (𝐼 × 𝐼)))
768, 75syl 17 . . . 4 (𝜑 → (𝑇 ∈ 𝒫 (𝐼 × 𝐼) ↔ 𝑇 ⊆ (𝐼 × 𝐼)))
7774, 76mpbird 249 . . 3 (𝜑𝑇 ∈ 𝒫 (𝐼 × 𝐼))
78 ovexd 6939 . . 3 (𝜑 → (𝑆 sSet ⟨(le‘ndx), ⟩) ∈ V)
7957, 73, 77, 78fvmptd 6535 . 2 (𝜑 → ((𝐼 ordPwSer 𝑅)‘𝑇) = (𝑆 sSet ⟨(le‘ndx), ⟩))
801, 79syl5eq 2873 1 (𝜑𝑂 = (𝑆 sSet ⟨(le‘ndx), ⟩))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386  wo 880   = wceq 1658  wcel 2166  wral 3117  wrex 3118  {crab 3121  Vcvv 3414  [wsbc 3662  csb 3757  wss 3798  𝒫 cpw 4378  {cpr 4399  cop 4403   class class class wbr 4873  {copab 4935  cmpt 4952   × cxp 5340  ccnv 5341  cima 5345  cfv 6123  (class class class)co 6905  𝑚 cmap 8122  Fincfn 8222  cn 11350  0cn0 11618  ndxcnx 16219   sSet csts 16220  Basecbs 16222  lecple 16312  ltcplt 17294   mPwSer cmps 19712   <bag cltb 19715   ordPwSer copws 19716
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-rep 4994  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-reu 3124  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-iun 4742  df-br 4874  df-opab 4936  df-mpt 4953  df-id 5250  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-opsr 19721
This theorem is referenced by:  opsrle  19836  opsrval2  19837
  Copyright terms: Public domain W3C validator