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

Metamath Proof Explorer

Theorem opsrval2

Description: Self-referential expression for the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015)

Ref Expression
Hypotheses opsrval2.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
opsrval2.o ⊢ 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 )
opsrval2.l ⊢ ≤ = ( le ‘ 𝑂 )
opsrval2.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
opsrval2.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
opsrval2.t ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝐼 × 𝐼 ) )
Assertion opsrval2 ( 𝜑 → 𝑂 = ( 𝑆 sSet ⟨ ( le ‘ ndx ) , ≤ ⟩ ) )

Proof

Step Hyp Ref Expression
1 opsrval2.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 opsrval2.o ⊢ 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 )
3 opsrval2.l ⊢ ≤ = ( le ‘ 𝑂 )
4 opsrval2.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
5 opsrval2.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
6 opsrval2.t ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝐼 × 𝐼 ) )
7 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
8 eqid ⊢ ( lt ‘ 𝑅 ) = ( lt ‘ 𝑅 )
9 eqid ⊢ ( 𝑇 <bag 𝐼 ) = ( 𝑇 <bag 𝐼 )
10 eqid ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
11 eqid ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑆 ) ∧ ( ∃ 𝑧 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑅 ) ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ( 𝑤 ( 𝑇 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑆 ) ∧ ( ∃ 𝑧 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑅 ) ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ( 𝑤 ( 𝑇 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) }
12 1 2 7 8 9 10 11 4 5 6 opsrval ⊢ ( 𝜑 → 𝑂 = ( 𝑆 sSet ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑆 ) ∧ ( ∃ 𝑧 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑅 ) ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ( 𝑤 ( 𝑇 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⟩ ) )
13 1 2 7 8 9 10 3 6 opsrle ⊢ ( 𝜑 → ≤ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑆 ) ∧ ( ∃ 𝑧 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑅 ) ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ( 𝑤 ( 𝑇 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } )
14 13 opeq2d ⊢ ( 𝜑 → ⟨ ( le ‘ ndx ) , ≤ ⟩ = ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑆 ) ∧ ( ∃ 𝑧 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑅 ) ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ( 𝑤 ( 𝑇 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⟩ )
15 14 oveq2d ⊢ ( 𝜑 → ( 𝑆 sSet ⟨ ( le ‘ ndx ) , ≤ ⟩ ) = ( 𝑆 sSet ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑆 ) ∧ ( ∃ 𝑧 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑅 ) ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ( 𝑤 ( 𝑇 <bag 𝐼 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⟩ ) )
16 12 15 eqtr4d ⊢ ( 𝜑 → 𝑂 = ( 𝑆 sSet ⟨ ( le ‘ ndx ) , ≤ ⟩ ) )