This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
11 biid ⊢ ( ∃ 𝑧 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑅 ) ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ( 𝑤 ( 𝑇 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ∃ 𝑧 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑅 ) ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ( 𝑤 ( 𝑇 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) )
12 eqid ⊢ ( le ‘ 𝑂 ) = ( le ‘ 𝑂 )
13 1 2 3 4 5 6 7 8 9 10 11 12 opsrtoslem2 ⊢ ( 𝜑 → 𝑂 ∈ Toset )