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 ) , ≤ ⟩ ) )