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

Theorem opsrval 20857
Description: The value of the "ordered power series" function. This is the same as mPwSer psrval 20728, 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 3418 . . . 4 (𝜑𝐼 ∈ V)
4 opsrval.r . . . . 5 (𝜑𝑅𝑊)
54elexd 3418 . . . 4 (𝜑𝑅 ∈ V)
62, 2xpexd 7492 . . . . 5 (𝜑 → (𝐼 × 𝐼) ∈ V)
7 pwexg 5245 . . . . 5 ((𝐼 × 𝐼) ∈ V → 𝒫 (𝐼 × 𝐼) ∈ V)
8 mptexg 6994 . . . . 5 (𝒫 (𝐼 × 𝐼) ∈ V → (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)) ∈ V)
96, 7, 83syl 18 . . . 4 (𝜑 → (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)) ∈ V)
10 simpl 486 . . . . . . . 8 ((𝑖 = 𝐼𝑠 = 𝑅) → 𝑖 = 𝐼)
1110sqxpeqd 5557 . . . . . . 7 ((𝑖 = 𝐼𝑠 = 𝑅) → (𝑖 × 𝑖) = (𝐼 × 𝐼))
1211pweqd 4507 . . . . . 6 ((𝑖 = 𝐼𝑠 = 𝑅) → 𝒫 (𝑖 × 𝑖) = 𝒫 (𝐼 × 𝐼))
13 ovexd 7205 . . . . . . 7 ((𝑖 = 𝐼𝑠 = 𝑅) → (𝑖 mPwSer 𝑠) ∈ V)
14 id 22 . . . . . . . . . 10 (𝑝 = (𝑖 mPwSer 𝑠) → 𝑝 = (𝑖 mPwSer 𝑠))
15 oveq12 7179 . . . . . . . . . 10 ((𝑖 = 𝐼𝑠 = 𝑅) → (𝑖 mPwSer 𝑠) = (𝐼 mPwSer 𝑅))
1614, 15sylan9eqr 2795 . . . . . . . . 9 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → 𝑝 = (𝐼 mPwSer 𝑅))
17 opsrval.s . . . . . . . . 9 𝑆 = (𝐼 mPwSer 𝑅)
1816, 17eqtr4di 2791 . . . . . . . 8 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → 𝑝 = 𝑆)
1918fveq2d 6678 . . . . . . . . . . . . 13 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (Base‘𝑝) = (Base‘𝑆))
20 opsrval.b . . . . . . . . . . . . 13 𝐵 = (Base‘𝑆)
2119, 20eqtr4di 2791 . . . . . . . . . . . 12 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (Base‘𝑝) = 𝐵)
2221sseq2d 3909 . . . . . . . . . . 11 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → ({𝑥, 𝑦} ⊆ (Base‘𝑝) ↔ {𝑥, 𝑦} ⊆ 𝐵))
23 ovex 7203 . . . . . . . . . . . . . . 15 (ℕ0m 𝑖) ∈ V
2423rabex 5200 . . . . . . . . . . . . . 14 { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ∈ V
2524a1i 11 . . . . . . . . . . . . 13 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} ∈ V)
2610adantr 484 . . . . . . . . . . . . . . . 16 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → 𝑖 = 𝐼)
2726oveq2d 7186 . . . . . . . . . . . . . . 15 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (ℕ0m 𝑖) = (ℕ0m 𝐼))
28 rabeq 3385 . . . . . . . . . . . . . . 15 ((ℕ0m 𝑖) = (ℕ0m 𝐼) → { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} = { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin})
2927, 28syl 17 . . . . . . . . . . . . . 14 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} = { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin})
30 opsrval.d . . . . . . . . . . . . . 14 𝐷 = { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}
3129, 30eqtr4di 2791 . . . . . . . . . . . . 13 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → { ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} = 𝐷)
32 simpr 488 . . . . . . . . . . . . . 14 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → 𝑑 = 𝐷)
33 simpllr 776 . . . . . . . . . . . . . . . . . 18 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → 𝑠 = 𝑅)
3433fveq2d 6678 . . . . . . . . . . . . . . . . 17 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (lt‘𝑠) = (lt‘𝑅))
35 opsrval.q . . . . . . . . . . . . . . . . 17 < = (lt‘𝑅)
3634, 35eqtr4di 2791 . . . . . . . . . . . . . . . 16 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (lt‘𝑠) = < )
3736breqd 5041 . . . . . . . . . . . . . . 15 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ↔ (𝑥𝑧) < (𝑦𝑧)))
3826adantr 484 . . . . . . . . . . . . . . . . . . 19 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → 𝑖 = 𝐼)
3938oveq2d 7186 . . . . . . . . . . . . . . . . . 18 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (𝑟 <bag 𝑖) = (𝑟 <bag 𝐼))
4039breqd 5041 . . . . . . . . . . . . . . . . 17 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (𝑤(𝑟 <bag 𝑖)𝑧𝑤(𝑟 <bag 𝐼)𝑧))
4140imbi1d 345 . . . . . . . . . . . . . . . 16 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → ((𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤)) ↔ (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))))
4232, 41raleqbidv 3304 . . . . . . . . . . . . . . 15 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤)) ↔ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))))
4337, 42anbi12d 634 . . . . . . . . . . . . . 14 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ↔ ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤)))))
4432, 43rexeqbidv 3305 . . . . . . . . . . . . 13 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (∃𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤)))))
4525, 31, 44sbcied2 3725 . . . . . . . . . . . 12 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤)))))
4645orbi1d 916 . . . . . . . . . . 11 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦) ↔ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦)))
4722, 46anbi12d 634 . . . . . . . . . 10 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦)) ↔ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))))
4847opabbidv 5096 . . . . . . . . 9 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))} = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))})
4948opeq2d 4768 . . . . . . . 8 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩ = ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)
5018, 49oveq12d 7188 . . . . . . 7 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩) = (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩))
5113, 50csbied 3826 . . . . . 6 ((𝑖 = 𝐼𝑠 = 𝑅) → (𝑖 mPwSer 𝑠) / 𝑝(𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩) = (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩))
5212, 51mpteq12dv 5115 . . . . 5 ((𝑖 = 𝐼𝑠 = 𝑅) → (𝑟 ∈ 𝒫 (𝑖 × 𝑖) ↦ (𝑖 mPwSer 𝑠) / 𝑝(𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)) = (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)))
53 df-opsr 20726 . . . . 5 ordPwSer = (𝑖 ∈ V, 𝑠 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑖 × 𝑖) ↦ (𝑖 mPwSer 𝑠) / 𝑝(𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0m 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)))
5452, 53ovmpoga 7319 . . . 4 ((𝐼 ∈ V ∧ 𝑅 ∈ V ∧ (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)) ∈ V) → (𝐼 ordPwSer 𝑅) = (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)))
553, 5, 9, 54syl3anc 1372 . . 3 (𝜑 → (𝐼 ordPwSer 𝑅) = (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)))
56 simpr 488 . . . . . . . . . . . . . . . 16 ((𝜑𝑟 = 𝑇) → 𝑟 = 𝑇)
5756oveq1d 7185 . . . . . . . . . . . . . . 15 ((𝜑𝑟 = 𝑇) → (𝑟 <bag 𝐼) = (𝑇 <bag 𝐼))
58 opsrval.c . . . . . . . . . . . . . . 15 𝐶 = (𝑇 <bag 𝐼)
5957, 58eqtr4di 2791 . . . . . . . . . . . . . 14 ((𝜑𝑟 = 𝑇) → (𝑟 <bag 𝐼) = 𝐶)
6059breqd 5041 . . . . . . . . . . . . 13 ((𝜑𝑟 = 𝑇) → (𝑤(𝑟 <bag 𝐼)𝑧𝑤𝐶𝑧))
6160imbi1d 345 . . . . . . . . . . . 12 ((𝜑𝑟 = 𝑇) → ((𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤)) ↔ (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤))))
6261ralbidv 3109 . . . . . . . . . . 11 ((𝜑𝑟 = 𝑇) → (∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤)) ↔ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤))))
6362anbi2d 632 . . . . . . . . . 10 ((𝜑𝑟 = 𝑇) → (((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ↔ ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤)))))
6463rexbidv 3207 . . . . . . . . 9 ((𝜑𝑟 = 𝑇) → (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤)))))
6564orbi1d 916 . . . . . . . 8 ((𝜑𝑟 = 𝑇) → ((∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦) ↔ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦)))
6665anbi2d 632 . . . . . . 7 ((𝜑𝑟 = 𝑇) → (({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦)) ↔ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))))
6766opabbidv 5096 . . . . . 6 ((𝜑𝑟 = 𝑇) → {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))} = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))})
68 opsrval.l . . . . . 6 = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}
6967, 68eqtr4di 2791 . . . . 5 ((𝜑𝑟 = 𝑇) → {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))} = )
7069opeq2d 4768 . . . 4 ((𝜑𝑟 = 𝑇) → ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩ = ⟨(le‘ndx), ⟩)
7170oveq2d 7186 . . 3 ((𝜑𝑟 = 𝑇) → (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩) = (𝑆 sSet ⟨(le‘ndx), ⟩))
72 opsrval.t . . . 4 (𝜑𝑇 ⊆ (𝐼 × 𝐼))
736, 72sselpwd 5194 . . 3 (𝜑𝑇 ∈ 𝒫 (𝐼 × 𝐼))
74 ovexd 7205 . . 3 (𝜑 → (𝑆 sSet ⟨(le‘ndx), ⟩) ∈ V)
7555, 71, 73, 74fvmptd 6782 . 2 (𝜑 → ((𝐼 ordPwSer 𝑅)‘𝑇) = (𝑆 sSet ⟨(le‘ndx), ⟩))
761, 75syl5eq 2785 1 (𝜑𝑂 = (𝑆 sSet ⟨(le‘ndx), ⟩))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wo 846   = wceq 1542  wcel 2114  wral 3053  wrex 3054  {crab 3057  Vcvv 3398  [wsbc 3680  csb 3790  wss 3843  𝒫 cpw 4488  {cpr 4518  cop 4522   class class class wbr 5030  {copab 5092  cmpt 5110   × cxp 5523  ccnv 5524  cima 5528  cfv 6339  (class class class)co 7170  m cmap 8437  Fincfn 8555  cn 11716  0cn0 11976  ndxcnx 16583   sSet csts 16584  Basecbs 16586  lecple 16675  ltcplt 17667   mPwSer cmps 20717   <bag cltb 20720   ordPwSer copws 20721
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7479
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-reu 3060  df-rab 3062  df-v 3400  df-sbc 3681  df-csb 3791  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-op 4523  df-uni 4797  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5429  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-iota 6297  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-ov 7173  df-oprab 7174  df-mpo 7175  df-opsr 20726
This theorem is referenced by:  opsrle  20858  opsrval2  20859
  Copyright terms: Public domain W3C validator