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

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 = ( 𝑖 ∈ V , 𝑠 ∈ V ↦ ( 𝑟 ∈ 𝒫 ( 𝑖 × 𝑖 ) ↦ ⦋ ( 𝑖 mPwSer 𝑠 ) / 𝑝 ⦌ ( 𝑝 sSet ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑝 ) ∧ ( [ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } / 𝑑 ] ∃ 𝑧 ∈ 𝑑 ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑠 ) ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑑 ( 𝑤 ( 𝑟 <bag 𝑖 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⟩ ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 copws ⊢ ordPwSer
1 vi ⊢ 𝑖
2 cvv ⊢ V
3 vs ⊢ 𝑠
4 vr ⊢ 𝑟
5 1 cv ⊢ 𝑖
6 5 5 cxp ⊢ ( 𝑖 × 𝑖 )
7 6 cpw ⊢ 𝒫 ( 𝑖 × 𝑖 )
8 cmps ⊢ mPwSer
9 3 cv ⊢ 𝑠
10 5 9 8 co ⊢ ( 𝑖 mPwSer 𝑠 )
11 vp ⊢ 𝑝
12 11 cv ⊢ 𝑝
13 csts ⊢ sSet
14 cple ⊢ le
15 cnx ⊢ ndx
16 15 14 cfv ⊢ ( le ‘ ndx )
17 vx ⊢ 𝑥
18 vy ⊢ 𝑦
19 17 cv ⊢ 𝑥
20 18 cv ⊢ 𝑦
21 19 20 cpr ⊢ { 𝑥 , 𝑦 }
22 cbs ⊢ Base
23 12 22 cfv ⊢ ( Base ‘ 𝑝 )
24 21 23 wss ⊢ { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑝 )
25 vh ⊢ ℎ
26 cn0 ⊢ ℕ0
27 cmap ⊢ ↑m
28 26 5 27 co ⊢ ( ℕ0 ↑m 𝑖 )
29 25 cv ⊢ ℎ
30 29 ccnv ⊢ ◡ ℎ
31 cn ⊢ ℕ
32 30 31 cima ⊢ ( ◡ ℎ “ ℕ )
33 cfn ⊢ Fin
34 32 33 wcel ⊢ ( ◡ ℎ “ ℕ ) ∈ Fin
35 34 25 28 crab ⊢ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
36 vd ⊢ 𝑑
37 vz ⊢ 𝑧
38 36 cv ⊢ 𝑑
39 37 cv ⊢ 𝑧
40 39 19 cfv ⊢ ( 𝑥 ‘ 𝑧 )
41 cplt ⊢ lt
42 9 41 cfv ⊢ ( lt ‘ 𝑠 )
43 39 20 cfv ⊢ ( 𝑦 ‘ 𝑧 )
44 40 43 42 wbr ⊢ ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑠 ) ( 𝑦 ‘ 𝑧 )
45 vw ⊢ 𝑤
46 45 cv ⊢ 𝑤
47 4 cv ⊢ 𝑟
48 cltb ⊢ <bag
49 47 5 48 co ⊢ ( 𝑟 <bag 𝑖 )
50 46 39 49 wbr ⊢ 𝑤 ( 𝑟 <bag 𝑖 ) 𝑧
51 46 19 cfv ⊢ ( 𝑥 ‘ 𝑤 )
52 46 20 cfv ⊢ ( 𝑦 ‘ 𝑤 )
53 51 52 wceq ⊢ ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 )
54 50 53 wi ⊢ ( 𝑤 ( 𝑟 <bag 𝑖 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) )
55 54 45 38 wral ⊢ ∀ 𝑤 ∈ 𝑑 ( 𝑤 ( 𝑟 <bag 𝑖 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) )
56 44 55 wa ⊢ ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑠 ) ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑑 ( 𝑤 ( 𝑟 <bag 𝑖 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) )
57 56 37 38 wrex ⊢ ∃ 𝑧 ∈ 𝑑 ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑠 ) ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑑 ( 𝑤 ( 𝑟 <bag 𝑖 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) )
58 57 36 35 wsbc ⊢ [ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } / 𝑑 ] ∃ 𝑧 ∈ 𝑑 ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑠 ) ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑑 ( 𝑤 ( 𝑟 <bag 𝑖 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) )
59 19 20 wceq ⊢ 𝑥 = 𝑦
60 58 59 wo ⊢ ( [ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } / 𝑑 ] ∃ 𝑧 ∈ 𝑑 ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑠 ) ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑑 ( 𝑤 ( 𝑟 <bag 𝑖 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 )
61 24 60 wa ⊢ ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑝 ) ∧ ( [ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } / 𝑑 ] ∃ 𝑧 ∈ 𝑑 ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑠 ) ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑑 ( 𝑤 ( 𝑟 <bag 𝑖 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) )
62 61 17 18 copab ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑝 ) ∧ ( [ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } / 𝑑 ] ∃ 𝑧 ∈ 𝑑 ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑠 ) ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑑 ( 𝑤 ( 𝑟 <bag 𝑖 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) }
63 16 62 cop ⊢ ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑝 ) ∧ ( [ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } / 𝑑 ] ∃ 𝑧 ∈ 𝑑 ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑠 ) ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑑 ( 𝑤 ( 𝑟 <bag 𝑖 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⟩
64 12 63 13 co ⊢ ( 𝑝 sSet ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑝 ) ∧ ( [ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } / 𝑑 ] ∃ 𝑧 ∈ 𝑑 ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑠 ) ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑑 ( 𝑤 ( 𝑟 <bag 𝑖 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⟩ )
65 11 10 64 csb ⊢ ⦋ ( 𝑖 mPwSer 𝑠 ) / 𝑝 ⦌ ( 𝑝 sSet ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑝 ) ∧ ( [ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } / 𝑑 ] ∃ 𝑧 ∈ 𝑑 ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑠 ) ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑑 ( 𝑤 ( 𝑟 <bag 𝑖 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⟩ )
66 4 7 65 cmpt ⊢ ( 𝑟 ∈ 𝒫 ( 𝑖 × 𝑖 ) ↦ ⦋ ( 𝑖 mPwSer 𝑠 ) / 𝑝 ⦌ ( 𝑝 sSet ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑝 ) ∧ ( [ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } / 𝑑 ] ∃ 𝑧 ∈ 𝑑 ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑠 ) ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑑 ( 𝑤 ( 𝑟 <bag 𝑖 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⟩ ) )
67 1 3 2 2 66 cmpo ⊢ ( 𝑖 ∈ V , 𝑠 ∈ V ↦ ( 𝑟 ∈ 𝒫 ( 𝑖 × 𝑖 ) ↦ ⦋ ( 𝑖 mPwSer 𝑠 ) / 𝑝 ⦌ ( 𝑝 sSet ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑝 ) ∧ ( [ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } / 𝑑 ] ∃ 𝑧 ∈ 𝑑 ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑠 ) ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑑 ( 𝑤 ( 𝑟 <bag 𝑖 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⟩ ) ) )
68 0 67 wceq ⊢ ordPwSer = ( 𝑖 ∈ V , 𝑠 ∈ V ↦ ( 𝑟 ∈ 𝒫 ( 𝑖 × 𝑖 ) ↦ ⦋ ( 𝑖 mPwSer 𝑠 ) / 𝑝 ⦌ ( 𝑝 sSet ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ ( Base ‘ 𝑝 ) ∧ ( [ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } / 𝑑 ] ∃ 𝑧 ∈ 𝑑 ( ( 𝑥 ‘ 𝑧 ) ( lt ‘ 𝑠 ) ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝑑 ( 𝑤 ( 𝑟 <bag 𝑖 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⟩ ) ) )