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

Theorem opsrval 20231
Description: The value of the "ordered power series" function. This is the same as mPwSer psrval 20118, 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 3491 . . . 4 (𝜑𝐼 ∈ V)
4 opsrval.r . . . . 5 (𝜑𝑅𝑊)
54elexd 3491 . . . 4 (𝜑𝑅 ∈ V)
62, 2xpexd 7449 . . . . 5 (𝜑 → (𝐼 × 𝐼) ∈ V)
7 pwexg 5252 . . . . 5 ((𝐼 × 𝐼) ∈ V → 𝒫 (𝐼 × 𝐼) ∈ V)
8 mptexg 6957 . . . . 5 (𝒫 (𝐼 × 𝐼) ∈ V → (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)) ∈ V)
96, 7, 83syl 18 . . . 4 (𝜑 → (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)) ∈ V)
10 simpl 486 . . . . . . . 8 ((𝑖 = 𝐼𝑠 = 𝑅) → 𝑖 = 𝐼)
1110sqxpeqd 5560 . . . . . . 7 ((𝑖 = 𝐼𝑠 = 𝑅) → (𝑖 × 𝑖) = (𝐼 × 𝐼))
1211pweqd 4531 . . . . . 6 ((𝑖 = 𝐼𝑠 = 𝑅) → 𝒫 (𝑖 × 𝑖) = 𝒫 (𝐼 × 𝐼))
13 ovexd 7165 . . . . . . 7 ((𝑖 = 𝐼𝑠 = 𝑅) → (𝑖 mPwSer 𝑠) ∈ V)
14 id 22 . . . . . . . . . 10 (𝑝 = (𝑖 mPwSer 𝑠) → 𝑝 = (𝑖 mPwSer 𝑠))
15 oveq12 7139 . . . . . . . . . 10 ((𝑖 = 𝐼𝑠 = 𝑅) → (𝑖 mPwSer 𝑠) = (𝐼 mPwSer 𝑅))
1614, 15sylan9eqr 2878 . . . . . . . . 9 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → 𝑝 = (𝐼 mPwSer 𝑅))
17 opsrval.s . . . . . . . . 9 𝑆 = (𝐼 mPwSer 𝑅)
1816, 17syl6eqr 2874 . . . . . . . 8 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → 𝑝 = 𝑆)
1918fveq2d 6647 . . . . . . . . . . . . 13 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (Base‘𝑝) = (Base‘𝑆))
20 opsrval.b . . . . . . . . . . . . 13 𝐵 = (Base‘𝑆)
2119, 20syl6eqr 2874 . . . . . . . . . . . 12 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (Base‘𝑝) = 𝐵)
2221sseq2d 3975 . . . . . . . . . . 11 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → ({𝑥, 𝑦} ⊆ (Base‘𝑝) ↔ {𝑥, 𝑦} ⊆ 𝐵))
23 ovex 7163 . . . . . . . . . . . . . . 15 (ℕ0m 𝑖) ∈ V
2423rabex 5208 . . . . . . . . . . . . . 14 { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ∈ V
2524a1i 11 . . . . . . . . . . . . 13 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ∈ V)
2610adantr 484 . . . . . . . . . . . . . . . 16 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → 𝑖 = 𝐼)
2726oveq2d 7146 . . . . . . . . . . . . . . 15 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (ℕ0m 𝑖) = (ℕ0m 𝐼))
28 rabeq 3460 . . . . . . . . . . . . . . 15 ((ℕ0m 𝑖) = (ℕ0m 𝐼) → { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} = { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin})
2927, 28syl 17 . . . . . . . . . . . . . 14 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} = { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin})
30 opsrval.d . . . . . . . . . . . . . 14 𝐷 = { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}
3129, 30syl6eqr 2874 . . . . . . . . . . . . 13 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} = 𝐷)
32 simpr 488 . . . . . . . . . . . . . 14 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → 𝑑 = 𝐷)
33 simpllr 775 . . . . . . . . . . . . . . . . . 18 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → 𝑠 = 𝑅)
3433fveq2d 6647 . . . . . . . . . . . . . . . . 17 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (lt‘𝑠) = (lt‘𝑅))
35 opsrval.q . . . . . . . . . . . . . . . . 17 < = (lt‘𝑅)
3634, 35syl6eqr 2874 . . . . . . . . . . . . . . . 16 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (lt‘𝑠) = < )
3736breqd 5050 . . . . . . . . . . . . . . 15 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ↔ (𝑥𝑧) < (𝑦𝑧)))
3826adantr 484 . . . . . . . . . . . . . . . . . . 19 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → 𝑖 = 𝐼)
3938oveq2d 7146 . . . . . . . . . . . . . . . . . 18 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (𝑟 <bag 𝑖) = (𝑟 <bag 𝐼))
4039breqd 5050 . . . . . . . . . . . . . . . . 17 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (𝑤(𝑟 <bag 𝑖)𝑧𝑤(𝑟 <bag 𝐼)𝑧))
4140imbi1d 345 . . . . . . . . . . . . . . . 16 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → ((𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤)) ↔ (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))))
4232, 41raleqbidv 3386 . . . . . . . . . . . . . . 15 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤)) ↔ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))))
4337, 42anbi12d 633 . . . . . . . . . . . . . 14 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ↔ ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤)))))
4432, 43rexeqbidv 3387 . . . . . . . . . . . . 13 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (∃𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤)))))
4525, 31, 44sbcied2 3792 . . . . . . . . . . . 12 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤)))))
4645orbi1d 914 . . . . . . . . . . 11 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦) ↔ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦)))
4722, 46anbi12d 633 . . . . . . . . . 10 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦)) ↔ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))))
4847opabbidv 5105 . . . . . . . . 9 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))} = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))})
4948opeq2d 4783 . . . . . . . 8 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩ = ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)
5018, 49oveq12d 7148 . . . . . . 7 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩) = (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩))
5113, 50csbied 3893 . . . . . 6 ((𝑖 = 𝐼𝑠 = 𝑅) → (𝑖 mPwSer 𝑠) / 𝑝(𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩) = (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩))
5212, 51mpteq12dv 5124 . . . . 5 ((𝑖 = 𝐼𝑠 = 𝑅) → (𝑟 ∈ 𝒫 (𝑖 × 𝑖) ↦ (𝑖 mPwSer 𝑠) / 𝑝(𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)) = (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)))
53 df-opsr 20116 . . . . 5 ordPwSer = (𝑖 ∈ V, 𝑠 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑖 × 𝑖) ↦ (𝑖 mPwSer 𝑠) / 𝑝(𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)))
5452, 53ovmpoga 7278 . . . 4 ((𝐼 ∈ V ∧ 𝑅 ∈ V ∧ (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)) ∈ V) → (𝐼 ordPwSer 𝑅) = (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)))
553, 5, 9, 54syl3anc 1368 . . 3 (𝜑 → (𝐼 ordPwSer 𝑅) = (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)))
56 simpr 488 . . . . . . . . . . . . . . . 16 ((𝜑𝑟 = 𝑇) → 𝑟 = 𝑇)
5756oveq1d 7145 . . . . . . . . . . . . . . 15 ((𝜑𝑟 = 𝑇) → (𝑟 <bag 𝐼) = (𝑇 <bag 𝐼))
58 opsrval.c . . . . . . . . . . . . . . 15 𝐶 = (𝑇 <bag 𝐼)
5957, 58syl6eqr 2874 . . . . . . . . . . . . . 14 ((𝜑𝑟 = 𝑇) → (𝑟 <bag 𝐼) = 𝐶)
6059breqd 5050 . . . . . . . . . . . . 13 ((𝜑𝑟 = 𝑇) → (𝑤(𝑟 <bag 𝐼)𝑧𝑤𝐶𝑧))
6160imbi1d 345 . . . . . . . . . . . 12 ((𝜑𝑟 = 𝑇) → ((𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤)) ↔ (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤))))
6261ralbidv 3185 . . . . . . . . . . 11 ((𝜑𝑟 = 𝑇) → (∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤)) ↔ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤))))
6362anbi2d 631 . . . . . . . . . 10 ((𝜑𝑟 = 𝑇) → (((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ↔ ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤)))))
6463rexbidv 3283 . . . . . . . . 9 ((𝜑𝑟 = 𝑇) → (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤)))))
6564orbi1d 914 . . . . . . . 8 ((𝜑𝑟 = 𝑇) → ((∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦) ↔ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦)))
6665anbi2d 631 . . . . . . 7 ((𝜑𝑟 = 𝑇) → (({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦)) ↔ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))))
6766opabbidv 5105 . . . . . 6 ((𝜑𝑟 = 𝑇) → {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))} = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))})
68 opsrval.l . . . . . 6 = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}
6967, 68syl6eqr 2874 . . . . 5 ((𝜑𝑟 = 𝑇) → {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))} = )
7069opeq2d 4783 . . . 4 ((𝜑𝑟 = 𝑇) → ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩ = ⟨(le‘ndx), ⟩)
7170oveq2d 7146 . . 3 ((𝜑𝑟 = 𝑇) → (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩) = (𝑆 sSet ⟨(le‘ndx), ⟩))
72 opsrval.t . . . 4 (𝜑𝑇 ⊆ (𝐼 × 𝐼))
736, 72sselpwd 5203 . . 3 (𝜑𝑇 ∈ 𝒫 (𝐼 × 𝐼))
74 ovexd 7165 . . 3 (𝜑 → (𝑆 sSet ⟨(le‘ndx), ⟩) ∈ V)
7555, 71, 73, 74fvmptd 6748 . 2 (𝜑 → ((𝐼 ordPwSer 𝑅)‘𝑇) = (𝑆 sSet ⟨(le‘ndx), ⟩))
761, 75syl5eq 2868 1 (𝜑𝑂 = (𝑆 sSet ⟨(le‘ndx), ⟩))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wo 844   = wceq 1538  wcel 2115  wral 3126  wrex 3127  {crab 3130  Vcvv 3471  [wsbc 3749  csb 3857  wss 3910  𝒫 cpw 4512  {cpr 4542  cop 4546   class class class wbr 5039  {copab 5101  cmpt 5119   × cxp 5526  ccnv 5527  cima 5531  cfv 6328  (class class class)co 7130  m cmap 8381  Fincfn 8484  cn 11615  0cn0 11875  ndxcnx 16459   sSet csts 16460  Basecbs 16462  lecple 16551  ltcplt 17530   mPwSer cmps 20107   <bag cltb 20110   ordPwSer copws 20111
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-rep 5163  ax-sep 5176  ax-nul 5183  ax-pow 5239  ax-pr 5303  ax-un 7436
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ne 3008  df-ral 3131  df-rex 3132  df-reu 3133  df-rab 3135  df-v 3473  df-sbc 3750  df-csb 3858  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-if 4441  df-pw 4514  df-sn 4541  df-pr 4543  df-op 4547  df-uni 4812  df-iun 4894  df-br 5040  df-opab 5102  df-mpt 5120  df-id 5433  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-ov 7133  df-oprab 7134  df-mpo 7135  df-opsr 20116
This theorem is referenced by:  opsrle  20232  opsrval2  20233
  Copyright terms: Public domain W3C validator