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

Theorem opsrtos 20259
 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 2824 . 2 (𝐼 mPwSer 𝑅) = (𝐼 mPwSer 𝑅)
7 eqid 2824 . 2 (Base‘(𝐼 mPwSer 𝑅)) = (Base‘(𝐼 mPwSer 𝑅))
8 eqid 2824 . 2 (lt‘𝑅) = (lt‘𝑅)
9 eqid 2824 . 2 (𝑇 <bag 𝐼) = (𝑇 <bag 𝐼)
10 eqid 2824 . 2 { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} = { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin}
11 biid 264 . 2 (∃𝑧 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ((𝑥𝑧)(lt‘𝑅)(𝑦𝑧) ∧ ∀𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} (𝑤(𝑇 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))) ↔ ∃𝑧 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} ((𝑥𝑧)(lt‘𝑅)(𝑦𝑧) ∧ ∀𝑤 ∈ { ∈ (ℕ0m 𝐼) ∣ ( “ ℕ) ∈ Fin} (𝑤(𝑇 <bag 𝐼)𝑧 → (𝑥𝑤) = (𝑦𝑤))))
12 eqid 2824 . 2 (le‘𝑂) = (le‘𝑂)
131, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12opsrtoslem2 20258 1 (𝜑𝑂 ∈ Toset)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2115  ∀wral 3133  ∃wrex 3134  {crab 3137   ⊆ wss 3919   class class class wbr 5052   We wwe 5500   × cxp 5540  ◡ccnv 5541   “ cima 5545  ‘cfv 6343  (class class class)co 7145   ↑m cmap 8396  Fincfn 8499  ℕcn 11630  ℕ0cn0 11890  Basecbs 16479  lecple 16568  ltcplt 17547  Tosetctos 17639   mPwSer cmps 20124
 Copyright terms: Public domain W3C validator