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

Theorem opsrval 21247
Description: The value of the "ordered power series" function. This is the same as mPwSer psrval 21118, 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 𝐷 = { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ 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 (𝜑𝐼𝑉)
32elexd 3452 . . . 4 (𝜑𝐼 ∈ V)
4 opsrval.r . . . . 5 (𝜑𝑅𝑊)
54elexd 3452 . . . 4 (𝜑𝑅 ∈ V)
62, 2xpexd 7601 . . . . 5 (𝜑 → (𝐼 × 𝐼) ∈ V)
7 pwexg 5301 . . . . 5 ((𝐼 × 𝐼) ∈ V → 𝒫 (𝐼 × 𝐼) ∈ V)
8 mptexg 7097 . . . . 5 (𝒫 (𝐼 × 𝐼) ∈ V → (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)) ∈ V)
96, 7, 83syl 18 . . . 4 (𝜑 → (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)) ∈ V)
10 simpl 483 . . . . . . . 8 ((𝑖 = 𝐼𝑠 = 𝑅) → 𝑖 = 𝐼)
1110sqxpeqd 5621 . . . . . . 7 ((𝑖 = 𝐼𝑠 = 𝑅) → (𝑖 × 𝑖) = (𝐼 × 𝐼))
1211pweqd 4552 . . . . . 6 ((𝑖 = 𝐼𝑠 = 𝑅) → 𝒫 (𝑖 × 𝑖) = 𝒫 (𝐼 × 𝐼))
13 ovexd 7310 . . . . . . 7 ((𝑖 = 𝐼𝑠 = 𝑅) → (𝑖 mPwSer 𝑠) ∈ V)
14 id 22 . . . . . . . . . 10 (𝑝 = (𝑖 mPwSer 𝑠) → 𝑝 = (𝑖 mPwSer 𝑠))
15 oveq12 7284 . . . . . . . . . 10 ((𝑖 = 𝐼𝑠 = 𝑅) → (𝑖 mPwSer 𝑠) = (𝐼 mPwSer 𝑅))
1614, 15sylan9eqr 2800 . . . . . . . . 9 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → 𝑝 = (𝐼 mPwSer 𝑅))
17 opsrval.s . . . . . . . . 9 𝑆 = (𝐼 mPwSer 𝑅)
1816, 17eqtr4di 2796 . . . . . . . 8 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → 𝑝 = 𝑆)
1918fveq2d 6778 . . . . . . . . . . . . 13 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (Base‘𝑝) = (Base‘𝑆))
20 opsrval.b . . . . . . . . . . . . 13 𝐵 = (Base‘𝑆)
2119, 20eqtr4di 2796 . . . . . . . . . . . 12 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (Base‘𝑝) = 𝐵)
2221sseq2d 3953 . . . . . . . . . . 11 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → ({𝑥, 𝑦} ⊆ (Base‘𝑝) ↔ {𝑥, 𝑦} ⊆ 𝐵))
23 ovex 7308 . . . . . . . . . . . . . . 15 (ℕ0m 𝑖) ∈ V
2423rabex 5256 . . . . . . . . . . . . . 14 { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ∈ V
2524a1i 11 . . . . . . . . . . . . 13 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ∈ V)
2610adantr 481 . . . . . . . . . . . . . . . 16 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → 𝑖 = 𝐼)
2726oveq2d 7291 . . . . . . . . . . . . . . 15 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (ℕ0m 𝑖) = (ℕ0m 𝐼))
28 rabeq 3418 . . . . . . . . . . . . . . 15 ((ℕ0m 𝑖) = (ℕ0m 𝐼) → { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} = { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin})
2927, 28syl 17 . . . . . . . . . . . . . 14 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} = { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin})
30 opsrval.d . . . . . . . . . . . . . 14 𝐷 = { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}
3129, 30eqtr4di 2796 . . . . . . . . . . . . 13 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} = 𝐷)
32 simpr 485 . . . . . . . . . . . . . 14 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → 𝑑 = 𝐷)
33 simpllr 773 . . . . . . . . . . . . . . . . . 18 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → 𝑠 = 𝑅)
3433fveq2d 6778 . . . . . . . . . . . . . . . . 17 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (lt‘𝑠) = (lt‘𝑅))
35 opsrval.q . . . . . . . . . . . . . . . . 17 < = (lt‘𝑅)
3634, 35eqtr4di 2796 . . . . . . . . . . . . . . . 16 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (lt‘𝑠) = < )
3736breqd 5085 . . . . . . . . . . . . . . 15 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ↔ (𝑥𝑧) < (𝑦𝑧)))
3826adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → 𝑖 = 𝐼)
3938oveq2d 7291 . . . . . . . . . . . . . . . . . 18 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (𝑟 <bag 𝑖) = (𝑟 <bag 𝐼))
4039breqd 5085 . . . . . . . . . . . . . . . . 17 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (𝑤(𝑟 <bag 𝑖)𝑧𝑤(𝑟 <bag 𝐼)𝑧))
4140imbi1d 342 . . . . . . . . . . . . . . . 16 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → ((𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤)) ↔ (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))))
4232, 41raleqbidv 3336 . . . . . . . . . . . . . . 15 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤)) ↔ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))))
4337, 42anbi12d 631 . . . . . . . . . . . . . 14 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ↔ ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤)))))
4432, 43rexeqbidv 3337 . . . . . . . . . . . . 13 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (∃𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤)))))
4525, 31, 44sbcied2 3763 . . . . . . . . . . . 12 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤)))))
4645orbi1d 914 . . . . . . . . . . 11 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦) ↔ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦)))
4722, 46anbi12d 631 . . . . . . . . . 10 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦)) ↔ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))))
4847opabbidv 5140 . . . . . . . . 9 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))} = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))})
4948opeq2d 4811 . . . . . . . 8 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩ = ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)
5018, 49oveq12d 7293 . . . . . . 7 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩) = (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩))
5113, 50csbied 3870 . . . . . 6 ((𝑖 = 𝐼𝑠 = 𝑅) → (𝑖 mPwSer 𝑠) / 𝑝(𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩) = (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩))
5212, 51mpteq12dv 5165 . . . . 5 ((𝑖 = 𝐼𝑠 = 𝑅) → (𝑟 ∈ 𝒫 (𝑖 × 𝑖) ↦ (𝑖 mPwSer 𝑠) / 𝑝(𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)) = (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)))
53 df-opsr 21116 . . . . 5 ordPwSer = (𝑖 ∈ V, 𝑠 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑖 × 𝑖) ↦ (𝑖 mPwSer 𝑠) / 𝑝(𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)))
5452, 53ovmpoga 7427 . . . 4 ((𝐼 ∈ V ∧ 𝑅 ∈ V ∧ (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)) ∈ V) → (𝐼 ordPwSer 𝑅) = (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)))
553, 5, 9, 54syl3anc 1370 . . 3 (𝜑 → (𝐼 ordPwSer 𝑅) = (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)))
56 simpr 485 . . . . . . . . . . . . . . . 16 ((𝜑𝑟 = 𝑇) → 𝑟 = 𝑇)
5756oveq1d 7290 . . . . . . . . . . . . . . 15 ((𝜑𝑟 = 𝑇) → (𝑟 <bag 𝐼) = (𝑇 <bag 𝐼))
58 opsrval.c . . . . . . . . . . . . . . 15 𝐶 = (𝑇 <bag 𝐼)
5957, 58eqtr4di 2796 . . . . . . . . . . . . . 14 ((𝜑𝑟 = 𝑇) → (𝑟 <bag 𝐼) = 𝐶)
6059breqd 5085 . . . . . . . . . . . . 13 ((𝜑𝑟 = 𝑇) → (𝑤(𝑟 <bag 𝐼)𝑧𝑤𝐶𝑧))
6160imbi1d 342 . . . . . . . . . . . 12 ((𝜑𝑟 = 𝑇) → ((𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤)) ↔ (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤))))
6261ralbidv 3112 . . . . . . . . . . 11 ((𝜑𝑟 = 𝑇) → (∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤)) ↔ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤))))
6362anbi2d 629 . . . . . . . . . 10 ((𝜑𝑟 = 𝑇) → (((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ↔ ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤)))))
6463rexbidv 3226 . . . . . . . . 9 ((𝜑𝑟 = 𝑇) → (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤)))))
6564orbi1d 914 . . . . . . . 8 ((𝜑𝑟 = 𝑇) → ((∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦) ↔ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦)))
6665anbi2d 629 . . . . . . 7 ((𝜑𝑟 = 𝑇) → (({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦)) ↔ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))))
6766opabbidv 5140 . . . . . 6 ((𝜑𝑟 = 𝑇) → {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))} = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))})
68 opsrval.l . . . . . 6 = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}
6967, 68eqtr4di 2796 . . . . 5 ((𝜑𝑟 = 𝑇) → {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))} = )
7069opeq2d 4811 . . . 4 ((𝜑𝑟 = 𝑇) → ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩ = ⟨(le‘ndx), ⟩)
7170oveq2d 7291 . . 3 ((𝜑𝑟 = 𝑇) → (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩) = (𝑆 sSet ⟨(le‘ndx), ⟩))
72 opsrval.t . . . 4 (𝜑𝑇 ⊆ (𝐼 × 𝐼))
736, 72sselpwd 5250 . . 3 (𝜑𝑇 ∈ 𝒫 (𝐼 × 𝐼))
74 ovexd 7310 . . 3 (𝜑 → (𝑆 sSet ⟨(le‘ndx), ⟩) ∈ V)
7555, 71, 73, 74fvmptd 6882 . 2 (𝜑 → ((𝐼 ordPwSer 𝑅)‘𝑇) = (𝑆 sSet ⟨(le‘ndx), ⟩))
761, 75eqtrid 2790 1 (𝜑𝑂 = (𝑆 sSet ⟨(le‘ndx), ⟩))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wo 844   = wceq 1539  wcel 2106  wral 3064  wrex 3065  {crab 3068  Vcvv 3432  [wsbc 3716  csb 3832  wss 3887  𝒫 cpw 4533  {cpr 4563  cop 4567   class class class wbr 5074  {copab 5136  cmpt 5157   × cxp 5587  ccnv 5588  cima 5592  cfv 6433  (class class class)co 7275  m cmap 8615  Fincfn 8733  cn 11973  0cn0 12233   sSet csts 16864  ndxcnx 16894  Basecbs 16912  lecple 16969  ltcplt 18026   mPwSer cmps 21107   <bag cltb 21110   ordPwSer copws 21111
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-ov 7278  df-oprab 7279  df-mpo 7280  df-opsr 21116
This theorem is referenced by:  opsrle  21248  opsrval2  21249
  Copyright terms: Public domain W3C validator