Metamath Proof Explorer

Definition df-opsr

Description: Define a total order on the set of all power series in s from the index set i given a wellordering r of i and a totally ordered base ring s . (Contributed by Mario Carneiro, 8-Feb-2015)

Ref Expression
Assertion df-opsr ⊢ ordPwSer = i ∈ V , s ∈ V ⟼ r ∈ 𝒫 i × i ⟼ ⦋ i mPwSer s / p⦌ p sSet ≤ ndx x y | x y ⊆ Base p ∧ [˙ h ∈ ℕ 0 i | h -1 ℕ ∈ Fin / d]˙ ∃ z ∈ d x ⁡ z < s y ⁡ z ∧ ∀ w ∈ d w r < bag i z → x ⁡ w = y ⁡ w ∨ x = y

Detailed syntax breakdown

Step Hyp Ref Expression
0 copws class ordPwSer
1 vi setvar i
2 cvv class V
3 vs setvar s
4 vr setvar r
5 1 cv setvar i
6 5 5 cxp class i × i
7 6 cpw class 𝒫 i × i
8 cmps class mPwSer
9 3 cv setvar s
10 5 9 8 co class i mPwSer s
11 vp setvar p
12 11 cv setvar p
13 csts class sSet
14 cple class le
15 cnx class ndx
16 15 14 cfv class ≤ ndx
17 vx setvar x
18 vy setvar y
19 17 cv setvar x
20 18 cv setvar y
21 19 20 cpr class x y
22 cbs class Base
23 12 22 cfv class Base p
24 21 23 wss wff x y ⊆ Base p
25 vh setvar h
26 cn0 class ℕ 0
27 cmap class ↑ 𝑚
28 26 5 27 co class ℕ 0 i
29 25 cv setvar h
30 29 ccnv class h -1
31 cn class ℕ
32 30 31 cima class h -1 ℕ
33 cfn class Fin
34 32 33 wcel wff h -1 ℕ ∈ Fin
35 34 25 28 crab class h ∈ ℕ 0 i | h -1 ℕ ∈ Fin
36 vd setvar d
37 vz setvar z
38 36 cv setvar d
39 37 cv setvar z
40 39 19 cfv class x ⁡ z
41 cplt class lt
42 9 41 cfv class < s
43 39 20 cfv class y ⁡ z
44 40 43 42 wbr wff x ⁡ z < s y ⁡ z
45 vw setvar w
46 45 cv setvar w
47 4 cv setvar r
48 cltb class < bag
49 47 5 48 co class r < bag i
50 46 39 49 wbr wff w r < bag i z
51 46 19 cfv class x ⁡ w
52 46 20 cfv class y ⁡ w
53 51 52 wceq wff x ⁡ w = y ⁡ w
54 50 53 wi wff w r < bag i z → x ⁡ w = y ⁡ w
55 54 45 38 wral wff ∀ w ∈ d w r < bag i z → x ⁡ w = y ⁡ w
56 44 55 wa wff x ⁡ z < s y ⁡ z ∧ ∀ w ∈ d w r < bag i z → x ⁡ w = y ⁡ w
57 56 37 38 wrex wff ∃ z ∈ d x ⁡ z < s y ⁡ z ∧ ∀ w ∈ d w r < bag i z → x ⁡ w = y ⁡ w
58 57 36 35 wsbc wff [˙ h ∈ ℕ 0 i | h -1 ℕ ∈ Fin / d]˙ ∃ z ∈ d x ⁡ z < s y ⁡ z ∧ ∀ w ∈ d w r < bag i z → x ⁡ w = y ⁡ w
59 19 20 wceq wff x = y
60 58 59 wo wff [˙ h ∈ ℕ 0 i | h -1 ℕ ∈ Fin / d]˙ ∃ z ∈ d x ⁡ z < s y ⁡ z ∧ ∀ w ∈ d w r < bag i z → x ⁡ w = y ⁡ w ∨ x = y
61 24 60 wa wff x y ⊆ Base p ∧ [˙ h ∈ ℕ 0 i | h -1 ℕ ∈ Fin / d]˙ ∃ z ∈ d x ⁡ z < s y ⁡ z ∧ ∀ w ∈ d w r < bag i z → x ⁡ w = y ⁡ w ∨ x = y
62 61 17 18 copab class x y | x y ⊆ Base p ∧ [˙ h ∈ ℕ 0 i | h -1 ℕ ∈ Fin / d]˙ ∃ z ∈ d x ⁡ z < s y ⁡ z ∧ ∀ w ∈ d w r < bag i z → x ⁡ w = y ⁡ w ∨ x = y
63 16 62 cop class ≤ ndx x y | x y ⊆ Base p ∧ [˙ h ∈ ℕ 0 i | h -1 ℕ ∈ Fin / d]˙ ∃ z ∈ d x ⁡ z < s y ⁡ z ∧ ∀ w ∈ d w r < bag i z → x ⁡ w = y ⁡ w ∨ x = y
64 12 63 13 co class p sSet ≤ ndx x y | x y ⊆ Base p ∧ [˙ h ∈ ℕ 0 i | h -1 ℕ ∈ Fin / d]˙ ∃ z ∈ d x ⁡ z < s y ⁡ z ∧ ∀ w ∈ d w r < bag i z → x ⁡ w = y ⁡ w ∨ x = y
65 11 10 64 csb class ⦋ i mPwSer s / p⦌ p sSet ≤ ndx x y | x y ⊆ Base p ∧ [˙ h ∈ ℕ 0 i | h -1 ℕ ∈ Fin / d]˙ ∃ z ∈ d x ⁡ z < s y ⁡ z ∧ ∀ w ∈ d w r < bag i z → x ⁡ w = y ⁡ w ∨ x = y
66 4 7 65 cmpt class r ∈ 𝒫 i × i ⟼ ⦋ i mPwSer s / p⦌ p sSet ≤ ndx x y | x y ⊆ Base p ∧ [˙ h ∈ ℕ 0 i | h -1 ℕ ∈ Fin / d]˙ ∃ z ∈ d x ⁡ z < s y ⁡ z ∧ ∀ w ∈ d w r < bag i z → x ⁡ w = y ⁡ w ∨ x = y
67 1 3 2 2 66 cmpo class i ∈ V , s ∈ V ⟼ r ∈ 𝒫 i × i ⟼ ⦋ i mPwSer s / p⦌ p sSet ≤ ndx x y | x y ⊆ Base p ∧ [˙ h ∈ ℕ 0 i | h -1 ℕ ∈ Fin / d]˙ ∃ z ∈ d x ⁡ z < s y ⁡ z ∧ ∀ w ∈ d w r < bag i z → x ⁡ w = y ⁡ w ∨ x = y
68 0 67 wceq wff ordPwSer = i ∈ V , s ∈ V ⟼ r ∈ 𝒫 i × i ⟼ ⦋ i mPwSer s / p⦌ p sSet ≤ ndx x y | x y ⊆ Base p ∧ [˙ h ∈ ℕ 0 i | h -1 ℕ ∈ Fin / d]˙ ∃ z ∈ d x ⁡ z < s y ⁡ z ∧ ∀ w ∈ d w r < bag i z → x ⁡ w = y ⁡ w ∨ x = y