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 ⊢ S = I mPwSer R
opsrval2.o ⊢ O = I ordPwSer R ⁡ T
opsrval2.l ⊢ ≤ ˙ = ≤ O
opsrval2.i ⊢ φ → I ∈ V
opsrval2.r ⊢ φ → R ∈ W
opsrval2.t ⊢ φ → T ⊆ I × I
Assertion opsrval2 ⊢ φ → O = S sSet ≤ ndx ≤ ˙

Proof

Step Hyp Ref Expression
1 opsrval2.s ⊢ S = I mPwSer R
2 opsrval2.o ⊢ O = I ordPwSer R ⁡ T
3 opsrval2.l ⊢ ≤ ˙ = ≤ O
4 opsrval2.i ⊢ φ → I ∈ V
5 opsrval2.r ⊢ φ → R ∈ W
6 opsrval2.t ⊢ φ → T ⊆ I × I
7 eqid ⊢ Base S = Base S
8 eqid ⊢ < R = < R
9 eqid ⊢ T < bag I = T < bag I
10 eqid ⊢ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin = h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
11 eqid ⊢ x y | x y ⊆ Base S ∧ ∃ z ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin x ⁡ z < R y ⁡ z ∧ ∀ w ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin w T < bag I z → x ⁡ w = y ⁡ w ∨ x = y = x y | x y ⊆ Base S ∧ ∃ z ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin x ⁡ z < R y ⁡ z ∧ ∀ w ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin w T < bag I z → x ⁡ w = y ⁡ w ∨ x = y
12 1 2 7 8 9 10 11 4 5 6 opsrval ⊢ φ → O = S sSet ≤ ndx x y | x y ⊆ Base S ∧ ∃ z ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin x ⁡ z < R y ⁡ z ∧ ∀ w ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin w T < bag I z → x ⁡ w = y ⁡ w ∨ x = y
13 1 2 7 8 9 10 3 6 opsrle ⊢ φ → ≤ ˙ = x y | x y ⊆ Base S ∧ ∃ z ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin x ⁡ z < R y ⁡ z ∧ ∀ w ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin w T < bag I z → x ⁡ w = y ⁡ w ∨ x = y
14 13 opeq2d ⊢ φ → ≤ ndx ≤ ˙ = ≤ ndx x y | x y ⊆ Base S ∧ ∃ z ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin x ⁡ z < R y ⁡ z ∧ ∀ w ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin w T < bag I z → x ⁡ w = y ⁡ w ∨ x = y
15 14 oveq2d ⊢ φ → S sSet ≤ ndx ≤ ˙ = S sSet ≤ ndx x y | x y ⊆ Base S ∧ ∃ z ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin x ⁡ z < R y ⁡ z ∧ ∀ w ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin w T < bag I z → x ⁡ w = y ⁡ w ∨ x = y
16 12 15 eqtr4d ⊢ φ → O = S sSet ≤ ndx ≤ ˙