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

Theorem opsrval 19295
 Description: The value of the "ordered power series" function. This is the same as mPwSer psrval 19183, 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 3185 . . . . 5 (𝐼𝑉𝐼 ∈ V)
42, 3syl 17 . . . 4 (𝜑𝐼 ∈ V)
5 opsrval.r . . . . 5 (𝜑𝑅𝑊)
6 elex 3185 . . . . 5 (𝑅𝑊𝑅 ∈ V)
75, 6syl 17 . . . 4 (𝜑𝑅 ∈ V)
8 xpexg 6858 . . . . . 6 ((𝐼𝑉𝐼𝑉) → (𝐼 × 𝐼) ∈ V)
92, 2, 8syl2anc 691 . . . . 5 (𝜑 → (𝐼 × 𝐼) ∈ V)
10 pwexg 4776 . . . . 5 ((𝐼 × 𝐼) ∈ V → 𝒫 (𝐼 × 𝐼) ∈ V)
11 mptexg 6389 . . . . 5 (𝒫 (𝐼 × 𝐼) ∈ V → (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)) ∈ V)
129, 10, 113syl 18 . . . 4 (𝜑 → (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)) ∈ V)
13 simpl 472 . . . . . . . 8 ((𝑖 = 𝐼𝑠 = 𝑅) → 𝑖 = 𝐼)
1413sqxpeqd 5065 . . . . . . 7 ((𝑖 = 𝐼𝑠 = 𝑅) → (𝑖 × 𝑖) = (𝐼 × 𝐼))
1514pweqd 4113 . . . . . 6 ((𝑖 = 𝐼𝑠 = 𝑅) → 𝒫 (𝑖 × 𝑖) = 𝒫 (𝐼 × 𝐼))
16 ovex 6577 . . . . . . . 8 (𝑖 mPwSer 𝑠) ∈ V
1716a1i 11 . . . . . . 7 ((𝑖 = 𝐼𝑠 = 𝑅) → (𝑖 mPwSer 𝑠) ∈ V)
18 id 22 . . . . . . . . . 10 (𝑝 = (𝑖 mPwSer 𝑠) → 𝑝 = (𝑖 mPwSer 𝑠))
19 oveq12 6558 . . . . . . . . . 10 ((𝑖 = 𝐼𝑠 = 𝑅) → (𝑖 mPwSer 𝑠) = (𝐼 mPwSer 𝑅))
2018, 19sylan9eqr 2666 . . . . . . . . 9 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → 𝑝 = (𝐼 mPwSer 𝑅))
21 opsrval.s . . . . . . . . 9 𝑆 = (𝐼 mPwSer 𝑅)
2220, 21syl6eqr 2662 . . . . . . . 8 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → 𝑝 = 𝑆)
2322fveq2d 6107 . . . . . . . . . . . . 13 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (Base‘𝑝) = (Base‘𝑆))
24 opsrval.b . . . . . . . . . . . . 13 𝐵 = (Base‘𝑆)
2523, 24syl6eqr 2662 . . . . . . . . . . . 12 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (Base‘𝑝) = 𝐵)
2625sseq2d 3596 . . . . . . . . . . 11 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → ({𝑥, 𝑦} ⊆ (Base‘𝑝) ↔ {𝑥, 𝑦} ⊆ 𝐵))
27 ovex 6577 . . . . . . . . . . . . . . 15 (ℕ0𝑚 𝑖) ∈ V
2827rabex 4740 . . . . . . . . . . . . . 14 { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} ∈ V
2928a1i 11 . . . . . . . . . . . . 13 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} ∈ V)
3013adantr 480 . . . . . . . . . . . . . . . 16 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → 𝑖 = 𝐼)
3130oveq2d 6565 . . . . . . . . . . . . . . 15 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (ℕ0𝑚 𝑖) = (ℕ0𝑚 𝐼))
32 rabeq 3166 . . . . . . . . . . . . . . 15 ((ℕ0𝑚 𝑖) = (ℕ0𝑚 𝐼) → { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} = { ∈ (ℕ0𝑚 𝐼) ∣ ( “ ℕ) ∈ Fin})
3331, 32syl 17 . . . . . . . . . . . . . 14 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} = { ∈ (ℕ0𝑚 𝐼) ∣ ( “ ℕ) ∈ Fin})
34 opsrval.d . . . . . . . . . . . . . 14 𝐷 = { ∈ (ℕ0𝑚 𝐼) ∣ ( “ ℕ) ∈ Fin}
3533, 34syl6eqr 2662 . . . . . . . . . . . . 13 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} = 𝐷)
36 simpr 476 . . . . . . . . . . . . . 14 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → 𝑑 = 𝐷)
37 simpllr 795 . . . . . . . . . . . . . . . . . 18 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → 𝑠 = 𝑅)
3837fveq2d 6107 . . . . . . . . . . . . . . . . 17 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (lt‘𝑠) = (lt‘𝑅))
39 opsrval.q . . . . . . . . . . . . . . . . 17 < = (lt‘𝑅)
4038, 39syl6eqr 2662 . . . . . . . . . . . . . . . 16 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (lt‘𝑠) = < )
4140breqd 4594 . . . . . . . . . . . . . . 15 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ↔ (𝑥𝑧) < (𝑦𝑧)))
4230adantr 480 . . . . . . . . . . . . . . . . . . 19 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → 𝑖 = 𝐼)
4342oveq2d 6565 . . . . . . . . . . . . . . . . . 18 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (𝑟 <bag 𝑖) = (𝑟 <bag 𝐼))
4443breqd 4594 . . . . . . . . . . . . . . . . 17 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (𝑤(𝑟 <bag 𝑖)𝑧𝑤(𝑟 <bag 𝐼)𝑧))
4544imbi1d 330 . . . . . . . . . . . . . . . 16 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → ((𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤)) ↔ (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))))
4636, 45raleqbidv 3129 . . . . . . . . . . . . . . 15 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤)) ↔ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))))
4741, 46anbi12d 743 . . . . . . . . . . . . . 14 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ↔ ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤)))))
4836, 47rexeqbidv 3130 . . . . . . . . . . . . 13 ((((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) ∧ 𝑑 = 𝐷) → (∃𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤)))))
4929, 35, 48sbcied2 3440 . . . . . . . . . . . 12 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → ([{ ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤)))))
5049orbi1d 735 . . . . . . . . . . 11 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (([{ ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦) ↔ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦)))
5126, 50anbi12d 743 . . . . . . . . . 10 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦)) ↔ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))))
5251opabbidv 4648 . . . . . . . . 9 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))} = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))})
5352opeq2d 4347 . . . . . . . 8 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩ = ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)
5422, 53oveq12d 6567 . . . . . . 7 (((𝑖 = 𝐼𝑠 = 𝑅) ∧ 𝑝 = (𝑖 mPwSer 𝑠)) → (𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩) = (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩))
5517, 54csbied 3526 . . . . . 6 ((𝑖 = 𝐼𝑠 = 𝑅) → (𝑖 mPwSer 𝑠) / 𝑝(𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩) = (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩))
5615, 55mpteq12dv 4663 . . . . 5 ((𝑖 = 𝐼𝑠 = 𝑅) → (𝑟 ∈ 𝒫 (𝑖 × 𝑖) ↦ (𝑖 mPwSer 𝑠) / 𝑝(𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)) = (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)))
57 df-opsr 19181 . . . . 5 ordPwSer = (𝑖 ∈ V, 𝑠 ∈ V ↦ (𝑟 ∈ 𝒫 (𝑖 × 𝑖) ↦ (𝑖 mPwSer 𝑠) / 𝑝(𝑝 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑝) ∧ ([{ ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} / 𝑑]𝑧𝑑 ((𝑥𝑧)(lt‘𝑠)(𝑦𝑧) ∧ ∀𝑤𝑑 (𝑤(𝑟 <bag 𝑖)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)))
5856, 57ovmpt2ga 6688 . . . 4 ((𝐼 ∈ V ∧ 𝑅 ∈ V ∧ (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)) ∈ V) → (𝐼 ordPwSer 𝑅) = (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)))
594, 7, 12, 58syl3anc 1318 . . 3 (𝜑 → (𝐼 ordPwSer 𝑅) = (𝑟 ∈ 𝒫 (𝐼 × 𝐼) ↦ (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)))
60 simpr 476 . . . . . . . . . . . . . . . 16 ((𝜑𝑟 = 𝑇) → 𝑟 = 𝑇)
6160oveq1d 6564 . . . . . . . . . . . . . . 15 ((𝜑𝑟 = 𝑇) → (𝑟 <bag 𝐼) = (𝑇 <bag 𝐼))
62 opsrval.c . . . . . . . . . . . . . . 15 𝐶 = (𝑇 <bag 𝐼)
6361, 62syl6eqr 2662 . . . . . . . . . . . . . 14 ((𝜑𝑟 = 𝑇) → (𝑟 <bag 𝐼) = 𝐶)
6463breqd 4594 . . . . . . . . . . . . 13 ((𝜑𝑟 = 𝑇) → (𝑤(𝑟 <bag 𝐼)𝑧𝑤𝐶𝑧))
6564imbi1d 330 . . . . . . . . . . . 12 ((𝜑𝑟 = 𝑇) → ((𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤)) ↔ (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤))))
6665ralbidv 2969 . . . . . . . . . . 11 ((𝜑𝑟 = 𝑇) → (∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤)) ↔ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤))))
6766anbi2d 736 . . . . . . . . . 10 ((𝜑𝑟 = 𝑇) → (((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ↔ ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤)))))
6867rexbidv 3034 . . . . . . . . 9 ((𝜑𝑟 = 𝑇) → (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤)))))
6968orbi1d 735 . . . . . . . 8 ((𝜑𝑟 = 𝑇) → ((∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦) ↔ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦)))
7069anbi2d 736 . . . . . . 7 ((𝜑𝑟 = 𝑇) → (({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦)) ↔ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))))
7170opabbidv 4648 . . . . . 6 ((𝜑𝑟 = 𝑇) → {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))} = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))})
72 opsrval.l . . . . . 6 = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤𝐶𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}
7371, 72syl6eqr 2662 . . . . 5 ((𝜑𝑟 = 𝑇) → {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))} = )
7473opeq2d 4347 . . . 4 ((𝜑𝑟 = 𝑇) → ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩ = ⟨(le‘ndx), ⟩)
7574oveq2d 6565 . . 3 ((𝜑𝑟 = 𝑇) → (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ (∃𝑧𝐷 ((𝑥𝑧) < (𝑦𝑧) ∧ ∀𝑤𝐷 (𝑤(𝑟 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩) = (𝑆 sSet ⟨(le‘ndx), ⟩))
76 opsrval.t . . . 4 (𝜑𝑇 ⊆ (𝐼 × 𝐼))
77 elpw2g 4754 . . . . 5 ((𝐼 × 𝐼) ∈ V → (𝑇 ∈ 𝒫 (𝐼 × 𝐼) ↔ 𝑇 ⊆ (𝐼 × 𝐼)))
789, 77syl 17 . . . 4 (𝜑 → (𝑇 ∈ 𝒫 (𝐼 × 𝐼) ↔ 𝑇 ⊆ (𝐼 × 𝐼)))
7976, 78mpbird 246 . . 3 (𝜑𝑇 ∈ 𝒫 (𝐼 × 𝐼))
80 ovex 6577 . . . 4 (𝑆 sSet ⟨(le‘ndx), ⟩) ∈ V
8180a1i 11 . . 3 (𝜑 → (𝑆 sSet ⟨(le‘ndx), ⟩) ∈ V)
8259, 75, 79, 81fvmptd 6197 . 2 (𝜑 → ((𝐼 ordPwSer 𝑅)‘𝑇) = (𝑆 sSet ⟨(le‘ndx), ⟩))
831, 82syl5eq 2656 1 (𝜑𝑂 = (𝑆 sSet ⟨(le‘ndx), ⟩))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897  {crab 2900  Vcvv 3173  [wsbc 3402  ⦋csb 3499   ⊆ wss 3540  𝒫 cpw 4108  {cpr 4127  ⟨cop 4131   class class class wbr 4583  {copab 4642   ↦ cmpt 4643   × cxp 5036  ◡ccnv 5037   “ cima 5041  ‘cfv 5804  (class class class)co 6549   ↑𝑚 cmap 7744  Fincfn 7841  ℕcn 10897  ℕ0cn0 11169  ndxcnx 15692   sSet csts 15693  Basecbs 15695  lecple 15775  ltcplt 16764   mPwSer cmps 19172
 Copyright terms: Public domain W3C validator