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

Theorem opsrval2 19395
 Description: Self-referential expression for the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015.)
Hypotheses
Ref Expression
opsrval2.s 𝑆 = (𝐼 mPwSer 𝑅)
opsrval2.o 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)
opsrval2.l = (le‘𝑂)
opsrval2.i (𝜑𝐼𝑉)
opsrval2.r (𝜑𝑅𝑊)
opsrval2.t (𝜑𝑇 ⊆ (𝐼 × 𝐼))
Assertion
Ref Expression
opsrval2 (𝜑𝑂 = (𝑆 sSet ⟨(le‘ndx), ⟩))

Proof of Theorem opsrval2
Dummy variables 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opsrval2.s . . 3 𝑆 = (𝐼 mPwSer 𝑅)
2 opsrval2.o . . 3 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)
3 eqid 2621 . . 3 (Base‘𝑆) = (Base‘𝑆)
4 eqid 2621 . . 3 (lt‘𝑅) = (lt‘𝑅)
5 eqid 2621 . . 3 (𝑇 <bag 𝐼) = (𝑇 <bag 𝐼)
6 eqid 2621 . . 3 { ∈ (ℕ0𝑚 𝐼) ∣ ( “ ℕ) ∈ Fin} = { ∈ (ℕ0𝑚 𝐼) ∣ ( “ ℕ) ∈ Fin}
7 eqid 2621 . . 3 {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑆) ∧ (∃𝑧 ∈ { ∈ (ℕ0𝑚 𝐼) ∣ ( “ ℕ) ∈ Fin} ((𝑥𝑧)(lt‘𝑅)(𝑦𝑧) ∧ ∀𝑤 ∈ { ∈ (ℕ0𝑚 𝐼) ∣ ( “ ℕ) ∈ Fin} (𝑤(𝑇 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))} = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑆) ∧ (∃𝑧 ∈ { ∈ (ℕ0𝑚 𝐼) ∣ ( “ ℕ) ∈ Fin} ((𝑥𝑧)(lt‘𝑅)(𝑦𝑧) ∧ ∀𝑤 ∈ { ∈ (ℕ0𝑚 𝐼) ∣ ( “ ℕ) ∈ Fin} (𝑤(𝑇 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}
8 opsrval2.i . . 3 (𝜑𝐼𝑉)
9 opsrval2.r . . 3 (𝜑𝑅𝑊)
10 opsrval2.t . . 3 (𝜑𝑇 ⊆ (𝐼 × 𝐼))
111, 2, 3, 4, 5, 6, 7, 8, 9, 10opsrval 19393 . 2 (𝜑𝑂 = (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑆) ∧ (∃𝑧 ∈ { ∈ (ℕ0𝑚 𝐼) ∣ ( “ ℕ) ∈ Fin} ((𝑥𝑧)(lt‘𝑅)(𝑦𝑧) ∧ ∀𝑤 ∈ { ∈ (ℕ0𝑚 𝐼) ∣ ( “ ℕ) ∈ Fin} (𝑤(𝑇 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩))
12 opsrval2.l . . . . 5 = (le‘𝑂)
131, 2, 3, 4, 5, 6, 12, 10opsrle 19394 . . . 4 (𝜑 = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑆) ∧ (∃𝑧 ∈ { ∈ (ℕ0𝑚 𝐼) ∣ ( “ ℕ) ∈ Fin} ((𝑥𝑧)(lt‘𝑅)(𝑦𝑧) ∧ ∀𝑤 ∈ { ∈ (ℕ0𝑚 𝐼) ∣ ( “ ℕ) ∈ Fin} (𝑤(𝑇 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))})
1413opeq2d 4377 . . 3 (𝜑 → ⟨(le‘ndx), ⟩ = ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑆) ∧ (∃𝑧 ∈ { ∈ (ℕ0𝑚 𝐼) ∣ ( “ ℕ) ∈ Fin} ((𝑥𝑧)(lt‘𝑅)(𝑦𝑧) ∧ ∀𝑤 ∈ { ∈ (ℕ0𝑚 𝐼) ∣ ( “ ℕ) ∈ Fin} (𝑤(𝑇 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩)
1514oveq2d 6620 . 2 (𝜑 → (𝑆 sSet ⟨(le‘ndx), ⟩) = (𝑆 sSet ⟨(le‘ndx), {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑆) ∧ (∃𝑧 ∈ { ∈ (ℕ0𝑚 𝐼) ∣ ( “ ℕ) ∈ Fin} ((𝑥𝑧)(lt‘𝑅)(𝑦𝑧) ∧ ∀𝑤 ∈ { ∈ (ℕ0𝑚 𝐼) ∣ ( “ ℕ) ∈ Fin} (𝑤(𝑇 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ∨ 𝑥 = 𝑦))}⟩))
1611, 15eqtr4d 2658 1 (𝜑𝑂 = (𝑆 sSet ⟨(le‘ndx), ⟩))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 383   ∧ wa 384   = wceq 1480   ∈ wcel 1987  ∀wral 2907  ∃wrex 2908  {crab 2911   ⊆ wss 3555  {cpr 4150  ⟨cop 4154   class class class wbr 4613  {copab 4672   × cxp 5072  ◡ccnv 5073   “ cima 5077  ‘cfv 5847  (class class class)co 6604   ↑𝑚 cmap 7802  Fincfn 7899  ℕcn 10964  ℕ0cn0 11236  ndxcnx 15778   sSet csts 15779  Basecbs 15781  lecple 15869  ltcplt 16862   mPwSer cmps 19270
 Copyright terms: Public domain W3C validator