Metamath Proof Explorer


Theorem opsrtos

Description: The ordered power series structure is a totally ordered set. (Contributed by Mario Carneiro, 10-Jan-2015)

Ref Expression
Hypotheses opsrso.o 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 )
opsrso.i ( 𝜑𝐼𝑉 )
opsrso.r ( 𝜑𝑅 ∈ Toset )
opsrso.t ( 𝜑𝑇 ⊆ ( 𝐼 × 𝐼 ) )
opsrso.w ( 𝜑𝑇 We 𝐼 )
Assertion opsrtos ( 𝜑𝑂 ∈ Toset )

Proof

Step Hyp Ref Expression
1 opsrso.o 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 )
2 opsrso.i ( 𝜑𝐼𝑉 )
3 opsrso.r ( 𝜑𝑅 ∈ Toset )
4 opsrso.t ( 𝜑𝑇 ⊆ ( 𝐼 × 𝐼 ) )
5 opsrso.w ( 𝜑𝑇 We 𝐼 )
6 eqid ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
7 eqid ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
8 eqid ( lt ‘ 𝑅 ) = ( lt ‘ 𝑅 )
9 eqid ( 𝑇 <bag 𝐼 ) = ( 𝑇 <bag 𝐼 )
10 eqid { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } = { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin }
11 biid ( ∃ 𝑧 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ( ( 𝑥𝑧 ) ( lt ‘ 𝑅 ) ( 𝑦𝑧 ) ∧ ∀ 𝑤 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ( 𝑤 ( 𝑇 <bag 𝐼 ) 𝑧 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ) ↔ ∃ 𝑧 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ( ( 𝑥𝑧 ) ( lt ‘ 𝑅 ) ( 𝑦𝑧 ) ∧ ∀ 𝑤 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ( 𝑤 ( 𝑇 <bag 𝐼 ) 𝑧 → ( 𝑥𝑤 ) = ( 𝑦𝑤 ) ) ) )
12 eqid ( le ‘ 𝑂 ) = ( le ‘ 𝑂 )
13 1 2 3 4 5 6 7 8 9 10 11 12 opsrtoslem2 ( 𝜑𝑂 ∈ Toset )