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 𝑖 ) 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ∨ 𝑥 = 𝑦 ) ) } ⟩ ) ) )