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

Theorem opsrtos 19886
 Description: The ordered power series structure is a totally ordered set. (Contributed by Mario Carneiro, 10-Jan-2015.)
Hypotheses
Ref Expression
opsrso.o 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)
opsrso.i (𝜑𝐼𝑉)
opsrso.r (𝜑𝑅 ∈ Toset)
opsrso.t (𝜑𝑇 ⊆ (𝐼 × 𝐼))
opsrso.w (𝜑𝑇 We 𝐼)
Assertion
Ref Expression
opsrtos (𝜑𝑂 ∈ Toset)

Proof of Theorem opsrtos
Dummy variables 𝑥 𝑦 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opsrso.o . 2 𝑂 = ((𝐼 ordPwSer 𝑅)‘𝑇)
2 opsrso.i . 2 (𝜑𝐼𝑉)
3 opsrso.r . 2 (𝜑𝑅 ∈ Toset)
4 opsrso.t . 2 (𝜑𝑇 ⊆ (𝐼 × 𝐼))
5 opsrso.w . 2 (𝜑𝑇 We 𝐼)
6 eqid 2778 . 2 (𝐼 mPwSer 𝑅) = (𝐼 mPwSer 𝑅)
7 eqid 2778 . 2 (Base‘(𝐼 mPwSer 𝑅)) = (Base‘(𝐼 mPwSer 𝑅))
8 eqid 2778 . 2 (lt‘𝑅) = (lt‘𝑅)
9 eqid 2778 . 2 (𝑇 <bag 𝐼) = (𝑇 <bag 𝐼)
10 eqid 2778 . 2 { ∈ (ℕ0𝑚 𝐼) ∣ ( “ ℕ) ∈ Fin} = { ∈ (ℕ0𝑚 𝐼) ∣ ( “ ℕ) ∈ Fin}
11 biid 253 . 2 (∃𝑧 ∈ { ∈ (ℕ0𝑚 𝐼) ∣ ( “ ℕ) ∈ Fin} ((𝑥𝑧)(lt‘𝑅)(𝑦𝑧) ∧ ∀𝑤 ∈ { ∈ (ℕ0𝑚 𝐼) ∣ ( “ ℕ) ∈ Fin} (𝑤(𝑇 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑧 ∈ { ∈ (ℕ0𝑚 𝐼) ∣ ( “ ℕ) ∈ Fin} ((𝑥𝑧)(lt‘𝑅)(𝑦𝑧) ∧ ∀𝑤 ∈ { ∈ (ℕ0𝑚 𝐼) ∣ ( “ ℕ) ∈ Fin} (𝑤(𝑇 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))))
12 eqid 2778 . 2 (le‘𝑂) = (le‘𝑂)
131, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12opsrtoslem2 19885 1 (𝜑𝑂 ∈ Toset)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 386   = wceq 1601   ∈ wcel 2107  ∀wral 3090  ∃wrex 3091  {crab 3094   ⊆ wss 3792   class class class wbr 4888   We wwe 5315   × cxp 5355  ◡ccnv 5356   “ cima 5360  ‘cfv 6137  (class class class)co 6924   ↑𝑚 cmap 8142  Fincfn 8243  ℕcn 11378  ℕ0cn0 11646  Basecbs 16259  lecple 16349  ltcplt 17331  Tosetctos 17423   mPwSer cmps 19752
 Copyright terms: Public domain W3C validator